[STATEMENT]
lemma returned_missing_cd_or_loop: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and \<pi>0: \<open>\<pi> 0 = \<pi>' 0\<close>
and notin': \<open>\<not>(\<exists> k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k')\<close> and nret: \<open>\<forall> n'. \<pi>' n' \<noteq> return\<close> and ret: \<open>\<pi> n = return\<close>
obtains i i' where \<open>i<k\<close> \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close> \<open>\<pi> (Suc i) \<noteq> \<pi>' (Suc i')\<close> \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall> j'> i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain f where icdf: \<open>\<forall> i'. f (Suc i') icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i'\<close> and ran: \<open>range f = {i'. \<forall> j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'}\<close> and icdf0: \<open>\<not> (\<exists>i'. f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i'. f (Suc i') icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i'; range f = {i'. \<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'}; \<nexists>i'. f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using path(2) path_nret_inf_icd_seq nret
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>'
\<lbrakk>is_path ?\<pi>; \<forall>i. ?\<pi> i \<noteq> local.return; \<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>?\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>?\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<forall>n'. \<pi>' n' \<noteq> local.return

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i'. f (Suc i') icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i'; range f = {i'. \<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'}; \<nexists>i'. f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i'. f (Suc i') icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i'
range f = {i'. \<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'}
\<nexists>i'. f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'

goal (1 subgoal):
 1. (\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<exists> j. \<not> (\<exists> i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> (f j))\<close>
[PROOF STATE]
proof (state)
this:
\<exists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j
[PROOF STEP]
obtain j where ni\<pi>: \<open>\<not> (\<exists> i. cs\<^bsup>\<pi>'\<^esup> (f j) = cs\<^bsup>\<pi>\<^esup> i)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (1 subgoal):
 1. (\<And>j. \<nexists>i. cs\<^bsup>\<pi>'\<^esup> f j = cs\<^bsup>\<pi>\<^esup> i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<nexists>i. cs\<^bsup>\<pi>'\<^esup> f j = cs\<^bsup>\<pi>\<^esup> i

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
note converged_cd_diverge_return[OF path(2,1) \<pi>0[symmetric] ni\<pi> ret] that
[PROOF STATE]
proof (state)
this:
(\<And>k k'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>\<^esup> k'; f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k; \<pi>' (Suc k) \<noteq> \<pi> (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>?i1 < k; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; \<pi> (Suc ?i1) \<noteq> \<pi>' (Suc ?i'1); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i1 \<or> (\<forall>j'>?i'1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?i'1)\<rbrakk> \<Longrightarrow> thesis

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>k k'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>\<^esup> k'; f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k; \<pi>' (Suc k) \<noteq> \<pi> (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>?i1 < k; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; \<pi> (Suc ?i1) \<noteq> \<pi>' (Suc ?i'1); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i1 \<or> (\<forall>j'>?i'1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?i'1)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain i k' where csk: \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> k'\<close> and cdj: \<open>f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close> and div:  \<open>\<pi> (Suc i) \<noteq> \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>k k'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>\<^esup> k'; f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k; \<pi>' (Suc k) \<noteq> \<pi> (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>?i1 < k; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; \<pi> (Suc ?i1) \<noteq> \<pi>' (Suc ?i'1); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i1 \<or> (\<forall>j'>?i'1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?i'1)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>i k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> k'; f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'; \<pi> (Suc i) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> k'
f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
\<pi> (Suc i) \<noteq> \<pi>' (Suc k')

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
have \<open>k' \<in> range f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' \<in> range f
[PROOF STEP]
using cdj
[PROOF STATE]
proof (prove)
using this:
f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. k' \<in> range f
[PROOF STEP]
proof (induction \<open>j\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f
 2. \<And>j. \<lbrakk>f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f; f (Suc j) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> k' \<in> range f
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (2 subgoals):
 1. f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f
 2. \<And>j. \<lbrakk>f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f; f (Suc j) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> k' \<in> range f
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. k' \<in> range f
[PROOF STEP]
using icdf0
[PROOF STATE]
proof (prove)
using this:
f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
\<nexists>i'. f 0 cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'

goal (1 subgoal):
 1. k' \<in> range f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k' \<in> range f

goal (1 subgoal):
 1. \<And>j. \<lbrakk>f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f; f (Suc j) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> k' \<in> range f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f; f (Suc j) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> k' \<in> range f
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f
f (Suc j) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. \<And>j. \<lbrakk>f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f; f (Suc j) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> k' \<in> range f
[PROOF STEP]
have icdfj: \<open>f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f j
[PROOF STEP]
using icdf
[PROOF STATE]
proof (prove)
using this:
\<forall>i'. f (Suc i') icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i'

goal (1 subgoal):
 1. f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f; f (Suc j) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> k' \<in> range f
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' \<in> range f
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> k' \<in> range f
 2. \<not> ?P \<Longrightarrow> k' \<in> range f
[PROOF STEP]
assume \<open>f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (state)
this:
f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (2 subgoals):
 1. ?P \<Longrightarrow> k' \<in> range f
 2. \<not> ?P \<Longrightarrow> k' \<in> range f
[PROOF STEP]
hence \<open>k' = f j\<close>
[PROOF STATE]
proof (prove)
using this:
f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. k' = f j
[PROOF STEP]
using icdfj
[PROOF STATE]
proof (prove)
using this:
f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f j

goal (1 subgoal):
 1. k' = f j
[PROOF STEP]
by (metis icd_uniq)
[PROOF STATE]
proof (state)
this:
k' = f j

goal (2 subgoals):
 1. ?P \<Longrightarrow> k' \<in> range f
 2. \<not> ?P \<Longrightarrow> k' \<in> range f
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
k' = f j

goal (1 subgoal):
 1. k' \<in> range f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' \<in> range f

goal (1 subgoal):
 1. \<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f
[PROOF STEP]
assume \<open>\<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (state)
this:
\<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. \<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f
[PROOF STEP]
hence \<open>f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
using cd_impl_icd_cd[OF Suc.prems icdfj]
[PROOF STATE]
proof (prove)
using this:
\<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
\<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. \<not> f (Suc j) icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. k' \<in> range f
[PROOF STEP]
using Suc.IH
[PROOF STATE]
proof (prove)
using this:
f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
f j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<Longrightarrow> k' \<in> range f

goal (1 subgoal):
 1. k' \<in> range f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' \<in> range f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k' \<in> range f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k' \<in> range f

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
hence alldep: \<open>\<forall> i'>k'. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
using this:
k' \<in> range f

goal (1 subgoal):
 1. \<forall>i'>k'. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
using ran
[PROOF STATE]
proof (prove)
using this:
k' \<in> range f
range f = {i'. \<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'}

goal (1 subgoal):
 1. \<forall>i'>k'. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i'>k'. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>i < k\<close>
[PROOF STATE]
proof (state)
this:
i < k

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
with alldep that[OF _ csk div]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i'>k'. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
\<lbrakk>i < k; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>k'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k')\<rbrakk> \<Longrightarrow> thesis
i < k
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i'>k'. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
\<lbrakk>i < k; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>k'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k')\<rbrakk> \<Longrightarrow> thesis
i < k

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<not> i < k\<close>
[PROOF STATE]
proof (state)
this:
\<not> i < k

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
hence ki: \<open>k\<le>i\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i < k

goal (1 subgoal):
 1. k \<le> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<le> i

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
have \<open>k \<noteq> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> i
[PROOF STEP]
using notin' csk
[PROOF STATE]
proof (prove)
using this:
\<nexists>k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> k'

goal (1 subgoal):
 1. k \<noteq> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<noteq> i

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
hence ki': \<open>k<i\<close>
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i

goal (1 subgoal):
 1. k < i
[PROOF STEP]
using ki
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i
k \<le> i

goal (1 subgoal):
 1. k < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < i

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
obtain ka k' where \<open>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'\<close> \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka\<close> \<open>\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using converged_cd_diverge[OF path \<pi>0 notin' ki' csk]
[PROOF STATE]
proof (prove)
using this:
(\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>ka < k\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. ka < k
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
is_path \<pi> \<and> ka < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{ka..k}. \<pi> j \<noteq> ipd (\<pi> ka))
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. ka < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ka < k

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k
\<lbrakk>?i1 < k; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; \<pi> (Suc ?i1) \<noteq> \<pi>' (Suc ?i'1); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i1 \<or> (\<forall>j'>?i'1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?i'1)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<not>(\<exists> j. \<not> (\<exists> i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> (f j)))\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
hence allin: \<open>\<forall> j. (\<exists> i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> (f j))\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (1 subgoal):
 1. \<forall>j. \<exists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>j. \<exists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
define f' where f': \<open>f' \<equiv> \<lambda> j. (SOME i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> (f j))\<close>
[PROOF STATE]
proof (state)
this:
f' \<equiv> \<lambda>j. SOME i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<forall> i. f' i < f' (Suc i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. f' i < f' (Suc i)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. f' i < f' (Suc i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. f' i < f' (Suc i)
[PROOF STEP]
have csi: \<open>cs\<^bsup>\<pi>'\<^esup> (f i) = cs\<^bsup>\<pi>\<^esup> (f' i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> f i = cs\<^bsup>\<pi>\<^esup> f' i
[PROOF STEP]
unfolding f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> f i = cs\<^bsup>\<pi>\<^esup> (SOME ia. cs\<^bsup>\<pi>\<^esup> ia = cs\<^bsup>\<pi>'\<^esup> f i)
[PROOF STEP]
using allin
[PROOF STATE]
proof (prove)
using this:
\<forall>j. \<exists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> f i = cs\<^bsup>\<pi>\<^esup> (SOME ia. cs\<^bsup>\<pi>\<^esup> ia = cs\<^bsup>\<pi>'\<^esup> f i)
[PROOF STEP]
by (metis (mono_tags) someI_ex)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> f i = cs\<^bsup>\<pi>\<^esup> f' i

goal (1 subgoal):
 1. \<And>i. f' i < f' (Suc i)
[PROOF STEP]
have cssuci: \<open>cs\<^bsup>\<pi>'\<^esup> (f (Suc i)) = cs\<^bsup>\<pi>\<^esup> (f' (Suc i))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> f (Suc i) = cs\<^bsup>\<pi>\<^esup> f' (Suc i)
[PROOF STEP]
unfolding f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> f (Suc i) = cs\<^bsup>\<pi>\<^esup> (SOME ia. cs\<^bsup>\<pi>\<^esup> ia = cs\<^bsup>\<pi>'\<^esup> f (Suc i))
[PROOF STEP]
using allin
[PROOF STATE]
proof (prove)
using this:
\<forall>j. \<exists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> f (Suc i) = cs\<^bsup>\<pi>\<^esup> (SOME ia. cs\<^bsup>\<pi>\<^esup> ia = cs\<^bsup>\<pi>'\<^esup> f (Suc i))
[PROOF STEP]
by (metis (mono_tags) someI_ex)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> f (Suc i) = cs\<^bsup>\<pi>\<^esup> f' (Suc i)

goal (1 subgoal):
 1. \<And>i. f' i < f' (Suc i)
[PROOF STEP]
have fi: \<open>f i < f (Suc i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i < f (Suc i)
[PROOF STEP]
using icdf
[PROOF STATE]
proof (prove)
using this:
\<forall>i'. f (Suc i') icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i'

goal (1 subgoal):
 1. f i < f (Suc i)
[PROOF STEP]
unfolding is_icdi_def is_cdi_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i'. is_path \<pi>' \<and> (is_path \<pi>' \<and> f i' < f (Suc i') \<and> \<pi>' (f (Suc i')) \<noteq> local.return \<and> (\<forall>j\<in>{f i'..f (Suc i')}. \<pi>' j \<noteq> ipd (\<pi>' (f i')))) \<and> (\<forall>m\<in>{f i'<..<f (Suc i')}. \<not> (is_path \<pi>' \<and> m < f (Suc i') \<and> \<pi>' (f (Suc i')) \<noteq> local.return \<and> (\<forall>j\<in>{m..f (Suc i')}. \<pi>' j \<noteq> ipd (\<pi>' m))))

goal (1 subgoal):
 1. f i < f (Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f i < f (Suc i)

goal (1 subgoal):
 1. \<And>i. f' i < f' (Suc i)
[PROOF STEP]
have \<open>f (Suc i) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i
[PROOF STEP]
using icdf
[PROOF STATE]
proof (prove)
using this:
\<forall>i'. f (Suc i') icd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i'

goal (1 subgoal):
 1. f (Suc i) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i
[PROOF STEP]
unfolding is_icdi_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i'. is_path \<pi>' \<and> f (Suc i') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i' \<and> (\<forall>m\<in>{f i'<..<f (Suc i')}. \<not> f (Suc i') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m)

goal (1 subgoal):
 1. f (Suc i) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f (Suc i) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i

goal (1 subgoal):
 1. \<And>i. f' i < f' (Suc i)
[PROOF STEP]
hence nreti: \<open>\<pi>' (f i) \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
f (Suc i) cd\<^bsup>\<pi>'\<^esup>\<rightarrow> f i

goal (1 subgoal):
 1. \<pi>' (f i) \<noteq> local.return
[PROOF STEP]
by (metis cd_not_ret)
[PROOF STATE]
proof (state)
this:
\<pi>' (f i) \<noteq> local.return

goal (1 subgoal):
 1. \<And>i. f' i < f' (Suc i)
[PROOF STEP]
show \<open>f' i < f' (Suc i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' i < f' (Suc i)
[PROOF STEP]
using cs_order[OF path(2,1) csi cssuci nreti fi]
[PROOF STATE]
proof (prove)
using this:
f' i < f' (Suc i)

goal (1 subgoal):
 1. f' i < f' (Suc i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f' i < f' (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. f' i < f' (Suc i)

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
hence kle: \<open>k < f' (Suc k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i. f' i < f' (Suc i)

goal (1 subgoal):
 1. k < f' (Suc k)
[PROOF STEP]
using mono_ge_id[of \<open>f'\<close> \<open>Suc k\<close>]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. f' i < f' (Suc i)
\<forall>i. f' i < f' (Suc i) \<Longrightarrow> Suc k \<le> f' (Suc k)

goal (1 subgoal):
 1. k < f' (Suc k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < f' (Suc k)

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
have cssk: \<open>cs\<^bsup>\<pi>\<^esup> (f' (Suc k)) = cs\<^bsup>\<pi>'\<^esup> (f (Suc k))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> f' (Suc k) = cs\<^bsup>\<pi>'\<^esup> f (Suc k)
[PROOF STEP]
unfolding f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (SOME i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f (Suc k)) = cs\<^bsup>\<pi>'\<^esup> f (Suc k)
[PROOF STEP]
using allin
[PROOF STATE]
proof (prove)
using this:
\<forall>j. \<exists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (SOME i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f (Suc k)) = cs\<^bsup>\<pi>'\<^esup> f (Suc k)
[PROOF STEP]
by (metis (mono_tags) someI_ex)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> f' (Suc k) = cs\<^bsup>\<pi>'\<^esup> f (Suc k)

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
obtain ka k' where \<open>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'\<close> \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka\<close> \<open>\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using converged_cd_diverge[OF path \<pi>0 notin' kle cssk]
[PROOF STATE]
proof (prove)
using this:
(\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>ka < k\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. ka < k
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
is_path \<pi> \<and> ka < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{ka..k}. \<pi> j \<noteq> ipd (\<pi> ka))
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. ka < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ka < k

goal (1 subgoal):
 1. \<nexists>j. \<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> f j \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k
\<lbrakk>?i1 < k; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; \<pi> (Suc ?i1) \<noteq> \<pi>' (Suc ?i'1); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i1 \<or> (\<forall>j'>?i'1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?i'1)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma missing_cd_or_loop: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and \<pi>0: \<open>\<pi> 0 = \<pi>' 0\<close> and notin': \<open>\<not>(\<exists> k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k')\<close>
obtains i i' where \<open>i < k\<close> \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close> \<open>\<pi> (Suc i) \<noteq> \<pi>' (Suc i')\<close> \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall> j'> i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<exists> n'. \<pi>' n' = return\<close>
[PROOF STATE]
proof (state)
this:
\<exists>n'. \<pi>' n' = local.return

goal (2 subgoals):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n'. \<pi>' n' = local.return
[PROOF STEP]
obtain n' where retn: \<open>\<pi>' n' = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>n'. \<pi>' n' = local.return

goal (1 subgoal):
 1. (\<And>n'. \<pi>' n' = local.return \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi>' n' = local.return

goal (2 subgoals):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note converged_cd_diverge_return[OF path \<pi>0 notin' retn]
[PROOF STATE]
proof (state)
this:
(\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain ka k' where \<open>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'\<close> \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka\<close> \<open>\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>ka k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka; \<pi> (Suc ka) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (2 subgoals):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (2 subgoals):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>ka < k\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. ka < k
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
is_path \<pi> \<and> ka < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{ka..k}. \<pi> j \<noteq> ipd (\<pi> ka))
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')

goal (1 subgoal):
 1. ka < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ka < k

goal (2 subgoals):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>'\<^esup> k'
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ka
\<pi> (Suc ka) \<noteq> \<pi>' (Suc k')
ka < k
\<lbrakk>?i1 < k; cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>'\<^esup> ?i'1; \<pi> (Suc ?i1) \<noteq> \<pi>' (Suc ?i'1); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i1 \<or> (\<forall>j'>?i'1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?i'1)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<not> (\<exists> n'. \<pi>' n' = return)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>n'. \<pi>' n' = local.return

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence notret: \<open>\<forall> n'. \<pi>' n' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>n'. \<pi>' n' = local.return

goal (1 subgoal):
 1. \<forall>n'. \<pi>' n' \<noteq> local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n'. \<pi>' n' \<noteq> local.return

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n'. \<pi>' n' \<noteq> local.return
[PROOF STEP]
obtain \<pi>l n where ipl: \<open>is_path \<pi>l\<close> and \<pi>l:  \<open>\<pi> k = \<pi>l 0\<close> and retn: \<open>\<pi>l n = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n'. \<pi>' n' \<noteq> local.return

goal (1 subgoal):
 1. (\<And>\<pi>l n. \<lbrakk>is_path \<pi>l; \<pi> k = \<pi>l 0; \<pi>l n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reaching_ret path(1) path_nodes
[PROOF STATE]
proof (prove)
using this:
\<forall>n'. \<pi>' n' \<noteq> local.return
?x \<in> local.nodes \<Longrightarrow> \<exists>\<pi> n. is_path \<pi> \<and> \<pi> 0 = ?x \<and> \<pi> n = local.return
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes

goal (1 subgoal):
 1. (\<And>\<pi>l n. \<lbrakk>is_path \<pi>l; \<pi> k = \<pi>l 0; \<pi>l n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_path \<pi>l
\<pi> k = \<pi>l 0
\<pi>l n = local.return

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence ip: \<open>is_path (\<pi>@\<^bsup>k\<^esup>\<pi>l)\<close> and l: \<open>(\<pi>@\<^bsup>k\<^esup>\<pi>l) k = \<pi> k\<close> and retl: \<open>(\<pi>@\<^bsup>k\<^esup>\<pi>l) (k + n) = return\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>l
\<pi> k = \<pi>l 0
\<pi>l n = local.return

goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>k\<^esup> \<pi>l) &&& (\<pi> @\<^bsup>k\<^esup> \<pi>l) k = \<pi> k &&& (\<pi> @\<^bsup>k\<^esup> \<pi>l) (k + n) = local.return
[PROOF STEP]
using path_cons[OF path(1) ipl \<pi>l]
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>l
\<pi> k = \<pi>l 0
\<pi>l n = local.return
is_path (\<pi> @\<^bsup>k\<^esup> \<pi>l)

goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>k\<^esup> \<pi>l) &&& (\<pi> @\<^bsup>k\<^esup> \<pi>l) k = \<pi> k &&& (\<pi> @\<^bsup>k\<^esup> \<pi>l) (k + n) = local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>k\<^esup> \<pi>l)
(\<pi> @\<^bsup>k\<^esup> \<pi>l) k = \<pi> k
(\<pi> @\<^bsup>k\<^esup> \<pi>l) (k + n) = local.return

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<pi>0': \<open>(\<pi>@\<^bsup>k\<^esup>\<pi>l) 0 = \<pi>' 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>l) 0 = \<pi>' 0
[PROOF STEP]
unfolding cs_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>l) 0 = \<pi>' 0
[PROOF STEP]
using  \<pi>l \<pi>0
[PROOF STATE]
proof (prove)
using this:
\<pi> k = \<pi>l 0
\<pi> 0 = \<pi>' 0

goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>l) 0 = \<pi>' 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>k\<^esup> \<pi>l) 0 = \<pi>' 0

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have eql: \<open>(\<pi>@\<^bsup>k\<^esup>\<pi>l) =\<^bsub>k\<^esub> \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>l) =\<^bsub>k\<^esub> \<pi>
[PROOF STEP]
by (metis path_append_eq_up_to)
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>k\<^esup> \<pi>l) =\<^bsub>k\<^esub> \<pi>

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have csl': \<open>cs\<^bsup>\<pi>@\<^bsup>k\<^esup>\<pi>l\<^esup>  k = cs\<^bsup>\<pi>\<^esup> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>\<^esup> k
[PROOF STEP]
using eql cs_path_swap ip path(1)
[PROOF STATE]
proof (prove)
using this:
(\<pi> @\<^bsup>k\<^esup> \<pi>l) =\<^bsub>k\<^esub> \<pi>
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> =\<^bsub>?k\<^esub> ?\<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k
is_path (\<pi> @\<^bsup>k\<^esup> \<pi>l)
is_path \<pi>

goal (1 subgoal):
 1. cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>\<^esup> k
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>\<^esup> k

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence notin: \<open>\<not>(\<exists> k'. cs\<^bsup>\<pi>@\<^bsup>k\<^esup>\<pi>l\<^esup>  k = cs\<^bsup>\<pi>'\<^esup> k')\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>\<^esup> k

goal (1 subgoal):
 1. \<nexists>k'. cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
[PROOF STEP]
using notin'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>\<^esup> k
\<nexists>k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'

goal (1 subgoal):
 1. \<nexists>k'. cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>k'. cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain i i' where *: \<open>i < k\<close> and csi: \<open>cs\<^bsup>\<pi>@\<^bsup>k\<^esup>\<pi>l\<^esup>  i = cs\<^bsup>\<pi>'\<^esup> i'\<close> and suci: \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>l) (Suc i) \<noteq> \<pi>' (Suc i')\<close>  and cdloop: \<open>k cd\<^bsup>\<pi>@\<^bsup>k\<^esup>\<pi>l\<^esup>\<rightarrow> i \<or> (\<forall> j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; (\<pi> @\<^bsup>k\<^esup> \<pi>l) (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using returned_missing_cd_or_loop[OF ip path(2) \<pi>0' notin notret retl]
[PROOF STATE]
proof (prove)
using this:
(\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; (\<pi> @\<^bsup>k\<^esup> \<pi>l) (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; (\<pi> @\<^bsup>k\<^esup> \<pi>l) (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i < k
cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
(\<pi> @\<^bsup>k\<^esup> \<pi>l) (Suc i) \<noteq> \<pi>' (Suc i')
k cd\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>i \<noteq> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> k
[PROOF STEP]
using notin csi
[PROOF STATE]
proof (prove)
using this:
\<nexists>k'. cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. i \<noteq> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<noteq> k

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence ik: \<open>i < k\<close>
[PROOF STATE]
proof (prove)
using this:
i \<noteq> k

goal (1 subgoal):
 1. i < k
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i \<noteq> k
i < k

goal (1 subgoal):
 1. i < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < k

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (prove)
using this:
i < k

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
[PROOF STEP]
using csi cs_path_swap_le[OF ip path(1) eql]
[PROOF STATE]
proof (prove)
using this:
i < k
cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
?k \<le> k \<Longrightarrow> cs\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup> ?k = cs\<^bsup>\<pi>\<^esup> ?k

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<pi> (Suc i) \<noteq> \<pi>' (Suc i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc i) \<noteq> \<pi>' (Suc i')
[PROOF STEP]
using ik eq_up_to_apply[OF eql, of \<open>Suc i\<close>] suci
[PROOF STATE]
proof (prove)
using this:
i < k
Suc i \<le> k \<Longrightarrow> (\<pi> @\<^bsup>k\<^esup> \<pi>l) (Suc i) = \<pi> (Suc i)
(\<pi> @\<^bsup>k\<^esup> \<pi>l) (Suc i) \<noteq> \<pi>' (Suc i')

goal (1 subgoal):
 1. \<pi> (Suc i) \<noteq> \<pi>' (Suc i')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (Suc i) \<noteq> \<pi>' (Suc i')

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> (Suc i) \<noteq> \<pi>' (Suc i')

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall> j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')
[PROOF STEP]
using cdloop cdi_path_swap_le[OF path(1) _ eql, of \<open>k\<close> \<open>i\<close>]
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')
\<lbrakk>k cd\<^bsup>\<pi> @\<^bsup>k\<^esup> \<pi>l\<^esup>\<rightarrow> i; k \<le> k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')

goal (1 subgoal):
 1. \<lbrakk>\<And>i i'. \<lbrakk>i < k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> thesis; \<nexists>n'. \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
\<pi> (Suc i) \<noteq> \<pi>' (Suc i')
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
\<pi> (Suc i) \<noteq> \<pi>' (Suc i')
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[OF *]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
\<pi> (Suc i) \<noteq> \<pi>' (Suc i')
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')
\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> ?i'1; \<pi> (Suc i) \<noteq> \<pi>' (Suc ?i'1); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>?i'1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?i'1)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_shift_set_cd: assumes \<open>is_path \<pi>\<close> shows \<open>{k + j| j . n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> j } = {i. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i }\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
assume \<open>i\<in>{k+j | j . n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> j }\<close>
[PROOF STATE]
proof (state)
this:
i \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}
[PROOF STEP]
obtain j where \<open>i = k+j\<close> \<open>n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>i = k + j; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = k + j
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
hence \<open>k+n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i\<close>
[PROOF STATE]
proof (prove)
using this:
i = k + j
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i
[PROOF STEP]
using cd_path_shift[OF _ assms, of \<open>k\<close> \<open>k+j\<close> \<open>k+n\<close>]
[PROOF STATE]
proof (prove)
using this:
i = k + j
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j
k \<le> k + j \<Longrightarrow> (k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j) = (k + n - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> k + j - k)

goal (1 subgoal):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
hence \<open>i\<in>{ i. k+n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i }\<close>
[PROOF STATE]
proof (prove)
using this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i

goal (1 subgoal):
 1. i \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i3 \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} \<Longrightarrow> ?i3 \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i3 \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} \<Longrightarrow> ?i3 \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?i3 \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} \<Longrightarrow> ?i3 \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
assume \<open>i\<in>{ i. k+n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i }\<close>
[PROOF STATE]
proof (state)
this:
i \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
hence *: \<open>k+n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i
[PROOF STEP]
obtain j where i: \<open>i = k+j\<close>
[PROOF STATE]
proof (prove)
using this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i

goal (1 subgoal):
 1. (\<And>j. i = k + j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis le_Suc_ex)
[PROOF STATE]
proof (state)
this:
i = k + j

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
hence \<open>k+n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k+j\<close>
[PROOF STATE]
proof (prove)
using this:
i = k + j

goal (1 subgoal):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i = k + j
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i

goal (1 subgoal):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
hence \<open>n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
using this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j

goal (1 subgoal):
 1. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j
[PROOF STEP]
using cd_path_shift[OF _ assms, of \<open>k\<close> \<open>k+j\<close> \<open>k+n\<close>]
[PROOF STATE]
proof (prove)
using this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j
k \<le> k + j \<Longrightarrow> (k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j) = (k + n - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> k + j - k)

goal (1 subgoal):
 1. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
hence \<open>i\<in>{k+j | j . n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> j }\<close>
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. i \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j
i = k + j

goal (1 subgoal):
 1. i \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i3 \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i} \<Longrightarrow> ?i3 \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?i3 \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} \<Longrightarrow> ?i3 \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
?i3 \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i} \<Longrightarrow> ?i3 \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} \<Longrightarrow> ?i3 \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
?i3 \<in> {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i} \<Longrightarrow> ?i3 \<in> {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j}

goal (1 subgoal):
 1. {k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{k + j |j. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> j} = {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_path_shift_set_cd: assumes path: \<open>is_path \<pi>\<close> shows \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> n = map \<pi> (sorted_list_of_set {i. k+n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i }) @ [\<pi> (k+n)]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
have mono:\<open>\<forall>n m. n < m \<longrightarrow> k + n < k + m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n m. n < m \<longrightarrow> k + n < k + m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n m. n < m \<longrightarrow> k + n < k + m

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
have fin: \<open>finite {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. is_path (\<pi> \<guillemotleft> k) \<and> i < n \<and> (\<pi> \<guillemotleft> k) n \<noteq> local.return \<and> (\<forall>j\<in>{i..n}. (\<pi> \<guillemotleft> k) j \<noteq> ipd ((\<pi> \<guillemotleft> k) i))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
have *: \<open>(\<lambda> x. k+x)`{i. n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> i} = {k + i | i. n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i} = {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i} = {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> n = map (\<pi>\<guillemotleft>k) (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> i}) @ [(\<pi>\<guillemotleft>k) n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map (\<pi> \<guillemotleft> k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [(\<pi> \<guillemotleft> k) n]
[PROOF STEP]
using cs_sorted_list_of_cd'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>?\<pi>\<^esup> ?k = map ?\<pi> (sorted_list_of_set {i. ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> i}) @ [?\<pi> ?k]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map (\<pi> \<guillemotleft> k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [(\<pi> \<guillemotleft> k) n]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map (\<pi> \<guillemotleft> k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [(\<pi> \<guillemotleft> k) n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map (\<pi> \<guillemotleft> k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [(\<pi> \<guillemotleft> k) n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
have \<open>\<dots> = map \<pi> (map (\<lambda> x. k+x) (sorted_list_of_set{i. n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> i})) @ [\<pi> (k+n)]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<pi> \<guillemotleft> k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [(\<pi> \<guillemotleft> k) n] = map \<pi> (map ((+) k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<pi> \<guillemotleft> k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [(\<pi> \<guillemotleft> k) n] = map \<pi> (map ((+) k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (\<pi> \<guillemotleft> k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [(\<pi> \<guillemotleft> k) n] = map \<pi> (map ((+) k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
have \<open>\<dots> = map \<pi> (sorted_list_of_set ((\<lambda> x. k+x)`{i. n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> i})) @ [\<pi> (k+n)]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (map ((+) k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)]
[PROOF STEP]
using sorted_list_of_set_map_mono[OF mono fin]
[PROOF STATE]
proof (prove)
using this:
map ((+) k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) = sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})

goal (1 subgoal):
 1. map \<pi> (map ((+) k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (map ((+) k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (map ((+) k) (sorted_list_of_set {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
have \<open>\<dots> = map \<pi> (sorted_list_of_set ({k + i | i. n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> i})) @ [\<pi> (k+n)]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [\<pi> (k + n)]
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
(+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i} = {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}

goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [\<pi> (k + n)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [\<pi> (k + n)]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set ((+) k ` {i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i})) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [\<pi> (k + n)]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
have \<open>\<dots> = map \<pi> (sorted_list_of_set ({i. k+n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> (k+n)]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
using path_shift_set_cd[OF path]
[PROOF STATE]
proof (prove)
using this:
{?k + j |j. ?n cd\<^bsup>\<pi> \<guillemotleft> ?k\<^esup>\<rightarrow> j} = {i. ?k + ?n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> ?k \<le> i}

goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {k + i |i. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> i}) @ [\<pi> (k + n)] = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = map \<pi> (sorted_list_of_set {i. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + n)]

goal:
No subgoals!
[PROOF STEP]
qed