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

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

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

goal (1 subgoal):
 1. \<exists>ns' ns''. [] = ns' @ ns'' \<and> n_ ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. [] = ns' @ ns'' \<and> n_ ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n_

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

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

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

goal (1 subgoal):
 1. n'' \<in> set ns \<or> n'' = nx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns \<or> n'' = nx

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

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' \<in> set ns"
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx
[PROOF STEP]
obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'\<rightarrow>\<^sub>d* n''" and "n'' ics-ns''\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. (\<And>ns' ns''. \<lbrakk>ns = ns' @ ns''; n ics-ns'\<rightarrow>\<^sub>d* n''; n'' ics-ns''\<rightarrow>\<^sub>d* nx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns''\<rightarrow>\<^sub>d* nx

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from \<open>n'' ics-ns''\<rightarrow>\<^sub>d* nx\<close> \<open>nx s\<longrightarrow>\<^bsub>cd\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' ics-ns''\<rightarrow>\<^sub>d* nx
nx s\<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
have "n'' ics-ns''@[nx]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' ics-ns''\<rightarrow>\<^sub>d* nx
nx s\<longrightarrow>\<^bsub>cd\<^esub> n'

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

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>ns = ns'@ns''\<close> \<open>n ics-ns'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' = nx"
[PROOF STATE]
proof (state)
this:
n'' = nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* 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 "nx ics-[]\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
nx s\<longrightarrow>\<^bsub>cd\<^esub> n'

goal (1 subgoal):
 1. nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
by(fastforce intro:icsSp_Nil SDG_edge_valid_SDG_node sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
nx ics-[]\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>nx s\<longrightarrow>\<^bsub>cd\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
nx s\<longrightarrow>\<^bsub>cd\<^esub> n'
nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
have "nx ics-[]@[nx]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx s\<longrightarrow>\<^bsub>cd\<^esub> n'
nx ics-[]\<rightarrow>\<^sub>d* nx

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

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>n ics-ns\<rightarrow>\<^sub>d* nx\<close> \<open>n'' = nx\<close>
[PROOF STATE]
proof (chain)
picking this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

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

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

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

goal (1 subgoal):
 1. n'' \<in> set ns \<or> n'' = nx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns \<or> n'' = nx

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

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' \<in> set ns"
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx
[PROOF STEP]
obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'\<rightarrow>\<^sub>d* n''" and "n'' ics-ns''\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. (\<And>ns' ns''. \<lbrakk>ns = ns' @ ns''; n ics-ns'\<rightarrow>\<^sub>d* n''; n'' ics-ns''\<rightarrow>\<^sub>d* nx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns''\<rightarrow>\<^sub>d* nx

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from \<open>n'' ics-ns''\<rightarrow>\<^sub>d* nx\<close> \<open>nx s-V\<rightarrow>\<^sub>d\<^sub>d n'\<close> \<open>nx \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' ics-ns''\<rightarrow>\<^sub>d* nx
nx s-V\<rightarrow>\<^sub>d\<^sub>d n'
nx \<noteq> n'
[PROOF STEP]
have "n'' ics-ns''@[nx]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' ics-ns''\<rightarrow>\<^sub>d* nx
nx s-V\<rightarrow>\<^sub>d\<^sub>d n'
nx \<noteq> n'

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

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>ns = ns'@ns''\<close> \<open>n ics-ns'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' = nx"
[PROOF STATE]
proof (state)
this:
n'' = nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* 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 "nx ics-[]\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
nx s-V\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
by(fastforce intro:icsSp_Nil SDG_edge_valid_SDG_node sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
nx ics-[]\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>nx s-V\<rightarrow>\<^sub>d\<^sub>d n'\<close> \<open>nx \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
nx s-V\<rightarrow>\<^sub>d\<^sub>d n'
nx \<noteq> n'
nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
have "nx ics-[]@[nx]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx s-V\<rightarrow>\<^sub>d\<^sub>d n'
nx \<noteq> n'
nx ics-[]\<rightarrow>\<^sub>d* nx

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

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>n ics-ns\<rightarrow>\<^sub>d* nx\<close> \<open>n'' = nx\<close>
[PROOF STATE]
proof (chain)
picking this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

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

goal (3 subgoals):
 1. \<And>n ns n''a p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''a; n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n''a; n''a s-p\<rightarrow>\<^bsub>sum\<^esub> n'; n'' \<in> set (ns @ [n''a])\<rbrakk> \<Longrightarrow> \<exists>ns' ns''. ns @ [n''a] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. \<And>n ns n''a p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''a; n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n''a; n''a s-p\<rightarrow>\<^bsub>call\<^esub> n'; n'' \<in> set (ns @ [n''a])\<rbrakk> \<Longrightarrow> \<exists>ns' ns''. ns @ [n''a] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 3. \<And>n ns n''a p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''a; n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n''a; n''a s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; n'' \<in> set (ns @ [n''a])\<rbrakk> \<Longrightarrow> \<exists>ns' ns''. ns @ [n''a] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
note IH = \<open>n'' \<in> set ns \<Longrightarrow>
      \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx\<close>
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx

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

goal (1 subgoal):
 1. n'' \<in> set ns \<or> n'' = nx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns \<or> n'' = nx

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

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' \<in> set ns"
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx
[PROOF STEP]
obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'\<rightarrow>\<^sub>d* n''" and "n'' ics-ns''\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. (\<And>ns' ns''. \<lbrakk>ns = ns' @ ns''; n ics-ns'\<rightarrow>\<^sub>d* n''; n'' ics-ns''\<rightarrow>\<^sub>d* nx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns''\<rightarrow>\<^sub>d* nx

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from \<open>n'' ics-ns''\<rightarrow>\<^sub>d* nx\<close> \<open>nx s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' ics-ns''\<rightarrow>\<^sub>d* nx
nx s-p\<rightarrow>\<^bsub>sum\<^esub> n'
[PROOF STEP]
have "n'' ics-ns''@[nx]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' ics-ns''\<rightarrow>\<^sub>d* nx
nx s-p\<rightarrow>\<^bsub>sum\<^esub> n'

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

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>ns = ns'@ns''\<close> \<open>n ics-ns'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' = nx"
[PROOF STATE]
proof (state)
this:
n'' = nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* 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]
have "valid_SDG_node nx"
[PROOF STATE]
proof (prove)
using this:
nx s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (1 subgoal):
 1. valid_SDG_node nx
[PROOF STEP]
by(fastforce elim:sum_SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
valid_SDG_node nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
hence "nx ics-[]\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node nx

goal (1 subgoal):
 1. nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
by(fastforce intro:icsSp_Nil)
[PROOF STATE]
proof (state)
this:
nx ics-[]\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>nx s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
nx s-p\<rightarrow>\<^bsub>sum\<^esub> n'
nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
have "nx ics-[]@[nx]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx s-p\<rightarrow>\<^bsub>sum\<^esub> n'
nx ics-[]\<rightarrow>\<^sub>d* nx

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

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>n ics-ns\<rightarrow>\<^sub>d* nx\<close> \<open>n'' = nx\<close>
[PROOF STATE]
proof (chain)
picking this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

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

goal (2 subgoals):
 1. \<And>n ns n''a p n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''a; n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n''a; n''a s-p\<rightarrow>\<^bsub>call\<^esub> n'; n'' \<in> set (ns @ [n''a])\<rbrakk> \<Longrightarrow> \<exists>ns' ns''. ns @ [n''a] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. \<And>n ns n''a p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''a; n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n''a; n''a s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; n'' \<in> set (ns @ [n''a])\<rbrakk> \<Longrightarrow> \<exists>ns' ns''. ns @ [n''a] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
note IH = \<open>n'' \<in> set ns \<Longrightarrow>
      \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx\<close>
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx

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

goal (1 subgoal):
 1. n'' \<in> set ns \<or> n'' = nx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns \<or> n'' = nx

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

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' \<in> set ns"
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx
[PROOF STEP]
obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'\<rightarrow>\<^sub>d* n''" and "n'' ics-ns''\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. (\<And>ns' ns''. \<lbrakk>ns = ns' @ ns''; n ics-ns'\<rightarrow>\<^sub>d* n''; n'' ics-ns''\<rightarrow>\<^sub>d* nx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns''\<rightarrow>\<^sub>d* nx

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

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

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>ns = ns'@ns''\<close> \<open>n ics-ns'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' = nx"
[PROOF STATE]
proof (state)
this:
n'' = nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* 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 "nx ics-[]\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
nx s-p\<rightarrow>\<^bsub>call\<^esub> n'

goal (1 subgoal):
 1. nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
by(fastforce intro:icsSp_Nil SDG_edge_valid_SDG_node sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
nx ics-[]\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>nx s-p\<rightarrow>\<^bsub>call\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
nx s-p\<rightarrow>\<^bsub>call\<^esub> n'
nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
have "nx ics-[]@[nx]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx s-p\<rightarrow>\<^bsub>call\<^esub> n'
nx ics-[]\<rightarrow>\<^sub>d* nx

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

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>n ics-ns\<rightarrow>\<^sub>d* nx\<close> \<open>n'' = nx\<close>
[PROOF STATE]
proof (chain)
picking this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<And>n ns n''a p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''a; n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n''a; n''a s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; n'' \<in> set (ns @ [n''a])\<rbrakk> \<Longrightarrow> \<exists>ns' ns''. ns @ [n''a] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n ns n''a p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''a; n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n''a; n''a s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; n'' \<in> set (ns @ [n''a])\<rbrakk> \<Longrightarrow> \<exists>ns' ns''. ns @ [n''a] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* 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
n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx
nx s-p:V\<rightarrow>\<^bsub>in\<^esub> n'
n'' \<in> set (ns @ [nx])

goal (1 subgoal):
 1. \<And>n ns n''a p V n'. \<lbrakk>n ics-ns\<rightarrow>\<^sub>d* n''a; n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n''a; n''a s-p:V\<rightarrow>\<^bsub>in\<^esub> n'; n'' \<in> set (ns @ [n''a])\<rbrakk> \<Longrightarrow> \<exists>ns' ns''. ns @ [n''a] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
note IH = \<open>n'' \<in> set ns \<Longrightarrow>
      \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx\<close>
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx

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

goal (1 subgoal):
 1. n'' \<in> set ns \<or> n'' = nx
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns \<or> n'' = nx

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

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' \<in> set ns"
[PROOF STATE]
proof (state)
this:
n'' \<in> set ns

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx
[PROOF STEP]
obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'\<rightarrow>\<^sub>d* n''" and "n'' ics-ns''\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. (\<And>ns' ns''. \<lbrakk>ns = ns' @ ns''; n ics-ns'\<rightarrow>\<^sub>d* n''; n'' ics-ns''\<rightarrow>\<^sub>d* nx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns''\<rightarrow>\<^sub>d* nx

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

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

goal (2 subgoals):
 1. n'' \<in> set ns \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
 2. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>ns = ns'@ns''\<close> \<open>n ics-ns'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns = ns' @ ns''
n ics-ns'\<rightarrow>\<^sub>d* n''
n'' ics-ns'' @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
assume "n'' = nx"
[PROOF STATE]
proof (state)
this:
n'' = nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* 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 "nx ics-[]\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
nx s-p:V\<rightarrow>\<^bsub>in\<^esub> n'

goal (1 subgoal):
 1. nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
by(fastforce intro:icsSp_Nil SDG_edge_valid_SDG_node sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
nx ics-[]\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<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'
nx ics-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
have "nx ics-[]@[nx]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx s-p:V\<rightarrow>\<^bsub>in\<^esub> n'
nx ics-[]\<rightarrow>\<^sub>d* nx

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

goal (1 subgoal):
 1. n'' = nx \<Longrightarrow> \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
with \<open>n ics-ns\<rightarrow>\<^sub>d* nx\<close> \<open>n'' = nx\<close>
[PROOF STATE]
proof (chain)
picking this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n ics-ns\<rightarrow>\<^sub>d* nx
n'' = nx
nx ics-[] @ [nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns @ [nx] = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns' ns''. ns = ns' @ ns'' \<and> n ics-ns'\<rightarrow>\<^sub>d* n'' \<and> n'' ics-ns''\<rightarrow>\<^sub>d* n'

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<exists>ns'. n ics-ns'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
proof(induct rule:realizable.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n ns n'. matched n ns n' \<Longrightarrow> \<exists>ns'. n ics-ns'\<rightarrow>\<^sub>d* n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>3
[PROOF STEP]
case (realizable_matched n ns n')
[PROOF STATE]
proof (state)
this:
matched n ns n'

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

goal (1 subgoal):
 1. (\<And>ns'. n is-ns'\<rightarrow>\<^sub>d* n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule matched_is_SDG_path)
[PROOF STATE]
proof (state)
this:
n is-ns'\<rightarrow>\<^sub>d* n'

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

goal (1 subgoal):
 1. \<exists>ns'. n ics-ns'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:is_SDG_path_ics_SDG_path)
[PROOF STATE]
proof (state)
this:
\<exists>ns'. n ics-ns'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>3
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>3
[PROOF STEP]
case (realizable_call n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3)
[PROOF STATE]
proof (state)
this:
realizable n\<^sub>0 ns n\<^sub>1
\<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
matched n\<^sub>2 ns' n\<^sub>3

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

goal (1 subgoal):
 1. (\<And>nsx. n\<^sub>0 ics-nsx\<rightarrow>\<^sub>d* n\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n\<^sub>0 ics-nsx\<rightarrow>\<^sub>d* n\<^sub>1

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

goal (1 subgoal):
 1. n\<^sub>0 ics-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>2
[PROOF STEP]
by(fastforce intro:SDG_edge_sum_SDG_edge icsSp_Append_call icsSp_Append_param_in)
[PROOF STATE]
proof (state)
this:
n\<^sub>0 ics-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>2

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

goal (1 subgoal):
 1. (\<And>nsx'. n\<^sub>2 is-nsx'\<rightarrow>\<^sub>d* n\<^sub>3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule matched_is_SDG_path)
[PROOF STATE]
proof (state)
this:
n\<^sub>2 is-nsx'\<rightarrow>\<^sub>d* n\<^sub>3

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>3
[PROOF STEP]
hence "n\<^sub>2 ics-nsx'\<rightarrow>\<^sub>d* n\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>2 is-nsx'\<rightarrow>\<^sub>d* n\<^sub>3

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

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

goal (1 subgoal):
 1. n\<^sub>0 ics-(nsx @ [n\<^sub>1]) @ nsx'\<rightarrow>\<^sub>d* n\<^sub>3
[PROOF STEP]
by(rule ics_SDG_path_Append)
[PROOF STATE]
proof (state)
this:
n\<^sub>0 ics-(nsx @ [n\<^sub>1]) @ nsx'\<rightarrow>\<^sub>d* n\<^sub>3

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

goal (1 subgoal):
 1. \<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>3
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ns'. n\<^sub>0 ics-ns'\<rightarrow>\<^sub>d* n\<^sub>3

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

goal:
No subgoals!
[PROOF STEP]
qed