[STATEMENT]
lemma irs_SDG_path_split:
  assumes "n irs-ns\<rightarrow>\<^sub>d* n'"
  obtains "n is-ns\<rightarrow>\<^sub>d* n'"
  | nsx nsx' nx nx' p where "ns = nsx@nx#nsx'" and "n irs-nsx\<rightarrow>\<^sub>d* nx"
  and "nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')" and "nx' is-nsx'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> thesis; \<And>nsx nx nsx' p nx'. \<lbrakk>ns = nsx @ nx # nsx'; n irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n irs-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n irs-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show "n is-ns\<rightarrow>\<^sub>d* n' \<or>
    (\<exists>nsx nx nsx' p nx'. ns = nsx@nx#nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and>
                        (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')"
[PROOF STATE]
proof (prove)
using this:
n irs-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
proof(induct rule:intra_return_sum_SDG_path.induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> n is-[]\<rightarrow>\<^sub>d* n \<or> (\<exists>nsx nx nsx' p nx'. [] = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n)
 2. \<And>n'' ns n' n. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s\<longrightarrow>\<^bsub>cd\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 4. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 5. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 6. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (irsSp_Nil n)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n

goal (6 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> n is-[]\<rightarrow>\<^sub>d* n \<or> (\<exists>nsx nx nsx' p nx'. [] = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n)
 2. \<And>n'' ns n' n. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s\<longrightarrow>\<^bsub>cd\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 4. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 5. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 6. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
[PROOF STEP]
have "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 (6 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> n is-[]\<rightarrow>\<^sub>d* n \<or> (\<exists>nsx nx nsx' p nx'. [] = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n)
 2. \<And>n'' ns n' n. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s\<longrightarrow>\<^bsub>cd\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 4. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 5. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 6. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n is-[]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. n is-[]\<rightarrow>\<^sub>d* n \<or> (\<exists>nsx nx nsx' p nx'. [] = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n is-[]\<rightarrow>\<^sub>d* n \<or> (\<exists>nsx nx nsx' p nx'. [] = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n)

goal (5 subgoals):
 1. \<And>n'' ns n' n. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s\<longrightarrow>\<^bsub>cd\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 4. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 5. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>n'' ns n' n. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s\<longrightarrow>\<^bsub>cd\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 4. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 5. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (irsSp_Cons_cdep n'' ns n' n)
[PROOF STATE]
proof (state)
this:
n'' irs-ns\<rightarrow>\<^sub>d* n'
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
n s\<longrightarrow>\<^bsub>cd\<^esub> n''

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

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
assume "n'' is-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
n'' is-ns\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n s\<longrightarrow>\<^bsub>cd\<^esub> n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n s\<longrightarrow>\<^bsub>cd\<^esub> n''
[PROOF STEP]
have "n is-[]@[n]\<rightarrow>\<^sub>d* n''"
[PROOF STATE]
proof (prove)
using this:
n s\<longrightarrow>\<^bsub>cd\<^esub> n''

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>n'' is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' is-ns\<rightarrow>\<^sub>d* n'
n is-[] @ [n]\<rightarrow>\<^sub>d* n''
[PROOF STEP]
have "n is-[n]@ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' is-ns\<rightarrow>\<^sub>d* n'
n is-[] @ [n]\<rightarrow>\<^sub>d* n''

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n is-[n] @ ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

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

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

goal (1 subgoal):
 1. (\<And>nsx nx nsx' p nx'. \<lbrakk>ns = nsx @ nx # nsx'; n'' irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = nsx @ nx # nsx'
n'' irs-nsx\<rightarrow>\<^sub>d* nx
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n'' irs-nsx\<rightarrow>\<^sub>d* nx\<close> \<open>n s\<longrightarrow>\<^bsub>cd\<^esub> n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' irs-nsx\<rightarrow>\<^sub>d* nx
n s\<longrightarrow>\<^bsub>cd\<^esub> n''
[PROOF STEP]
have "n irs-n#nsx\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
n'' irs-nsx\<rightarrow>\<^sub>d* nx
n s\<longrightarrow>\<^bsub>cd\<^esub> n''

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

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>ns = nsx@nx#nsx'\<close> \<open>nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')\<close>
        \<open>nx' is-nsx'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = nsx @ nx # nsx'
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ns = nsx @ nx # nsx'
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal (4 subgoals):
 1. \<And>n'' ns n' n V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 4. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n'' ns n' n V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-V\<rightarrow>\<^sub>d\<^sub>d n''; n \<noteq> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 4. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (irsSp_Cons_ddep n'' ns n' n V)
[PROOF STATE]
proof (state)
this:
n'' irs-ns\<rightarrow>\<^sub>d* n'
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
n s-V\<rightarrow>\<^sub>d\<^sub>d n''
n \<noteq> n''

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

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
assume "n'' is-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
n'' is-ns\<rightarrow>\<^sub>d* n'

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

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>n'' is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' is-ns\<rightarrow>\<^sub>d* n'
n is-[] @ [n]\<rightarrow>\<^sub>d* n''
[PROOF STEP]
have "n is-[n]@ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' is-ns\<rightarrow>\<^sub>d* n'
n is-[] @ [n]\<rightarrow>\<^sub>d* n''

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n is-[n] @ ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

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

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

goal (1 subgoal):
 1. (\<And>nsx nx nsx' p nx'. \<lbrakk>ns = nsx @ nx # nsx'; n'' irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = nsx @ nx # nsx'
n'' irs-nsx\<rightarrow>\<^sub>d* nx
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n'' irs-nsx\<rightarrow>\<^sub>d* nx\<close> \<open>n s-V\<rightarrow>\<^sub>d\<^sub>d n''\<close> \<open>n \<noteq> n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' irs-nsx\<rightarrow>\<^sub>d* nx
n s-V\<rightarrow>\<^sub>d\<^sub>d n''
n \<noteq> n''
[PROOF STEP]
have "n irs-n#nsx\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
n'' irs-nsx\<rightarrow>\<^sub>d* nx
n s-V\<rightarrow>\<^sub>d\<^sub>d n''
n \<noteq> n''

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

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>ns = nsx@nx#nsx'\<close> \<open>nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')\<close>
        \<open>nx' is-nsx'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = nsx @ nx # nsx'
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ns = nsx @ nx # nsx'
nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal (3 subgoals):
 1. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>sum\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 3. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (irsSp_Cons_sum n'' ns n' n p)
[PROOF STATE]
proof (state)
this:
n'' irs-ns\<rightarrow>\<^sub>d* n'
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
n s-p\<rightarrow>\<^bsub>sum\<^esub> n''

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

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
assume "n'' is-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
n'' is-ns\<rightarrow>\<^sub>d* n'

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

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>n'' is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' is-ns\<rightarrow>\<^sub>d* n'
n is-[] @ [n]\<rightarrow>\<^sub>d* n''
[PROOF STEP]
have "n is-[n]@ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' is-ns\<rightarrow>\<^sub>d* n'
n is-[] @ [n]\<rightarrow>\<^sub>d* n''

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n is-[n] @ ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

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

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

goal (1 subgoal):
 1. (\<And>nsx nx nsx' p' nx'. \<lbrakk>ns = nsx @ nx # nsx'; n'' irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = nsx @ nx # nsx'
n'' irs-nsx\<rightarrow>\<^sub>d* nx
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'

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

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

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>ns = nsx@nx#nsx'\<close> \<open>nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')\<close>
        \<open>nx' is-nsx'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = nsx @ nx # nsx'
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ns = nsx @ nx # nsx'
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal (2 subgoals):
 1. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (irsSp_Cons_return n'' ns n' n p)
[PROOF STATE]
proof (state)
this:
n'' irs-ns\<rightarrow>\<^sub>d* n'
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
n s-p\<rightarrow>\<^bsub>ret\<^esub> n''

goal (2 subgoals):
 1. \<And>n'' ns n' n p. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n'' is-ns\<rightarrow>\<^sub>d* n' \<or>
      (\<exists>nsx nx nsx' p nx'. ns = nsx@nx#nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and>
                        (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
assume "n'' is-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
n'' is-ns\<rightarrow>\<^sub>d* n'

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

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
hence "n irs-[]\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<close> \<open>n'' is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n s-p\<rightarrow>\<^bsub>ret\<^esub> n''
n'' is-ns\<rightarrow>\<^sub>d* n'
n irs-[]\<rightarrow>\<^sub>d* n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n s-p\<rightarrow>\<^bsub>ret\<^esub> n''
n'' is-ns\<rightarrow>\<^sub>d* n'
n irs-[]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

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

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

goal (1 subgoal):
 1. (\<And>nsx nx nsx' p' nx'. \<lbrakk>ns = nsx @ nx # nsx'; n'' irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = nsx @ nx # nsx'
n'' irs-nsx\<rightarrow>\<^sub>d* nx
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n'' irs-nsx\<rightarrow>\<^sub>d* nx\<close> \<open>n s-p\<rightarrow>\<^bsub>ret\<^esub> n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' irs-nsx\<rightarrow>\<^sub>d* nx
n s-p\<rightarrow>\<^bsub>ret\<^esub> n''
[PROOF STEP]
have "n irs-n#nsx\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
n'' irs-nsx\<rightarrow>\<^sub>d* nx
n s-p\<rightarrow>\<^bsub>ret\<^esub> n''

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

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>ns = nsx@nx#nsx'\<close> \<open>nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')\<close>
        \<open>nx' is-nsx'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = nsx @ nx # nsx'
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns = nsx @ nx # nsx'
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal (1 subgoal):
 1. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
case (irsSp_Cons_param_out n'' ns n' n p V)
[PROOF STATE]
proof (state)
this:
n'' irs-ns\<rightarrow>\<^sub>d* n'
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''

goal (1 subgoal):
 1. \<And>n'' ns n' n p V. \<lbrakk>n'' irs-ns\<rightarrow>\<^sub>d* n'; n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n'); n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<rbrakk> \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n'' is-ns\<rightarrow>\<^sub>d* n' \<or>
      (\<exists>nsx nx nsx' p nx'. ns = nsx@nx#nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and>
                        (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n'' is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
assume "n'' is-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
n'' is-ns\<rightarrow>\<^sub>d* n'

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

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
hence "n irs-[]\<rightarrow>\<^sub>d* n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

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

goal (2 subgoals):
 1. n'' is-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
 2. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<close> \<open>n'' is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''
n'' is-ns\<rightarrow>\<^sub>d* n'
n irs-[]\<rightarrow>\<^sub>d* n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''
n'' is-ns\<rightarrow>\<^sub>d* n'
n irs-[]\<rightarrow>\<^sub>d* n

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

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

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

goal (1 subgoal):
 1. (\<And>nsx nx nsx' p' nx'. \<lbrakk>ns = nsx @ nx # nsx'; n'' irs-nsx\<rightarrow>\<^sub>d* nx; nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx'); nx' is-nsx'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ns = nsx @ nx # nsx'
n'' irs-nsx\<rightarrow>\<^sub>d* nx
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
from \<open>n'' irs-nsx\<rightarrow>\<^sub>d* nx\<close> \<open>n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' irs-nsx\<rightarrow>\<^sub>d* nx
n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''
[PROOF STEP]
have "n irs-n#nsx\<rightarrow>\<^sub>d* nx"
[PROOF STATE]
proof (prove)
using this:
n'' irs-nsx\<rightarrow>\<^sub>d* nx
n s-p:V\<rightarrow>\<^bsub>out\<^esub> n''

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

goal (1 subgoal):
 1. \<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n'' irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
with \<open>ns = nsx@nx#nsx'\<close> \<open>nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')\<close>
        \<open>nx' is-nsx'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
ns = nsx @ nx # nsx'
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ns = nsx @ nx # nsx'
nx s-p'\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p':V\<rightarrow>\<^bsub>out\<^esub> nx')
nx' is-nsx'\<rightarrow>\<^sub>d* n'
n irs-n # nsx\<rightarrow>\<^sub>d* nx

goal (1 subgoal):
 1. n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n is-n # ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. n # ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n' \<or> (\<exists>nsx nx nsx' p nx'. ns = nsx @ nx # nsx' \<and> n irs-nsx\<rightarrow>\<^sub>d* nx \<and> (nx s-p\<rightarrow>\<^bsub>ret\<^esub> nx' \<or> (\<exists>V. nx s-p:V\<rightarrow>\<^bsub>out\<^esub> nx')) \<and> nx' is-nsx'\<rightarrow>\<^sub>d* n')

goal:
No subgoals!
[PROOF STEP]
qed