[STATEMENT]
lemma intra_SDG_path_intra_CFG_path:
  assumes "n i-ns\<rightarrow>\<^sub>d* n'"
  obtains as where "parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>n i-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n i-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show "\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
n i-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
proof(induct rule:intra_SDG_path.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<And>n ns n'' n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
case (iSp_Nil n)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n

goal (3 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<And>n ns n'' n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
[PROOF STEP]
have "valid_node (parent_node n)"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

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

goal (3 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<And>n ns n'' n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
hence "parent_node n -[]\<rightarrow>* parent_node n"
[PROOF STATE]
proof (prove)
using this:
valid_node (parent_node n)

goal (1 subgoal):
 1. parent_node n -[]\<rightarrow>* parent_node n
[PROOF STEP]
by(rule empty_path)
[PROOF STATE]
proof (state)
this:
parent_node n -[]\<rightarrow>* parent_node n

goal (3 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<And>n ns n'' n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
parent_node n -[]\<rightarrow>* parent_node n

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

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
case (iSp_Append_cdep n ns n'' n')
[PROOF STATE]
proof (state)
this:
n i-ns\<rightarrow>\<^sub>d* n''
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
n'' \<longrightarrow>\<^bsub>cd\<^esub> n'

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
[PROOF STEP]
obtain as where "parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''

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

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' \<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n'' \<longrightarrow>\<^bsub>cd\<^esub> n'

goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
proof(rule cdep_edge_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. parent_node n'' controls parent_node n' \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
assume "parent_node n'' controls parent_node n'"
[PROOF STATE]
proof (state)
this:
parent_node n'' controls parent_node n'

goal (3 subgoals):
 1. parent_node n'' controls parent_node n' \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
parent_node n'' controls parent_node n'
[PROOF STEP]
obtain as' where "parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'" and "as' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
parent_node n'' controls parent_node n'

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

goal (3 subgoals):
 1. parent_node n'' controls parent_node n' \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
with \<open>parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
as' \<noteq> []
[PROOF STEP]
have "parent_node n -as@as'\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
as' \<noteq> []

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

goal (3 subgoals):
 1. parent_node n'' controls parent_node n' \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
parent_node n -as @ as'\<rightarrow>\<^sub>\<iota>* parent_node n'

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

goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
fix a Q r p fs a'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
assume "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "a' \<in> get_return_edges a"
        and "parent_node n'' = targetnode a" and "parent_node n' = sourcenode a'"
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
parent_node n'' = targetnode a
parent_node n' = sourcenode a'

goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
parent_node n'' = targetnode a
parent_node n' = sourcenode a'
[PROOF STEP]
obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
        and "targetnode a'' = sourcenode a'" and "kind a'' = (\<lambda>cf. False)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
parent_node n'' = targetnode a
parent_node n' = sourcenode a'

goal (1 subgoal):
 1. (\<And>a''. \<lbrakk>valid_edge a''; sourcenode a'' = targetnode a; targetnode a'' = sourcenode a'; kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest:intra_proc_additional_edge)
[PROOF STATE]
proof (state)
this:
valid_edge a''
sourcenode a'' = targetnode a
targetnode a'' = sourcenode a'
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
hence "targetnode a -[a'']\<rightarrow>\<^sub>\<iota>* sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a''
sourcenode a'' = targetnode a
targetnode a'' = sourcenode a'
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

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

goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
with \<open>parent_node n'' = targetnode a\<close> \<open>parent_node n' = sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n'' = targetnode a
parent_node n' = sourcenode a'
targetnode a -[a'']\<rightarrow>\<^sub>\<iota>* sourcenode a'
[PROOF STEP]
have "\<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n' \<and> as' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
parent_node n'' = targetnode a
parent_node n' = sourcenode a'
targetnode a -[a'']\<rightarrow>\<^sub>\<iota>* sourcenode a'

goal (1 subgoal):
 1. \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n' \<and> as' \<noteq> []
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n' \<and> as' \<noteq> []

goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n' \<and> as' \<noteq> []
[PROOF STEP]
obtain as' where "parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'" and "as' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
\<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n' \<and> as' \<noteq> []

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

goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
with \<open>parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
as' \<noteq> []
[PROOF STEP]
have "parent_node n -as@as'\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
as' \<noteq> []

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

goal (2 subgoals):
 1. \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n'' = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
parent_node n -as @ as'\<rightarrow>\<^sub>\<iota>* parent_node n'

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

goal (1 subgoal):
 1. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
assume "n'' = CFG_node m" and "m = parent_node n'"
[PROOF STATE]
proof (state)
this:
n'' = CFG_node m
m = parent_node n'

goal (1 subgoal):
 1. \<And>m. \<lbrakk>n'' = CFG_node m; m = parent_node n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
with \<open>parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
n'' = CFG_node m
m = parent_node n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
n'' = CFG_node m
m = parent_node n'

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

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

goal (1 subgoal):
 1. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
case (iSp_Append_ddep n ns n'' V n')
[PROOF STATE]
proof (state)
this:
n i-ns\<rightarrow>\<^sub>d* n''
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
n'' -V\<rightarrow>\<^sub>d\<^sub>d n'
n'' \<noteq> n'

goal (1 subgoal):
 1. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
[PROOF STEP]
obtain as where "parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''

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

goal (1 subgoal):
 1. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>n'' -V\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -V\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "n'' influences V in n'"
[PROOF STATE]
proof (prove)
using this:
n'' -V\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. n'' influences V in n'
[PROOF STEP]
by(fastforce elim:SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
n'' influences V in n'

goal (1 subgoal):
 1. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n'' influences V in n'
[PROOF STEP]
obtain as' where "parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
n'' influences V in n'

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

goal (1 subgoal):
 1. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
with \<open>parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
have "parent_node n -as@as'\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'

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

goal (1 subgoal):
 1. \<And>n ns n'' V n'. \<lbrakk>n i-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' -V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
parent_node n -as @ as'\<rightarrow>\<^sub>\<iota>* parent_node n'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cdep_SDG_path_intra_SDG_path:
  "n cd-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n i-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n cd-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n i-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:cdep_SDG_path.induct,auto intro:intra_SDG_path.intros)


[STATEMENT]
lemma Entry_cdep_SDG_path:
  assumes "(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'" and "inner_node n'" and "\<not> method_exit n'"
  obtains ns where "CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'"
  and "ns \<noteq> []" and "\<forall>n'' \<in> set ns. parent_node n'' \<in> set(sourcenodes as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'; ns \<noteq> []; \<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>inner_node n'\<close> \<open>\<not> method_exit n'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'
inner_node n'
\<not> method_exit n'
[PROOF STEP]
show "\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and>
    (\<forall>n'' \<in> set ns. parent_node n'' \<in> set(sourcenodes as))"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'
inner_node n'
\<not> method_exit n'

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(induct as arbitrary:n' rule:length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. (_Entry_) -ys\<rightarrow>\<^sub>\<iota>* x \<longrightarrow> inner_node x \<longrightarrow> \<not> method_exit x \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node x \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes ys)))); (_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'; inner_node n'; \<not> method_exit n'\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes xs))
[PROOF STEP]
fix as n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. (_Entry_) -ys\<rightarrow>\<^sub>\<iota>* x \<longrightarrow> inner_node x \<longrightarrow> \<not> method_exit x \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node x \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes ys)))); (_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'; inner_node n'; \<not> method_exit n'\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes xs))
[PROOF STEP]
assume IH:"\<forall>as'. length as' < length as \<longrightarrow>
      (\<forall>n''. (_Entry_) -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> inner_node n'' \<longrightarrow> \<not> method_exit n'' \<longrightarrow>
        (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and>
              (\<forall>nx\<in>set ns. parent_node nx \<in> set (sourcenodes as'))))"
      and "(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'" and "inner_node n'" and "\<not> method_exit n'"
[PROOF STATE]
proof (state)
this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. (_Entry_) -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> inner_node n'' \<longrightarrow> \<not> method_exit n'' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>nx\<in>set ns. parent_node nx \<in> set (sourcenodes as'))))
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'
inner_node n'
\<not> method_exit n'

goal (1 subgoal):
 1. \<And>xs n'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. (_Entry_) -ys\<rightarrow>\<^sub>\<iota>* x \<longrightarrow> inner_node x \<longrightarrow> \<not> method_exit x \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node x \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes ys)))); (_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'; inner_node n'; \<not> method_exit n'\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes xs))
[PROOF STEP]
thus "\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and>
      (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))"
[PROOF STATE]
proof (prove)
using this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. (_Entry_) -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> inner_node n'' \<longrightarrow> \<not> method_exit n'' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>nx\<in>set ns. parent_node nx \<in> set (sourcenodes as'))))
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'
inner_node n'
\<not> method_exit n'

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. (_Entry_) -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> inner_node n'' \<longrightarrow> \<not> method_exit n'' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>nx\<in>set ns. parent_node nx \<in> set (sourcenodes as')))); (_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'; inner_node n'; \<not> method_exit n'\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
have "\<exists>ax asx zs. (_Entry_) -ax#asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax#asx)) \<and>
                        as = (ax#asx)@zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
proof(cases "n' \<in> set (sourcenodes as)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n' \<in> set (sourcenodes as)

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
hence "\<exists>n'' \<in> set(sourcenodes as). n' = n''"
[PROOF STATE]
proof (prove)
using this:
n' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>n''\<in>set (sourcenodes as). n' = n''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>n''\<in>set (sourcenodes as). n' = n''

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n''\<in>set (sourcenodes as). n' = n''
[PROOF STEP]
obtain ns' ns'' where "sourcenodes as = ns'@n'#ns''"
          and "\<forall>n'' \<in> set ns'. n' \<noteq> n''"
[PROOF STATE]
proof (prove)
using this:
\<exists>n''\<in>set (sourcenodes as). n' = n''

goal (1 subgoal):
 1. (\<And>ns' ns''. \<lbrakk>sourcenodes as = ns' @ n' # ns''; \<forall>n''\<in>set ns'. n' \<noteq> n''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:split_list_first_propE)
[PROOF STATE]
proof (state)
this:
sourcenodes as = ns' @ n' # ns''
\<forall>n''\<in>set ns'. n' \<noteq> n''

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
from \<open>sourcenodes as = ns'@n'#ns''\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenodes as = ns' @ n' # ns''
[PROOF STEP]
obtain xs ys ax
          where "sourcenodes xs = ns'" and "as = xs@ax#ys"
          and "sourcenode ax = n'"
[PROOF STATE]
proof (prove)
using this:
sourcenodes as = ns' @ n' # ns''

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

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
from \<open>\<forall>n'' \<in> set ns'. n' \<noteq> n''\<close> \<open>sourcenodes xs = ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n''\<in>set ns'. n' \<noteq> n''
sourcenodes xs = ns'
[PROOF STEP]
have "n' \<notin> set(sourcenodes xs)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n''\<in>set ns'. n' \<noteq> n''
sourcenodes xs = ns'

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

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
from \<open>(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>as = xs@ax#ys\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'
as = xs @ ax # ys
[PROOF STEP]
have "(_Entry_) -xs@ax#ys\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'
as = xs @ ax # ys

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

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
with \<open>sourcenode ax = n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode ax = n'
(_Entry_) -xs @ ax # ys\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "(_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
sourcenode ax = n'
(_Entry_) -xs @ ax # ys\<rightarrow>\<^sub>\<iota>* n'

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

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
with \<open>inner_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node n'
(_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "xs \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
inner_node n'
(_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. xs \<noteq> []
[PROOF STEP]
by(fastforce elim:path.cases simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
with \<open>n' \<notin> set(sourcenodes xs)\<close> \<open>(_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>as = xs@ax#ys\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<notin> set (sourcenodes xs)
(_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'
as = xs @ ax # ys
xs \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' \<notin> set (sourcenodes xs)
(_Entry_) -xs\<rightarrow>\<^sub>\<iota>* n'
as = xs @ ax # ys
xs \<noteq> []

goal (1 subgoal):
 1. \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
by(cases xs) auto
[PROOF STATE]
proof (state)
this:
\<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs

goal (1 subgoal):
 1. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n' \<notin> set (sourcenodes as)

goal (1 subgoal):
 1. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
with \<open>(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>inner_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'
inner_node n'
n' \<notin> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'
inner_node n'
n' \<notin> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
by(cases as)(auto elim:path.cases simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
\<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs

goal (1 subgoal):
 1. \<lbrakk>\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. (_Entry_) -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> inner_node n'' \<longrightarrow> \<not> method_exit n'' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>nx\<in>set ns. parent_node nx \<in> set (sourcenodes as')))); (_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'; inner_node n'; \<not> method_exit n'\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
obtain ax asx zs where "(_Entry_) -ax#asx\<rightarrow>\<^sub>\<iota>* n'"
        and "n' \<notin> set (sourcenodes (ax#asx))" and "as = (ax#asx)@zs"
[PROOF STATE]
proof (prove)
using this:
\<exists>ax asx zs. (_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs

goal (1 subgoal):
 1. (\<And>ax asx zs. \<lbrakk>(_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n'; n' \<notin> set (sourcenodes (ax # asx)); as = (ax # asx) @ zs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n'
n' \<notin> set (sourcenodes (ax # asx))
as = (ax # asx) @ zs

goal (1 subgoal):
 1. \<lbrakk>\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. (_Entry_) -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> inner_node n'' \<longrightarrow> \<not> method_exit n'' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>nx\<in>set ns. parent_node nx \<in> set (sourcenodes as')))); (_Entry_) -as\<rightarrow>\<^sub>\<iota>* n'; inner_node n'; \<not> method_exit n'\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(cases "\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and>
          valid_edge a'' \<and> intra_kind(kind a'') \<longrightarrow> n' postdominates targetnode a''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a''

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
have "(_Exit_) -[]\<rightarrow>\<^sub>\<iota>* (_Exit_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (_Exit_) -[]\<rightarrow>\<^sub>\<iota>* (_Exit_)
[PROOF STEP]
by(fastforce intro:empty_path simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
(_Exit_) -[]\<rightarrow>\<^sub>\<iota>* (_Exit_)

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "\<not> n' postdominates (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
(_Exit_) -[]\<rightarrow>\<^sub>\<iota>* (_Exit_)

goal (1 subgoal):
 1. \<not> n' postdominates (_Exit_)
[PROOF STEP]
by(fastforce simp:postdominate_def sourcenodes_def method_exit_def)
[PROOF STATE]
proof (state)
this:
\<not> n' postdominates (_Exit_)

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>(_Entry_) -ax#asx\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "(_Entry_) -[]@ax#asx\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n'

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

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>(_Entry_) -ax#asx\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have [simp]:"sourcenode ax = (_Entry_)"
          and "valid_edge ax"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -ax # asx\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. sourcenode ax = (_Entry_) &&& valid_edge ax
[PROOF STEP]
by(auto intro:path_split_Cons simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
sourcenode ax = (_Entry_)
valid_edge ax

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from Entry_Exit_edge
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. valid_edge a \<and> sourcenode a = (_Entry_) \<and> targetnode a = (_Exit_) \<and> kind a = (\<lambda>s. False)\<^sub>\<surd>
[PROOF STEP]
obtain a' where "sourcenode a' = (_Entry_)"
          and "targetnode a' = (_Exit_)" and "valid_edge a'"
          and "intra_kind(kind a')"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. valid_edge a \<and> sourcenode a = (_Entry_) \<and> targetnode a = (_Exit_) \<and> kind a = (\<lambda>s. False)\<^sub>\<surd>

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>sourcenode a' = (_Entry_); targetnode a' = (_Exit_); valid_edge a'; intra_kind (kind a')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
sourcenode a' = (_Entry_)
targetnode a' = (_Exit_)
valid_edge a'
intra_kind (kind a')

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>(_Entry_) -[]@ax#asx\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>\<not> n' postdominates (_Exit_)\<close>
          \<open>valid_edge ax\<close> True \<open>sourcenode ax = (_Entry_)\<close>
          \<open>n' \<notin> set (sourcenodes (ax#asx))\<close> \<open>inner_node n'\<close> \<open>\<not> method_exit n'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -[] @ ax # asx\<rightarrow>\<^sub>\<iota>* n'
\<not> n' postdominates (_Exit_)
valid_edge ax
\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a''
sourcenode ax = (_Entry_)
n' \<notin> set (sourcenodes (ax # asx))
inner_node n'
\<not> method_exit n'
sourcenode a' = (_Entry_)
targetnode a' = (_Exit_)
valid_edge a'
intra_kind (kind a')
[PROOF STEP]
have "sourcenode ax controls n'"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -[] @ ax # asx\<rightarrow>\<^sub>\<iota>* n'
\<not> n' postdominates (_Exit_)
valid_edge ax
\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a''
sourcenode ax = (_Entry_)
n' \<notin> set (sourcenodes (ax # asx))
inner_node n'
\<not> method_exit n'
sourcenode a' = (_Entry_)
targetnode a' = (_Exit_)
valid_edge a'
intra_kind (kind a')

goal (1 subgoal):
 1. sourcenode ax controls n'
[PROOF STEP]
by -(erule which_node_intra_standard_control_dependence_source
                     [of _ _ _ _ _ _ a'],auto)
[PROOF STATE]
proof (state)
this:
sourcenode ax controls n'

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "CFG_node (_Entry_) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
sourcenode ax controls n'

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

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "CFG_node (_Entry_) cd-[]@[CFG_node (_Entry_)]\<rightarrow>\<^sub>d* CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'

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

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CFG_node (_Entry_) cd-[] @ [CFG_node (_Entry_)]\<rightarrow>\<^sub>d* CFG_node n'

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>as = (ax#asx)@zs\<close>
[PROOF STATE]
proof (chain)
picking this:
as = (ax # asx) @ zs
[PROOF STEP]
have "(_Entry_) \<in> set(sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
as = (ax # asx) @ zs

goal (1 subgoal):
 1. (_Entry_) \<in> set (sourcenodes as)
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes as)

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cd-[] @ [CFG_node (_Entry_)]\<rightarrow>\<^sub>d* CFG_node n'
(_Entry_) \<in> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cd-[] @ [CFG_node (_Entry_)]\<rightarrow>\<^sub>d* CFG_node n'
(_Entry_) \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'')

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "\<exists>a' \<in> set asx. \<exists>a''. sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and>
          intra_kind(kind a'') \<and> \<not> n' postdominates targetnode a''"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'')

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

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a'\<in>set asx. \<exists>a''. sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''
[PROOF STEP]
obtain ax' asx' asx'' where "asx = asx'@ax'#asx'' \<and>
          (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and>
          intra_kind(kind a'') \<and> \<not> n' postdominates targetnode a'') \<and>
          (\<forall>z \<in> set asx''. \<not> (\<exists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and>
          intra_kind(kind a'') \<and> \<not> n' postdominates targetnode a''))"
[PROOF STATE]
proof (prove)
using this:
\<exists>a'\<in>set asx. \<exists>a''. sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''

goal (1 subgoal):
 1. (\<And>asx' ax' asx''. asx = asx' @ ax' # asx'' \<and> (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<and> (\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast elim!:split_list_last_propE)
[PROOF STATE]
proof (state)
this:
asx = asx' @ ax' # asx'' \<and> (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<and> (\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'')

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
asx = asx' @ ax' # asx'' \<and> (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<and> (\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'')
[PROOF STEP]
obtain ai where "asx = asx'@ax'#asx''"
          and "sourcenode ax' = sourcenode ai"
          and "valid_edge ai" and "intra_kind(kind ai)"
          and "\<not> n' postdominates targetnode ai"
          and "\<forall>z \<in> set asx''. \<not> (\<exists>a''. sourcenode z = sourcenode a'' \<and>
          valid_edge a'' \<and> intra_kind(kind a'') \<and> \<not> n' postdominates targetnode a'')"
[PROOF STATE]
proof (prove)
using this:
asx = asx' @ ax' # asx'' \<and> (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<and> (\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'')

goal (1 subgoal):
 1. (\<And>ai. \<lbrakk>asx = asx' @ ax' # asx''; sourcenode ax' = sourcenode ai; valid_edge ai; intra_kind (kind ai); \<not> n' postdominates targetnode ai; \<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
asx = asx' @ ax' # asx''
sourcenode ax' = sourcenode ai
valid_edge ai
intra_kind (kind ai)
\<not> n' postdominates targetnode ai
\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''

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

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

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

goal (1 subgoal):
 1. n' \<notin> set (sourcenodes (ax' # asx''))
[PROOF STEP]
by(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
n' \<notin> set (sourcenodes (ax' # asx''))

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>inner_node n'\<close> \<open>\<not> n' postdominates targetnode ai\<close>
          \<open>n' \<notin> set (sourcenodes (ax'#asx''))\<close> \<open>sourcenode ax' = sourcenode ai\<close>
          \<open>\<forall>z \<in> set asx''. \<not> (\<exists>a''. sourcenode z = sourcenode a'' \<and>
          valid_edge a'' \<and> intra_kind(kind a'') \<and> \<not> n' postdominates targetnode a'')\<close>
          \<open>valid_edge ai\<close> \<open>intra_kind(kind ai)\<close> \<open>\<not> method_exit n'\<close>
          \<open>(_Entry_) -(ax#asx')@ax'#asx''\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node n'
\<not> n' postdominates targetnode ai
n' \<notin> set (sourcenodes (ax' # asx''))
sourcenode ax' = sourcenode ai
\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''
valid_edge ai
intra_kind (kind ai)
\<not> method_exit n'
(_Entry_) -(ax # asx') @ ax' # asx''\<rightarrow>\<^sub>\<iota>* n'
n' \<notin> set (sourcenodes (ax' # asx''))
[PROOF STEP]
have "sourcenode ax' controls n'"
[PROOF STATE]
proof (prove)
using this:
inner_node n'
\<not> n' postdominates targetnode ai
n' \<notin> set (sourcenodes (ax' # asx''))
sourcenode ax' = sourcenode ai
\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''
valid_edge ai
intra_kind (kind ai)
\<not> method_exit n'
(_Entry_) -(ax # asx') @ ax' # asx''\<rightarrow>\<^sub>\<iota>* n'
n' \<notin> set (sourcenodes (ax' # asx''))

goal (1 subgoal):
 1. sourcenode ax' controls n'
[PROOF STEP]
by(fastforce intro!:which_node_intra_standard_control_dependence_source)
[PROOF STATE]
proof (state)
this:
sourcenode ax' controls n'

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
sourcenode ax' controls n'

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

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

goal (1 subgoal):
 1. (_Entry_) -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax' &&& valid_edge ax'
[PROOF STEP]
by(auto intro:path_split simp:intra_path_def simp del:append_Cons)
[PROOF STATE]
proof (state)
this:
(_Entry_) -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'
valid_edge ax'

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

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

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>valid_edge ax'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ax'
[PROOF STEP]
have "valid_node (sourcenode ax')"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax'

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

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "inner_node (sourcenode ax')"
[PROOF STATE]
proof (prove)
using this:
valid_node (sourcenode ax')

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. inner_node (sourcenode ax') \<Longrightarrow> inner_node (sourcenode ax')
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
inner_node (sourcenode ax')

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

goal (1 subgoal):
 1. intra_kind (kind ax')
[PROOF STEP]
by(simp add:intra_path_def)
[PROOF STATE]
proof (state)
this:
intra_kind (kind ax')

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
have "\<not> method_exit (sourcenode ax')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> method_exit (sourcenode ax')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. method_exit (sourcenode ax') \<Longrightarrow> False
[PROOF STEP]
assume "method_exit (sourcenode ax')"
[PROOF STATE]
proof (state)
this:
method_exit (sourcenode ax')

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

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

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

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

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>sourcenode ax' = 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>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix x Q f p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume " sourcenode ax' = sourcenode x"
              and "valid_edge x" and "kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f"
[PROOF STATE]
proof (state)
this:
sourcenode ax' = sourcenode x
valid_edge x
kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>valid_edge x\<close> \<open>kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close> \<open>sourcenode ax' = sourcenode x\<close>
            \<open>valid_edge ax'\<close> \<open>intra_kind (kind ax')\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge x
kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f
sourcenode ax' = sourcenode x
valid_edge ax'
intra_kind (kind ax')
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
valid_edge x
kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f
sourcenode ax' = sourcenode x
valid_edge ax'
intra_kind (kind ax')

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce dest:return_edges_only simp:intra_kind_def)
[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 (sourcenode ax')

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with IH \<open>length (ax#asx') < length as\<close> \<open>(_Entry_) -ax#asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'\<close>
          \<open>inner_node (sourcenode ax')\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. (_Entry_) -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> inner_node n'' \<longrightarrow> \<not> method_exit n'' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>nx\<in>set ns. parent_node nx \<in> set (sourcenodes as'))))
length (ax # asx') < length as
(_Entry_) -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'
inner_node (sourcenode ax')
\<not> method_exit (sourcenode ax')
[PROOF STEP]
obtain ns where "CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')"
          and "ns \<noteq> []"
          and "\<forall>n'' \<in> set ns. parent_node n'' \<in> set(sourcenodes (ax#asx'))"
[PROOF STATE]
proof (prove)
using this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. (_Entry_) -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> inner_node n'' \<longrightarrow> \<not> method_exit n'' \<longrightarrow> (\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>nx\<in>set ns. parent_node nx \<in> set (sourcenodes as'))))
length (ax # asx') < length as
(_Entry_) -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'
inner_node (sourcenode ax')
\<not> method_exit (sourcenode ax')

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

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')\<close>
          \<open>CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')
CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'
[PROOF STEP]
have "CFG_node (_Entry_) cd-ns@[CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')
CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'

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

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

goal (1 subgoal):
 1. sourcenode ax' \<in> set (sourcenodes as)
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
sourcenode ax' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>\<forall>n'' \<in> set ns. parent_node n'' \<in> set(sourcenodes (ax#asx'))\<close>
          \<open>as = (ax#asx)@zs\<close> \<open>asx = asx'@ax'#asx''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes (ax # asx'))
as = (ax # asx) @ zs
asx = asx' @ ax' # asx''
sourcenode ax' \<in> set (sourcenodes as)
[PROOF STEP]
have "\<forall>n'' \<in> set (ns@[CFG_node (sourcenode ax')]).
          parent_node n'' \<in> set(sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes (ax # asx'))
as = (ax # asx) @ zs
asx = asx' @ ax' # asx''
sourcenode ax' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<forall>n''\<in>set (ns @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)
[PROOF STEP]
by(fastforce simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>n''\<in>set (ns @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>CFG_node (_Entry_) cd-ns@[CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Entry_) cd-ns @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'
\<forall>n''\<in>set (ns @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Entry_) cd-ns @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'
\<forall>n''\<in>set (ns @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node (_Entry_) cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed