[STATEMENT]
lemma is_SDG_path_intra_CFG_path:
  assumes "n is-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 is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-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 is-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_sum_SDG_path.induct)
[PROOF STATE]
proof (state)
goal (4 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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s\<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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
case (isSp_Nil n)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n

goal (4 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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s\<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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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 "parent_node n -[]\<rightarrow>* parent_node n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

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

goal (4 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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s\<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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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 (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s\<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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s\<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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
case (isSp_Append_cdep n ns n'' n')
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n''
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'

goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s\<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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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 (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s\<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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
have "n'' \<longrightarrow>\<^bsub>cd\<^esub> n'"
[PROOF STATE]
proof (prove)
using this:
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'

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

goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s\<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 is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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:
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" "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 (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
case (isSp_Append_ddep n ns n'' V n')
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n''
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
n'' \<noteq> n'

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "n'' influences V in n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'

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

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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 (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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 (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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 (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
case (isSp_Append_sum n ns n'' p n')
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n''
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'
[PROOF STEP]
obtain ns' where "matched n'' ns' n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'

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

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matched n'' ns' n'
[PROOF STEP]
obtain as' where "parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
matched n'' ns' n'

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

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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(fastforce intro:path_Append simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
parent_node n -as @ as'\<rightarrow>\<^sub>\<iota>* parent_node n'

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> 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 ics_SDG_path_valid_SDG_node:
  assumes "n ics-ns\<rightarrow>\<^sub>d* n'" shows "valid_SDG_node n" and "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
using \<open>n ics-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (prove)
using this:
n ics-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
by(induct rule:intra_call_sum_SDG_path.induct,
   auto intro:sum_SDG_edge_valid_SDG_node valid_SDG_CFG_node)


[STATEMENT]
lemma ics_SDG_path_Append:
  "\<lbrakk>n'' ics-ns'\<rightarrow>\<^sub>d* n'; n ics-ns\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> n ics-ns@ns'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n'' ics-ns'\<rightarrow>\<^sub>d* n'; n ics-ns\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> n ics-ns @ ns'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:intra_call_sum_SDG_path.induct,
   auto intro:intra_call_sum_SDG_path.intros simp:append_assoc[THEN sym]
                                        simp del:append_assoc)


[STATEMENT]
lemma is_SDG_path_ics_SDG_path:
  "n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n ics-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n ics-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:intra_sum_SDG_path.induct,auto intro:intra_call_sum_SDG_path.intros)


[STATEMENT]
lemma cc_SDG_path_ics_SDG_path:
  "n cc-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n ics-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n cc-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n ics-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:call_cdep_SDG_path.induct,
  auto intro:intra_call_sum_SDG_path.intros SDG_edge_sum_SDG_edge)