[STATEMENT]
lemma cd_induct[consumes 1, case_names base IS]: assumes prem: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and base: \<open>\<And> i. i icd\<^bsup>\<pi>\<^esup>\<rightarrow>k \<Longrightarrow> P i\<close>
and IH: \<open>\<And> k' i'. k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> P k' \<Longrightarrow> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k' \<Longrightarrow> P i'\<close> shows \<open>P i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P i
[PROOF STEP]
using prem IH
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>?k'1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P ?k'1; ?i'1 icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k'1\<rbrakk> \<Longrightarrow> P ?i'1

goal (1 subgoal):
 1. P i
[PROOF STEP]
proof (induction \<open>i\<close> rule: less_induct,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; ?P5 x\<rbrakk> \<Longrightarrow> P x
 2. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> ?P5 x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
case (less i)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < i; ?y1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P ?y1
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>?k'1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P ?k'1; ?i'1 icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k'1\<rbrakk> \<Longrightarrow> P ?i'1

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; ?P5 x\<rbrakk> \<Longrightarrow> P x
 2. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> ?P5 x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
assume \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (state)
this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; ?P5 x\<rbrakk> \<Longrightarrow> P x
 2. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> ?P5 x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
thus \<open>P i\<close>
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. P i
[PROOF STEP]
using base
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
?i1 icd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> P ?i1

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
case (less i')
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < i'; ?y1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P ?y1
i' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>?k'1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P ?k'1; ?i'1 icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k'1\<rbrakk> \<Longrightarrow> P ?i'1

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
assume \<open>\<not> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (state)
this:
\<not> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
obtain k' where k': \<open> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<close> \<open>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'; k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less cd_split
[PROOF STATE]
proof (prove)
using this:
\<not> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>?y1 < i'; ?y1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P ?y1
i' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>?k'1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P ?k'1; ?i'1 icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k'1\<rbrakk> \<Longrightarrow> P ?i'1
\<lbrakk>?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; \<not> ?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; \<And>m. \<lbrakk>?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
hence icdk: \<open>i' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
using this:
i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'
k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
note ih=less(3)[OF k'(2)  _ k'(1)]
[PROOF STATE]
proof (state)
this:
P k' \<Longrightarrow> P i'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
have ki: \<open>k' < i'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < i'
[PROOF STEP]
using k' is_icdi_def is_cdi_def
[PROOF STATE]
proof (prove)
using this:
i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'
k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
(?n icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n') = (is_path ?\<pi> \<and> ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n' \<and> (\<forall>m\<in>{?n'<..<?n}. \<not> ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m))
(?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (is_path ?\<pi> \<and> ?k < ?i \<and> ?\<pi> ?i \<noteq> local.return \<and> (\<forall>j\<in>{?k..?i}. ?\<pi> j \<noteq> ipd (?\<pi> ?k)))

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
have \<open>P k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P k'
[PROOF STEP]
using less(1)[OF ki k'(2) ] less(3)
[PROOF STATE]
proof (prove)
using this:
(\<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i') \<Longrightarrow> P k'
\<lbrakk>?k'1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P ?k'1; ?i'1 icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k'1\<rbrakk> \<Longrightarrow> P ?i'1

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; y cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'\<rbrakk> \<Longrightarrow> P y; x cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; P k'; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> P i'; \<not> x icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
thus \<open>P i'\<close>
[PROOF STATE]
proof (prove)
using this:
P k'

goal (1 subgoal):
 1. P i'
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
P k'
P k' \<Longrightarrow> P i'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cdi_prefix: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m \<Longrightarrow> m < n' \<Longrightarrow> n' \<le> n \<Longrightarrow> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; m < n'; n' \<le> n\<rbrakk> \<Longrightarrow> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_path \<pi> \<and> m < n \<and> \<pi> n \<noteq> local.return \<and> (\<forall>j\<in>{m..n}. \<pi> j \<noteq> ipd (\<pi> m)); m < n'; n' \<le> n\<rbrakk> \<Longrightarrow> is_path \<pi> \<and> m < n' \<and> \<pi> n' \<noteq> local.return \<and> (\<forall>j\<in>{m..n'}. \<pi> j \<noteq> ipd (\<pi> m))
[PROOF STEP]
by (simp, metis term_path_stable)


[STATEMENT]
lemma cr_wn': assumes 1: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> and nc: \<open>\<not> m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> and 3: \<open>m < m'\<close> shows \<open>n < m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n < m' \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> n < m'\<close>
[PROOF STATE]
proof (state)
this:
\<not> n < m'

goal (1 subgoal):
 1. \<not> n < m' \<Longrightarrow> False
[PROOF STEP]
hence \<open>m' \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> n < m'

goal (1 subgoal):
 1. m' \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m' \<le> n

goal (1 subgoal):
 1. \<not> n < m' \<Longrightarrow> False
[PROOF STEP]
hence \<open>m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
m' \<le> n

goal (1 subgoal):
 1. m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
by (metis 1 3 cdi_prefix)
[PROOF STATE]
proof (state)
this:
m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. \<not> n < m' \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. False
[PROOF STEP]
using nc
[PROOF STATE]
proof (prove)
using this:
m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
\<not> m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cr_wn'': assumes \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> and \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close> and \<open>\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close> and  \<open>i \<le> j\<close> shows \<open>m \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> m \<le> n \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not>m\<le>n\<close>
[PROOF STATE]
proof (state)
this:
\<not> m \<le> n

goal (1 subgoal):
 1. \<not> m \<le> n \<Longrightarrow> False
[PROOF STEP]
hence nm: \<open>n < m\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> m \<le> n

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

goal (1 subgoal):
 1. \<not> m \<le> n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n < m

goal (1 subgoal):
 1. \<not> m \<le> n \<Longrightarrow> False
[PROOF STEP]
have \<open>m<j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < j
[PROOF STEP]
using assms(1) assms(4)
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
i \<le> j

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

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

goal (1 subgoal):
 1. \<not> m \<le> n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n < m
m < j
[PROOF STEP]
have \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close>
[PROOF STATE]
proof (prove)
using this:
n < m
m < j

goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n
[PROOF STEP]
using assms(2) cdi_prefix
[PROOF STATE]
proof (prove)
using this:
n < m
m < j
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n
\<lbrakk>?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m; ?m < ?n'; ?n' \<le> ?n\<rbrakk> \<Longrightarrow> ?n' cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m

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

goal (1 subgoal):
 1. \<not> m \<le> n \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n
\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ret_no_cd: assumes \<open>\<pi> n = return\<close> shows \<open>\<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis assms is_cdi_def)


[STATEMENT]
lemma ipd_not_self: assumes \<open>x \<in> nodes\<close> \<open>x\<noteq> return\<close> shows \<open>x \<noteq> ipd x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> ipd x
[PROOF STEP]
by (metis is_ipd_def assms ipd_is_ipd)


[STATEMENT]
lemma icd_cs: assumes \<open>l icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> l]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> l]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> l]
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have \<open>k = (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (prove)
using this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> l]
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
k = (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
k = (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_not_pd: assumes \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>\<pi> l \<noteq> \<pi> k\<close> shows \<open>\<not> \<pi> l pd\<rightarrow> \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<pi> l pd\<rightarrow> \<pi> k
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> k \<Longrightarrow> False
[PROOF STEP]
assume pd: \<open>\<pi> l pd\<rightarrow> \<pi> k\<close>
[PROOF STATE]
proof (state)
this:
\<pi> l pd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> k \<Longrightarrow> False
[PROOF STEP]
have nret: \<open>\<pi> k \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k \<noteq> local.return
[PROOF STEP]
by (metis assms(1) pd pd_ret_is_ret ret_no_cd)
[PROOF STATE]
proof (state)
this:
\<pi> k \<noteq> local.return

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> k \<Longrightarrow> False
[PROOF STEP]
have kl: \<open>k < l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < l
[PROOF STEP]
by (metis is_cdi_def assms(1))
[PROOF STATE]
proof (state)
this:
k < l

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> k \<Longrightarrow> False
[PROOF STEP]
have path: \<open>is_path \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi>
[PROOF STEP]
by (metis is_cdi_def assms(1))
[PROOF STATE]
proof (state)
this:
is_path \<pi>

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> k \<Longrightarrow> False
[PROOF STEP]
from path_pd_ipd[OF path nret assms(2) pd kl]
[PROOF STATE]
proof (chain)
picking this:
(\<And>la. \<lbrakk>k < la; la \<le> l; \<pi> la = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain n where \<open>k < n\<close> \<open>n \<le> l\<close> \<open>\<pi> n = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>la. \<lbrakk>k < la; la \<le> l; \<pi> la = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>k < n; n \<le> l; \<pi> n = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
k < n
n \<le> l
\<pi> n = ipd (\<pi> k)

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> k \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
k < n
n \<le> l
\<pi> n = ipd (\<pi> k)

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
k < n
n \<le> l
\<pi> n = ipd (\<pi> k)
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
k < n
n \<le> l
\<pi> n = ipd (\<pi> k)
is_path \<pi> \<and> k < l \<and> \<pi> l \<noteq> local.return \<and> (\<forall>j\<in>{k..l}. \<pi> j \<noteq> ipd (\<pi> k))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_ipd_is_cd: assumes \<open>k<m\<close> \<open>\<pi> m = ipd (\<pi> k)\<close> \<open>\<forall> n \<in> {k..<m}. \<pi> n \<noteq> ipd (\<pi> k)\<close> and mcdj: \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
 2. \<not> ?P \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
assume \<open>j < k\<close>
[PROOF STATE]
proof (state)
this:
j < k

goal (2 subgoals):
 1. ?P \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
 2. \<not> ?P \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
using this:
j < k

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
by (metis mcdj assms(1) cdi_prefix less_imp_le_nat)
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

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

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

goal (1 subgoal):
 1. \<not> j < k \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
have \<open>k < j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < j
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k < j \<Longrightarrow> False
[PROOF STEP]
using kj assms mcdj
[PROOF STATE]
proof (prove)
using this:
k \<le> j
k < m
\<pi> m = ipd (\<pi> k)
\<forall>n\<in>{k..<m}. \<pi> n \<noteq> ipd (\<pi> k)
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. \<not> k < j \<Longrightarrow> False
[PROOF STEP]
by (auto, metis is_cdi_def is_ipd_def cd_not_pd ipd_is_ipd path_nodes term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
k < j

goal (1 subgoal):
 1. \<not> j < k \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < j

goal (1 subgoal):
 1. \<not> j < k \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
have \<open>j < m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < m
[PROOF STEP]
using mcdj is_cdi_def
[PROOF STATE]
proof (prove)
using this:
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
(?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (is_path ?\<pi> \<and> ?k < ?i \<and> ?\<pi> ?i \<noteq> local.return \<and> (\<forall>j\<in>{?k..?i}. ?\<pi> j \<noteq> ipd (?\<pi> ?k)))

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

goal (1 subgoal):
 1. \<not> j < k \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
hence \<open>\<forall> n \<in> {k..j}. \<pi> n \<noteq> ipd(\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
j < m

goal (1 subgoal):
 1. \<forall>n\<in>{k..j}. \<pi> n \<noteq> ipd (\<pi> k)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
j < m
\<forall>n\<in>{k..<m}. \<pi> n \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. \<forall>n\<in>{k..j}. \<pi> n \<noteq> ipd (\<pi> k)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>{k..j}. \<pi> n \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. \<not> j < k \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < j
\<forall>n\<in>{k..j}. \<pi> n \<noteq> ipd (\<pi> k)
[PROOF STEP]
have \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
k < j
\<forall>n\<in>{k..j}. \<pi> n \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis mcdj is_cdi_def term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis mcdj cd_trans)
[PROOF STATE]
proof (state)
this:
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis is_cdi_def is_ipd_def assms(2) cd_not_pd ipd_is_ipd path_nodes term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> j < k \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipd_pd_cd0: assumes lcd: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> shows \<open>ipd (\<pi> 0) pd\<rightarrow> (\<pi> n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
obtain k l where \<pi>0: \<open>\<pi> 0 = k\<close> and \<pi>n: \<open>\<pi> n = l\<close> and cdi: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k l. \<lbrakk>\<pi> 0 = k; \<pi> n = l; n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lcd
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0

goal (1 subgoal):
 1. (\<And>k l. \<lbrakk>\<pi> 0 = k; \<pi> n = l; n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> 0 < n \<and> \<pi> n \<noteq> local.return \<and> (\<forall>j\<in>{0..n}. \<pi> j \<noteq> ipd (\<pi> 0))

goal (1 subgoal):
 1. (\<And>k l. \<lbrakk>\<pi> 0 = k; \<pi> n = l; is_path \<pi> \<and> 0 < n \<and> \<pi> n \<noteq> local.return \<and> (\<forall>j\<in>{0..n}. \<pi> j \<noteq> ipd (\<pi> 0))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi> 0 = k
\<pi> n = l
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have nret: \<open>k \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> local.return
[PROOF STEP]
by (metis is_cdi_def \<pi>0 cdi term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
k \<noteq> local.return

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have  path: \<open>is_path \<pi>\<close> and ipd: \<open>\<forall> i\<le>n. \<pi> i \<noteq> ipd k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi> &&& \<forall>i\<le>n. \<pi> i \<noteq> ipd k
[PROOF STEP]
using cdi
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0

goal (1 subgoal):
 1. is_path \<pi> &&& \<forall>i\<le>n. \<pi> i \<noteq> ipd k
[PROOF STEP]
unfolding is_cdi_def \<pi>0
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> 0 < n \<and> \<pi> n \<noteq> local.return \<and> (\<forall>j\<in>{0..n}. \<pi> j \<noteq> ipd k)

goal (1 subgoal):
 1. is_path \<pi> &&& \<forall>i\<le>n. \<pi> i \<noteq> ipd k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path \<pi>
\<forall>i\<le>n. \<pi> i \<noteq> ipd k

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
is_path \<pi>
\<forall>i\<le>n. \<pi> i \<noteq> ipd k

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
fix \<pi>' n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
assume path': \<open>is_path \<pi>'\<close>
    and \<pi>'0: \<open>\<pi>' 0 = l\<close>
    and ret: \<open>\<pi>' n' = return\<close>
[PROOF STATE]
proof (state)
this:
is_path \<pi>'
\<pi>' 0 = l
\<pi>' n' = local.return

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have \<open>is_path (\<pi> @\<^bsup>n\<^esup>  \<pi>')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')
[PROOF STEP]
using path path' \<pi>n \<pi>'0
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
\<pi> n = l
\<pi>' 0 = l

goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')
[PROOF STEP]
by (metis path_cons)
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have \<open>(\<pi> @\<^bsup>n\<^esup>  \<pi>') (n+n') = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>n\<^esup> \<pi>') (n + n') = local.return
[PROOF STEP]
using ret \<pi>n \<pi>'0
[PROOF STATE]
proof (prove)
using this:
\<pi>' n' = local.return
\<pi> n = l
\<pi>' 0 = l

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

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') (n + n') = local.return

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have \<open>(\<pi> @\<^bsup>n\<^esup>  \<pi>') 0 = k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>n\<^esup> \<pi>') 0 = k
[PROOF STEP]
using \<pi>0
[PROOF STATE]
proof (prove)
using this:
\<pi> 0 = k

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

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') 0 = k

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have \<open>ipd k pd\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd k pd\<rightarrow> k
[PROOF STEP]
by (metis is_ipd_def path \<pi>0 ipd_is_ipd nret path_nodes)
[PROOF STATE]
proof (state)
this:
ipd k pd\<rightarrow> k

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')
(\<pi> @\<^bsup>n\<^esup> \<pi>') (n + n') = local.return
(\<pi> @\<^bsup>n\<^esup> \<pi>') 0 = k
ipd k pd\<rightarrow> k
[PROOF STEP]
obtain k' where k': \<open>k' \<le> n+n'\<close> \<open>(\<pi> @\<^bsup>n\<^esup>  \<pi>') k' = ipd k\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')
(\<pi> @\<^bsup>n\<^esup> \<pi>') (n + n') = local.return
(\<pi> @\<^bsup>n\<^esup> \<pi>') 0 = k
ipd k pd\<rightarrow> k

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>k' \<le> n + n'; (\<pi> @\<^bsup>n\<^esup> \<pi>') k' = ipd k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis pd_intro)
[PROOF STATE]
proof (state)
this:
k' \<le> n + n'
(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = ipd k

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have \<open>\<not> k'\<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k' \<le> n
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k' \<le> n \<Longrightarrow> False
[PROOF STEP]
assume \<open>k' \<le> n\<close>
[PROOF STATE]
proof (state)
this:
k' \<le> n

goal (1 subgoal):
 1. k' \<le> n \<Longrightarrow> False
[PROOF STEP]
hence \<open>(\<pi> @\<^bsup>n\<^esup>  \<pi>') k' = \<pi> k'\<close>
[PROOF STATE]
proof (prove)
using this:
k' \<le> n

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

goal (1 subgoal):
 1. k' \<le> n \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = \<pi> k'

goal (1 subgoal):
 1. False
[PROOF STEP]
using k'(2) ipd
[PROOF STATE]
proof (prove)
using this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = \<pi> k'
(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = ipd k
\<forall>i\<le>n. \<pi> i \<noteq> ipd k

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis \<open>k' \<le> n\<close>)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> k' \<le> n

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
hence \<open>(\<pi> @\<^bsup>n\<^esup>  \<pi>') k' = \<pi>' (k' - n)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> k' \<le> n

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

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = \<pi>' (k' - n)

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have \<open>(k' - n) \<le> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' - n \<le> n'
[PROOF STEP]
using k'
[PROOF STATE]
proof (prove)
using this:
k' \<le> n + n'
(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = ipd k

goal (1 subgoal):
 1. k' - n \<le> n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k' - n \<le> n'

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = \<pi>' (k' - n)
k' - n \<le> n'
[PROOF STEP]
have \<open>\<exists> k'\<le>n'. \<pi>' k' = ipd k\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = \<pi>' (k' - n)
k' - n \<le> n'

goal (1 subgoal):
 1. \<exists>k'\<le>n'. \<pi>' k' = ipd k
[PROOF STEP]
unfolding k'
[PROOF STATE]
proof (prove)
using this:
ipd k = \<pi>' (k' - n)
k' - n \<le> n'

goal (1 subgoal):
 1. \<exists>k'\<le>n'. \<pi>' k' = ipd k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k'\<le>n'. \<pi>' k' = ipd k

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_path ?\<pi>'3; ?\<pi>'3 0 = l; ?\<pi>'3 ?n'3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k'\<le>?n'3. ?\<pi>'3 k' = ipd k

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_path ?\<pi>'3; ?\<pi>'3 0 = l; ?\<pi>'3 ?n'3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k'\<le>?n'3. ?\<pi>'3 k' = ipd k

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
have \<open>l \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> local.nodes
[PROOF STEP]
by (metis \<pi>n path path_nodes)
[PROOF STATE]
proof (state)
this:
l \<in> local.nodes

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_path ?\<pi>'3; ?\<pi>'3 0 = l; ?\<pi>'3 ?n'3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k'\<le>?n'3. ?\<pi>'3 k' = ipd k
l \<in> local.nodes
[PROOF STEP]
show \<open>ipd (\<pi> 0) pd\<rightarrow> (\<pi> n)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>'3; ?\<pi>'3 0 = l; ?\<pi>'3 ?n'3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k'\<le>?n'3. ?\<pi>'3 k' = ipd k
l \<in> local.nodes

goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> n
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>'3; ?\<pi>'3 0 = l; ?\<pi>'3 ?n'3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k'\<le>?n'3. ?\<pi>'3 k' = ipd k
l \<in> local.nodes

goal (1 subgoal):
 1. \<pi> n \<in> local.nodes \<and> (\<forall>\<pi>' na. is_path \<pi>' \<and> \<pi>' 0 = \<pi> n \<and> \<pi>' na = local.return \<longrightarrow> (\<exists>k\<le>na. \<pi>' k = ipd (\<pi> 0)))
[PROOF STEP]
by (simp add: \<pi>0 \<pi>n)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> 0) pd\<rightarrow> \<pi> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipd_pd_cd: assumes lcd: \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> shows \<open>ipd (\<pi> k) pd\<rightarrow> (\<pi> l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
have \<open>l-k cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow>0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
[PROOF STEP]
using lcd cd_path_shift0 is_cdi_def
[PROOF STATE]
proof (prove)
using this:
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
is_path ?\<pi> \<Longrightarrow> (?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?k cd\<^bsup>?\<pi> \<guillemotleft> ?k\<^esup>\<rightarrow> 0)
(?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (is_path ?\<pi> \<and> ?k < ?i \<and> ?\<pi> ?i \<noteq> local.return \<and> (\<forall>j\<in>{?k..?i}. ?\<pi> j \<noteq> ipd (?\<pi> ?k)))

goal (1 subgoal):
 1. l - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
note ipd_pd_cd0[OF this]
[PROOF STATE]
proof (state)
this:
ipd ((\<pi> \<guillemotleft> k) 0) pd\<rightarrow> (\<pi> \<guillemotleft> k) (l - k)

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ipd ((\<pi> \<guillemotleft> k) 0) pd\<rightarrow> (\<pi> \<guillemotleft> k) (l - k)

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
have \<open>(\<pi> \<guillemotleft> k) 0 = \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) 0 = \<pi> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) 0 = \<pi> k

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) 0 = \<pi> k

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
have \<open>k < l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < l
[PROOF STEP]
using lcd
[PROOF STATE]
proof (prove)
using this:
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. k < l
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> k < l \<and> \<pi> l \<noteq> local.return \<and> (\<forall>j\<in>{k..l}. \<pi> j \<noteq> ipd (\<pi> k))

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

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k < l
[PROOF STEP]
have \<open>(\<pi> \<guillemotleft> k) (l - k) = \<pi> l\<close>
[PROOF STATE]
proof (prove)
using this:
k < l

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) (l - k) = \<pi> l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) (l - k) = \<pi> l

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
ipd ((\<pi> \<guillemotleft> k) 0) pd\<rightarrow> (\<pi> \<guillemotleft> k) (l - k)
(\<pi> \<guillemotleft> k) 0 = \<pi> k
(\<pi> \<guillemotleft> k) (l - k) = \<pi> l
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
l - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
ipd ((\<pi> \<guillemotleft> k) 0) pd\<rightarrow> (\<pi> \<guillemotleft> k) (l - k)
(\<pi> \<guillemotleft> k) 0 = \<pi> k
(\<pi> \<guillemotleft> k) (l - k) = \<pi> l

goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ipd (\<pi> k) pd\<rightarrow> \<pi> l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_is_cd_ipd: assumes km: \<open>k<m\<close> and ipd: \<open>\<pi> m = ipd (\<pi> k)\<close> \<open>\<forall> n \<in> {k..<m}. \<pi> n \<noteq> ipd (\<pi> k)\<close> and cdj: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> and nipdj: \<open>ipd (\<pi> j) \<noteq> \<pi> m\<close> shows \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
have path: \<open>is_path \<pi>\<close>
  and jk: \<open>j < k\<close>
  and nretj: \<open>\<pi> k \<noteq> return\<close>
  and nipd: \<open>\<forall> l \<in> {j..k}. \<pi> l \<noteq> ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_path \<pi> &&& j < k) &&& \<pi> k \<noteq> local.return &&& \<forall>l\<in>{j..k}. \<pi> l \<noteq> ipd (\<pi> j)
[PROOF STEP]
using  cdj is_cdi_def
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
(?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (is_path ?\<pi> \<and> ?k < ?i \<and> ?\<pi> ?i \<noteq> local.return \<and> (\<forall>j\<in>{?k..?i}. ?\<pi> j \<noteq> ipd (?\<pi> ?k)))

goal (1 subgoal):
 1. (is_path \<pi> &&& j < k) &&& \<pi> k \<noteq> local.return &&& \<forall>l\<in>{j..k}. \<pi> l \<noteq> ipd (\<pi> j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path \<pi>
j < k
\<pi> k \<noteq> local.return
\<forall>l\<in>{j..k}. \<pi> l \<noteq> ipd (\<pi> j)

goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
have pd: \<open>ipd (\<pi> j) pd\<rightarrow> \<pi> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> j) pd\<rightarrow> \<pi> m
[PROOF STEP]
by (metis atLeastAtMost_iff cdj ipd(1) ipd_pd_cd jk le_refl less_imp_le nipd nretj path path_nodes pd_pd_ipd)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> j) pd\<rightarrow> \<pi> m

goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
have nretm: \<open>\<pi> m \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> m \<noteq> local.return
[PROOF STEP]
by (metis nipdj pd pd_ret_is_ret)
[PROOF STATE]
proof (state)
this:
\<pi> m \<noteq> local.return

goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
have jm: \<open>j < m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < m
[PROOF STEP]
using jk km
[PROOF STATE]
proof (prove)
using this:
j < k
k < m

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

goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
show \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
assume ncdj: \<open>\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (state)
this:
\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<exists> l \<in> {j..m}. \<pi> l = ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. \<exists>l\<in>{j..m}. \<pi> l = ipd (\<pi> j)
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
\<not> (is_path \<pi> \<and> j < m \<and> \<pi> m \<noteq> local.return \<and> (\<forall>ja\<in>{j..m}. \<pi> ja \<noteq> ipd (\<pi> j)))

goal (1 subgoal):
 1. \<exists>l\<in>{j..m}. \<pi> l = ipd (\<pi> j)
[PROOF STEP]
by (metis jm nretm path)
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>{j..m}. \<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<in>{j..m}. \<pi> l = ipd (\<pi> j)
[PROOF STEP]
obtain l
    where jl: \<open>j \<le> l\<close> and \<open>l \<le> m\<close>
    and lipd: \<open>\<pi> l = ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>{j..m}. \<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>j \<le> l; l \<le> m; \<pi> l = ipd (\<pi> j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
j \<le> l
l \<le> m
\<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
hence lm: \<open>l < m\<close>
[PROOF STATE]
proof (prove)
using this:
j \<le> l
l \<le> m
\<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. l < m
[PROOF STEP]
using nipdj
[PROOF STATE]
proof (prove)
using this:
j \<le> l
l \<le> m
\<pi> l = ipd (\<pi> j)
ipd (\<pi> j) \<noteq> \<pi> m

goal (1 subgoal):
 1. l < m
[PROOF STEP]
by (metis le_eq_less_or_eq)
[PROOF STATE]
proof (state)
this:
l < m

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
have npd: \<open>\<not> ipd (\<pi> k) pd\<rightarrow> \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ipd (\<pi> k) pd\<rightarrow> \<pi> l
[PROOF STEP]
by (metis ipd(1) lipd nipdj pd pd_antisym)
[PROOF STATE]
proof (state)
this:
\<not> ipd (\<pi> k) pd\<rightarrow> \<pi> l

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
have nd: \<open>\<pi> l \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> l \<in> local.nodes
[PROOF STEP]
using path path_nodes
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes

goal (1 subgoal):
 1. \<pi> l \<in> local.nodes
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> l \<in> local.nodes

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
from no_pd_path[OF nd npd]
[PROOF STATE]
proof (chain)
picking this:
(\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> l; \<pi>' n = local.return; \<forall>ka\<le>n. \<pi>' ka \<noteq> ipd (\<pi> k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<pi>' n where path': \<open>is_path \<pi>'\<close> and \<pi>'0: \<open>\<pi>' 0 = \<pi> l\<close> and \<pi>'n: \<open>\<pi>' n = return\<close> and nipd: \<open>\<forall> ka\<le>n. \<pi>' ka \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> l; \<pi>' n = local.return; \<forall>ka\<le>n. \<pi>' ka \<noteq> ipd (\<pi> k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
let \<open>?\<pi>\<close> = \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>') \<guillemotleft> k\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
have path'': \<open>is_path ?\<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k)
[PROOF STEP]
by (metis \<pi>'0 path path' path_cons path_path_shift)
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k)

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k)

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
have kl: \<open>k < l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < l
[PROOF STEP]
using lipd cdj jl
[PROOF STATE]
proof (prove)
using this:
\<pi> l = ipd (\<pi> j)
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
j \<le> l

goal (1 subgoal):
 1. k < l
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
\<pi> l = ipd (\<pi> j)
is_path \<pi> \<and> j < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>ja\<in>{j..k}. \<pi> ja \<noteq> ipd (\<pi> j))
j \<le> l

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

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
have \<open>?\<pi> 0 = \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) 0 = \<pi> k
[PROOF STEP]
using kl
[PROOF STATE]
proof (prove)
using this:
k < l

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

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) 0 = \<pi> k

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
have \<open>?\<pi> (l + n - k) = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) (l + n - k) = local.return
[PROOF STEP]
using \<pi>'n \<pi>'0 kl
[PROOF STATE]
proof (prove)
using this:
\<pi>' n = local.return
\<pi>' 0 = \<pi> l
k < l

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

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) (l + n - k) = local.return

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
have \<open>ipd (\<pi> k) pd\<rightarrow> \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> k
[PROOF STEP]
by (metis is_ipd_def ipd_is_ipd nretj path path_nodes)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> k) pd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k)
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) 0 = \<pi> k
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) (l + n - k) = local.return
ipd (\<pi> k) pd\<rightarrow> \<pi> k
[PROOF STEP]
obtain l' where l': \<open>l' \<le> (l + n - k)\<close> \<open>?\<pi> l' = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k)
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) 0 = \<pi> k
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) (l + n - k) = local.return
ipd (\<pi> k) pd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' \<le> l + n - k; (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) l' = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k)
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) 0 = \<pi> k
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) (l + n - k) = local.return
\<pi> k \<in> local.nodes \<and> (\<forall>\<pi>' n. is_path \<pi>' \<and> \<pi>' 0 = \<pi> k \<and> \<pi>' n = local.return \<longrightarrow> (\<exists>ka\<le>n. \<pi>' ka = ipd (\<pi> k)))

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' \<le> l + n - k; (\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) l' = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l' \<le> l + n - k
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) l' = ipd (\<pi> k)

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume *: \<open>k + l' \<le> l\<close>
[PROOF STATE]
proof (state)
this:
k + l' \<le> l

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<pi> (k + l') = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
k + l' \<le> l

goal (1 subgoal):
 1. \<pi> (k + l') = ipd (\<pi> k)
[PROOF STEP]
using l'
[PROOF STATE]
proof (prove)
using this:
k + l' \<le> l
l' \<le> l + n - k
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) l' = ipd (\<pi> k)

goal (1 subgoal):
 1. \<pi> (k + l') = ipd (\<pi> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (k + l') = ipd (\<pi> k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> (k + l') = ipd (\<pi> k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
have \<open>k + l' < m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + l' < m
[PROOF STEP]
by (metis "*" dual_order.strict_trans2 lm)
[PROOF STATE]
proof (state)
this:
k + l' < m

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> (k + l') = ipd (\<pi> k)
k + l' < m
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + l') = ipd (\<pi> k)
k + l' < m

goal (1 subgoal):
 1. False
[PROOF STEP]
using ipd(2)
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + l') = ipd (\<pi> k)
k + l' < m
\<forall>n\<in>{k..<m}. \<pi> n \<noteq> ipd (\<pi> k)

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

goal (1 subgoal):
 1. \<not> k + l' \<le> l \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k + l' \<le> l \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> k + l' \<le> l\<close>
[PROOF STATE]
proof (state)
this:
\<not> k + l' \<le> l

goal (1 subgoal):
 1. \<not> k + l' \<le> l \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<pi>' (k + l' - l) = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> k + l' \<le> l

goal (1 subgoal):
 1. \<pi>' (k + l' - l) = ipd (\<pi> k)
[PROOF STEP]
using l'
[PROOF STATE]
proof (prove)
using this:
\<not> k + l' \<le> l
l' \<le> l + n - k
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) l' = ipd (\<pi> k)

goal (1 subgoal):
 1. \<pi>' (k + l' - l) = ipd (\<pi> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>' (k + l' - l) = ipd (\<pi> k)

goal (1 subgoal):
 1. \<not> k + l' \<le> l \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>' (k + l' - l) = ipd (\<pi> k)

goal (1 subgoal):
 1. \<not> k + l' \<le> l \<Longrightarrow> False
[PROOF STEP]
have \<open>k + l' - l \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + l' - l \<le> n
[PROOF STEP]
using l' kl
[PROOF STATE]
proof (prove)
using this:
l' \<le> l + n - k
(\<pi> @\<^bsup>l\<^esup> \<pi>' \<guillemotleft> k) l' = ipd (\<pi> k)
k < l

goal (1 subgoal):
 1. k + l' - l \<le> n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
k + l' - l \<le> n

goal (1 subgoal):
 1. \<not> k + l' \<le> l \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi>' (k + l' - l) = ipd (\<pi> k)
k + l' - l \<le> n
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k + l' - l) = ipd (\<pi> k)
k + l' - l \<le> n

goal (1 subgoal):
 1. False
[PROOF STEP]
using nipd
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k + l' - l) = ipd (\<pi> k)
k + l' - l \<le> n
\<forall>ka\<le>n. \<pi>' ka \<noteq> ipd (\<pi> k)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipd_icd_greatest_cd_not_ipd: assumes ipd: \<open>\<pi> m = ipd (\<pi> k)\<close> \<open>\<forall> n \<in> {k..<m}. \<pi> n \<noteq> ipd (\<pi> k)\<close>
and km: \<open>k < m\<close> and icdj: \<open>m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> shows \<open>j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
let \<open>?j\<close> = \<open>GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
have kcdj: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
using assms cd_ipd_is_cd is_icdi_def
[PROOF STATE]
proof (prove)
using this:
\<pi> m = ipd (\<pi> k)
\<forall>n\<in>{k..<m}. \<pi> n \<noteq> ipd (\<pi> k)
k < m
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j
\<lbrakk>?k < ?m; ?\<pi> ?m = ipd (?\<pi> ?k); \<forall>n\<in>{?k..<?m}. ?\<pi> n \<noteq> ipd (?\<pi> ?k); ?m cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j\<rbrakk> \<Longrightarrow> ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j
(?n icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n') = (is_path ?\<pi> \<and> ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n' \<and> (\<forall>m\<in>{?n'<..<?n}. \<not> ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m))

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

goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
have nipd: \<open>ipd (\<pi> j) \<noteq> \<pi> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> j) \<noteq> \<pi> m
[PROOF STEP]
using icdj
[PROOF STATE]
proof (prove)
using this:
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

goal (1 subgoal):
 1. ipd (\<pi> j) \<noteq> \<pi> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ipd (\<pi> j) \<noteq> \<pi> m

goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
have bound: \<open>\<And> j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m \<Longrightarrow> j \<le> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m \<Longrightarrow> j \<le> k
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. (is_path \<pi> \<and> j < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>ja\<in>{j..k}. \<pi> ja \<noteq> ipd (\<pi> j))) \<and> ipd (\<pi> j) \<noteq> \<pi> m \<Longrightarrow> j \<le> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1 \<and> ipd (\<pi> ?j1) \<noteq> \<pi> m \<Longrightarrow> ?j1 \<le> k

goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
have exists: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m\<close> (is \<open>?P j\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m
[PROOF STEP]
using kcdj nipd
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
ipd (\<pi> j) \<noteq> \<pi> m

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

goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
note GreatestI_nat[of \<open>?P\<close> _ \<open>k\<close>, OF exists] Greatest_le_nat[of \<open>?P\<close> \<open>j\<close> \<open>k\<close>, OF exists]
[PROOF STATE]
proof (state)
this:
(\<And>y. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> ipd (\<pi> y) \<noteq> \<pi> m \<Longrightarrow> y \<le> k) \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m) \<and> ipd (\<pi> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m)) \<noteq> \<pi> m
(\<And>y. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> ipd (\<pi> y) \<noteq> \<pi> m \<Longrightarrow> y \<le> k) \<Longrightarrow> j \<le> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m)

goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
hence kcdj': \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j\<close> and ipd': \<open>ipd (\<pi> ?j) \<noteq> \<pi> m\<close> and jj: \<open>j \<le> ?j\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>y. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> ipd (\<pi> y) \<noteq> \<pi> m \<Longrightarrow> y \<le> k) \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m) \<and> ipd (\<pi> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m)) \<noteq> \<pi> m
(\<And>y. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> ipd (\<pi> y) \<noteq> \<pi> m \<Longrightarrow> y \<le> k) \<Longrightarrow> j \<le> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m)

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) &&& ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)) \<noteq> \<pi> m &&& j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
using bound
[PROOF STATE]
proof (prove)
using this:
(\<And>y. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> ipd (\<pi> y) \<noteq> \<pi> m \<Longrightarrow> y \<le> k) \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m) \<and> ipd (\<pi> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m)) \<noteq> \<pi> m
(\<And>y. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> ipd (\<pi> y) \<noteq> \<pi> m \<Longrightarrow> y \<le> k) \<Longrightarrow> j \<le> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> \<pi> m)
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1 \<and> ipd (\<pi> ?j1) \<noteq> \<pi> m \<Longrightarrow> ?j1 \<le> k

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) &&& ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)) \<noteq> \<pi> m &&& j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)) \<noteq> \<pi> m
j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
hence mcdj': \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j\<close>
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)) \<noteq> \<pi> m
j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
using ipd km cd_is_cd_ipd
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)) \<noteq> \<pi> m
j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
\<pi> m = ipd (\<pi> k)
\<forall>n\<in>{k..<m}. \<pi> n \<noteq> ipd (\<pi> k)
k < m
\<lbrakk>?k < ?m; ?\<pi> ?m = ipd (?\<pi> ?k); \<forall>n\<in>{?k..<?m}. ?\<pi> n \<noteq> ipd (?\<pi> ?k); ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j; ipd (?\<pi> ?j) \<noteq> ?\<pi> ?m\<rbrakk> \<Longrightarrow> ?m cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j

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

goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
show \<open>j = ?j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) \<Longrightarrow> False
[PROOF STEP]
assume \<open>j \<noteq> ?j\<close>
[PROOF STATE]
proof (state)
this:
j \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal (1 subgoal):
 1. j \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) \<Longrightarrow> False
[PROOF STEP]
hence jlj: \<open>j < ?j\<close>
[PROOF STATE]
proof (prove)
using this:
j \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal (1 subgoal):
 1. j < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
using jj
[PROOF STATE]
proof (prove)
using this:
j \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

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

goal (1 subgoal):
 1. j \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal (1 subgoal):
 1. j \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) \<Longrightarrow> False
[PROOF STEP]
have \<open>?j < m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) < m
[PROOF STEP]
using kcdj' km
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
k < m

goal (1 subgoal):
 1. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) < m
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> (GREATEST j. (is_path \<pi> \<and> j < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>ja\<in>{j..k}. \<pi> ja \<noteq> ipd (\<pi> j))) \<and> ipd (\<pi> j) \<noteq> \<pi> m) < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{GREATEST j. (is_path \<pi> \<and> j < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>ja\<in>{j..k}. \<pi> ja \<noteq> ipd (\<pi> j))) \<and> ipd (\<pi> j) \<noteq> \<pi> m..k}. \<pi> j \<noteq> ipd (\<pi> (GREATEST j. (is_path \<pi> \<and> j < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>ja\<in>{j..k}. \<pi> ja \<noteq> ipd (\<pi> j))) \<and> ipd (\<pi> j) \<noteq> \<pi> m)))
k < m

goal (1 subgoal):
 1. (GREATEST j. (is_path \<pi> \<and> j < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>ja\<in>{j..k}. \<pi> ja \<noteq> ipd (\<pi> j))) \<and> ipd (\<pi> j) \<noteq> \<pi> m) < m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) < m

goal (1 subgoal):
 1. j \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) < m
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
j < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) < m

goal (1 subgoal):
 1. False
[PROOF STEP]
using icdj mcdj'
[PROOF STATE]
proof (prove)
using this:
j < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) < m
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding is_icdi_def
[PROOF STATE]
proof (prove)
using this:
j < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m) < m
is_path \<pi> \<and> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> (\<forall>ma\<in>{j<..<m}. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> ma)
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_impl_icd_cd: assumes \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> and \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<not> i icd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
[PROOF STEP]
using assms cd_split icd_uniq
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<not> i icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
\<lbrakk>?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; \<not> ?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; \<And>m. \<lbrakk>?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>?m icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n; ?m icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n'\<rbrakk> \<Longrightarrow> ?n = ?n'

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
[PROOF STEP]
by metis


[STATEMENT]
lemma cdi_is_cd_icdi: assumes \<open>k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<longleftrightarrow> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> i = j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i) = (j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> i = j)
[PROOF STEP]
by (metis assms cd_impl_icd_cd cd_trans icd_imp_cd icd_uniq)


[STATEMENT]
lemma same_ipd_stable: assumes \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> \<open>i<j\<close> \<open>ipd (\<pi> i) = ipd (\<pi> k)\<close> shows \<open>ipd (\<pi> j) = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
have jcdi: \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
by (metis is_cdi_def assms(1,2,3) cr_wn' le_antisym less_imp_le_nat)
[PROOF STATE]
proof (state)
this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i

goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
have 1: \<open>ipd (\<pi> j) pd\<rightarrow> \<pi> k \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> j) pd\<rightarrow> \<pi> k
[PROOF STEP]
by (metis assms(2) ipd_pd_cd)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> j) pd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
have 2: \<open>ipd (\<pi> k) pd\<rightarrow> \<pi> j \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> \<pi> j
[PROOF STEP]
by (metis assms(4) ipd_pd_cd jcdi)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> k) pd\<rightarrow> \<pi> j

goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
have 3: \<open>ipd (\<pi> k) pd\<rightarrow> (ipd (\<pi> j))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> k) pd\<rightarrow> ipd (\<pi> j)
[PROOF STEP]
by (metis 2 IFC_def.is_cdi_def assms(1,2,4) atLeastAtMost_iff jcdi less_imp_le pd_node2 pd_pd_ipd)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> k) pd\<rightarrow> ipd (\<pi> j)

goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
have 4: \<open>ipd (\<pi> j) pd\<rightarrow> (ipd (\<pi> k))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> j) pd\<rightarrow> ipd (\<pi> k)
[PROOF STEP]
by (metis 1 2 IFC_def.is_ipd_def assms(2) cd_not_pd ipd_is_ipd jcdi pd_node2 ret_no_cd)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> j) pd\<rightarrow> ipd (\<pi> k)

goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
using 3 4 pd_antisym
[PROOF STATE]
proof (prove)
using this:
ipd (\<pi> k) pd\<rightarrow> ipd (\<pi> j)
ipd (\<pi> j) pd\<rightarrow> ipd (\<pi> k)
\<lbrakk>?x pd\<rightarrow> ?y; ?y pd\<rightarrow> ?x\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. ipd (\<pi> j) = ipd (\<pi> k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ipd (\<pi> j) = ipd (\<pi> k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma icd_pd_intermediate': assumes icd: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>  and j: \<open>k < j\<close> \<open>j < i\<close> shows \<open>\<pi> i pd\<rightarrow> (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
k < j
j < i

goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
proof (induction \<open>i - j\<close> arbitrary: \<open>j\<close> rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
case (less j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i - ?j1 < i - j; k < ?j1; ?j1 < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ?j1
k < j
j < i

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
have \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
using less.prems icd
[PROOF STATE]
proof (prove)
using this:
k < j
j < i
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
have \<open>is_path \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi>
[PROOF STEP]
using icd
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. is_path \<pi>
[PROOF STEP]
by (metis is_icdi_def)
[PROOF STATE]
proof (state)
this:
is_path \<pi>

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path \<pi>

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
have \<open>\<pi> i \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> i \<noteq> local.return
[PROOF STEP]
using icd
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
is_path \<pi>
\<pi> i \<noteq> local.return
[PROOF STEP]
have \<open>\<exists> l. j \<le> l \<and> l \<le> i \<and> \<pi> l = ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
is_path \<pi>
\<pi> i \<noteq> local.return

goal (1 subgoal):
 1. \<exists>l\<ge>j. l \<le> i \<and> \<pi> l = ipd (\<pi> j)
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
\<not> (is_path \<pi> \<and> j < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{j..i}. \<pi> j \<noteq> ipd (\<pi> j)))
is_path \<pi>
\<pi> i \<noteq> local.return

goal (1 subgoal):
 1. \<exists>l\<ge>j. l \<le> i \<and> \<pi> l = ipd (\<pi> j)
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
\<not> (is_path \<pi> \<and> j < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{j..i}. \<pi> j \<noteq> ipd (\<pi> j)))
is_path \<pi>
\<pi> i \<noteq> local.return
k < j
j < i

goal (1 subgoal):
 1. \<exists>l\<ge>j. l \<le> i \<and> \<pi> l = ipd (\<pi> j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>j. l \<le> i \<and> \<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<ge>j. l \<le> i \<and> \<pi> l = ipd (\<pi> j)
[PROOF STEP]
obtain l where l: \<open>j \<le> l\<close> \<open>l \<le> i\<close> \<open>\<pi> l = ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<ge>j. l \<le> i \<and> \<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>j \<le> l; l \<le> i; \<pi> l = ipd (\<pi> j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j \<le> l
l \<le> i
\<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
hence lpd: \<open>\<pi> l pd\<rightarrow> (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
j \<le> l
l \<le> i
\<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> j
[PROOF STEP]
by (metis is_ipd_def \<open>\<pi> i \<noteq> return\<close> \<open>is_path \<pi>\<close> ipd_is_ipd path_nodes term_path_stable)
[PROOF STATE]
proof (state)
this:
\<pi> l pd\<rightarrow> \<pi> j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<And>ja. \<lbrakk>i - ja < i - j; k < ja; ja < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ja; k < j; j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
 2. \<not> ?P \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
assume \<open>l = i\<close>
[PROOF STATE]
proof (state)
this:
l = i

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
 2. \<not> ?P \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
l = i

goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
using lpd
[PROOF STATE]
proof (prove)
using this:
l = i
\<pi> l pd\<rightarrow> \<pi> j

goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> i pd\<rightarrow> \<pi> j

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
assume \<open>l \<noteq> i\<close>
[PROOF STATE]
proof (state)
this:
l \<noteq> i

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
hence \<open>l < i\<close>
[PROOF STATE]
proof (prove)
using this:
l \<noteq> i

goal (1 subgoal):
 1. l < i
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
l \<noteq> i
j \<le> l
l \<le> i
\<pi> l = ipd (\<pi> j)

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

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l < i

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
have \<open>j \<noteq> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<noteq> l
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
j \<le> l
l \<le> i
\<pi> l = ipd (\<pi> j)

goal (1 subgoal):
 1. j \<noteq> l
[PROOF STEP]
by (metis is_ipd_def \<open>\<pi> i \<noteq> return\<close> \<open>is_path \<pi>\<close> ipd_is_ipd path_nodes term_path_stable)
[PROOF STATE]
proof (state)
this:
j \<noteq> l

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
hence \<open>j < l\<close>
[PROOF STATE]
proof (prove)
using this:
j \<noteq> l

goal (1 subgoal):
 1. j < l
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
j \<noteq> l
j \<le> l
l \<le> i
\<pi> l = ipd (\<pi> j)

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

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < l

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
hence \<open>i - l < i - j\<close>
[PROOF STATE]
proof (prove)
using this:
j < l

goal (1 subgoal):
 1. i - l < i - j
[PROOF STEP]
by (metis diff_less_mono2 less.prems(2))
[PROOF STATE]
proof (state)
this:
i - l < i - j

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i - l < i - j

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
have \<open>k < l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < l
[PROOF STEP]
by (metis l(1) less.prems(1) linorder_neqE_nat not_le order.strict_trans)
[PROOF STATE]
proof (state)
this:
k < l

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l < i
j < l
i - l < i - j
k < l
[PROOF STEP]
have \<open>\<pi> i pd\<rightarrow> (\<pi> l)\<close>
[PROOF STATE]
proof (prove)
using this:
l < i
j < l
i - l < i - j
k < l

goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> l
[PROOF STEP]
using less.hyps
[PROOF STATE]
proof (prove)
using this:
l < i
j < l
i - l < i - j
k < l
\<lbrakk>i - ?j1 < i - j; k < ?j1; ?j1 < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> ?j1

goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> i pd\<rightarrow> \<pi> l

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> i pd\<rightarrow> \<pi> l

goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
using lpd
[PROOF STATE]
proof (prove)
using this:
\<pi> i pd\<rightarrow> \<pi> l
\<pi> l pd\<rightarrow> \<pi> j

goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
by (metis pd_trans)
[PROOF STATE]
proof (state)
this:
\<pi> i pd\<rightarrow> \<pi> j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> i pd\<rightarrow> \<pi> j

goal:
No subgoals!
[PROOF STEP]
qed