[STATEMENT]
lemma is_SDG_path_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 "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 (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]
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 (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" 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 (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]
have "\<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (1 subgoal):
 1. \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
proof(rule sum_edge_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a Q r fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n'' = CFG_node (sourcenode a); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
fix a Q fs a'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a Q r fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n'' = CFG_node (sourcenode a); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
assume "valid_edge a" and "a' \<in> get_return_edges a"
        and "n'' = CFG_node (sourcenode a)" and "n' = CFG_node (targetnode a')"
[PROOF STATE]
proof (state)
this:
valid_edge a
a' \<in> get_return_edges a
n'' = CFG_node (sourcenode a)
n' = CFG_node (targetnode a')

goal (2 subgoals):
 1. \<And>a Q r fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n'' = CFG_node (sourcenode a); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
obtain a'' where "sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. (\<And>a''. sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a' \<Longrightarrow> thesis; valid_edge a; a' \<in> get_return_edges a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(drule call_return_node_edge)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a' \<Longrightarrow> thesis; a' \<in> get_return_edges a\<rbrakk> \<Longrightarrow> ?a'4 \<in> get_return_edges a
 2. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a' \<Longrightarrow> thesis; a' \<in> get_return_edges a; \<exists>a''. valid_edge a'' \<and> sourcenode a'' = sourcenode a \<and> targetnode a'' = targetnode ?a'4 \<and> kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(auto simp:intra_path_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a''. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>* targetnode a' \<and> intra_kind (kind a'') \<Longrightarrow> thesis; a' \<in> get_return_edges a; valid_edge a''; sourcenode a'' = sourcenode a; targetnode a'' = targetnode a'; kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(drule path_edge)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a''. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>* targetnode a' \<and> intra_kind (kind a'') \<Longrightarrow> thesis; a' \<in> get_return_edges a; sourcenode a'' = sourcenode a; targetnode a'' = targetnode a'; kind a'' = (\<lambda>cf. False)\<^sub>\<surd>; sourcenode a'' -[a'']\<rightarrow>* targetnode a''\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a'

goal (2 subgoals):
 1. \<And>a Q r fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n'' = CFG_node (sourcenode a); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
 2. \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
with \<open>n'' = CFG_node (sourcenode a)\<close> \<open>n' = CFG_node (targetnode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' = CFG_node (sourcenode a)
n' = CFG_node (targetnode a')
sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n'' = CFG_node (sourcenode a)
n' = CFG_node (targetnode a')
sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a'

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

goal (1 subgoal):
 1. \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<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>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
fix a Q p fs a' ns x x' ins outs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
assume "valid_edge a" and "a' \<in> get_return_edges a"
        and "n'' = Actual_in (sourcenode a, x)"
        and "n' = Actual_out (targetnode a', x')"
[PROOF STATE]
proof (state)
this:
valid_edge a
a' \<in> get_return_edges a
n'' = Actual_in (sourcenode a, x)
n' = Actual_out (targetnode a', x')

goal (1 subgoal):
 1. \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
obtain a'' where "sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. (\<And>a''. sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a' \<Longrightarrow> thesis; valid_edge a; a' \<in> get_return_edges a\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(drule call_return_node_edge)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a' \<Longrightarrow> thesis; a' \<in> get_return_edges a\<rbrakk> \<Longrightarrow> ?a'4 \<in> get_return_edges a
 2. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a' \<Longrightarrow> thesis; a' \<in> get_return_edges a; \<exists>a''. valid_edge a'' \<and> sourcenode a'' = sourcenode a \<and> targetnode a'' = targetnode ?a'4 \<and> kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(auto simp:intra_path_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a''. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>* targetnode a' \<and> intra_kind (kind a'') \<Longrightarrow> thesis; a' \<in> get_return_edges a; valid_edge a''; sourcenode a'' = sourcenode a; targetnode a'' = targetnode a'; kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(drule path_edge)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a''. \<lbrakk>\<And>a''. sourcenode a -[a'']\<rightarrow>* targetnode a' \<and> intra_kind (kind a'') \<Longrightarrow> thesis; a' \<in> get_return_edges a; sourcenode a'' = sourcenode a; targetnode a'' = targetnode a'; kind a'' = (\<lambda>cf. False)\<^sub>\<surd>; sourcenode a'' -[a'']\<rightarrow>* targetnode a''\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a'

goal (1 subgoal):
 1. \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n'' = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
with \<open>n'' = Actual_in (sourcenode a, x)\<close> \<open>n' = Actual_out (targetnode a', x')\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' = Actual_in (sourcenode a, x)
n' = Actual_out (targetnode a', x')
sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n'' = Actual_in (sourcenode a, x)
n' = Actual_out (targetnode a', x')
sourcenode a -[a'']\<rightarrow>\<^sub>\<iota>* targetnode a'

goal (1 subgoal):
 1. \<exists>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
by simp 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 (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:
\<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]
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'' 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