[STATEMENT]
lemma ics_SDG_path_realizable:
  assumes "n ics-ns\<rightarrow>\<^sub>d* n'"
  obtains ns' where "realizable n ns' n'" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>realizable n ns' n'; set ns \<subseteq> set ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ns'. realizable n ns' n' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
from \<open>n ics-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n ics-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show "\<exists>ns'. realizable n ns' n' \<and> set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
n ics-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns'. realizable n ns' n' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
proof(induct rule:intra_call_sum_SDG_path.induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>ns'. realizable n ns' n \<and> set [] \<subseteq> set ns'
 2. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 6. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (icsSp_Nil n)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n

goal (6 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>ns'. realizable n ns' n \<and> set [] \<subseteq> set ns'
 2. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 6. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "matched n [] n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

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

goal (6 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>ns'. realizable n ns' n \<and> set [] \<subseteq> set ns'
 2. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 6. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
matched n [] n

goal (1 subgoal):
 1. \<exists>ns'. realizable n ns' n \<and> set [] \<subseteq> set ns'
[PROOF STEP]
by(fastforce intro:realizable_matched)
[PROOF STATE]
proof (state)
this:
\<exists>ns'. realizable n ns' n \<and> set [] \<subseteq> set ns'

goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (icsSp_Append_cdep n ns n'' n')
[PROOF STATE]
proof (state)
this:
n ics-ns\<rightarrow>\<^sub>d* n''
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'

goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
obtain ns' where "realizable n ns' n''" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'

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

goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[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 "valid_SDG_node n''"
[PROOF STATE]
proof (prove)
using this:
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'

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

goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "n'' i-[]\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n''

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

goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'
n'' i-[]\<rightarrow>\<^sub>d* n''
[PROOF STEP]
have "n'' i-[]@[n'']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'
n'' i-[]\<rightarrow>\<^sub>d* n''

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

goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "matched n'' [n''] n'"
[PROOF STATE]
proof (prove)
using this:
n'' i-[] @ [n'']\<rightarrow>\<^sub>d* n'

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

goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>realizable n ns' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns' n''
matched n'' [n''] n'
[PROOF STEP]
have "realizable n (ns'@[n'']) n'"
[PROOF STATE]
proof (prove)
using this:
realizable n ns' n''
matched n'' [n''] n'

goal (1 subgoal):
 1. realizable n (ns' @ [n'']) n'
[PROOF STEP]
by(rule realizable_Append_matched)
[PROOF STATE]
proof (state)
this:
realizable n (ns' @ [n'']) n'

goal (5 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 5. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'']) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'']) n'

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

goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (icsSp_Append_ddep n ns n'' V n')
[PROOF STATE]
proof (state)
this:
n ics-ns\<rightarrow>\<^sub>d* n''
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
n'' \<noteq> n'

goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
obtain ns' where "realizable n ns' n''" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'

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

goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[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 "valid_SDG_node n''"
[PROOF STATE]
proof (prove)
using this:
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'

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

goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "n'' i-[]\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n''

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

goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'\<close> \<open>n'' \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
n'' \<noteq> n'
n'' i-[]\<rightarrow>\<^sub>d* n''
[PROOF STEP]
have "n'' i-[]@[n'']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
n'' \<noteq> n'
n'' i-[]\<rightarrow>\<^sub>d* n''

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

goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "matched n'' [n''] n'"
[PROOF STATE]
proof (prove)
using this:
n'' i-[] @ [n'']\<rightarrow>\<^sub>d* n'

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

goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>realizable n ns' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns' n''
matched n'' [n''] n'
[PROOF STEP]
have "realizable n (ns'@[n'']) n'"
[PROOF STATE]
proof (prove)
using this:
realizable n ns' n''
matched n'' [n''] n'

goal (1 subgoal):
 1. realizable n (ns' @ [n'']) n'
[PROOF STEP]
by(fastforce intro:realizable_Append_matched)
[PROOF STATE]
proof (state)
this:
realizable n (ns' @ [n'']) n'

goal (4 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'']) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'']) n'

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

goal (3 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (icsSp_Append_sum n ns n'' p n')
[PROOF STATE]
proof (state)
this:
n ics-ns\<rightarrow>\<^sub>d* n''
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (3 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
obtain ns' where "realizable n ns' n''" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'

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

goal (3 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[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]
show ?case
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (1 subgoal):
 1. \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
fix a Q r 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
assume "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" 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
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')

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
[PROOF STEP]
have match':"matched (CFG_node (targetnode a)) [CFG_node (targetnode a)]
        (CFG_node (sourcenode a'))"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a

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

goal (2 subgoals):
 1. \<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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>n'' = CFG_node (sourcenode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n'' = CFG_node (sourcenode a)
[PROOF STEP]
have "n'' -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n'' = CFG_node (sourcenode a)

goal (1 subgoal):
 1. n'' -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)
[PROOF STEP]
by(fastforce intro:SDG_call_edge)
[PROOF STATE]
proof (state)
this:
n'' -p\<rightarrow>\<^bsub>call\<^esub> 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "matched n'' [] n''"
[PROOF STATE]
proof (prove)
using this:
n'' -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)

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

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[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]
have "valid_edge a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. valid_edge a'
[PROOF STEP]
by(rule get_return_edges_valid)
[PROOF STATE]
proof (state)
this:
valid_edge 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a

goal (1 subgoal):
 1. (\<And>Q' f'. kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:call_return_edges)
[PROOF STATE]
proof (state)
this:
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>n' = CFG_node (targetnode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n' = CFG_node (targetnode a')
[PROOF STEP]
have "CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n' = CFG_node (targetnode a')

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

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>matched n'' [] n''\<close> \<open>n'' -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)\<close>
        match' \<open>CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'\<close> \<open>valid_edge a\<close>
        \<open>a' \<in> get_return_edges a\<close> \<open>n' = CFG_node (targetnode a')\<close>
        \<open>n'' = CFG_node (sourcenode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n'' [] n''
n'' -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)
matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'
valid_edge a
a' \<in> get_return_edges a
n' = CFG_node (targetnode a')
n'' = CFG_node (sourcenode a)
[PROOF STEP]
have "matched n'' ([]@n''#[CFG_node (targetnode a)]@[CFG_node (sourcenode a')])
        n'"
[PROOF STATE]
proof (prove)
using this:
matched n'' [] n''
n'' -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)
matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'
valid_edge a
a' \<in> get_return_edges a
n' = CFG_node (targetnode a')
n'' = CFG_node (sourcenode a)

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

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>realizable n ns' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns' n''
matched n'' ([] @ n'' # [CFG_node (targetnode a)] @ [CFG_node (sourcenode a')]) n'
[PROOF STEP]
have "realizable n
        (ns'@(n''#[CFG_node (targetnode a),CFG_node (sourcenode a')])) n'"
[PROOF STATE]
proof (prove)
using this:
realizable n ns' n''
matched n'' ([] @ n'' # [CFG_node (targetnode a)] @ [CFG_node (sourcenode a')]) n'

goal (1 subgoal):
 1. realizable n (ns' @ [n'', CFG_node (targetnode a), CFG_node (sourcenode a')]) n'
[PROOF STEP]
by(fastforce intro:realizable_Append_matched)
[PROOF STATE]
proof (state)
this:
realizable n (ns' @ [n'', CFG_node (targetnode a), CFG_node (sourcenode a')]) n'

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'', CFG_node (targetnode a), CFG_node (sourcenode a')]) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'', CFG_node (targetnode a), CFG_node (sourcenode a')]) n'

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

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
fix a Q r 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
assume "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "a' \<in> get_return_edges a"
        and match':"matched (Formal_in (targetnode a,x)) ns''
                            (Formal_out (sourcenode a',x'))"
        and "n'' = Actual_in (sourcenode a,x)"
        and "n' = Actual_out (targetnode a',x')" and "(p,ins,outs) \<in> set procs"
        and "x < length ins" and "x' < length outs"
[PROOF STATE]
proof (state)
this:
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

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>n'' = Actual_in (sourcenode a,x)\<close>
        \<open>(p,ins,outs) \<in> set procs\<close> \<open>x < length ins\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n'' = Actual_in (sourcenode a, x)
(p, ins, outs) \<in> set procs
x < length ins
[PROOF STEP]
have "n'' -p:ins!x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a,x)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n'' = Actual_in (sourcenode a, x)
(p, ins, outs) \<in> set procs
x < length ins

goal (1 subgoal):
 1. n'' -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a, x)
[PROOF STEP]
by(fastforce intro!:SDG_param_in_edge)
[PROOF STATE]
proof (state)
this:
n'' -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "matched n'' [] n''"
[PROOF STATE]
proof (prove)
using this:
n'' -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a, x)

goal (1 subgoal):
 1. matched n'' [] n''
[PROOF STEP]
by(fastforce intro:matched_Nil SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
matched n'' [] 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[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]
have "valid_edge a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. valid_edge a'
[PROOF STEP]
by(rule get_return_edges_valid)
[PROOF STATE]
proof (state)
this:
valid_edge 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a

goal (1 subgoal):
 1. (\<And>Q' f'. kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:call_return_edges)
[PROOF STATE]
proof (state)
this:
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>n' = Actual_out (targetnode a',x')\<close>
        \<open>(p,ins,outs) \<in> set procs\<close> \<open>x' < length outs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n' = Actual_out (targetnode a', x')
(p, ins, outs) \<in> set procs
x' < length outs
[PROOF STEP]
have "Formal_out (sourcenode a',x') -p:outs!x'\<rightarrow>\<^bsub>out\<^esub> n'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n' = Actual_out (targetnode a', x')
(p, ins, outs) \<in> set procs
x' < length outs

goal (1 subgoal):
 1. Formal_out (sourcenode a', x') -p:outs ! x'\<rightarrow>\<^bsub>out\<^esub> n'
[PROOF STEP]
by(fastforce intro:SDG_param_out_edge)
[PROOF STATE]
proof (state)
this:
Formal_out (sourcenode a', x') -p:outs ! x'\<rightarrow>\<^bsub>out\<^esub> 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>matched n'' [] n''\<close> \<open>n'' -p:ins!x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a,x)\<close>
        match' \<open>Formal_out (sourcenode a',x') -p:outs!x'\<rightarrow>\<^bsub>out\<^esub> n'\<close> \<open>valid_edge a\<close>
        \<open>a' \<in> get_return_edges a\<close> \<open>n' = Actual_out (targetnode a',x')\<close>
        \<open>n'' = Actual_in (sourcenode a,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n'' [] n''
n'' -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a, x)
matched (Formal_in (targetnode a, x)) ns'' (Formal_out (sourcenode a', x'))
Formal_out (sourcenode a', x') -p:outs ! x'\<rightarrow>\<^bsub>out\<^esub> n'
valid_edge a
a' \<in> get_return_edges a
n' = Actual_out (targetnode a', x')
n'' = Actual_in (sourcenode a, x)
[PROOF STEP]
have "matched n'' ([]@n''#ns''@[Formal_out (sourcenode a',x')]) n'"
[PROOF STATE]
proof (prove)
using this:
matched n'' [] n''
n'' -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a, x)
matched (Formal_in (targetnode a, x)) ns'' (Formal_out (sourcenode a', x'))
Formal_out (sourcenode a', x') -p:outs ! x'\<rightarrow>\<^bsub>out\<^esub> n'
valid_edge a
a' \<in> get_return_edges a
n' = Actual_out (targetnode a', x')
n'' = Actual_in (sourcenode a, x)

goal (1 subgoal):
 1. matched n'' ([] @ n'' # ns'' @ [Formal_out (sourcenode a', x')]) n'
[PROOF STEP]
by(fastforce intro:matched_bracket_param)
[PROOF STATE]
proof (state)
this:
matched n'' ([] @ n'' # ns'' @ [Formal_out (sourcenode a', x')]) 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>realizable n ns' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns' n''
matched n'' ([] @ n'' # ns'' @ [Formal_out (sourcenode a', x')]) n'
[PROOF STEP]
have "realizable n (ns'@(n''#ns''@[Formal_out (sourcenode a',x')])) n'"
[PROOF STATE]
proof (prove)
using this:
realizable n ns' n''
matched n'' ([] @ n'' # ns'' @ [Formal_out (sourcenode a', x')]) n'

goal (1 subgoal):
 1. realizable n (ns' @ n'' # ns'' @ [Formal_out (sourcenode a', x')]) n'
[PROOF STEP]
by(fastforce intro:realizable_Append_matched)
[PROOF STATE]
proof (state)
this:
realizable n (ns' @ n'' # ns'' @ [Formal_out (sourcenode a', x')]) 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>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
set ns \<subseteq> set ns'
realizable n (ns' @ n'' # ns'' @ [Formal_out (sourcenode a', x')]) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set ns'
realizable n (ns' @ n'' # ns'' @ [Formal_out (sourcenode a', x')]) n'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'

goal (2 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (icsSp_Append_call n ns n'' p n')
[PROOF STATE]
proof (state)
this:
n ics-ns\<rightarrow>\<^sub>d* n''
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'

goal (2 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
obtain ns' where "realizable n ns' n''" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'

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

goal (2 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'
[PROOF STEP]
have "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'

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

goal (2 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "matched n' [] n'"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n'

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

goal (2 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>realizable n ns' n''\<close> \<open>n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns' n''
n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'
matched n' [] n'
[PROOF STEP]
have "realizable n (ns'@n''#[]) n'"
[PROOF STATE]
proof (prove)
using this:
realizable n ns' n''
n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'
matched n' [] n'

goal (1 subgoal):
 1. realizable n (ns' @ [n'']) n'
[PROOF STEP]
by(fastforce intro:realizable_call sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
realizable n (ns' @ [n'']) n'

goal (2 subgoals):
 1. \<And>n ns n'' p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'']) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'']) n'

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

goal (1 subgoal):
 1. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (icsSp_Append_param_in n ns n'' p V n')
[PROOF STATE]
proof (state)
this:
n ics-ns\<rightarrow>\<^sub>d* n''
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'

goal (1 subgoal):
 1. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
obtain ns' where "realizable n ns' n''" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'

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

goal (1 subgoal):
 1. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'
[PROOF STEP]
have "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'

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

goal (1 subgoal):
 1. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
hence "matched n' [] n'"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n'

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

goal (1 subgoal):
 1. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>realizable n ns' n''\<close> \<open>n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns' n''
n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'
matched n' [] n'
[PROOF STEP]
have "realizable n (ns'@n''#[]) n'"
[PROOF STATE]
proof (prove)
using this:
realizable n ns' n''
n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'
matched n' [] n'

goal (1 subgoal):
 1. realizable n (ns' @ [n'']) n'
[PROOF STEP]
by(fastforce intro:realizable_call sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
realizable n (ns' @ [n'']) n'

goal (1 subgoal):
 1. \<And>n ns n'' p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. realizable n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. realizable n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'']) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set ns'
realizable n (ns' @ [n'']) n'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns'. realizable n ns' n' \<and> set ns \<subseteq> set ns'

goal:
No subgoals!
[PROOF STEP]
qed