[STATEMENT]
lemma intra_sum_SDG_path_rev_induct [consumes 1, case_names "isSp_Nil"
  "isSp_Cons_cdep"  "isSp_Cons_ddep"  "isSp_Cons_sum"]:
  assumes "n is-ns\<rightarrow>\<^sub>d* n'"
  and refl:"\<And>n. valid_SDG_node n \<Longrightarrow> P n [] n"
  and step_cdep:"\<And>n ns n' n''. \<lbrakk>n s\<longrightarrow>\<^bsub>cd\<^esub> n''; n'' is-ns\<rightarrow>\<^sub>d* n'; P n'' ns n'\<rbrakk>
                 \<Longrightarrow> P n (n#ns) n'"
  and step_ddep:"\<And>n ns n' V n''. \<lbrakk>n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''; n'' is-ns\<rightarrow>\<^sub>d* n';
                                  P n'' ns n'\<rbrakk> \<Longrightarrow> P n (n#ns) n'"
  and step_sum:"\<And>n ns n' p n''. \<lbrakk>n s-p\<rightarrow>\<^bsub>sum\<^esub> n''; n'' is-ns\<rightarrow>\<^sub>d* n'; P n'' ns n'\<rbrakk>
                 \<Longrightarrow> P n (n#ns) n'"
  shows "P n ns n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P n ns n'
[PROOF STEP]
using \<open>n is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. P n ns n'
[PROOF STEP]
proof(induct ns arbitrary:n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. n is-[]\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n [] n'
 2. \<And>a ns n. \<lbrakk>\<And>n. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n ns n'; n is-a # ns\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> P n (a # ns) n'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n is-[]\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<And>n. n is-[]\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n [] n'
 2. \<And>a ns n. \<lbrakk>\<And>n. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n ns n'; n is-a # ns\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> P n (a # ns) n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n is-[]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. P n [] n'
[PROOF STEP]
by(fastforce elim:intra_sum_SDG_path.cases intro:refl)
[PROOF STATE]
proof (state)
this:
P n [] n'

goal (1 subgoal):
 1. \<And>a ns n. \<lbrakk>\<And>n. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n ns n'; n is-a # ns\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> P n (a # ns) n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ns n. \<lbrakk>\<And>n. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n ns n'; n is-a # ns\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> P n (a # ns) n'
[PROOF STEP]
case (Cons nx nsx)
[PROOF STATE]
proof (state)
this:
?n is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P ?n nsx n'
n is-nx # nsx\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<And>a ns n. \<lbrakk>\<And>n. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n ns n'; n is-a # ns\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> P n (a # ns) n'
[PROOF STEP]
note IH = \<open>\<And>n. n is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n nsx n'\<close>
[PROOF STATE]
proof (state)
this:
?n is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P ?n nsx n'

goal (1 subgoal):
 1. \<And>a ns n. \<lbrakk>\<And>n. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n ns n'; n is-a # ns\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> P n (a # ns) n'
[PROOF STEP]
from \<open>n is-nx#nsx\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-nx # nsx\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have [simp]:"n = nx"
[PROOF STATE]
proof (prove)
using this:
n is-nx # nsx\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n = nx
[PROOF STEP]
by(fastforce dest:is_SDG_path_hd)
[PROOF STATE]
proof (state)
this:
n = nx

goal (1 subgoal):
 1. \<And>a ns n. \<lbrakk>\<And>n. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n ns n'; n is-a # ns\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> P n (a # ns) n'
[PROOF STEP]
from \<open>n is-nx#nsx\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-nx # nsx\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n') \<or>
    (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')) \<or>
    (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')"
[PROOF STATE]
proof (prove)
using this:
n is-nx # nsx\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')
[PROOF STEP]
proof(induct nsx arbitrary:n' rule:rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n'. n is-[nx]\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')
 2. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n is-[nx]\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<And>n'. n is-[nx]\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')
 2. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n is-[nx]\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-[nx]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "n is-[]\<rightarrow>\<^sub>d* nx"
      and disj:"nx s\<longrightarrow>\<^bsub>cd\<^esub> n' \<or> (\<exists>V. nx s-V\<rightarrow>\<^sub>d\<^sub>d n' \<and> nx \<noteq> n') \<or> (\<exists>p. nx s-p\<rightarrow>\<^bsub>sum\<^esub> n')"
[PROOF STATE]
proof (prove)
using this:
n is-[nx]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n is-[]\<rightarrow>\<^sub>d* nx &&& nx s\<longrightarrow>\<^bsub>cd\<^esub> n' \<or> (\<exists>V. nx s-V\<rightarrow>\<^sub>d\<^sub>d n' \<and> nx \<noteq> n') \<or> (\<exists>p. nx s-p\<rightarrow>\<^bsub>sum\<^esub> n')
[PROOF STEP]
by(induct n ns\<equiv>"[nx]" n' rule:intra_sum_SDG_path.induct,auto)
[PROOF STATE]
proof (state)
this:
n is-[]\<rightarrow>\<^sub>d* nx
nx s\<longrightarrow>\<^bsub>cd\<^esub> n' \<or> (\<exists>V. nx s-V\<rightarrow>\<^sub>d\<^sub>d n' \<and> nx \<noteq> n') \<or> (\<exists>p. nx s-p\<rightarrow>\<^bsub>sum\<^esub> n')

goal (2 subgoals):
 1. \<And>n'. n is-[nx]\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')
 2. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n is-[]\<rightarrow>\<^sub>d* nx\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-[]\<rightarrow>\<^sub>d* nx
[PROOF STEP]
have [simp]:"n = nx"
[PROOF STATE]
proof (prove)
using this:
n is-[]\<rightarrow>\<^sub>d* nx

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

goal (2 subgoals):
 1. \<And>n'. n is-[nx]\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')
 2. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from disj
[PROOF STATE]
proof (chain)
picking this:
nx s\<longrightarrow>\<^bsub>cd\<^esub> n' \<or> (\<exists>V. nx s-V\<rightarrow>\<^sub>d\<^sub>d n' \<and> nx \<noteq> n') \<or> (\<exists>p. nx s-p\<rightarrow>\<^bsub>sum\<^esub> n')
[PROOF STEP]
have "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
nx s\<longrightarrow>\<^bsub>cd\<^esub> n' \<or> (\<exists>V. nx s-V\<rightarrow>\<^sub>d\<^sub>d n' \<and> nx \<noteq> n') \<or> (\<exists>p. nx s-p\<rightarrow>\<^bsub>sum\<^esub> n')

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

goal (2 subgoals):
 1. \<And>n'. n is-[nx]\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')
 2. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
hence "n' is-[]\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n'

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

goal (2 subgoals):
 1. \<And>n'. n is-[nx]\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')
 2. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with disj
[PROOF STATE]
proof (chain)
picking this:
nx s\<longrightarrow>\<^bsub>cd\<^esub> n' \<or> (\<exists>V. nx s-V\<rightarrow>\<^sub>d\<^sub>d n' \<and> nx \<noteq> n') \<or> (\<exists>p. nx s-p\<rightarrow>\<^bsub>sum\<^esub> n')
n' is-[]\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
nx s\<longrightarrow>\<^bsub>cd\<^esub> n' \<or> (\<exists>V. nx s-V\<rightarrow>\<^sub>d\<^sub>d n' \<and> nx \<noteq> n') \<or> (\<exists>p. nx s-p\<rightarrow>\<^bsub>sum\<^esub> n')
n' is-[]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-[]\<rightarrow>\<^sub>d* n')

goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
n is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')
n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
note \<open>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow>
      ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or>
      (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or>
      (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<close>
[PROOF STATE]
proof (state)
this:
n is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')

goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n'); n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>n is-nx#xs@[x]\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'
n is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n is-nx # xs @ [x]\<rightarrow>\<^sub>d* n'
n is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')

goal (1 subgoal):
 1. ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
proof(induct n "nx#xs@[x]" n' rule:intra_sum_SDG_path.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (isSp_Append_cdep m ms m'' n')
[PROOF STATE]
proof (state)
this:
m is-ms\<rightarrow>\<^sub>d* m''
\<lbrakk>ms = nx # xs @ [x]; \<And>n'. m is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'')
m'' s\<longrightarrow>\<^bsub>cd\<^esub> n'
ms @ [m''] = nx # xs @ [x]
m is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')

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

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

goal (1 subgoal):
 1. ms = nx # xs &&& m'' = x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
ms = nx # xs
m'' = x

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

goal (1 subgoal):
 1. m is-nx # xs\<rightarrow>\<^sub>d* m''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m is-nx # xs\<rightarrow>\<^sub>d* m''

goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')
[PROOF STEP]
obtain n'' where "n'' is-xs\<rightarrow>\<^sub>d* m''"
        and "(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')"
[PROOF STATE]
proof (prove)
using this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')

goal (1 subgoal):
 1. (\<And>n''. \<lbrakk>n'' is-xs\<rightarrow>\<^sub>d* m''; (m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n'' is-xs\<rightarrow>\<^sub>d* m''
(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')

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

goal (1 subgoal):
 1. n'' is-xs @ [m'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(rule intra_sum_SDG_path.intros)
[PROOF STATE]
proof (state)
this:
n'' is-xs @ [m'']\<rightarrow>\<^sub>d* n'

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

goal (1 subgoal):
 1. ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (isSp_Append_ddep m ms m'' V n')
[PROOF STATE]
proof (state)
this:
m is-ms\<rightarrow>\<^sub>d* m''
\<lbrakk>ms = nx # xs @ [x]; \<And>n'. m is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'')
m'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
m'' \<noteq> n'
ms @ [m''] = nx # xs @ [x]
m is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
note IH = \<open>\<And>n'. m is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow>
        ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or>
        (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or>
        (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<close>
[PROOF STATE]
proof (state)
this:
m is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')

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

goal (1 subgoal):
 1. ms = nx # xs &&& m'' = x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
ms = nx # xs
m'' = x

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

goal (1 subgoal):
 1. m is-nx # xs\<rightarrow>\<^sub>d* m''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m is-nx # xs\<rightarrow>\<^sub>d* m''

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')
[PROOF STEP]
obtain n'' where "n'' is-xs\<rightarrow>\<^sub>d* m''"
        and "(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')"
[PROOF STATE]
proof (prove)
using this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')

goal (1 subgoal):
 1. (\<And>n''. \<lbrakk>n'' is-xs\<rightarrow>\<^sub>d* m''; (m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n'' is-xs\<rightarrow>\<^sub>d* m''
(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')

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

goal (1 subgoal):
 1. n'' is-xs @ [m'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(rule intra_sum_SDG_path.intros)
[PROOF STATE]
proof (state)
this:
n'' is-xs @ [m'']\<rightarrow>\<^sub>d* n'

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

goal (1 subgoal):
 1. ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (isSp_Append_sum m ms m'' p n')
[PROOF STATE]
proof (state)
this:
m is-ms\<rightarrow>\<^sub>d* m''
\<lbrakk>ms = nx # xs @ [x]; \<And>n'. m is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* m'')
m'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'
ms @ [m''] = nx # xs @ [x]
m is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
note IH = \<open>\<And>n'. m is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow>
        ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or>
        (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or>
        (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<close>
[PROOF STATE]
proof (state)
this:
m is-nx # xs\<rightarrow>\<^sub>d* ?n' \<Longrightarrow> ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* ?n')

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>ms @ [m''] = nx#xs@[x]\<close>
[PROOF STATE]
proof (chain)
picking this:
ms @ [m''] = nx # xs @ [x]
[PROOF STEP]
have [simp]:"ms = nx#xs"
        and [simp]:"m'' = x"
[PROOF STATE]
proof (prove)
using this:
ms @ [m''] = nx # xs @ [x]

goal (1 subgoal):
 1. ms = nx # xs &&& m'' = x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
ms = nx # xs
m'' = x

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

goal (1 subgoal):
 1. m is-nx # xs\<rightarrow>\<^sub>d* m''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m is-nx # xs\<rightarrow>\<^sub>d* m''

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')
[PROOF STEP]
obtain n'' where "n'' is-xs\<rightarrow>\<^sub>d* m''"
        and "(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')"
[PROOF STATE]
proof (prove)
using this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* m'')

goal (1 subgoal):
 1. (\<And>n''. \<lbrakk>n'' is-xs\<rightarrow>\<^sub>d* m''; (m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n'' is-xs\<rightarrow>\<^sub>d* m''
(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')

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

goal (1 subgoal):
 1. n'' is-xs @ [m'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(rule intra_sum_SDG_path.intros)
[PROOF STATE]
proof (state)
this:
n'' is-xs @ [m'']\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<lbrakk>ns = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''a. n s\<longrightarrow>\<^bsub>cd\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'') \<or> (\<exists>n''a V. n s-V\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n \<noteq> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n'')) \<or> (\<exists>n''a p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n''a \<and> n''a is-xs @ [x]\<rightarrow>\<^sub>d* n''); n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] = nx # xs @ [x]; \<And>n'. n is-nx # xs\<rightarrow>\<^sub>d* n' \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs\<rightarrow>\<^sub>d* n')\<rbrakk> \<Longrightarrow> ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')\<close>
[PROOF STATE]
proof (chain)
picking this:
(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')
n'' is-xs @ [m'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<or> (\<exists>V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'')) \<or> (\<exists>p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'')
n'' is-xs @ [m'']\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. ((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((\<exists>n''. m s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. m s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> m \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. m s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-xs @ [x]\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')

goal (1 subgoal):
 1. \<And>a ns n. \<lbrakk>\<And>n. n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n ns n'; n is-a # ns\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> P n (a # ns) n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')

goal (1 subgoal):
 1. P n (nx # nsx) n'
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n') \<or> (\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n')) \<or> (\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n') \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
proof(erule disjE)+
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 3. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
assume "\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (3 subgoals):
 1. \<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 3. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'
[PROOF STEP]
obtain n'' where "n s\<longrightarrow>\<^bsub>cd\<^esub> n''" and "n'' is-nsx\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
\<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. (\<And>n''. \<lbrakk>n s\<longrightarrow>\<^bsub>cd\<^esub> n''; n'' is-nsx\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n s\<longrightarrow>\<^bsub>cd\<^esub> n''
n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (3 subgoals):
 1. \<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 3. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
from IH[OF \<open>n'' is-nsx\<rightarrow>\<^sub>d* n'\<close>]
[PROOF STATE]
proof (chain)
picking this:
P n'' nsx n'
[PROOF STEP]
have "P n'' nsx n'"
[PROOF STATE]
proof (prove)
using this:
P n'' nsx n'

goal (1 subgoal):
 1. P n'' nsx n'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P n'' nsx n'

goal (3 subgoals):
 1. \<exists>n''. n s\<longrightarrow>\<^bsub>cd\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 3. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
from step_cdep[OF \<open>n s\<longrightarrow>\<^bsub>cd\<^esub> n''\<close> \<open>n'' is-nsx\<rightarrow>\<^sub>d* n'\<close> this]
[PROOF STATE]
proof (chain)
picking this:
P n (n # nsx) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P n (n # nsx) n'

goal (1 subgoal):
 1. P n (nx # nsx) n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P n (nx # nsx) n'

goal (2 subgoals):
 1. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
assume "\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'
[PROOF STEP]
obtain n'' V where "n s-V\<rightarrow>\<^sub>d\<^sub>d n''" and "n \<noteq> n''" and "n'' is-nsx\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
\<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. (\<And>V n''. \<lbrakk>n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''; n'' is-nsx\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n s-V\<rightarrow>\<^sub>d\<^sub>d n''
n \<noteq> n''
n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
from IH[OF \<open>n'' is-nsx\<rightarrow>\<^sub>d* n'\<close>]
[PROOF STATE]
proof (chain)
picking this:
P n'' nsx n'
[PROOF STEP]
have "P n'' nsx n'"
[PROOF STATE]
proof (prove)
using this:
P n'' nsx n'

goal (1 subgoal):
 1. P n'' nsx n'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P n'' nsx n'

goal (2 subgoals):
 1. \<exists>n'' V. n s-V\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n \<noteq> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
 2. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
from step_ddep[OF \<open>n s-V\<rightarrow>\<^sub>d\<^sub>d n''\<close> \<open>n \<noteq> n''\<close> \<open>n'' is-nsx\<rightarrow>\<^sub>d* n'\<close> this]
[PROOF STATE]
proof (chain)
picking this:
P n (n # nsx) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P n (n # nsx) n'

goal (1 subgoal):
 1. P n (nx # nsx) n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P n (nx # nsx) n'

goal (1 subgoal):
 1. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
assume "\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'
[PROOF STEP]
obtain n'' p where "n s-p\<rightarrow>\<^bsub>sum\<^esub> n''" and "n'' is-nsx\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
\<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. (\<And>p n''. \<lbrakk>n s-p\<rightarrow>\<^bsub>sum\<^esub> n''; n'' is-nsx\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n s-p\<rightarrow>\<^bsub>sum\<^esub> n''
n'' is-nsx\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
from IH[OF \<open>n'' is-nsx\<rightarrow>\<^sub>d* n'\<close>]
[PROOF STATE]
proof (chain)
picking this:
P n'' nsx n'
[PROOF STEP]
have "P n'' nsx n'"
[PROOF STATE]
proof (prove)
using this:
P n'' nsx n'

goal (1 subgoal):
 1. P n'' nsx n'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P n'' nsx n'

goal (1 subgoal):
 1. \<exists>n'' p. n s-p\<rightarrow>\<^bsub>sum\<^esub> n'' \<and> n'' is-nsx\<rightarrow>\<^sub>d* n' \<Longrightarrow> P n (nx # nsx) n'
[PROOF STEP]
from step_sum[OF \<open>n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<close> \<open>n'' is-nsx\<rightarrow>\<^sub>d* n'\<close> this]
[PROOF STATE]
proof (chain)
picking this:
P n (n # nsx) n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P n (n # nsx) n'

goal (1 subgoal):
 1. P n (nx # nsx) n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P n (nx # nsx) n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P n (nx # nsx) n'

goal:
No subgoals!
[PROOF STEP]
qed