[STATEMENT]
lemma irs_SDG_path_matched:
  assumes "n irs-ns\<rightarrow>\<^sub>d* n''" and "n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'"
  obtains nx nsx where "matched nx nsx n'" and "n \<in> set nsx"
  and "nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>nx nsx. \<lbrakk>matched nx nsx n'; n \<in> set nsx; nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
n irs-ns\<rightarrow>\<^sub>d* n''
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'
[PROOF STEP]
show "\<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and>
                 nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')"
[PROOF STATE]
proof (prove)
using this:
n irs-ns\<rightarrow>\<^sub>d* n''
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'

goal (1 subgoal):
 1. \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
proof(induct ns arbitrary:n'' n' p V rule:length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
fix ns n'' n' p V
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
assume IH:"\<forall>ns'. length ns' < length ns \<longrightarrow>
      (\<forall>n''. n irs-ns'\<rightarrow>\<^sub>d* n'' \<longrightarrow>
      (\<forall>nx' p' V'. (n'' s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> n'' s-p':V'\<rightarrow>\<^bsub>out\<^esub> nx') \<longrightarrow>
        (\<exists>nx nsx. matched nx nsx nx' \<and> n \<in> set nsx \<and>
                  nx s-p'\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx'))))"
      and "n irs-ns\<rightarrow>\<^sub>d* n''" and "n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'"
[PROOF STATE]
proof (state)
this:
\<forall>ns'. length ns' < length ns \<longrightarrow> (\<forall>n''. n irs-ns'\<rightarrow>\<^sub>d* n'' \<longrightarrow> (\<forall>nx' p' V'. n'' s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> n'' s-p':V'\<rightarrow>\<^bsub>out\<^esub> nx' \<longrightarrow> (\<exists>nx nsx. matched nx nsx nx' \<and> n \<in> set nsx \<and> nx s-p'\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx'))))
n irs-ns\<rightarrow>\<^sub>d* n''
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'

goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'
[PROOF STEP]
have "valid_SDG_node n''"
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'

goal (1 subgoal):
 1. valid_SDG_node n''
[PROOF STEP]
by(fastforce intro:sum_SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n''

goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'
[PROOF STEP]
have "n'' -p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' -p:V\<rightarrow>\<^bsub>out\<^esub> n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'

goal (1 subgoal):
 1. n'' -p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' -p:V\<rightarrow>\<^bsub>out\<^esub> n'
[PROOF STEP]
by(fastforce intro:sum_SDG_edge_SDG_edge SDG_edge_sum_SDG_edge)
[PROOF STATE]
proof (state)
this:
n'' -p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' -p:V\<rightarrow>\<^bsub>out\<^esub> n'

goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'
[PROOF STEP]
have "CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')"
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'

goal (1 subgoal):
 1. CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')
[PROOF STEP]
by(fastforce elim:sum_SDG_edge.cases intro:sum_SDG_return_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')

goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')
[PROOF STEP]
obtain a Q f where "valid_edge a" and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f"
      and "parent_node n'' = sourcenode a" and "parent_node n' = targetnode a"
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')

goal (1 subgoal):
 1. (\<And>a Q f. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; parent_node n'' = sourcenode a; parent_node n' = targetnode a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:sum_SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
parent_node n'' = sourcenode a
parent_node n' = targetnode a

goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
obtain a' Q' r' fs'
      where "a \<in> get_return_edges a'" and "valid_edge a'" and "kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'"
      and "CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. (\<And>a' Q' r' fs'. \<lbrakk>a \<in> get_return_edges a'; valid_edge a'; kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'; CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule return_edge_determines_call_and_sum_edge)
[PROOF STATE]
proof (state)
this:
a \<in> get_return_edges a'
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)

goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
[PROOF STEP]
have "CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'

goal (1 subgoal):
 1. CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
[PROOF STEP]
by(fastforce intro:sum_SDG_call_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')

goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')
[PROOF STEP]
have "get_proc (parent_node n'') = p"
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')

goal (1 subgoal):
 1. get_proc (parent_node n'') = p
[PROOF STEP]
by(auto elim!:sum_SDG_edge.cases intro:get_proc_return)
[PROOF STATE]
proof (state)
this:
get_proc (parent_node n'') = p

goal (1 subgoal):
 1. \<And>xs n'' n' p V. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n irs-ys\<rightarrow>\<^sub>d* x \<longrightarrow> (\<forall>xa xb xc. x s-xb\<rightarrow>\<^bsub>ret\<^esub> xa \<or> x s-xb:xc\<rightarrow>\<^bsub>out\<^esub> xa \<longrightarrow> (\<exists>nx nsx. matched nx nsx xa \<and> n \<in> set nsx \<and> nx s-xb\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node xa)))); n irs-xs\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>n irs-ns\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n irs-ns\<rightarrow>\<^sub>d* n''
[PROOF STEP]
show "\<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and>
                   nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')"
[PROOF STATE]
proof (prove)
using this:
n irs-ns\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
proof(rule irs_SDG_path_split)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
assume "n is-ns\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n''

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "valid_SDG_node n"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. valid_SDG_node n
[PROOF STEP]
by(rule is_SDG_path_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
[PROOF STEP]
obtain asx where "(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

goal (1 subgoal):
 1. (\<And>asx. (_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:valid_SDG_CFG_node Entry_path)
[PROOF STATE]
proof (state)
this:
(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node n

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node n
[PROOF STEP]
obtain asx' where "(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n"
        and "\<forall>a' \<in> set asx'. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node n

goal (1 subgoal):
 1. (\<And>asx'. \<lbrakk>(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n; \<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule valid_Entry_path_ascending_path)
[PROOF STATE]
proof (state)
this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n
\<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>n is-ns\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n''
[PROOF STEP]
obtain as where "parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule is_SDG_path_CFG_path)
[PROOF STATE]
proof (state)
this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "get_proc (parent_node n) = get_proc (parent_node n'')"
[PROOF STATE]
proof (prove)
using this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''

goal (1 subgoal):
 1. get_proc (parent_node n) = get_proc (parent_node n'')
[PROOF STEP]
by(rule intra_path_get_procs)
[PROOF STATE]
proof (state)
this:
get_proc (parent_node n) = get_proc (parent_node n'')

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
[PROOF STEP]
have "valid_node (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

goal (1 subgoal):
 1. valid_node (parent_node n)
[PROOF STEP]
by(rule valid_SDG_CFG_node)
[PROOF STATE]
proof (state)
this:
valid_node (parent_node n)

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "valid_SDG_node (CFG_node (parent_node n))"
[PROOF STATE]
proof (prove)
using this:
valid_node (parent_node n)

goal (1 subgoal):
 1. valid_SDG_node (CFG_node (parent_node n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_SDG_node (CFG_node (parent_node n))

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
have "\<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
        targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
proof(cases "\<forall>a' \<in> set asx'. intra_kind(kind a')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>a'\<in>set asx'. intra_kind (kind a')

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
with \<open>(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n
\<forall>a'\<in>set asx'. intra_kind (kind a')
[PROOF STEP]
have "(_Entry_) -asx'\<rightarrow>\<^sub>\<iota>* parent_node n"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n
\<forall>a'\<in>set asx'. intra_kind (kind a')

goal (1 subgoal):
 1. (_Entry_) -asx'\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
by(fastforce simp:intra_path_def vp_def)
[PROOF STATE]
proof (state)
this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<iota>* parent_node n

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
hence "get_proc (_Entry_) = get_proc (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<iota>* parent_node n

goal (1 subgoal):
 1. get_proc (_Entry_) = get_proc (parent_node n)
[PROOF STEP]
by(rule intra_path_get_procs)
[PROOF STATE]
proof (state)
this:
get_proc (_Entry_) = get_proc (parent_node n)

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
with get_proc_Entry
[PROOF STATE]
proof (chain)
picking this:
get_proc (_Entry_) = Main
get_proc (_Entry_) = get_proc (parent_node n)
[PROOF STEP]
have "get_proc (parent_node n) = Main"
[PROOF STATE]
proof (prove)
using this:
get_proc (_Entry_) = Main
get_proc (_Entry_) = get_proc (parent_node n)

goal (1 subgoal):
 1. get_proc (parent_node n) = Main
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
get_proc (parent_node n) = Main

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
from \<open>get_proc (parent_node n) = get_proc (parent_node n'')\<close>
          \<open>get_proc (parent_node n) = Main\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (parent_node n) = get_proc (parent_node n'')
get_proc (parent_node n) = Main
[PROOF STEP]
have "get_proc (parent_node n'') = Main"
[PROOF STATE]
proof (prove)
using this:
get_proc (parent_node n) = get_proc (parent_node n'')
get_proc (parent_node n) = Main

goal (1 subgoal):
 1. get_proc (parent_node n'') = Main
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
get_proc (parent_node n'') = Main

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
have "get_proc (sourcenode a) = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. get_proc (sourcenode a) = p
[PROOF STEP]
by(rule get_proc_return)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a) = p

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
with \<open>parent_node n'' = sourcenode a\<close> \<open>get_proc (parent_node n'') = Main\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n'' = sourcenode a
get_proc (parent_node n'') = Main
get_proc (sourcenode a) = p
[PROOF STEP]
have "p = Main"
[PROOF STATE]
proof (prove)
using this:
parent_node n'' = sourcenode a
get_proc (parent_node n'') = Main
get_proc (sourcenode a) = p

goal (1 subgoal):
 1. p = Main
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = Main

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
with \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
p = Main
[PROOF STEP]
have "kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f"
[PROOF STATE]
proof (prove)
using this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
p = Main

goal (1 subgoal):
 1. kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
with \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule Main_no_return_source)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
assume "\<not> (\<forall>a'\<in>set asx'. intra_kind (kind a'))"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a'\<in>set asx'. intra_kind (kind a'))

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
with \<open>\<forall>a' \<in> set asx'. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
\<not> (\<forall>a'\<in>set asx'. intra_kind (kind a'))
[PROOF STEP]
have "\<exists>a' \<in> set asx'. \<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
[PROOF STATE]
proof (prove)
using this:
\<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
\<not> (\<forall>a'\<in>set asx'. intra_kind (kind a'))

goal (1 subgoal):
 1. \<exists>a'\<in>set asx'. \<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
by(fastforce simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
\<exists>a'\<in>set asx'. \<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a'\<in>set asx'. \<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain as a' as' where "asx' = as@a'#as'"
          and "\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
          and "\<forall>a' \<in> set as'. \<not> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a'\<in>set asx'. \<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>as a' as'. \<lbrakk>asx' = as @ a' # as'; \<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; \<forall>a'\<in>set as'. \<nexists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule split_list_last_propE)
[PROOF STATE]
proof (state)
this:
asx' = as @ a' # as'
\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<forall>a'\<in>set as'. \<nexists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
with \<open>\<forall>a' \<in> set asx'. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
asx' = as @ a' # as'
\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<forall>a'\<in>set as'. \<nexists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "\<forall>a'\<in>set as'. intra_kind (kind a')"
[PROOF STATE]
proof (prove)
using this:
\<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
asx' = as @ a' # as'
\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<forall>a'\<in>set as'. \<nexists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. \<forall>a'\<in>set as'. intra_kind (kind a')
[PROOF STEP]
by(auto simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
\<forall>a'\<in>set as'. intra_kind (kind a')

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
from \<open>(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n\<close> \<open>asx' = as@a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n
asx' = as @ a' # as'
[PROOF STEP]
have "valid_edge a'" and "targetnode a' -as'\<rightarrow>* parent_node n"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node n
asx' = as @ a' # as'

goal (1 subgoal):
 1. valid_edge a' &&& targetnode a' -as'\<rightarrow>* parent_node n
[PROOF STEP]
by(auto dest:path_split simp:vp_def)
[PROOF STATE]
proof (state)
this:
valid_edge a'
targetnode a' -as'\<rightarrow>* parent_node n

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
with \<open>\<forall>a'\<in>set as'. intra_kind (kind a')\<close> \<open>\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a'\<in>set as'. intra_kind (kind a')
\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a'
targetnode a' -as'\<rightarrow>* parent_node n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>a'\<in>set as'. intra_kind (kind a')
\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a'
targetnode a' -as'\<rightarrow>* parent_node n

goal (1 subgoal):
 1. \<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
by(fastforce simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
\<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
obtain ax asx Qx rx fsx px where "valid_edge ax"
        and "kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx" and "targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n"
[PROOF STATE]
proof (prove)
using this:
\<exists>a as. valid_edge a \<and> (\<exists>Q p r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> targetnode a -as\<rightarrow>\<^sub>\<iota>* parent_node n

goal (1 subgoal):
 1. (\<And>ax Qx rx px fsx asx. \<lbrakk>valid_edge ax; kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx; targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
valid_edge ax
kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx
targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge ax\<close> \<open>kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ax
kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx
[PROOF STEP]
have "get_proc (targetnode ax) = px"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax
kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx

goal (1 subgoal):
 1. get_proc (targetnode ax) = px
[PROOF STEP]
by(rule get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc (targetnode ax) = px

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n
[PROOF STEP]
have "get_proc (targetnode ax) = get_proc (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n

goal (1 subgoal):
 1. get_proc (targetnode ax) = get_proc (parent_node n)
[PROOF STEP]
by(rule intra_path_get_procs)
[PROOF STATE]
proof (state)
this:
get_proc (targetnode ax) = get_proc (parent_node n)

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>get_proc (parent_node n) = get_proc (parent_node n'')\<close>
        \<open>get_proc (targetnode ax) = px\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (parent_node n) = get_proc (parent_node n'')
get_proc (targetnode ax) = px
get_proc (targetnode ax) = get_proc (parent_node n)
[PROOF STEP]
have "get_proc (parent_node n'') = px"
[PROOF STATE]
proof (prove)
using this:
get_proc (parent_node n) = get_proc (parent_node n'')
get_proc (targetnode ax) = px
get_proc (targetnode ax) = get_proc (parent_node n)

goal (1 subgoal):
 1. get_proc (parent_node n'') = px
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
get_proc (parent_node n'') = px

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>get_proc (parent_node n'') = p\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (parent_node n'') = p
get_proc (parent_node n'') = px
[PROOF STEP]
have [simp]:"px = p"
[PROOF STATE]
proof (prove)
using this:
get_proc (parent_node n'') = p
get_proc (parent_node n'') = px

goal (1 subgoal):
 1. px = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
px = p

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>valid_edge ax\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
        \<open>kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
valid_edge ax
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx
[PROOF STEP]
have "targetnode a' = targetnode ax"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
valid_edge ax
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx

goal (1 subgoal):
 1. targetnode a' = targetnode ax
[PROOF STEP]
by simp(rule same_proc_call_unique_target)
[PROOF STATE]
proof (state)
this:
targetnode a' = targetnode ax

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
have "parent_node n \<noteq> (_Exit_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parent_node n \<noteq> (_Exit_)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. parent_node n = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
assume "parent_node n = (_Exit_)"
[PROOF STATE]
proof (state)
this:
parent_node n = (_Exit_)

goal (1 subgoal):
 1. parent_node n = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
from \<open>n is-ns\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n''
[PROOF STEP]
obtain as where "parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule is_SDG_path_CFG_path)
[PROOF STATE]
proof (state)
this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''

goal (1 subgoal):
 1. parent_node n = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
with \<open>parent_node n = (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n = (_Exit_)
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
[PROOF STEP]
have "(_Exit_) -as\<rightarrow>* parent_node n''"
[PROOF STATE]
proof (prove)
using this:
parent_node n = (_Exit_)
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''

goal (1 subgoal):
 1. (_Exit_) -as\<rightarrow>* parent_node n''
[PROOF STEP]
by(simp add:intra_path_def)
[PROOF STATE]
proof (state)
this:
(_Exit_) -as\<rightarrow>* parent_node n''

goal (1 subgoal):
 1. parent_node n = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
hence "parent_node n'' = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
(_Exit_) -as\<rightarrow>* parent_node n''

goal (1 subgoal):
 1. parent_node n'' = (_Exit_)
[PROOF STEP]
by(fastforce dest:path_Exit_source)
[PROOF STATE]
proof (state)
this:
parent_node n'' = (_Exit_)

goal (1 subgoal):
 1. parent_node n = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
from \<open>get_proc (parent_node n'') = p\<close> \<open>parent_node n'' = (_Exit_)\<close>
          \<open>parent_node n'' = sourcenode a\<close> get_proc_Exit
[PROOF STATE]
proof (chain)
picking this:
get_proc (parent_node n'') = p
parent_node n'' = (_Exit_)
parent_node n'' = sourcenode a
get_proc (_Exit_) = Main
[PROOF STEP]
have "p = Main"
[PROOF STATE]
proof (prove)
using this:
get_proc (parent_node n'') = p
parent_node n'' = (_Exit_)
parent_node n'' = sourcenode a
get_proc (_Exit_) = Main

goal (1 subgoal):
 1. p = Main
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = Main

goal (1 subgoal):
 1. parent_node n = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
with \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
p = Main
[PROOF STEP]
have "kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f"
[PROOF STATE]
proof (prove)
using this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
p = Main

goal (1 subgoal):
 1. kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f

goal (1 subgoal):
 1. parent_node n = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>Main\<^esub>f

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule Main_no_return_source)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
parent_node n \<noteq> (_Exit_)

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
have "\<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
proof(cases "targetnode a' = parent_node n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. targetnode a' = parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
 2. targetnode a' \<noteq> parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
targetnode a' = parent_node n

goal (2 subgoals):
 1. targetnode a' = parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
 2. targetnode a' \<noteq> parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
with \<open>valid_SDG_node (CFG_node (parent_node n))\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node (CFG_node (parent_node n))
targetnode a' = parent_node n
[PROOF STEP]
have "CFG_node (targetnode a') cd-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node (CFG_node (parent_node n))
targetnode a' = parent_node n

goal (1 subgoal):
 1. CFG_node (targetnode a') cd-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
by(fastforce intro:cdSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (2 subgoals):
 1. targetnode a' = parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
 2. targetnode a' \<noteq> parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (1 subgoal):
 1. \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (1 subgoal):
 1. targetnode a' \<noteq> parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. targetnode a' \<noteq> parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
targetnode a' \<noteq> parent_node n

goal (1 subgoal):
 1. targetnode a' \<noteq> parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
with \<open>targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n\<close> \<open>parent_node n \<noteq> (_Exit_)\<close>
          \<open>valid_edge ax\<close> \<open>kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx\<close> \<open>targetnode a' = targetnode ax\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n
parent_node n \<noteq> (_Exit_)
valid_edge ax
kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx
targetnode a' = targetnode ax
targetnode a' \<noteq> parent_node n
[PROOF STEP]
obtain nsx
          where "CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
targetnode ax -asx\<rightarrow>\<^sub>\<iota>* parent_node n
parent_node n \<noteq> (_Exit_)
valid_edge ax
kind ax = Qx:rx\<hookrightarrow>\<^bsub>px\<^esub>fsx
targetnode a' = targetnode ax
targetnode a' \<noteq> parent_node n

goal (1 subgoal):
 1. (\<And>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:in_proc_cdep_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (1 subgoal):
 1. targetnode a' \<noteq> parent_node n \<Longrightarrow> \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (1 subgoal):
 1. \<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
obtain nsx
        where "CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (1 subgoal):
 1. (\<And>nsx. CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "CFG_node (targetnode a') i-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (1 subgoal):
 1. CFG_node (targetnode a') i-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
by(rule cdep_SDG_path_intra_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') i-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (2 subgoals):
 1. n is-ns\<rightarrow>\<^sub>d* n'' \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
proof(cases ns)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ns = []

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>n is-ns\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n''
ns = []
[PROOF STEP]
have "n = n''"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n''
ns = []

goal (1 subgoal):
 1. n = n''
[PROOF STEP]
by(fastforce elim:intra_sum_SDG_path.cases)
[PROOF STATE]
proof (state)
this:
n = n''

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close> \<open>a \<in> get_return_edges a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
a \<in> get_return_edges a'
[PROOF STEP]
have "matched (CFG_node (targetnode a')) [CFG_node (targetnode a')]
          (CFG_node (sourcenode a))"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
a \<in> get_return_edges a'

goal (1 subgoal):
 1. matched (CFG_node (targetnode a')) [CFG_node (targetnode a')] (CFG_node (sourcenode a))
[PROOF STEP]
by(rule intra_proc_matched)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) [CFG_node (targetnode a')] (CFG_node (sourcenode a))

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_SDG_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n''
[PROOF STEP]
have "n'' = CFG_node (parent_node n'') \<or> CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n''

goal (1 subgoal):
 1. n'' = CFG_node (parent_node n'') \<or> CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''
[PROOF STEP]
by(rule valid_SDG_node_cases)
[PROOF STATE]
proof (state)
this:
n'' = CFG_node (parent_node n'') \<or> CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "\<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (prove)
using this:
n'' = CFG_node (parent_node n'') \<or> CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''

goal (1 subgoal):
 1. \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' = CFG_node (parent_node n'') \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
 2. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
assume "n'' = CFG_node (parent_node n'')"
[PROOF STATE]
proof (state)
this:
n'' = CFG_node (parent_node n'')

goal (2 subgoals):
 1. n'' = CFG_node (parent_node n'') \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
 2. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
with \<open>valid_SDG_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n''
n'' = CFG_node (parent_node n'')
[PROOF STEP]
have "CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n''
n'' = CFG_node (parent_node n'')

goal (1 subgoal):
 1. CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* n''
[PROOF STEP]
by(fastforce intro:iSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* n''

goal (2 subgoals):
 1. n'' = CFG_node (parent_node n'') \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
 2. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
assume "CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''"
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''

goal (1 subgoal):
 1. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
from \<open>valid_SDG_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n''
[PROOF STEP]
have "valid_node (parent_node n'')"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n''

goal (1 subgoal):
 1. valid_node (parent_node n'')
[PROOF STEP]
by(rule valid_SDG_CFG_node)
[PROOF STATE]
proof (state)
this:
valid_node (parent_node n'')

goal (1 subgoal):
 1. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
hence "valid_SDG_node (CFG_node (parent_node n''))"
[PROOF STATE]
proof (prove)
using this:
valid_node (parent_node n'')

goal (1 subgoal):
 1. valid_SDG_node (CFG_node (parent_node n''))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_SDG_node (CFG_node (parent_node n''))

goal (1 subgoal):
 1. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
hence "CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n'')"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node (CFG_node (parent_node n''))

goal (1 subgoal):
 1. CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n'')
[PROOF STEP]
by(rule iSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n'')

goal (1 subgoal):
 1. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
with \<open>CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''
CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n'')
[PROOF STEP]
have "CFG_node (parent_node n'') i-[]@[CFG_node (parent_node n'')]\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n''
CFG_node (parent_node n'') i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n'')

goal (1 subgoal):
 1. CFG_node (parent_node n'') i-[] @ [CFG_node (parent_node n'')]\<rightarrow>\<^sub>d* n''
[PROOF STEP]
by(fastforce intro:iSp_Append_cdep sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n'') i-[] @ [CFG_node (parent_node n'')]\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. CFG_node (parent_node n'') \<longrightarrow>\<^bsub>cd\<^esub> n'' \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n'') i-[] @ [CFG_node (parent_node n'')]\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. \<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>parent_node n'' = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n'' = sourcenode a
\<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
obtain nsx where "CFG_node (sourcenode a) i-nsx\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (prove)
using this:
parent_node n'' = sourcenode a
\<exists>nsx. CFG_node (parent_node n'') i-nsx\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. (\<And>nsx. CFG_node (sourcenode a) i-nsx\<rightarrow>\<^sub>d* n'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a) i-nsx\<rightarrow>\<^sub>d* n''

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>matched (CFG_node (targetnode a')) [CFG_node (targetnode a')]
          (CFG_node (sourcenode a))\<close>
[PROOF STATE]
proof (chain)
picking this:
matched (CFG_node (targetnode a')) [CFG_node (targetnode a')] (CFG_node (sourcenode a))
CFG_node (sourcenode a) i-nsx\<rightarrow>\<^sub>d* n''
[PROOF STEP]
have "matched (CFG_node (targetnode a')) ([CFG_node (targetnode a')]@nsx) n''"
[PROOF STATE]
proof (prove)
using this:
matched (CFG_node (targetnode a')) [CFG_node (targetnode a')] (CFG_node (sourcenode a))
CFG_node (sourcenode a) i-nsx\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. matched (CFG_node (targetnode a')) ([CFG_node (targetnode a')] @ nsx) n''
[PROOF STEP]
by(fastforce intro:matched_Append intra_SDG_path_matched)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) ([CFG_node (targetnode a')] @ nsx) n''

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) ([CFG_node (targetnode a')] @ nsx) n''

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
[PROOF STEP]
have "CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'

goal (1 subgoal):
 1. CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
[PROOF STEP]
by(fastforce intro:SDG_call_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
[PROOF STEP]
have "valid_SDG_node (CFG_node (sourcenode a'))"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'

goal (1 subgoal):
 1. valid_SDG_node (CFG_node (sourcenode a'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_SDG_node (CFG_node (sourcenode a'))

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node (CFG_node (sourcenode a'))

goal (1 subgoal):
 1. matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))
[PROOF STEP]
by(rule matched_Nil)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
matched (CFG_node (targetnode a')) ([CFG_node (targetnode a')] @ nsx) n''
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))
[PROOF STEP]
have "matched (CFG_node (sourcenode a'))
          ([]@(CFG_node (sourcenode a'))#([CFG_node (targetnode a')]@nsx)@[n'']) n'"
[PROOF STATE]
proof (prove)
using this:
matched (CFG_node (targetnode a')) ([CFG_node (targetnode a')] @ nsx) n''
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))

goal (1 subgoal):
 1. matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ([CFG_node (targetnode a')] @ nsx) @ [n'']) n'
[PROOF STEP]
using \<open>n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<close> \<open>parent_node n' = targetnode a\<close>
            \<open>parent_node n'' = sourcenode a\<close> \<open>valid_edge a'\<close> \<open>a \<in> get_return_edges a'\<close>
[PROOF STATE]
proof (prove)
using this:
matched (CFG_node (targetnode a')) ([CFG_node (targetnode a')] @ nsx) n''
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'
parent_node n' = targetnode a
parent_node n'' = sourcenode a
valid_edge a'
a \<in> get_return_edges a'

goal (1 subgoal):
 1. matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ([CFG_node (targetnode a')] @ nsx) @ [n'']) n'
[PROOF STEP]
by(fastforce intro:matched_bracket_call dest:sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ([CFG_node (targetnode a')] @ nsx) @ [n'']) n'

goal (2 subgoals):
 1. ns = [] \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
 2. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>n = n''\<close> \<open>CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)\<close>
          \<open>parent_node n' = targetnode a\<close>
[PROOF STATE]
proof (chain)
picking this:
n = n''
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
parent_node n' = targetnode a
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ([CFG_node (targetnode a')] @ nsx) @ [n'']) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = n''
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
parent_node n' = targetnode a
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ([CFG_node (targetnode a')] @ nsx) @ [n'']) n'

goal (1 subgoal):
 1. \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
ns = a_ # list_

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>n is-ns\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n''
ns = a_ # list_
[PROOF STEP]
have "n \<in> set ns"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n''
ns = a_ # list_

goal (1 subgoal):
 1. n \<in> set ns
[PROOF STEP]
by(induct rule:intra_sum_SDG_path_rev_induct) auto
[PROOF STATE]
proof (state)
this:
n \<in> set ns

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>n is-ns\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n''
[PROOF STEP]
obtain ns' where "matched n ns' n''"
          and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>matched n ns' n''; set ns \<subseteq> set ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule is_SDG_path_matched)
[PROOF STATE]
proof (state)
this:
matched n ns' n''
set ns \<subseteq> set ns'

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>n \<in> set ns\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set ns
matched n ns' n''
set ns \<subseteq> set ns'
[PROOF STEP]
have "n \<in> set ns'"
[PROOF STATE]
proof (prove)
using this:
n \<in> set ns
matched n ns' n''
set ns \<subseteq> set ns'

goal (1 subgoal):
 1. n \<in> set ns'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n \<in> set ns'

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
[PROOF STEP]
have "n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

goal (1 subgoal):
 1. n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by(rule valid_SDG_node_cases)
[PROOF STATE]
proof (state)
this:
n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "\<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = CFG_node (parent_node n) \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
 2. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
assume "n = CFG_node (parent_node n)"
[PROOF STATE]
proof (state)
this:
n = CFG_node (parent_node n)

goal (2 subgoals):
 1. n = CFG_node (parent_node n) \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
 2. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = CFG_node (parent_node n)
[PROOF STEP]
have "CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = CFG_node (parent_node n)

goal (1 subgoal):
 1. CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* n
[PROOF STEP]
by(fastforce intro:iSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* n

goal (2 subgoals):
 1. n = CFG_node (parent_node n) \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
 2. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
assume "CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>valid_SDG_node (CFG_node (parent_node n))\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node (CFG_node (parent_node n))
[PROOF STEP]
have "CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node (CFG_node (parent_node n))

goal (1 subgoal):
 1. CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
by(rule iSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)
[PROOF STEP]
have "CFG_node (parent_node n) i-[]@[CFG_node (parent_node n)]\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
CFG_node (parent_node n) i-[]\<rightarrow>\<^sub>d* CFG_node (parent_node n)

goal (1 subgoal):
 1. CFG_node (parent_node n) i-[] @ [CFG_node (parent_node n)]\<rightarrow>\<^sub>d* n
[PROOF STEP]
by(fastforce intro:iSp_Append_cdep sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) i-[] @ [CFG_node (parent_node n)]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n \<Longrightarrow> \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n) i-[] @ [CFG_node (parent_node n)]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. \<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n
[PROOF STEP]
obtain nsx' where "CFG_node (parent_node n) i-nsx'\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
\<exists>nsx. CFG_node (parent_node n) i-nsx\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. (\<And>nsx'. CFG_node (parent_node n) i-nsx'\<rightarrow>\<^sub>d* n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) i-nsx'\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>CFG_node (targetnode a') i-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a') i-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
CFG_node (parent_node n) i-nsx'\<rightarrow>\<^sub>d* n
[PROOF STEP]
have "CFG_node (targetnode a') i-nsx@nsx'\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') i-nsx\<rightarrow>\<^sub>d* CFG_node (parent_node n)
CFG_node (parent_node n) i-nsx'\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. CFG_node (targetnode a') i-nsx @ nsx'\<rightarrow>\<^sub>d* n
[PROOF STEP]
by -(rule intra_SDG_path_Append)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') i-nsx @ nsx'\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "matched (CFG_node (targetnode a')) (nsx@nsx') n"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') i-nsx @ nsx'\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. matched (CFG_node (targetnode a')) (nsx @ nsx') n
[PROOF STEP]
by(rule intra_SDG_path_matched)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) (nsx @ nsx') n

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>matched n ns' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n ns' n''
matched (CFG_node (targetnode a')) (nsx @ nsx') n
[PROOF STEP]
have "matched (CFG_node (targetnode a')) ((nsx@nsx')@ns') n''"
[PROOF STATE]
proof (prove)
using this:
matched n ns' n''
matched (CFG_node (targetnode a')) (nsx @ nsx') n

goal (1 subgoal):
 1. matched (CFG_node (targetnode a')) ((nsx @ nsx') @ ns') n''
[PROOF STEP]
by(rule matched_Append)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) ((nsx @ nsx') @ ns') n''

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) ((nsx @ nsx') @ ns') n''

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
[PROOF STEP]
have "CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'

goal (1 subgoal):
 1. CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
[PROOF STEP]
by(fastforce intro:SDG_call_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
[PROOF STEP]
have "valid_SDG_node (CFG_node (sourcenode a'))"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'

goal (1 subgoal):
 1. valid_SDG_node (CFG_node (sourcenode a'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_SDG_node (CFG_node (sourcenode a'))

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node (CFG_node (sourcenode a'))

goal (1 subgoal):
 1. matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))
[PROOF STEP]
by(rule matched_Nil)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
matched (CFG_node (targetnode a')) ((nsx @ nsx') @ ns') n''
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))
[PROOF STEP]
have "matched (CFG_node (sourcenode a'))
          ([]@(CFG_node (sourcenode a'))#((nsx@nsx')@ns')@[n'']) n'"
[PROOF STATE]
proof (prove)
using this:
matched (CFG_node (targetnode a')) ((nsx @ nsx') @ ns') n''
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))

goal (1 subgoal):
 1. matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ((nsx @ nsx') @ ns') @ [n'']) n'
[PROOF STEP]
using  \<open>n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'\<close> \<open>parent_node n' = targetnode a\<close>
            \<open>parent_node n'' = sourcenode a\<close> \<open>valid_edge a'\<close> \<open>a \<in> get_return_edges a'\<close>
[PROOF STATE]
proof (prove)
using this:
matched (CFG_node (targetnode a')) ((nsx @ nsx') @ ns') n''
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))
n'' s-p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' s-p:V\<rightarrow>\<^bsub>out\<^esub> n'
parent_node n' = targetnode a
parent_node n'' = sourcenode a
valid_edge a'
a \<in> get_return_edges a'

goal (1 subgoal):
 1. matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ((nsx @ nsx') @ ns') @ [n'']) n'
[PROOF STEP]
by(fastforce intro:matched_bracket_call dest:sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ((nsx @ nsx') @ ns') @ [n'']) n'

goal (1 subgoal):
 1. \<And>a list. ns = a # list \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)\<close>
          \<open>parent_node n' = targetnode a\<close> \<open>n \<in> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
parent_node n' = targetnode a
n \<in> set ns'
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ((nsx @ nsx') @ ns') @ [n'']) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
parent_node n' = targetnode a
n \<in> set ns'
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # ((nsx @ nsx') @ ns') @ [n'']) n'

goal (1 subgoal):
 1. \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
fix ms ms' m m' px
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
assume "ns = ms@m#ms'" and "n irs-ms\<rightarrow>\<^sub>d* m"
        and "m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')" and "m' is-ms'\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (state)
this:
ns = ms @ m # ms'
n irs-ms\<rightarrow>\<^sub>d* m
m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')
m' is-ms'\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>ns = ms@m#ms'\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = ms @ m # ms'
[PROOF STEP]
have "length ms < length ns"
[PROOF STATE]
proof (prove)
using this:
ns = ms @ m # ms'

goal (1 subgoal):
 1. length ms < length ns
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length ms < length ns

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with IH \<open>n irs-ms\<rightarrow>\<^sub>d* m\<close> \<open>m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>ns'. length ns' < length ns \<longrightarrow> (\<forall>n''. n irs-ns'\<rightarrow>\<^sub>d* n'' \<longrightarrow> (\<forall>nx' p' V'. n'' s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> n'' s-p':V'\<rightarrow>\<^bsub>out\<^esub> nx' \<longrightarrow> (\<exists>nx nsx. matched nx nsx nx' \<and> n \<in> set nsx \<and> nx s-p'\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx'))))
n irs-ms\<rightarrow>\<^sub>d* m
m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')
length ms < length ns
[PROOF STEP]
obtain mx msx
        where "matched mx msx m'" and "n \<in> set msx"
        and "mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')"
[PROOF STATE]
proof (prove)
using this:
\<forall>ns'. length ns' < length ns \<longrightarrow> (\<forall>n''. n irs-ns'\<rightarrow>\<^sub>d* n'' \<longrightarrow> (\<forall>nx' p' V'. n'' s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> n'' s-p':V'\<rightarrow>\<^bsub>out\<^esub> nx' \<longrightarrow> (\<exists>nx nsx. matched nx nsx nx' \<and> n \<in> set nsx \<and> nx s-p'\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node nx'))))
n irs-ms\<rightarrow>\<^sub>d* m
m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')
length ms < length ns

goal (1 subgoal):
 1. (\<And>mx msx. \<lbrakk>matched mx msx m'; n \<in> set msx; mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
matched mx msx m'
n \<in> set msx
mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>m' is-ms'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
m' is-ms'\<rightarrow>\<^sub>d* n''
[PROOF STEP]
obtain msx' where "matched m' msx' n''"
[PROOF STATE]
proof (prove)
using this:
m' is-ms'\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. (\<And>msx'. matched m' msx' n'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule is_SDG_path_matched)
[PROOF STATE]
proof (state)
this:
matched m' msx' n''

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>matched mx msx m'\<close>
[PROOF STATE]
proof (chain)
picking this:
matched mx msx m'
matched m' msx' n''
[PROOF STEP]
have "matched mx (msx@msx') n''"
[PROOF STATE]
proof (prove)
using this:
matched mx msx m'
matched m' msx' n''

goal (1 subgoal):
 1. matched mx (msx @ msx') n''
[PROOF STEP]
by -(rule matched_Append)
[PROOF STATE]
proof (state)
this:
matched mx (msx @ msx') n''

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')\<close>
[PROOF STATE]
proof (chain)
picking this:
m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')
[PROOF STEP]
have "m -px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m -px:V\<rightarrow>\<^bsub>out\<^esub> m')"
[PROOF STATE]
proof (prove)
using this:
m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')

goal (1 subgoal):
 1. m -px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m -px:V\<rightarrow>\<^bsub>out\<^esub> m')
[PROOF STEP]
by(auto intro:sum_SDG_edge_SDG_edge SDG_edge_sum_SDG_edge)
[PROOF STATE]
proof (state)
this:
m -px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m -px:V\<rightarrow>\<^bsub>out\<^esub> m')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')\<close>
[PROOF STATE]
proof (chain)
picking this:
m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')
[PROOF STEP]
have "CFG_node (parent_node m) s-px\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node m')"
[PROOF STATE]
proof (prove)
using this:
m s-px\<rightarrow>\<^bsub>ret\<^esub> m' \<or> (\<exists>V. m s-px:V\<rightarrow>\<^bsub>out\<^esub> m')

goal (1 subgoal):
 1. CFG_node (parent_node m) s-px\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node m')
[PROOF STEP]
by(fastforce elim:sum_SDG_edge.cases intro:sum_SDG_return_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node m) s-px\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node m')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CFG_node (parent_node m) s-px\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node m')
[PROOF STEP]
obtain ax Qx fx where "valid_edge ax" and "kind ax = Qx\<hookleftarrow>\<^bsub>px\<^esub>fx"
      and "parent_node m = sourcenode ax" and "parent_node m' = targetnode ax"
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node m) s-px\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node m')

goal (1 subgoal):
 1. (\<And>ax Qx fx. \<lbrakk>valid_edge ax; kind ax = Qx\<hookleftarrow>\<^bsub>px\<^esub>fx; parent_node m = sourcenode ax; parent_node m' = targetnode ax\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:sum_SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
valid_edge ax
kind ax = Qx\<hookleftarrow>\<^bsub>px\<^esub>fx
parent_node m = sourcenode ax
parent_node m' = targetnode ax

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge ax\<close> \<open>kind ax = Qx\<hookleftarrow>\<^bsub>px\<^esub>fx\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ax
kind ax = Qx\<hookleftarrow>\<^bsub>px\<^esub>fx
[PROOF STEP]
obtain ax' Qx' rx' fsx'
        where "ax \<in> get_return_edges ax'" and "valid_edge ax'"
        and "kind ax' = Qx':rx'\<hookrightarrow>\<^bsub>px\<^esub>fsx'"
        and "CFG_node (sourcenode ax') s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode ax)"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax
kind ax = Qx\<hookleftarrow>\<^bsub>px\<^esub>fx

goal (1 subgoal):
 1. (\<And>ax' Qx' rx' fsx'. \<lbrakk>ax \<in> get_return_edges ax'; valid_edge ax'; kind ax' = Qx':rx'\<hookrightarrow>\<^bsub>px\<^esub>fsx'; CFG_node (sourcenode ax') s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode ax)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule return_edge_determines_call_and_sum_edge)
[PROOF STATE]
proof (state)
this:
ax \<in> get_return_edges ax'
valid_edge ax'
kind ax' = Qx':rx'\<hookrightarrow>\<^bsub>px\<^esub>fsx'
CFG_node (sourcenode ax') s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode ax)

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>valid_edge ax'\<close> \<open>kind ax' = Qx':rx'\<hookrightarrow>\<^bsub>px\<^esub>fsx'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ax'
kind ax' = Qx':rx'\<hookrightarrow>\<^bsub>px\<^esub>fsx'
[PROOF STEP]
have "CFG_node (sourcenode ax') s-px\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode ax')"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax'
kind ax' = Qx':rx'\<hookrightarrow>\<^bsub>px\<^esub>fsx'

goal (1 subgoal):
 1. CFG_node (sourcenode ax') s-px\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode ax')
[PROOF STEP]
by(fastforce intro:sum_SDG_call_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode ax') s-px\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode ax')

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
from \<open>mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')\<close>
[PROOF STATE]
proof (chain)
picking this:
mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')
[PROOF STEP]
have "valid_SDG_node mx"
[PROOF STATE]
proof (prove)
using this:
mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')

goal (1 subgoal):
 1. valid_SDG_node mx
[PROOF STEP]
by(rule sum_SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
valid_SDG_node mx

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
have "\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
proof(cases "targetnode a' = parent_node mx")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. targetnode a' = parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. targetnode a' \<noteq> parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
targetnode a' = parent_node mx

goal (2 subgoals):
 1. targetnode a' = parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. targetnode a' \<noteq> parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
from \<open>valid_SDG_node mx\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node mx
[PROOF STEP]
have "mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node mx

goal (1 subgoal):
 1. mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx
[PROOF STEP]
by(rule valid_SDG_node_cases)
[PROOF STATE]
proof (state)
this:
mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (2 subgoals):
 1. targetnode a' = parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. targetnode a' \<noteq> parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mx = CFG_node (parent_node mx) \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
assume "mx = CFG_node (parent_node mx)"
[PROOF STATE]
proof (state)
this:
mx = CFG_node (parent_node mx)

goal (2 subgoals):
 1. mx = CFG_node (parent_node mx) \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with \<open>valid_SDG_node mx\<close> True
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node mx
targetnode a' = parent_node mx
mx = CFG_node (parent_node mx)
[PROOF STEP]
have "CFG_node (targetnode a') cd-[]\<rightarrow>\<^sub>d* mx"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node mx
targetnode a' = parent_node mx
mx = CFG_node (parent_node mx)

goal (1 subgoal):
 1. CFG_node (targetnode a') cd-[]\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by(fastforce intro:cdSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-[]\<rightarrow>\<^sub>d* mx

goal (2 subgoals):
 1. mx = CFG_node (parent_node mx) \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-[]\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
assume "CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx"
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with \<open>valid_edge a'\<close> True[THEN sym]
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
parent_node mx = targetnode a'
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx
[PROOF STEP]
have "CFG_node (targetnode a') cd-[]@[CFG_node (targetnode a')]\<rightarrow>\<^sub>d* mx"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
parent_node mx = targetnode a'
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by(fastforce intro:cdep_SDG_path.intros)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. targetnode a' \<noteq> parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. targetnode a' \<noteq> parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
targetnode a' \<noteq> parent_node mx

goal (1 subgoal):
 1. targetnode a' \<noteq> parent_node mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
proof(cases "\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx
            \<longrightarrow> ai \<notin> get_return_edges a'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a'

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a'

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
assume "parent_node mx = (_Exit_)"
[PROOF STATE]
proof (state)
this:
parent_node mx = (_Exit_)

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with \<open>mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')\<close>
[PROOF STATE]
proof (chain)
picking this:
mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')
parent_node mx = (_Exit_)
[PROOF STEP]
obtain ai where "valid_edge ai" and "sourcenode ai = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')
parent_node mx = (_Exit_)

goal (1 subgoal):
 1. (\<And>ai. \<lbrakk>valid_edge ai; sourcenode ai = (_Exit_)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule sum_SDG_edge.cases,auto)
[PROOF STATE]
proof (state)
this:
valid_edge ai
sourcenode ai = (_Exit_)

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
valid_edge ai
sourcenode ai = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule Exit_source)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
parent_node mx = (_Exit_) \<Longrightarrow> False

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
hence "parent_node mx \<noteq> (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
parent_node mx = (_Exit_) \<Longrightarrow> False

goal (1 subgoal):
 1. parent_node mx \<noteq> (_Exit_)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
parent_node mx \<noteq> (_Exit_)

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
from \<open>valid_SDG_node mx\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node mx
[PROOF STEP]
have "valid_node (parent_node mx)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node mx

goal (1 subgoal):
 1. valid_node (parent_node mx)
[PROOF STEP]
by(rule valid_SDG_CFG_node)
[PROOF STATE]
proof (state)
this:
valid_node (parent_node mx)

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_node (parent_node mx)
[PROOF STEP]
obtain asx where "(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node mx"
[PROOF STATE]
proof (prove)
using this:
valid_node (parent_node mx)

goal (1 subgoal):
 1. (\<And>asx. (_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node mx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce intro:Entry_path)
[PROOF STATE]
proof (state)
this:
(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node mx

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node mx
[PROOF STEP]
obtain asx' where "(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx"
            and "\<forall>a' \<in> set asx'. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* parent_node mx

goal (1 subgoal):
 1. (\<And>asx'. \<lbrakk>(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx; \<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule valid_Entry_path_ascending_path)
[PROOF STATE]
proof (state)
this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx
\<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
from \<open>mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')\<close>
[PROOF STATE]
proof (chain)
picking this:
mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')
[PROOF STEP]
obtain nsi where "matched mx nsi (CFG_node (parent_node m'))"
[PROOF STATE]
proof (prove)
using this:
mx s-px\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node m')

goal (1 subgoal):
 1. (\<And>nsi. matched mx nsi (CFG_node (parent_node m')) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule sum_SDG_summary_edge_matched)
[PROOF STATE]
proof (state)
this:
matched mx nsi (CFG_node (parent_node m'))

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matched mx nsi (CFG_node (parent_node m'))
[PROOF STEP]
obtain asi where "parent_node mx -asi\<rightarrow>\<^bsub>sl\<^esub>* parent_node m'"
[PROOF STATE]
proof (prove)
using this:
matched mx nsi (CFG_node (parent_node m'))

goal (1 subgoal):
 1. (\<And>asi. parent_node mx -asi\<rightarrow>\<^bsub>sl\<^esub>* parent_node m' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:matched_same_level_CFG_path)
[PROOF STATE]
proof (state)
this:
parent_node mx -asi\<rightarrow>\<^bsub>sl\<^esub>* parent_node m'

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
hence "get_proc (parent_node mx) = get_proc (parent_node m')"
[PROOF STATE]
proof (prove)
using this:
parent_node mx -asi\<rightarrow>\<^bsub>sl\<^esub>* parent_node m'

goal (1 subgoal):
 1. get_proc (parent_node mx) = get_proc (parent_node m')
[PROOF STEP]
by(rule slp_get_proc)
[PROOF STATE]
proof (state)
this:
get_proc (parent_node mx) = get_proc (parent_node m')

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
from \<open>m' is-ms'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
m' is-ms'\<rightarrow>\<^sub>d* n''
[PROOF STEP]
obtain nsi' where "matched m' nsi' n''"
[PROOF STATE]
proof (prove)
using this:
m' is-ms'\<rightarrow>\<^sub>d* n''

goal (1 subgoal):
 1. (\<And>nsi'. matched m' nsi' n'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule is_SDG_path_matched)
[PROOF STATE]
proof (state)
this:
matched m' nsi' n''

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matched m' nsi' n''
[PROOF STEP]
obtain asi' where "parent_node m' -asi'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''"
[PROOF STATE]
proof (prove)
using this:
matched m' nsi' n''

goal (1 subgoal):
 1. (\<And>asi'. parent_node m' -asi'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule matched_same_level_CFG_path)
[PROOF STATE]
proof (state)
this:
parent_node m' -asi'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
hence "get_proc (parent_node m') = get_proc (parent_node n'')"
[PROOF STATE]
proof (prove)
using this:
parent_node m' -asi'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''

goal (1 subgoal):
 1. get_proc (parent_node m') = get_proc (parent_node n'')
[PROOF STEP]
by(rule slp_get_proc)
[PROOF STATE]
proof (state)
this:
get_proc (parent_node m') = get_proc (parent_node n'')

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with \<open>get_proc (parent_node mx) = get_proc (parent_node m')\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (parent_node mx) = get_proc (parent_node m')
get_proc (parent_node m') = get_proc (parent_node n'')
[PROOF STEP]
have "get_proc (parent_node mx) = get_proc (parent_node n'')"
[PROOF STATE]
proof (prove)
using this:
get_proc (parent_node mx) = get_proc (parent_node m')
get_proc (parent_node m') = get_proc (parent_node n'')

goal (1 subgoal):
 1. get_proc (parent_node mx) = get_proc (parent_node n'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
get_proc (parent_node mx) = get_proc (parent_node n'')

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
from \<open>get_proc (parent_node n'') = p\<close>
            \<open>get_proc (parent_node mx) = get_proc (parent_node n'')\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (parent_node n'') = p
get_proc (parent_node mx) = get_proc (parent_node n'')
[PROOF STEP]
have "get_proc (parent_node mx) = p"
[PROOF STATE]
proof (prove)
using this:
get_proc (parent_node n'') = p
get_proc (parent_node mx) = get_proc (parent_node n'')

goal (1 subgoal):
 1. get_proc (parent_node mx) = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
get_proc (parent_node mx) = p

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
have "\<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
proof(cases "\<forall>a' \<in> set asx'. intra_kind(kind a')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>a'\<in>set asx'. intra_kind (kind a')

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
with \<open>(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx
\<forall>a'\<in>set asx'. intra_kind (kind a')
[PROOF STEP]
have "(_Entry_) -asx'\<rightarrow>\<^sub>\<iota>* parent_node mx"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx
\<forall>a'\<in>set asx'. intra_kind (kind a')

goal (1 subgoal):
 1. (_Entry_) -asx'\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
by(simp add:vp_def intra_path_def)
[PROOF STATE]
proof (state)
this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<iota>* parent_node mx

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
hence "get_proc (_Entry_) = get_proc (parent_node mx)"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<iota>* parent_node mx

goal (1 subgoal):
 1. get_proc (_Entry_) = get_proc (parent_node mx)
[PROOF STEP]
by(rule intra_path_get_procs)
[PROOF STATE]
proof (state)
this:
get_proc (_Entry_) = get_proc (parent_node mx)

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
with \<open>get_proc (parent_node mx) = p\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (parent_node mx) = p
get_proc (_Entry_) = get_proc (parent_node mx)
[PROOF STEP]
have "get_proc (_Entry_) = p"
[PROOF STATE]
proof (prove)
using this:
get_proc (parent_node mx) = p
get_proc (_Entry_) = get_proc (parent_node mx)

goal (1 subgoal):
 1. get_proc (_Entry_) = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
get_proc (_Entry_) = p

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
with \<open>CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')
get_proc (_Entry_) = p
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n'') s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (parent_node n')
get_proc (_Entry_) = p

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(erule sum_SDG_edge.cases,
                auto intro:Main_no_return_source simp:get_proc_Entry)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<forall>a'\<in>set asx'. intra_kind (kind a') \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
 2. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a'\<in>set asx'. intra_kind (kind a'))

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
hence "\<exists>a' \<in> set asx'. \<not> intra_kind (kind a')"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>a'\<in>set asx'. intra_kind (kind a'))

goal (1 subgoal):
 1. \<exists>a'\<in>set asx'. \<not> intra_kind (kind a')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>a'\<in>set asx'. \<not> intra_kind (kind a')

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a'\<in>set asx'. \<not> intra_kind (kind a')
[PROOF STEP]
obtain ai as' as'' where "asx' = as'@ai#as''"
              and "\<not> intra_kind (kind ai)" and "\<forall>a' \<in> set as''. intra_kind (kind a')"
[PROOF STATE]
proof (prove)
using this:
\<exists>a'\<in>set asx'. \<not> intra_kind (kind a')

goal (1 subgoal):
 1. (\<And>as' ai as''. \<lbrakk>asx' = as' @ ai # as''; \<not> intra_kind (kind ai); \<forall>a'\<in>set as''. intra_kind (kind a')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:split_list_last_propE)
[PROOF STATE]
proof (state)
this:
asx' = as' @ ai # as''
\<not> intra_kind (kind ai)
\<forall>a'\<in>set as''. intra_kind (kind a')

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
from \<open>asx' = as'@ai#as''\<close> \<open>\<not> intra_kind (kind ai)\<close>
              \<open>\<forall>a' \<in> set asx'. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<close>
[PROOF STATE]
proof (chain)
picking this:
asx' = as' @ ai # as''
\<not> intra_kind (kind ai)
\<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
obtain Qi ri pi fsi where "kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi"
              and "\<forall>a' \<in> set as'. intra_kind(kind a') \<or>
              (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)"
[PROOF STATE]
proof (prove)
using this:
asx' = as' @ ai # as''
\<not> intra_kind (kind ai)
\<forall>a'\<in>set asx'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)

goal (1 subgoal):
 1. (\<And>Qi ri pi fsi. \<lbrakk>kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi; \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi
\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
from \<open>(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx\<close> \<open>asx' = as'@ai#as''\<close>
              \<open>\<forall>a' \<in> set as''. intra_kind (kind a')\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx
asx' = as' @ ai # as''
\<forall>a'\<in>set as''. intra_kind (kind a')
[PROOF STEP]
have "valid_edge ai" and "targetnode ai -as''\<rightarrow>\<^sub>\<iota>* parent_node mx"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -asx'\<rightarrow>\<^sub>\<surd>* parent_node mx
asx' = as' @ ai # as''
\<forall>a'\<in>set as''. intra_kind (kind a')

goal (1 subgoal):
 1. valid_edge ai &&& targetnode ai -as''\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
by(auto intro:path_split simp:vp_def intra_path_def)
[PROOF STATE]
proof (state)
this:
valid_edge ai
targetnode ai -as''\<rightarrow>\<^sub>\<iota>* parent_node mx

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
hence "get_proc (targetnode ai) = get_proc (parent_node mx)"
[PROOF STATE]
proof (prove)
using this:
valid_edge ai
targetnode ai -as''\<rightarrow>\<^sub>\<iota>* parent_node mx

goal (1 subgoal):
 1. get_proc (targetnode ai) = get_proc (parent_node mx)
[PROOF STEP]
by -(rule intra_path_get_procs)
[PROOF STATE]
proof (state)
this:
get_proc (targetnode ai) = get_proc (parent_node mx)

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
with \<open>get_proc (parent_node mx) = p\<close> \<open>valid_edge ai\<close>
              \<open>kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (parent_node mx) = p
valid_edge ai
kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi
get_proc (targetnode ai) = get_proc (parent_node mx)
[PROOF STEP]
have [simp]:"pi = p"
[PROOF STATE]
proof (prove)
using this:
get_proc (parent_node mx) = p
valid_edge ai
kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi
get_proc (targetnode ai) = get_proc (parent_node mx)

goal (1 subgoal):
 1. pi = p
[PROOF STEP]
by(fastforce dest:get_proc_call)
[PROOF STATE]
proof (state)
this:
pi = p

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
from \<open>valid_edge ai\<close> \<open>valid_edge a'\<close>
              \<open>kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ai
valid_edge a'
kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
[PROOF STEP]
have "targetnode ai = targetnode a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge ai
valid_edge a'
kind ai = Qi:ri\<hookrightarrow>\<^bsub>pi\<^esub>fsi
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'

goal (1 subgoal):
 1. targetnode ai = targetnode a'
[PROOF STEP]
by(fastforce intro:same_proc_call_unique_target)
[PROOF STATE]
proof (state)
this:
targetnode ai = targetnode a'

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set asx'. intra_kind (kind a')) \<Longrightarrow> \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
with \<open>targetnode ai -as''\<rightarrow>\<^sub>\<iota>* parent_node mx\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode ai -as''\<rightarrow>\<^sub>\<iota>* parent_node mx
targetnode ai = targetnode a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
targetnode ai -as''\<rightarrow>\<^sub>\<iota>* parent_node mx
targetnode ai = targetnode a'

goal (1 subgoal):
 1. \<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
[PROOF STEP]
obtain asx where "targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx"
[PROOF STATE]
proof (prove)
using this:
\<exists>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx

goal (1 subgoal):
 1. (\<And>asx. targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
from this \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
            \<open>parent_node mx \<noteq> (_Exit_)\<close> \<open>targetnode a' \<noteq> parent_node mx\<close> True
[PROOF STATE]
proof (chain)
picking this:
targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
parent_node mx \<noteq> (_Exit_)
targetnode a' \<noteq> parent_node mx
\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a'
[PROOF STEP]
obtain msi
            where "CFG_node(targetnode a') cd-msi\<rightarrow>\<^sub>d* CFG_node(parent_node mx)"
[PROOF STATE]
proof (prove)
using this:
targetnode a' -asx\<rightarrow>\<^sub>\<iota>* parent_node mx
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
parent_node mx \<noteq> (_Exit_)
targetnode a' \<noteq> parent_node mx
\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a'

goal (1 subgoal):
 1. (\<And>msi. CFG_node (targetnode a') cd-msi\<rightarrow>\<^sub>d* CFG_node (parent_node mx) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:in_proc_cdep_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-msi\<rightarrow>\<^sub>d* CFG_node (parent_node mx)

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
from \<open>valid_SDG_node mx\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node mx
[PROOF STEP]
have "mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node mx

goal (1 subgoal):
 1. mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx
[PROOF STEP]
by(rule valid_SDG_node_cases)
[PROOF STATE]
proof (state)
this:
mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (2 subgoals):
 1. \<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a' \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mx = CFG_node (parent_node mx) \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
assume "mx = CFG_node (parent_node mx)"
[PROOF STATE]
proof (state)
this:
mx = CFG_node (parent_node mx)

goal (2 subgoals):
 1. mx = CFG_node (parent_node mx) \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with \<open>CFG_node(targetnode a')cd-msi\<rightarrow>\<^sub>d* CFG_node(parent_node mx)\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a') cd-msi\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
mx = CFG_node (parent_node mx)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-msi\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
mx = CFG_node (parent_node mx)

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
assume "CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx"
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with \<open>CFG_node(targetnode a')cd-msi\<rightarrow>\<^sub>d* CFG_node(parent_node mx)\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a') cd-msi\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx
[PROOF STEP]
have "CFG_node(targetnode a') cd-msi@[CFG_node(parent_node mx)]\<rightarrow>\<^sub>d* mx"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-msi\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. CFG_node (targetnode a') cd-msi @ [CFG_node (parent_node mx)]\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by(fastforce intro:cdSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-msi @ [CFG_node (parent_node mx)]\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-msi @ [CFG_node (parent_node mx)]\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a')

goal (1 subgoal):
 1. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a')
[PROOF STEP]
obtain ai where "valid_edge ai" and "sourcenode ai = parent_node mx"
            and "ai \<in> get_return_edges a'"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a')

goal (1 subgoal):
 1. (\<And>ai. \<lbrakk>valid_edge ai; sourcenode ai = parent_node mx; ai \<in> get_return_edges a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
valid_edge ai
sourcenode ai = parent_node mx
ai \<in> get_return_edges a'

goal (1 subgoal):
 1. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
valid_edge ai
sourcenode ai = parent_node mx
ai \<in> get_return_edges a'
[PROOF STEP]
have "CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (parent_node mx)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
valid_edge ai
sourcenode ai = parent_node mx
ai \<in> get_return_edges a'

goal (1 subgoal):
 1. CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (parent_node mx)
[PROOF STEP]
by(auto intro:SDG_proc_entry_exit_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (parent_node mx)

goal (1 subgoal):
 1. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (parent_node mx)
[PROOF STEP]
have cd_path:"CFG_node (targetnode a') cd-[]@[CFG_node (targetnode a')]\<rightarrow>\<^sub>d*
                        CFG_node (parent_node mx)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (parent_node mx)

goal (1 subgoal):
 1. CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
[PROOF STEP]
by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (parent_node mx)

goal (1 subgoal):
 1. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
from \<open>valid_SDG_node mx\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node mx
[PROOF STEP]
have "mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node mx

goal (1 subgoal):
 1. mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx
[PROOF STEP]
by(rule valid_SDG_node_cases)
[PROOF STATE]
proof (state)
this:
mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. \<not> (\<forall>ai. valid_edge ai \<and> sourcenode ai = parent_node mx \<longrightarrow> ai \<notin> get_return_edges a') \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mx = CFG_node (parent_node mx) \<or> CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mx = CFG_node (parent_node mx) \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
assume "mx = CFG_node (parent_node mx)"
[PROOF STATE]
proof (state)
this:
mx = CFG_node (parent_node mx)

goal (2 subgoals):
 1. mx = CFG_node (parent_node mx) \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
 2. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with cd_path
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
mx = CFG_node (parent_node mx)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
mx = CFG_node (parent_node mx)

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
assume "CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx"
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
with cd_path
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx
[PROOF STEP]
have "CFG_node (targetnode a')
              cd-[CFG_node (targetnode a')]@[CFG_node (parent_node mx)]\<rightarrow>\<^sub>d* mx"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (parent_node mx)
CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx

goal (1 subgoal):
 1. CFG_node (targetnode a') cd-[CFG_node (targetnode a')] @ [CFG_node (parent_node mx)]\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by(fastforce intro:cdSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-[CFG_node (targetnode a')] @ [CFG_node (parent_node mx)]\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. CFG_node (parent_node mx) \<longrightarrow>\<^bsub>cd\<^esub> mx \<Longrightarrow> \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-[CFG_node (targetnode a')] @ [CFG_node (parent_node mx)]\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. \<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
obtain msx''
        where "CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx"
[PROOF STATE]
proof (prove)
using this:
\<exists>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. (\<And>msx''. CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
hence "CFG_node (targetnode a') i-msx''\<rightarrow>\<^sub>d* mx"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') cd-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. CFG_node (targetnode a') i-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
by(rule cdep_SDG_path_intra_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') i-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
CFG_node (targetnode a') i-msx''\<rightarrow>\<^sub>d* mx
[PROOF STEP]
have "matched (CFG_node (targetnode a')) ([]@msx'') mx"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
CFG_node (targetnode a') i-msx''\<rightarrow>\<^sub>d* mx

goal (1 subgoal):
 1. matched (CFG_node (targetnode a')) ([] @ msx'') mx
[PROOF STEP]
by(fastforce intro:matched_Append_intra_SDG_path matched_Nil)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) ([] @ msx'') mx

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>matched mx (msx@msx') n''\<close>
[PROOF STATE]
proof (chain)
picking this:
matched mx (msx @ msx') n''
matched (CFG_node (targetnode a')) ([] @ msx'') mx
[PROOF STEP]
have "matched (CFG_node (targetnode a')) (msx''@(msx@msx')) n''"
[PROOF STATE]
proof (prove)
using this:
matched mx (msx @ msx') n''
matched (CFG_node (targetnode a')) ([] @ msx'') mx

goal (1 subgoal):
 1. matched (CFG_node (targetnode a')) (msx'' @ msx @ msx') n''
[PROOF STEP]
by(fastforce intro:matched_Append)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) (msx'' @ msx @ msx') n''

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')\<close>
        \<open>n'' -p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' -p:V\<rightarrow>\<^bsub>out\<^esub> n'\<close> \<open>a \<in> get_return_edges a'\<close>
        \<open>parent_node n'' = sourcenode a\<close> \<open>parent_node n' = targetnode a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
n'' -p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' -p:V\<rightarrow>\<^bsub>out\<^esub> n'
a \<in> get_return_edges a'
parent_node n'' = sourcenode a
parent_node n' = targetnode a
matched (CFG_node (targetnode a')) (msx'' @ msx @ msx') n''
[PROOF STEP]
have "matched (CFG_node (sourcenode a'))
        ([]@CFG_node (sourcenode a')#(msx''@(msx@msx'))@[n'']) n'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
n'' -p\<rightarrow>\<^bsub>ret\<^esub> n' \<or> n'' -p:V\<rightarrow>\<^bsub>out\<^esub> n'
a \<in> get_return_edges a'
parent_node n'' = sourcenode a
parent_node n' = targetnode a
matched (CFG_node (targetnode a')) (msx'' @ msx @ msx') n''

goal (1 subgoal):
 1. matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # (msx'' @ msx @ msx') @ [n'']) n'
[PROOF STEP]
by(fastforce intro:matched_bracket_call matched_Nil sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # (msx'' @ msx @ msx') @ [n'']) n'

goal (1 subgoal):
 1. \<And>nsx nsx' nx nx' p. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
with \<open>n \<in> set msx\<close> \<open>CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)\<close>
        \<open>parent_node n' = targetnode a\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set msx
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
parent_node n' = targetnode a
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # (msx'' @ msx @ msx') @ [n'']) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> set msx
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
parent_node n' = targetnode a
matched (CFG_node (sourcenode a')) ([] @ CFG_node (sourcenode a') # (msx'' @ msx @ msx') @ [n'']) n'

goal (1 subgoal):
 1. \<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>nx nsx. matched nx nsx n' \<and> n \<in> set nsx \<and> nx s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (parent_node n')

goal:
No subgoals!
[PROOF STEP]
qed