[STATEMENT]
lemma Entry_cc_SDG_path_to_inner_node:
  assumes "valid_SDG_node n" and "parent_node n \<noteq> (_Exit_)"
  obtains ns where "CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
obtain m where "m = parent_node n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m = parent_node n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m = parent_node n

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<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. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
thus "\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
valid_node (parent_node n)

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
proof(cases "parent_node n" rule:valid_node_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. parent_node n = (_Entry_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. parent_node n = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 3. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case Entry
[PROOF STATE]
proof (state)
this:
parent_node n = (_Entry_)

goal (3 subgoals):
 1. parent_node n = (_Entry_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. parent_node n = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 3. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
parent_node n = (_Entry_)
[PROOF STEP]
have "n = CFG_node (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
parent_node n = (_Entry_)

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

goal (3 subgoals):
 1. parent_node n = (_Entry_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. parent_node n = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 3. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<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 (_Entry_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = CFG_node (_Entry_)

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
by(fastforce intro:ccSp_Nil)
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n

goal (2 subgoals):
 1. parent_node n = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. parent_node n = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case Exit
[PROOF STATE]
proof (state)
this:
parent_node n = (_Exit_)

goal (2 subgoals):
 1. parent_node n = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>parent_node n \<noteq> (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n \<noteq> (_Exit_)
parent_node n = (_Exit_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
parent_node n \<noteq> (_Exit_)
parent_node n = (_Exit_)

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

goal (2 subgoals):
 1. parent_node n = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case inner
[PROOF STATE]
proof (state)
this:
inner_node (parent_node n)

goal (1 subgoal):
 1. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>m = parent_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
m = parent_node n
inner_node (parent_node n)
[PROOF STEP]
obtain asx where "(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* m"
[PROOF STATE]
proof (prove)
using this:
m = parent_node n
inner_node (parent_node n)

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

goal (1 subgoal):
 1. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* m
[PROOF STEP]
obtain as where "(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m"
      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:
(_Entry_) -asx\<rightarrow>\<^sub>\<surd>* m

goal (1 subgoal):
 1. (\<And>as. \<lbrakk>(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m; \<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 -(erule valid_Entry_path_ascending_path,fastforce)
[PROOF STATE]
proof (state)
this:
(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m
\<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. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>inner_node (parent_node n)\<close> \<open>m = parent_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node (parent_node n)
m = parent_node n
[PROOF STEP]
have "inner_node m"
[PROOF STATE]
proof (prove)
using this:
inner_node (parent_node n)
m = parent_node n

goal (1 subgoal):
 1. inner_node m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inner_node m

goal (1 subgoal):
 1. inner_node (parent_node n) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m\<close> \<open>m = parent_node n\<close> \<open>valid_SDG_node n\<close>
      \<open>\<forall>a' \<in> set as. 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:
(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m
m = parent_node n
valid_SDG_node n
\<forall>a'\<in>set as. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
inner_node m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m
m = parent_node n
valid_SDG_node n
\<forall>a'\<in>set as. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
inner_node m

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
proof(induct as arbitrary:m n rule:length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs m n. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. (_Entry_) -ys\<rightarrow>\<^sub>\<surd>* x \<longrightarrow> (\<forall>xa. x = parent_node xa \<longrightarrow> valid_SDG_node xa \<longrightarrow> (\<forall>a'\<in>set ys. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node x \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* xa))); (_Entry_) -xs\<rightarrow>\<^sub>\<surd>* m; m = parent_node n; valid_SDG_node n; \<forall>a'\<in>set xs. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); inner_node m\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
fix as m n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs m n. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. (_Entry_) -ys\<rightarrow>\<^sub>\<surd>* x \<longrightarrow> (\<forall>xa. x = parent_node xa \<longrightarrow> valid_SDG_node xa \<longrightarrow> (\<forall>a'\<in>set ys. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node x \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* xa))); (_Entry_) -xs\<rightarrow>\<^sub>\<surd>* m; m = parent_node n; valid_SDG_node n; \<forall>a'\<in>set xs. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); inner_node m\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
assume IH:"\<forall>as'. length as' < length as \<longrightarrow>
        (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow>
        (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow>
        (\<forall>a' \<in> set as'. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow>
        inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))"
        and "(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m"
        and "m = parent_node n" and "valid_SDG_node n" and "inner_node m"
        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 (state)
this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))
(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m
m = parent_node n
valid_SDG_node n
inner_node m
\<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. \<And>xs m n. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. (_Entry_) -ys\<rightarrow>\<^sub>\<surd>* x \<longrightarrow> (\<forall>xa. x = parent_node xa \<longrightarrow> valid_SDG_node xa \<longrightarrow> (\<forall>a'\<in>set ys. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node x \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* xa))); (_Entry_) -xs\<rightarrow>\<^sub>\<surd>* m; m = parent_node n; valid_SDG_node n; \<forall>a'\<in>set xs. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); inner_node m\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
show "\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
proof(cases "\<forall>a' \<in> set as. intra_kind(kind a')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>a'\<in>set as. intra_kind (kind a')

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

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

goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
have "\<not> method_exit m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> method_exit m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. method_exit m \<Longrightarrow> False
[PROOF STEP]
assume "method_exit m"
[PROOF STATE]
proof (state)
this:
method_exit m

goal (1 subgoal):
 1. method_exit m \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
method_exit m

goal (1 subgoal):
 1. False
[PROOF STEP]
proof(rule method_exit_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = (_Exit_) \<Longrightarrow> False
 2. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "m = (_Exit_)"
[PROOF STATE]
proof (state)
this:
m = (_Exit_)

goal (2 subgoals):
 1. m = (_Exit_) \<Longrightarrow> False
 2. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>inner_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node m
m = (_Exit_)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
inner_node m
m = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(simp add:inner_node_def)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix a Q f p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "m = sourcenode a" and "valid_edge a"
              and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f"
[PROOF STATE]
proof (state)
this:
m = sourcenode a
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m
[PROOF STEP]
have "get_proc m = Main"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m

goal (1 subgoal):
 1. get_proc m = Main
[PROOF STEP]
by(fastforce dest:intra_path_get_procs simp:get_proc_Entry)
[PROOF STATE]
proof (state)
this:
get_proc m = Main

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[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 (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>get_proc m = Main\<close> \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc m = Main
m = sourcenode a
get_proc (sourcenode a) = p
[PROOF STEP]
have "p = Main"
[PROOF STATE]
proof (prove)
using this:
get_proc m = Main
m = sourcenode a
get_proc (sourcenode a) = p

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

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>m = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<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
p = Main
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
p = Main

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> method_exit m

goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>inner_node m\<close> \<open>(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node m
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m
\<not> method_exit m
[PROOF STEP]
obtain ns where "CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m"
          and "ns \<noteq> []" and "\<forall>n'' \<in> set ns. parent_node n'' \<in> set(sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
inner_node m
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m
\<not> method_exit m

goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m; ns \<noteq> []; \<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule Entry_cdep_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
ns \<noteq> []
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as)

goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
ns \<noteq> []
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as)
[PROOF STEP]
obtain n' where "n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m"
          and "parent_node n' \<in> set(sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
ns \<noteq> []
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m; parent_node n' \<in> set (sourcenodes as)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule cdep_SDG_path.cases,auto)
[PROOF STATE]
proof (state)
this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
parent_node n' \<in> set (sourcenodes as)

goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>parent_node n' \<in> set(sourcenodes as)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n' \<in> set (sourcenodes as)
[PROOF STEP]
obtain ms ms'
          where "sourcenodes as = ms@(parent_node n')#ms'"
[PROOF STATE]
proof (prove)
using this:
parent_node n' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. (\<And>ms ms'. sourcenodes as = ms @ parent_node n' # ms' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:split_list simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
sourcenodes as = ms @ parent_node n' # ms'

goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sourcenodes as = ms @ parent_node n' # ms'
[PROOF STEP]
obtain as' a as'' where "ms = sourcenodes as'"
          and "ms' = sourcenodes as''" and "as = as'@a#as''"
          and "parent_node n' = sourcenode a"
[PROOF STATE]
proof (prove)
using this:
sourcenodes as = ms @ parent_node n' # ms'

goal (1 subgoal):
 1. (\<And>as' as'' a. \<lbrakk>ms = sourcenodes as'; ms' = sourcenodes as''; as = as' @ a # as''; parent_node n' = sourcenode a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
ms = sourcenodes as'
ms' = sourcenodes as''
as = as' @ a # as''
parent_node n' = sourcenode a

goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m
ms = sourcenodes as'
ms' = sourcenodes as''
as = as' @ a # as''
parent_node n' = sourcenode a
[PROOF STEP]
have "(_Entry_) -as'\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* m
ms = sourcenodes as'
ms' = sourcenodes as''
as = as' @ a # as''
parent_node n' = sourcenode a

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

goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
[PROOF STEP]
have "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m

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

goal (2 subgoals):
 1. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
hence n'_cases:
          "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. \<forall>a'\<in>set as. intra_kind (kind a') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
proof(cases "as' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as' = []

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

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

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from n'_cases
[PROOF STATE]
proof (chain)
picking this:
n' = CFG_node (parent_node n') \<or> CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
have "\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m"
[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>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n' = CFG_node (parent_node n') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
 2. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[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>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
 2. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
with \<open>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m\<close> \<open>parent_node n' = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
parent_node n' = (_Entry_)
n' = CFG_node (parent_node n')
[PROOF STEP]
have "CFG_node (_Entry_) cd-[]@[CFG_node (_Entry_)]\<rightarrow>\<^sub>d* CFG_node m"
[PROOF STATE]
proof (prove)
using this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
parent_node n' = (_Entry_)
n' = CFG_node (parent_node n')

goal (1 subgoal):
 1. CFG_node (_Entry_) cd-[] @ [CFG_node (_Entry_)]\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
by -(rule cdSp_Append_cdep,rule cdSp_Nil,auto)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cd-[] @ [CFG_node (_Entry_)]\<rightarrow>\<^sub>d* CFG_node m

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

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m

goal (1 subgoal):
 1. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[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>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
with \<open>parent_node n' = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n' = (_Entry_)
CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
have "CFG_node (_Entry_) cd-[]@[CFG_node (_Entry_)]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
parent_node n' = (_Entry_)
CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n'

goal (1 subgoal):
 1. CFG_node (_Entry_) cd-[] @ [CFG_node (_Entry_)]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by -(rule cdSp_Append_cdep,rule cdSp_Nil,auto)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cd-[] @ [CFG_node (_Entry_)]\<rightarrow>\<^sub>d* n'

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

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

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

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
obtain ns where "CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node m

goal (1 subgoal):
 1. (\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce intro:cdep_SDG_path_cc_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
proof(cases "n = CFG_node m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = CFG_node m

goal (2 subgoals):
 1. n = CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m
n = CFG_node m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m
n = CFG_node m

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> CFG_node m

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>inner_node m\<close> \<open>valid_SDG_node n\<close> \<open>m = parent_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node m
valid_SDG_node n
m = parent_node n
n \<noteq> CFG_node m
[PROOF STEP]
have "CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
using this:
inner_node m
valid_SDG_node n
m = parent_node n
n \<noteq> CFG_node m

goal (1 subgoal):
 1. CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by(fastforce intro:SDG_parent_cdep_edge inner_is_valid)
[PROOF STATE]
proof (state)
this:
CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n

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

goal (1 subgoal):
 1. CFG_node (_Entry_) cc-ns @ [CFG_node m]\<rightarrow>\<^sub>d* n
[PROOF STEP]
by(fastforce intro:ccSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns @ [CFG_node m]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns @ [CFG_node m]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n

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

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as' \<noteq> []

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>as = as'@a#as''\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
as' \<noteq> []
[PROOF STEP]
have "length as' < length as"
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''
as' \<noteq> []

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

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>(_Entry_) -as'\<rightarrow>\<^sub>\<iota>* parent_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
have "valid_node (parent_node n')"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as'\<rightarrow>\<^sub>\<iota>* parent_node n'

goal (1 subgoal):
 1. valid_node (parent_node n')
[PROOF STEP]
by(fastforce intro:path_valid_node simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
valid_node (parent_node n')

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
hence "inner_node (parent_node n')"
[PROOF STATE]
proof (prove)
using this:
valid_node (parent_node n')

goal (1 subgoal):
 1. inner_node (parent_node n')
[PROOF STEP]
proof(cases "parent_node n'" rule:valid_node_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. parent_node n' = (_Entry_) \<Longrightarrow> inner_node (parent_node n')
 2. parent_node n' = (_Exit_) \<Longrightarrow> inner_node (parent_node n')
 3. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
case Entry
[PROOF STATE]
proof (state)
this:
parent_node n' = (_Entry_)

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

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

goal (3 subgoals):
 1. parent_node n' = (_Entry_) \<Longrightarrow> inner_node (parent_node n')
 2. parent_node n' = (_Exit_) \<Longrightarrow> inner_node (parent_node n')
 3. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
as' \<noteq> []
(_Entry_) -as'\<rightarrow>* (_Entry_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
as' \<noteq> []
(_Entry_) -as'\<rightarrow>* (_Entry_)

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

goal (3 subgoals):
 1. parent_node n' = (_Entry_) \<Longrightarrow> inner_node (parent_node n')
 2. parent_node n' = (_Exit_) \<Longrightarrow> inner_node (parent_node n')
 3. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (2 subgoals):
 1. parent_node n' = (_Exit_) \<Longrightarrow> inner_node (parent_node n')
 2. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. parent_node n' = (_Exit_) \<Longrightarrow> inner_node (parent_node n')
 2. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
case Exit
[PROOF STATE]
proof (state)
this:
parent_node n' = (_Exit_)

goal (2 subgoals):
 1. parent_node n' = (_Exit_) \<Longrightarrow> inner_node (parent_node n')
 2. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
with \<open>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
parent_node n' = (_Exit_)
[PROOF STEP]
have "n' = CFG_node (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
parent_node n' = (_Exit_)

goal (1 subgoal):
 1. n' = CFG_node (_Exit_)
[PROOF STEP]
by -(rule valid_SDG_node_parent_Exit,erule SDG_edge_valid_SDG_node,simp)
[PROOF STATE]
proof (state)
this:
n' = CFG_node (_Exit_)

goal (2 subgoals):
 1. parent_node n' = (_Exit_) \<Longrightarrow> inner_node (parent_node n')
 2. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
with \<open>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m\<close> Exit
[PROOF STATE]
proof (chain)
picking this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
parent_node n' = (_Exit_)
n' = CFG_node (_Exit_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
parent_node n' = (_Exit_)
n' = CFG_node (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp(erule Exit_no_SDG_edge_source)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. parent_node n' = (_Exit_) \<Longrightarrow> inner_node (parent_node n')
 2. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
case inner
[PROOF STATE]
proof (state)
this:
inner_node (parent_node n')

goal (1 subgoal):
 1. inner_node (parent_node n') \<Longrightarrow> inner_node (parent_node n')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
inner_node (parent_node n')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inner_node (parent_node n')

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>valid_node (parent_node n')\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node (parent_node n')
[PROOF STEP]
have "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. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>(_Entry_) -as'\<rightarrow>\<^sub>\<iota>* (parent_node n')\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
have "(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* (parent_node n')"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as'\<rightarrow>\<^sub>\<iota>* parent_node n'

goal (1 subgoal):
 1. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'
[PROOF STEP]
by(rule intra_path_vp)
[PROOF STATE]
proof (state)
this:
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>\<forall>a' \<in> set as. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<close>
            \<open>as = as'@a#as''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a'\<in>set as. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
as = as' @ a # as''
[PROOF STEP]
have "\<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:
\<forall>a'\<in>set as. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
as = as' @ a # as''

goal (1 subgoal):
 1. \<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 STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<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. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with IH \<open>length as' < length as\<close> \<open>(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* (parent_node n')\<close>
            \<open>valid_SDG_node (CFG_node (parent_node n'))\<close> \<open>inner_node (parent_node n')\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))
length as' < length as
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'
valid_SDG_node (CFG_node (parent_node n'))
inner_node (parent_node n')
\<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 STEP]
obtain ns where "CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')"
[PROOF STATE]
proof (prove)
using this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))
length as' < length as
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'
valid_SDG_node (CFG_node (parent_node n'))
inner_node (parent_node n')
\<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. (\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="as'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n') \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'; valid_SDG_node (CFG_node (parent_node n')); inner_node (parent_node n'); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n') \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'; valid_node (parent_node n'); inner_node (parent_node n'); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); \<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> inner_node (parent_node n') \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="(parent_node n')" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n') \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'; valid_node (parent_node n'); inner_node (parent_node n'); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n' \<longrightarrow> (\<forall>n'a. parent_node n' = parent_node n'a \<longrightarrow> valid_SDG_node n'a \<longrightarrow> inner_node (parent_node n'a) \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'a))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n') \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'; valid_node (parent_node n'); inner_node (parent_node n'); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); \<forall>n'a. parent_node n' = parent_node n'a \<longrightarrow> valid_SDG_node n'a \<longrightarrow> inner_node (parent_node n'a) \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="CFG_node (parent_node n')" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n') \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* parent_node n'; valid_node (parent_node n'); inner_node (parent_node n'); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); parent_node n' = parent_node (CFG_node (parent_node n')) \<longrightarrow> valid_SDG_node (CFG_node (parent_node n')) \<longrightarrow> inner_node (parent_node (CFG_node (parent_node n'))) \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n'))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from n'_cases
[PROOF STATE]
proof (chain)
picking this:
n' = CFG_node (parent_node n') \<or> CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
have "\<exists>ns. CFG_node (_Entry_) cc-ns\<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>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n' = CFG_node (parent_node n') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'
 2. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<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>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'
 2. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')
n' = CFG_node (parent_node n')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')
n' = CFG_node (parent_node n')

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'

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

goal (1 subgoal):
 1. CFG_node (_Entry_) cc-ns @ [CFG_node (parent_node n')]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:ccSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns @ [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>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns @ [CFG_node (parent_node n')]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'

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

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
obtain ns' where "CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'

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

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

goal (1 subgoal):
 1. CFG_node (_Entry_) cc-ns' @ [n']\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
by(fastforce intro:ccSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns' @ [n']\<rightarrow>\<^sub>d* CFG_node m

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
proof(cases "n = CFG_node m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = CFG_node m

goal (2 subgoals):
 1. n = CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>CFG_node (_Entry_) cc-ns'@[n']\<rightarrow>\<^sub>d* CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cc-ns' @ [n']\<rightarrow>\<^sub>d* CFG_node m
n = CFG_node m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns' @ [n']\<rightarrow>\<^sub>d* CFG_node m
n = CFG_node m

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> CFG_node m

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>inner_node m\<close> \<open>valid_SDG_node n\<close> \<open>m = parent_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node m
valid_SDG_node n
m = parent_node n
n \<noteq> CFG_node m
[PROOF STEP]
have "CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
using this:
inner_node m
valid_SDG_node n
m = parent_node n
n \<noteq> CFG_node m

goal (1 subgoal):
 1. CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by(fastforce intro:SDG_parent_cdep_edge inner_is_valid)
[PROOF STATE]
proof (state)
this:
CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n

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

goal (1 subgoal):
 1. CFG_node (_Entry_) cc-(ns' @ [n']) @ [CFG_node m]\<rightarrow>\<^sub>d* n
[PROOF STEP]
by(fastforce intro:ccSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-(ns' @ [n']) @ [CFG_node m]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-(ns' @ [n']) @ [CFG_node m]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n

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

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

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a'\<in>set as. intra_kind (kind a'))

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
hence "\<exists>a' \<in> set as. \<not> intra_kind (kind a')"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>a'\<in>set as. intra_kind (kind a'))

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

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a'\<in>set as. \<not> intra_kind (kind a')
[PROOF STEP]
obtain a as' as'' where "as = as'@a#as''" and "\<not> intra_kind (kind a)"
          and "\<forall>a' \<in> set as''. intra_kind (kind a')"
[PROOF STATE]
proof (prove)
using this:
\<exists>a'\<in>set as. \<not> intra_kind (kind a')

goal (1 subgoal):
 1. (\<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<not> intra_kind (kind a); \<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:
as = as' @ a # as''
\<not> intra_kind (kind a)
\<forall>a'\<in>set as''. intra_kind (kind a')

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>\<forall>a' \<in> set as. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<close>
          \<open>as = as'@a#as''\<close> \<open>\<not> intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a'\<in>set as. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
as = as' @ a # as''
\<not> intra_kind (kind a)
[PROOF STEP]
obtain Q r p fs where "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
          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:
\<forall>a'\<in>set as. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
as = as' @ a # as''
\<not> intra_kind (kind a)

goal (1 subgoal):
 1. (\<And>Q r p fs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; \<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 a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<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 as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
from \<open>as = as'@a#as''\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
[PROOF STEP]
have "length as' < length as"
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''

goal (1 subgoal):
 1. length as' < length as
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length as' < length as

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

goal (1 subgoal):
 1. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a &&& valid_edge a &&& targetnode a -as''\<rightarrow>\<^sub>\<surd>* m
[PROOF STEP]
by(auto intro:vp_split)
[PROOF STATE]
proof (state)
this:
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a
valid_edge a
targetnode a -as''\<rightarrow>\<^sub>\<surd>* m

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
hence "valid_SDG_node (CFG_node (sourcenode a))"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a
valid_edge a
targetnode a -as''\<rightarrow>\<^sub>\<surd>* m

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. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
have "\<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
proof(cases "targetnode a = m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. targetnode a = m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
 2. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
targetnode a = m

goal (2 subgoals):
 1. targetnode a = m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
 2. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[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
targetnode a = m
[PROOF STEP]
have "CFG_node (sourcenode a) -p\<rightarrow>\<^bsub>call\<^esub> CFG_node m"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = m

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

goal (2 subgoals):
 1. targetnode a = m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
 2. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
have "\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
proof(cases "as' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
 2. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as' = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
 2. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
with \<open>(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a
as' = []
[PROOF STEP]
have "(_Entry_) = sourcenode a"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a
as' = []

goal (1 subgoal):
 1. (_Entry_) = sourcenode a
[PROOF STEP]
by(fastforce simp:vp_def)
[PROOF STATE]
proof (state)
this:
(_Entry_) = sourcenode a

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
 2. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
with \<open>CFG_node (sourcenode a) -p\<rightarrow>\<^bsub>call\<^esub> CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (sourcenode a) -p\<rightarrow>\<^bsub>call\<^esub> CFG_node m
(_Entry_) = sourcenode a
[PROOF STEP]
have "CFG_node (_Entry_) cc-[]\<rightarrow>\<^sub>d* CFG_node (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
CFG_node (sourcenode a) -p\<rightarrow>\<^bsub>call\<^esub> CFG_node m
(_Entry_) = sourcenode a

goal (1 subgoal):
 1. CFG_node (_Entry_) cc-[]\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
by(fastforce intro:ccSp_Nil SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-[]\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
 2. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-[]\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as' \<noteq> []

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
from \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
[PROOF STEP]
have "valid_node (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a

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

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
hence "inner_node (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
valid_node (sourcenode a)

goal (1 subgoal):
 1. inner_node (sourcenode a)
[PROOF STEP]
proof(cases "sourcenode a" rule:valid_node_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sourcenode a = (_Entry_) \<Longrightarrow> inner_node (sourcenode a)
 2. sourcenode a = (_Exit_) \<Longrightarrow> inner_node (sourcenode a)
 3. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
case Entry
[PROOF STATE]
proof (state)
this:
sourcenode a = (_Entry_)

goal (3 subgoals):
 1. sourcenode a = (_Entry_) \<Longrightarrow> inner_node (sourcenode a)
 2. sourcenode a = (_Exit_) \<Longrightarrow> inner_node (sourcenode a)
 3. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
with \<open>(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a
sourcenode a = (_Entry_)
[PROOF STEP]
have "(_Entry_) -as'\<rightarrow>* (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a
sourcenode a = (_Entry_)

goal (1 subgoal):
 1. (_Entry_) -as'\<rightarrow>* (_Entry_)
[PROOF STEP]
by(fastforce simp:vp_def)
[PROOF STATE]
proof (state)
this:
(_Entry_) -as'\<rightarrow>* (_Entry_)

goal (3 subgoals):
 1. sourcenode a = (_Entry_) \<Longrightarrow> inner_node (sourcenode a)
 2. sourcenode a = (_Exit_) \<Longrightarrow> inner_node (sourcenode a)
 3. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
as' \<noteq> []
(_Entry_) -as'\<rightarrow>* (_Entry_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
as' \<noteq> []
(_Entry_) -as'\<rightarrow>* (_Entry_)

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

goal (3 subgoals):
 1. sourcenode a = (_Entry_) \<Longrightarrow> inner_node (sourcenode a)
 2. sourcenode a = (_Exit_) \<Longrightarrow> inner_node (sourcenode a)
 3. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (2 subgoals):
 1. sourcenode a = (_Exit_) \<Longrightarrow> inner_node (sourcenode a)
 2. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sourcenode a = (_Exit_) \<Longrightarrow> inner_node (sourcenode a)
 2. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
case Exit
[PROOF STATE]
proof (state)
this:
sourcenode a = (_Exit_)

goal (2 subgoals):
 1. sourcenode a = (_Exit_) \<Longrightarrow> inner_node (sourcenode a)
 2. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
with \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
sourcenode a = (_Exit_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
sourcenode a = (_Exit_)

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

goal (2 subgoals):
 1. sourcenode a = (_Exit_) \<Longrightarrow> inner_node (sourcenode a)
 2. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
case inner
[PROOF STATE]
proof (state)
this:
inner_node (sourcenode a)

goal (1 subgoal):
 1. inner_node (sourcenode a) \<Longrightarrow> inner_node (sourcenode a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
inner_node (sourcenode a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inner_node (sourcenode a)

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
with IH \<open>length as' < length as\<close> \<open>(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a\<close>
              \<open>valid_SDG_node (CFG_node (sourcenode a))\<close>
              \<open>\<forall>a' \<in> set as'. 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>as'. length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))
length as' < length as
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a
valid_SDG_node (CFG_node (sourcenode a))
\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
inner_node (sourcenode a)
[PROOF STEP]
obtain ns where "CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))
length as' < length as
(_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a
valid_SDG_node (CFG_node (sourcenode a))
\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
inner_node (sourcenode a)

goal (1 subgoal):
 1. (\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="as'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a) \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a; valid_SDG_node (CFG_node (sourcenode a)); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); inner_node (sourcenode a); length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a) \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a; valid_node (sourcenode a); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); inner_node (sourcenode a); \<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> inner_node (parent_node n') \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="sourcenode a" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a) \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a; valid_node (sourcenode a); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); inner_node (sourcenode a); (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a \<longrightarrow> (\<forall>n'. sourcenode a = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> inner_node (parent_node n') \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a) \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a; valid_node (sourcenode a); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); inner_node (sourcenode a); \<forall>n'. sourcenode a = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> inner_node (parent_node n') \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="CFG_node (sourcenode a)" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a) \<Longrightarrow> thesis; length as' < length as; (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* sourcenode a; valid_node (sourcenode a); \<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); inner_node (sourcenode a); sourcenode a = parent_node (CFG_node (sourcenode a)) \<longrightarrow> valid_SDG_node (CFG_node (sourcenode a)) \<longrightarrow> inner_node (parent_node (CFG_node (sourcenode a))) \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (2 subgoals):
 1. targetnode a = m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
 2. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
obtain ns where "CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (1 subgoal):
 1. (\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (2 subgoals):
 1. targetnode a = m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
 2. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
with \<open>CFG_node (sourcenode a) -p\<rightarrow>\<^bsub>call\<^esub> CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (sourcenode a) -p\<rightarrow>\<^bsub>call\<^esub> CFG_node m
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (sourcenode a) -p\<rightarrow>\<^bsub>call\<^esub> CFG_node m
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (1 subgoal):
 1. \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
by(fastforce intro:ccSp_Append_call)
[PROOF STATE]
proof (state)
this:
\<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m

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

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
from \<open>targetnode a -as''\<rightarrow>\<^sub>\<surd>* m\<close> \<open>\<forall>a' \<in> set as''. intra_kind (kind a')\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -as''\<rightarrow>\<^sub>\<surd>* m
\<forall>a'\<in>set as''. intra_kind (kind a')
[PROOF STEP]
have "targetnode a -as''\<rightarrow>\<^sub>\<iota>* m"
[PROOF STATE]
proof (prove)
using this:
targetnode a -as''\<rightarrow>\<^sub>\<surd>* m
\<forall>a'\<in>set as''. intra_kind (kind a')

goal (1 subgoal):
 1. targetnode a -as''\<rightarrow>\<^sub>\<iota>* m
[PROOF STEP]
by(fastforce simp:vp_def intra_path_def)
[PROOF STATE]
proof (state)
this:
targetnode a -as''\<rightarrow>\<^sub>\<iota>* m

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
hence "get_proc (targetnode a) = get_proc m"
[PROOF STATE]
proof (prove)
using this:
targetnode a -as''\<rightarrow>\<^sub>\<iota>* m

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

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[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 "get_proc (targetnode a) = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

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

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
from \<open>inner_node m\<close> \<open>valid_edge a\<close> \<open>targetnode a -as''\<rightarrow>\<^sub>\<iota>* m\<close>
            \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>targetnode a \<noteq> m\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node m
valid_edge a
targetnode a -as''\<rightarrow>\<^sub>\<iota>* m
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a \<noteq> m
[PROOF STEP]
obtain ns where "CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m"
            and "ns \<noteq> []"
            and "\<forall>n'' \<in> set ns. parent_node n'' \<in> set(sourcenodes as'')"
[PROOF STATE]
proof (prove)
using this:
inner_node m
valid_edge a
targetnode a -as''\<rightarrow>\<^sub>\<iota>* m
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a \<noteq> m

goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m; ns \<noteq> []; \<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:in_proc_cdep_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m
ns \<noteq> []
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as'')

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m
ns \<noteq> []
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as'')
[PROOF STEP]
obtain n' where "n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m"
            and "parent_node n' \<in> set(sourcenodes as'')"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m
ns \<noteq> []
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as'')

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m; parent_node n' \<in> set (sourcenodes as'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule cdep_SDG_path.cases,auto)
[PROOF STATE]
proof (state)
this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
parent_node n' \<in> set (sourcenodes as'')

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
from \<open>(parent_node n') \<in> set(sourcenodes as'')\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n' \<in> set (sourcenodes as'')
[PROOF STEP]
obtain ms ms'
            where "sourcenodes as'' = ms@(parent_node n')#ms'"
[PROOF STATE]
proof (prove)
using this:
parent_node n' \<in> set (sourcenodes as'')

goal (1 subgoal):
 1. (\<And>ms ms'. sourcenodes as'' = ms @ parent_node n' # ms' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:split_list simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
sourcenodes as'' = ms @ parent_node n' # ms'

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sourcenodes as'' = ms @ parent_node n' # ms'
[PROOF STEP]
obtain xs a' ys where "ms = sourcenodes xs"
            and "ms' = sourcenodes ys" and "as'' = xs@a'#ys"
            and "parent_node n' = sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
sourcenodes as'' = ms @ parent_node n' # ms'

goal (1 subgoal):
 1. (\<And>xs ys a'. \<lbrakk>ms = sourcenodes xs; ms' = sourcenodes ys; as'' = xs @ a' # ys; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
ms = sourcenodes xs
ms' = sourcenodes ys
as'' = xs @ a' # ys
parent_node n' = sourcenode a'

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
from \<open>(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m\<close> \<open>as = as'@a#as''\<close> \<open>as'' = xs@a'#ys\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m
as = as' @ a # as''
as'' = xs @ a' # ys
[PROOF STEP]
have "(_Entry_) -(as'@a#xs)@a'#ys\<rightarrow>\<^sub>\<surd>* m"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>\<^sub>\<surd>* m
as = as' @ a # as''
as'' = xs @ a' # ys

goal (1 subgoal):
 1. (_Entry_) -(as' @ a # xs) @ a' # ys\<rightarrow>\<^sub>\<surd>* m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(_Entry_) -(as' @ a # xs) @ a' # ys\<rightarrow>\<^sub>\<surd>* m

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
hence "(_Entry_) -as'@a#xs\<rightarrow>\<^sub>\<surd>* sourcenode a'"
            and "valid_edge a'"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -(as' @ a # xs) @ a' # ys\<rightarrow>\<^sub>\<surd>* m

goal (1 subgoal):
 1. (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a' &&& valid_edge a'
[PROOF STEP]
by(auto intro:vp_split)
[PROOF STATE]
proof (state)
this:
(_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'
valid_edge a'

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
from \<open>as = as'@a#as''\<close> \<open>as'' = xs@a'#ys\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
as'' = xs @ a' # ys
[PROOF STEP]
have "length (as'@a#xs) < length as"
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''
as'' = xs @ a' # ys

goal (1 subgoal):
 1. length (as' @ a # xs) < length as
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (as' @ a # xs) < length as

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
from \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
[PROOF STEP]
have "valid_node (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'

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

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
hence "inner_node (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
valid_node (sourcenode a')

goal (1 subgoal):
 1. inner_node (sourcenode a')
[PROOF STEP]
proof(cases "sourcenode a'" rule:valid_node_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sourcenode a' = (_Entry_) \<Longrightarrow> inner_node (sourcenode a')
 2. sourcenode a' = (_Exit_) \<Longrightarrow> inner_node (sourcenode a')
 3. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
case Entry
[PROOF STATE]
proof (state)
this:
sourcenode a' = (_Entry_)

goal (3 subgoals):
 1. sourcenode a' = (_Entry_) \<Longrightarrow> inner_node (sourcenode a')
 2. sourcenode a' = (_Exit_) \<Longrightarrow> inner_node (sourcenode a')
 3. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
with \<open>(_Entry_) -as'@a#xs\<rightarrow>\<^sub>\<surd>* sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'
sourcenode a' = (_Entry_)
[PROOF STEP]
have "(_Entry_) -as'@a#xs\<rightarrow>* (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'
sourcenode a' = (_Entry_)

goal (1 subgoal):
 1. (_Entry_) -as' @ a # xs\<rightarrow>* (_Entry_)
[PROOF STEP]
by(fastforce simp:vp_def)
[PROOF STATE]
proof (state)
this:
(_Entry_) -as' @ a # xs\<rightarrow>* (_Entry_)

goal (3 subgoals):
 1. sourcenode a' = (_Entry_) \<Longrightarrow> inner_node (sourcenode a')
 2. sourcenode a' = (_Exit_) \<Longrightarrow> inner_node (sourcenode a')
 3. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as' @ a # xs\<rightarrow>* (_Entry_)

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

goal (3 subgoals):
 1. sourcenode a' = (_Entry_) \<Longrightarrow> inner_node (sourcenode a')
 2. sourcenode a' = (_Exit_) \<Longrightarrow> inner_node (sourcenode a')
 3. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (2 subgoals):
 1. sourcenode a' = (_Exit_) \<Longrightarrow> inner_node (sourcenode a')
 2. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sourcenode a' = (_Exit_) \<Longrightarrow> inner_node (sourcenode a')
 2. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
case Exit
[PROOF STATE]
proof (state)
this:
sourcenode a' = (_Exit_)

goal (2 subgoals):
 1. sourcenode a' = (_Exit_) \<Longrightarrow> inner_node (sourcenode a')
 2. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
with \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
sourcenode a' = (_Exit_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
sourcenode a' = (_Exit_)

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

goal (2 subgoals):
 1. sourcenode a' = (_Exit_) \<Longrightarrow> inner_node (sourcenode a')
 2. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
case inner
[PROOF STATE]
proof (state)
this:
inner_node (sourcenode a')

goal (1 subgoal):
 1. inner_node (sourcenode a') \<Longrightarrow> inner_node (sourcenode a')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
inner_node (sourcenode a')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inner_node (sourcenode a')

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[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. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
from \<open>\<forall>a' \<in> set as. intra_kind(kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<close>
            \<open>as = as'@a#as''\<close> \<open>as'' = xs@a'#ys\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a'\<in>set as. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
as = as' @ a # as''
as'' = xs @ a' # ys
[PROOF STEP]
have "\<forall>a' \<in> set (as'@a#xs).
            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:
\<forall>a'\<in>set as. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
as = as' @ a # as''
as'' = xs @ a' # ys

goal (1 subgoal):
 1. \<forall>a'\<in>set (as' @ a # xs). intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a'\<in>set (as' @ a # xs). intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
with IH \<open>length (as'@a#xs) < length as\<close>
            \<open>(_Entry_) -as'@a#xs\<rightarrow>\<^sub>\<surd>* sourcenode a'\<close>
            \<open>valid_SDG_node (CFG_node (sourcenode a'))\<close>
            \<open>inner_node (sourcenode a')\<close> \<open>parent_node n' = sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))
length (as' @ a # xs) < length as
(_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'
valid_SDG_node (CFG_node (sourcenode a'))
inner_node (sourcenode a')
parent_node n' = sourcenode a'
\<forall>a'\<in>set (as' @ a # xs). intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
obtain ns where "CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')"
[PROOF STATE]
proof (prove)
using this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as'\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set as'. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))
length (as' @ a # xs) < length as
(_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'
valid_SDG_node (CFG_node (sourcenode a'))
inner_node (sourcenode a')
parent_node n' = sourcenode a'
\<forall>a'\<in>set (as' @ a # xs). intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)

goal (1 subgoal):
 1. (\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="as'@a#xs" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n') \<Longrightarrow> thesis; length (as' @ a # xs) < length as; (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'; valid_SDG_node (CFG_node (sourcenode a')); inner_node (sourcenode a'); parent_node n' = sourcenode a'; \<forall>a'\<in>set (as' @ a # xs). intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); length (as' @ a # xs) < length as \<longrightarrow> (\<forall>m'. (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> (\<forall>a'\<in>set (as' @ a # xs). intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)) \<longrightarrow> inner_node m' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a') \<Longrightarrow> thesis; Suc (length as' + length xs) < length as; (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'; valid_node (sourcenode a'); inner_node (sourcenode a'); parent_node n' = sourcenode a'; \<forall>m'. (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* m' \<longrightarrow> (\<forall>n'. m' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> inner_node (parent_node n') \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')); intra_kind (kind a) \<or> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); \<forall>a'\<in>set as' \<union> set xs. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="sourcenode a'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a') \<Longrightarrow> thesis; Suc (length as' + length xs) < length as; (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'; valid_node (sourcenode a'); inner_node (sourcenode a'); parent_node n' = sourcenode a'; intra_kind (kind a) \<or> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); \<forall>a'\<in>set as' \<union> set xs. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a' \<longrightarrow> (\<forall>n'. sourcenode a' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> inner_node (parent_node n') \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n'))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a') \<Longrightarrow> thesis; Suc (length as' + length xs) < length as; (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'; valid_node (sourcenode a'); inner_node (sourcenode a'); parent_node n' = sourcenode a'; intra_kind (kind a) \<or> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); \<forall>a'\<in>set as' \<union> set xs. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); \<forall>n'. sourcenode a' = parent_node n' \<longrightarrow> valid_SDG_node n' \<longrightarrow> inner_node (parent_node n') \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="CFG_node (sourcenode a')" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a') \<Longrightarrow> thesis; Suc (length as' + length xs) < length as; (_Entry_) -as' @ a # xs\<rightarrow>\<^sub>\<surd>* sourcenode a'; valid_node (sourcenode a'); inner_node (sourcenode a'); parent_node n' = sourcenode a'; intra_kind (kind a) \<or> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); \<forall>a'\<in>set as' \<union> set xs. intra_kind (kind a') \<or> (\<exists>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs); sourcenode a' = parent_node (CFG_node (sourcenode a')) \<longrightarrow> valid_SDG_node (CFG_node (sourcenode a')) \<longrightarrow> inner_node (parent_node (CFG_node (sourcenode a'))) \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode a'))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
from \<open>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
[PROOF STEP]
have "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m

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

goal (1 subgoal):
 1. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
hence "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. targetnode a \<noteq> m \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
thus ?thesis
[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>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n' = CFG_node (parent_node n') \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
 2. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[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>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
 2. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
with \<open>CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')\<close>
              \<open>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
n' = CFG_node (parent_node n')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
n' = CFG_node (parent_node n')

goal (1 subgoal):
 1. \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
by(fastforce intro:ccSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
\<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m

goal (1 subgoal):
 1. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[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>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
with \<open>CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')
CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
have "CFG_node (_Entry_) cc-ns@[CFG_node (parent_node n')]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node (parent_node n')
CFG_node (parent_node n') \<longrightarrow>\<^bsub>cd\<^esub> n'

goal (1 subgoal):
 1. CFG_node (_Entry_) cc-ns @ [CFG_node (parent_node n')]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:ccSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns @ [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>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
with \<open>n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
CFG_node (_Entry_) cc-ns @ [CFG_node (parent_node n')]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' \<longrightarrow>\<^bsub>cd\<^esub> CFG_node m
CFG_node (_Entry_) cc-ns @ [CFG_node (parent_node n')]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
by(fastforce intro:ccSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
\<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m
[PROOF STEP]
obtain ns where "CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. CFG_node (_Entry_) cc-ns'\<rightarrow>\<^sub>d* CFG_node m

goal (1 subgoal):
 1. (\<And>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m

goal (1 subgoal):
 1. \<not> (\<forall>a'\<in>set as. intra_kind (kind a')) \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
proof(cases "n = CFG_node m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = CFG_node m

goal (2 subgoals):
 1. n = CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
 2. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m
n = CFG_node m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m
n = CFG_node m

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> CFG_node m

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>inner_node m\<close> \<open>valid_SDG_node n\<close> \<open>m = parent_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node m
valid_SDG_node n
m = parent_node n
n \<noteq> CFG_node m
[PROOF STEP]
have "CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
using this:
inner_node m
valid_SDG_node n
m = parent_node n
n \<noteq> CFG_node m

goal (1 subgoal):
 1. CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by(fastforce intro:SDG_parent_cdep_edge inner_is_valid)
[PROOF STATE]
proof (state)
this:
CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. n \<noteq> CFG_node m \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
with \<open>CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m
CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* CFG_node m
CFG_node m \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n
[PROOF STEP]
by(fastforce dest:ccSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cc-ns\<rightarrow>\<^sub>d* n

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed