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

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

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

goal (1 subgoal):
 1. \<exists>ns''. realizable n (ns @ ns'') n''
[PROOF STEP]
by(rule_tac x="[]" in exI) fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns''. realizable n (ns @ ns'') n''

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

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

goal (1 subgoal):
 1. (\<And>ns''. realizable n (ns @ ns'') nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
realizable n (ns @ ns'') nx

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>ns''. realizable n (ns @ ns'') nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
realizable n (ns @ ns'') nx

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>ns''. realizable n (ns @ ns'') nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
realizable n (ns @ ns'') nx

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

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

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

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

goal (3 subgoals):
 1. \<And>na nsa n'' p n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
 2. \<And>na nsa n'' p n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
 3. \<And>na nsa n'' p V n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
realizable n ((ns @ ns'') @ nsx) n'

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

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

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

goal (1 subgoal):
 1. (\<And>ns''. realizable n (ns @ ns'') nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
realizable n (ns @ ns'') nx

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

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

goal (2 subgoals):
 1. \<And>na nsa n'' p n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p\<rightarrow>\<^bsub>call\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
 2. \<And>na nsa n'' p V n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
realizable n ((ns @ ns'') @ [nx]) n'

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

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

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

goal (1 subgoal):
 1. (\<And>ns''. realizable n (ns @ ns'') nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
realizable n (ns @ ns'') nx

goal (1 subgoal):
 1. \<And>na nsa n'' p V n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
[PROOF STEP]
from \<open>nx s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
nx s-p:V\<rightarrow>\<^bsub>in\<^esub> n'
[PROOF STEP]
have "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
nx 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>na nsa n'' p V n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
[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>na nsa n'' p V n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
[PROOF STEP]
with \<open>realizable n (ns@ns'') nx\<close> \<open>nx s-p:V\<rightarrow>\<^bsub>in\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n (ns @ ns'') nx
nx s-p:V\<rightarrow>\<^bsub>in\<^esub> n'
matched n' [] n'
[PROOF STEP]
have "realizable n ((ns@ns'')@[nx]) n'"
[PROOF STATE]
proof (prove)
using this:
realizable n (ns @ ns'') nx
nx s-p:V\<rightarrow>\<^bsub>in\<^esub> n'
matched n' [] n'

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

goal (1 subgoal):
 1. \<And>na nsa n'' p V n'. \<lbrakk>na ics-nsa\<rightarrow>\<^sub>d* n''; realizable n ns na \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n''; n'' s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; realizable n ns na\<rbrakk> \<Longrightarrow> \<exists>ns''. realizable n (ns @ ns'') n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
realizable n ((ns @ ns'') @ [nx]) n'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irs_SDG_path_Append:
  "\<lbrakk>n irs-ns\<rightarrow>\<^sub>d* n''; n'' irs-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n irs-ns@ns'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n irs-ns\<rightarrow>\<^sub>d* n''; n'' irs-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n irs-ns @ ns'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:intra_return_sum_SDG_path.induct,
   auto intro:intra_return_sum_SDG_path.intros)


[STATEMENT]
lemma is_SDG_path_irs_SDG_path:
  "n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n irs-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n irs-ns\<rightarrow>\<^sub>d* 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> n irs-[]\<rightarrow>\<^sub>d* n
 2. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* n'
 3. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* n'
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* 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> n irs-[]\<rightarrow>\<^sub>d* n
 2. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* n'
 3. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* n'
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

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

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

goal (1 subgoal):
 1. n'' irs-[n'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:irsSp_Cons_cdep irsSp_Nil sum_SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
n'' irs-[n'']\<rightarrow>\<^sub>d* n'

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

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

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

goal (1 subgoal):
 1. n'' irs-[n'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:irsSp_Cons_ddep irsSp_Nil sum_SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
n'' irs-[n'']\<rightarrow>\<^sub>d* n'

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

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

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* 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''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
case (isSp_Append_sum n ns n'' p n')
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n''
n irs-ns\<rightarrow>\<^sub>d* 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''; n irs-ns\<rightarrow>\<^sub>d* n''; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> n irs-ns @ [n'']\<rightarrow>\<^sub>d* 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 "n'' irs-[n'']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (1 subgoal):
 1. n'' irs-[n'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:irsSp_Cons_sum irsSp_Nil sum_SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
n'' irs-[n'']\<rightarrow>\<^sub>d* n'

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

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

goal:
No subgoals!
[PROOF STEP]
qed