[STATEMENT]
lemma icd_pd_intermediate: assumes icd: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>  and j: \<open>k < j\<close> \<open>j \<le> 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 assms icd_pd_intermediate'[OF assms(1,2)]
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
k < j
j \<le> i
j < i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j

goal (1 subgoal):
 1. \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
apply (cases \<open>j < i\<close>,metis)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k; k < j; j \<le> i; j < i \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j; \<not> j < i\<rbrakk> \<Longrightarrow> \<pi> i pd\<rightarrow> \<pi> j
[PROOF STEP]
by (metis is_icdi_def le_neq_trans path_nodes pd_refl)


[STATEMENT]
lemma no_icd_pd: assumes path: \<open>is_path \<pi>\<close> and noicd: \<open>\<forall> l\<ge>n. \<not> k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> and nk: \<open>n \<le> k\<close> shows \<open>\<pi> k pd\<rightarrow> \<pi> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
 2. \<not> ?P \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
assume \<open>\<pi> k = return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> k = local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
 2. \<not> ?P \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> k = local.return

goal (1 subgoal):
 1. \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
by (metis path path_nodes return_pd)
[PROOF STATE]
proof (state)
this:
\<pi> k pd\<rightarrow> \<pi> n

goal (1 subgoal):
 1. \<pi> k \<noteq> local.return \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> k \<noteq> local.return \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
assume nret: \<open>\<pi> k \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> k \<noteq> local.return

goal (1 subgoal):
 1. \<pi> k \<noteq> local.return \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
have nocd: \<open>\<And> l. n\<le>l \<Longrightarrow> \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. n \<le> l \<Longrightarrow> \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume kcd: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> and nl: \<open>n \<le> l\<close>
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
n \<le> l

goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>(k - n) cd\<^bsup>\<pi>\<guillemotleft>n\<^esup>\<rightarrow> (l - n)\<close>
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
n \<le> l

goal (1 subgoal):
 1. k - n cd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l - n
[PROOF STEP]
using cd_path_shift[OF nl path]
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
n \<le> l
(?i cd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = (?i - n cd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l - n)

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

goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<exists> l. (k - n) icd\<^bsup>\<pi>\<guillemotleft>n\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (prove)
using this:
k - n cd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l - n

goal (1 subgoal):
 1. \<exists>l. k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l
[PROOF STEP]
using excd_impl_exicd
[PROOF STATE]
proof (prove)
using this:
k - n cd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l - n
\<exists>k. ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> \<exists>k. ?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l
[PROOF STEP]
obtain l' where "k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l'"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. (\<And>l'. k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (l' + n)\<close>
[PROOF STATE]
proof (prove)
using this:
k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l' + n
[PROOF STEP]
using icd_path_shift[of \<open>n\<close> \<open>l' + n\<close> \<open>\<pi>\<close> \<open>k\<close>] path
[PROOF STATE]
proof (prove)
using this:
k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l'
\<lbrakk>n \<le> l' + n; is_path \<pi>\<rbrakk> \<Longrightarrow> (k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l' + n) = (k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l' + n - n)
is_path \<pi>

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

goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l' + n

goal (1 subgoal):
 1. False
[PROOF STEP]
using noicd
[PROOF STATE]
proof (prove)
using this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l' + n
\<forall>l\<ge>n. \<not> k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l

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:
n \<le> ?l1 \<Longrightarrow> \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?l1

goal (1 subgoal):
 1. \<pi> k \<noteq> local.return \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
hence \<open>\<And>l. n \<le> l \<Longrightarrow> l<k \<Longrightarrow> \<exists> j \<in> {l..k}. \<pi> j = ipd (\<pi> l)\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> ?l1 \<Longrightarrow> \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?l1

goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l)
[PROOF STEP]
using path nret
[PROOF STATE]
proof (prove)
using this:
n \<le> ?l1 \<Longrightarrow> \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?l1
is_path \<pi>
\<pi> k \<noteq> local.return

goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l)
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
n \<le> ?l1 \<Longrightarrow> \<not> (is_path \<pi> \<and> ?l1 < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{?l1..k}. \<pi> j \<noteq> ipd (\<pi> ?l1)))
is_path \<pi>
\<pi> k \<noteq> local.return

goal (1 subgoal):
 1. \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)

goal (1 subgoal):
 1. \<pi> k \<noteq> local.return \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)

goal (1 subgoal):
 1. \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
using nk
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)
n \<le> k

goal (1 subgoal):
 1. \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
proof (induction \<open>k - n\<close> arbitrary: \<open>n\<close> rule: less_induct,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; ?P5 na\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
 2. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; \<not> ?P5 na\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
case (less n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k - ?n1 < k - n; \<And>l. \<lbrakk>?n1 \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); ?n1 \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> ?n1
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)
n \<le> k

goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; ?P5 na\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
 2. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; \<not> ?P5 na\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
assume \<open>n = k\<close>
[PROOF STATE]
proof (state)
this:
n = k

goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; ?P5 na\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
 2. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; \<not> ?P5 na\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
n = k

goal (1 subgoal):
 1. \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
using pd_refl path path_nodes
[PROOF STATE]
proof (prove)
using this:
n = k
?x \<in> local.nodes \<Longrightarrow> ?x pd\<rightarrow> ?x
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes

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

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; na \<noteq> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; na \<noteq> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
case (less n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k - ?n1 < k - n; \<And>l. \<lbrakk>?n1 \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); ?n1 \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> ?n1
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)
n \<le> k

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; na \<noteq> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
assume \<open>n \<noteq> k\<close>
[PROOF STATE]
proof (state)
this:
n \<noteq> k

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; na \<noteq> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
hence nk: \<open>n < k\<close>
[PROOF STATE]
proof (prove)
using this:
n \<noteq> k

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

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

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; na \<noteq> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
with less(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)
n < k
[PROOF STEP]
obtain j where jnk: \<open>j \<in> {n..k}\<close> and ipdj: \<open>\<pi> j = ipd (\<pi> n)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)
n < k

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<in> {n..k}; \<pi> j = ipd (\<pi> n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j \<in> {n..k}
\<pi> j = ipd (\<pi> n)

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; na \<noteq> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
have nretn: \<open>\<pi> n \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> n \<noteq> local.return
[PROOF STEP]
using nk nret term_path_stable path
[PROOF STATE]
proof (prove)
using this:
n < k
\<pi> k \<noteq> local.return
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?\<pi> ?j = local.return
is_path \<pi>

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

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; na \<noteq> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
with ipd_is_ipd path path_nodes is_ipd_def ipdj
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> local.nodes; ?x \<noteq> local.return\<rbrakk> \<Longrightarrow> ipd ?x ipd\<rightarrow> ?x
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes
(?y ipd\<rightarrow> ?x) = (?x \<noteq> ?y \<and> ?y pd\<rightarrow> ?x \<and> (\<forall>z. z \<noteq> ?x \<and> z pd\<rightarrow> ?x \<longrightarrow> z pd\<rightarrow> ?y))
\<pi> j = ipd (\<pi> n)
\<pi> n \<noteq> local.return
[PROOF STEP]
have jpdn: \<open>\<pi> j pd\<rightarrow> \<pi> n\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> local.nodes; ?x \<noteq> local.return\<rbrakk> \<Longrightarrow> ipd ?x ipd\<rightarrow> ?x
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes
(?y ipd\<rightarrow> ?x) = (?x \<noteq> ?y \<and> ?y pd\<rightarrow> ?x \<and> (\<forall>z. z \<noteq> ?x \<and> z pd\<rightarrow> ?x \<longrightarrow> z pd\<rightarrow> ?y))
\<pi> j = ipd (\<pi> n)
\<pi> n \<noteq> local.return

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

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>n. \<lbrakk>k - n < k - na; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n; \<And>l. \<lbrakk>na \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); na \<le> k; \<And>l. \<lbrakk>n \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); n \<le> k; na \<noteq> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> na
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
 2. \<not> ?P \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
assume \<open>j = k\<close>
[PROOF STATE]
proof (state)
this:
j = k

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

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

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

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

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

goal (1 subgoal):
 1. j < k
[PROOF STEP]
using jnk
[PROOF STATE]
proof (prove)
using this:
j \<noteq> k
j \<in> {n..k}

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

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

goal (1 subgoal):
 1. j \<noteq> n
[PROOF STEP]
by (metis ipd_not_self nretn path path_nodes)
[PROOF STATE]
proof (state)
this:
j \<noteq> n

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

goal (1 subgoal):
 1. n < j
[PROOF STEP]
using jnk
[PROOF STATE]
proof (prove)
using this:
j \<noteq> n
j \<in> {n..k}

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

goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
have *: \<open>k - j < k - n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k - j < k - n
[PROOF STEP]
using jk nj
[PROOF STATE]
proof (prove)
using this:
j < k
n < j

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

goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
with less(1)[OF *] less(2) jk nj
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>l. \<lbrakk>j \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); j \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> j
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)
j < k
n < j
k - j < k - n
[PROOF STEP]
have \<open>\<pi> k pd\<rightarrow> \<pi> j\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>l. \<lbrakk>j \<le> l; l < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{l..k}. \<pi> j = ipd (\<pi> l); j \<le> k\<rbrakk> \<Longrightarrow> \<pi> k pd\<rightarrow> \<pi> j
\<lbrakk>n \<le> ?l1; ?l1 < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{?l1..k}. \<pi> j = ipd (\<pi> ?l1)
j < k
n < j
k - j < k - n

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

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

goal (1 subgoal):
 1. \<pi> k pd\<rightarrow> \<pi> n
[PROOF STEP]
using jpdn pd_trans
[PROOF STATE]
proof (prove)
using this:
\<pi> k pd\<rightarrow> \<pi> j
\<pi> j pd\<rightarrow> \<pi> n
\<lbrakk>?y pd\<rightarrow> ?x; ?z pd\<rightarrow> ?y\<rbrakk> \<Longrightarrow> ?z pd\<rightarrow> ?x

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma first_pd_no_cd: assumes path: \<open>is_path \<pi>\<close> and pd: \<open>\<pi> n pd\<rightarrow> \<pi> 0\<close> and first: \<open>\<forall> l < n. \<pi> l \<noteq> \<pi> n\<close> shows \<open>\<forall> l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
[PROOF STEP]
proof (rule ccontr, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l) \<Longrightarrow> False
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (1 subgoal):
 1. \<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
[PROOF STEP]
obtain l where ncdl: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (1 subgoal):
 1. (\<And>l. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l

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

goal (1 subgoal):
 1. l < n
[PROOF STEP]
using is_cdi_def
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
(?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 < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < n

goal (1 subgoal):
 1. \<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l) \<Longrightarrow> False
[PROOF STEP]
have \<open>\<not> \<pi> n pd\<rightarrow> \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<pi> n pd\<rightarrow> \<pi> l
[PROOF STEP]
using ncdl cd_not_pd
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l
\<lbrakk>?l cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; ?\<pi> ?l \<noteq> ?\<pi> ?k\<rbrakk> \<Longrightarrow> \<not> ?\<pi> ?l pd\<rightarrow> ?\<pi> ?k

goal (1 subgoal):
 1. \<not> \<pi> n pd\<rightarrow> \<pi> l
[PROOF STEP]
by (metis ln first)
[PROOF STATE]
proof (state)
this:
\<not> \<pi> n pd\<rightarrow> \<pi> l

goal (1 subgoal):
 1. \<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<pi> n pd\<rightarrow> \<pi> l
[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 not\<pi>n: \<open>\<forall> j\<le> n'. \<pi>' j \<noteq> \<pi> n\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> \<pi> n pd\<rightarrow> \<pi> l

goal (1 subgoal):
 1. (\<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> l; \<pi>' n' = local.return; \<forall>j\<le>n'. \<pi>' j \<noteq> \<pi> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<pi> l \<in> local.nodes \<and> (\<forall>\<pi>' na. is_path \<pi>' \<and> \<pi>' 0 = \<pi> l \<and> \<pi>' na = local.return \<longrightarrow> (\<exists>k\<le>na. \<pi>' k = \<pi> n)))

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l) \<Longrightarrow> False
[PROOF STEP]
have \<open>?\<pi> 0 = \<pi> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0

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

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

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

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

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<le> n' + l; (\<pi> @\<^bsup>l\<^esup> \<pi>') j = \<pi> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pd
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')
(\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0
(\<pi> @\<^bsup>l\<^esup> \<pi>') (n' + l) = local.return
\<pi> n pd\<rightarrow> \<pi> 0

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

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

goal (1 subgoal):
 1. \<not> (\<forall>l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l) \<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>j \<le> l\<close>
[PROOF STATE]
proof (state)
this:
j \<le> l

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
j \<le> l

goal (1 subgoal):
 1. False
[PROOF STEP]
using jn first ln
[PROOF STATE]
proof (prove)
using this:
j \<le> l
(\<pi> @\<^bsup>l\<^esup> \<pi>') j = \<pi> n
\<forall>l<n. \<pi> l \<noteq> \<pi> n
l < n

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

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

goal (1 subgoal):
 1. \<not> j \<le> l \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> j \<le> l

goal (1 subgoal):
 1. False
[PROOF STEP]
using j jn not\<pi>n
[PROOF STATE]
proof (prove)
using this:
\<not> j \<le> l
j \<le> n' + l
(\<pi> @\<^bsup>l\<^esup> \<pi>') j = \<pi> n
\<forall>j\<le>n'. \<pi>' j \<noteq> \<pi> n

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


[STATEMENT]
lemma first_pd_no_icd: assumes path: \<open>is_path \<pi>\<close> and pd: \<open>\<pi> n pd\<rightarrow> \<pi> 0\<close> and first: \<open>\<forall> l < n. \<pi> l \<noteq> \<pi> n\<close> shows \<open>\<forall> l. \<not> n icd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l. \<not> n icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
[PROOF STEP]
by (metis first first_pd_no_cd icd_imp_cd path pd)


[STATEMENT]
lemma path_nret_ex_nipd: assumes \<open>is_path \<pi>\<close> \<open>\<forall> i. \<pi> i \<noteq> return\<close> shows \<open>\<forall> i. (\<exists> j\<ge>i. (\<forall> k>j. \<pi> k \<noteq> ipd (\<pi> j)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)
[PROOF STEP]
proof(rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)) \<Longrightarrow> False
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> (\<exists>j\<ge>i. \<forall> k>j. \<pi> k \<noteq> ipd (\<pi> j))\<close>
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j))

goal (1 subgoal):
 1. \<And>i. \<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)) \<Longrightarrow> False
[PROOF STEP]
hence *: \<open>\<forall> j\<ge>i. (\<exists>k>j. \<pi> k = ipd (\<pi> j))\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j))

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

goal (1 subgoal):
 1. \<And>i. \<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)) \<Longrightarrow> False
[PROOF STEP]
have \<open>\<forall> j. (\<exists>k>j. (\<pi>\<guillemotleft>i) k = ipd ((\<pi>\<guillemotleft>i) j))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
[PROOF STEP]
have \<open>i + j \<ge> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> i + j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<le> i + j

goal (1 subgoal):
 1. \<And>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> i + j
[PROOF STEP]
obtain k where k: \<open>k>i+j\<close> \<open>\<pi> k = ipd (\<pi> (i+j))\<close>
[PROOF STATE]
proof (prove)
using this:
i \<le> i + j

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>i + j < k; \<pi> k = ipd (\<pi> (i + j))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i \<le> i + j
\<forall>j\<ge>i. \<exists>k>j. \<pi> k = ipd (\<pi> j)

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

goal (1 subgoal):
 1. \<And>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
[PROOF STEP]
hence \<open>(\<pi>\<guillemotleft>i) (k - i) = ipd ((\<pi>\<guillemotleft>i) j)\<close>
[PROOF STATE]
proof (prove)
using this:
i + j < k
\<pi> k = ipd (\<pi> (i + j))

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

goal (1 subgoal):
 1. \<And>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> i) (k - i) = ipd ((\<pi> \<guillemotleft> i) j)

goal (1 subgoal):
 1. \<And>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
[PROOF STEP]
have \<open>k - i > j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < k - i
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
i + j < k
\<pi> k = ipd (\<pi> (i + j))

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

goal (1 subgoal):
 1. \<And>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> i) (k - i) = ipd ((\<pi> \<guillemotleft> i) j)
j < k - i
[PROOF STEP]
show \<open>\<exists>k>j. (\<pi>\<guillemotleft>i) k = ipd ((\<pi>\<guillemotleft>i) j)\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> i) (k - i) = ipd ((\<pi> \<guillemotleft> i) j)
j < k - i

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)

goal (1 subgoal):
 1. \<And>i. \<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)

goal (1 subgoal):
 1. \<And>i. \<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)) \<Longrightarrow> False
[PROOF STEP]
have \<open>is_path (\<pi>\<guillemotleft>i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> i)
[PROOF STEP]
using assms(1) path_path_shift
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)

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

goal (1 subgoal):
 1. \<And>i. \<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
is_path (\<pi> \<guillemotleft> i)
[PROOF STEP]
obtain k where \<open>(\<pi>\<guillemotleft>i) k = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
is_path (\<pi> \<guillemotleft> i)

goal (1 subgoal):
 1. (\<And>k. (\<pi> \<guillemotleft> i) k = local.return \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using all_ipd_imp_ret
[PROOF STATE]
proof (prove)
using this:
\<forall>j. \<exists>k>j. (\<pi> \<guillemotleft> i) k = ipd ((\<pi> \<guillemotleft> i) j)
is_path (\<pi> \<guillemotleft> i)
\<lbrakk>is_path ?\<pi>; \<forall>i. ?\<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. ?\<pi> j = ipd (?\<pi> i))\<rbrakk> \<Longrightarrow> \<exists>j. ?\<pi> j = local.return

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

goal (1 subgoal):
 1. \<And>i. \<not> (\<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)) \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> i) k = local.return

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> i) k = local.return
\<forall>i. \<pi> i \<noteq> local.return

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_nret_ex_all_cd: assumes \<open>is_path \<pi>\<close> \<open>\<forall> i. \<pi> i \<noteq> return\<close> shows \<open>\<forall> i. (\<exists> j\<ge>i. (\<forall> k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<exists>j\<ge>i. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<exists>j\<ge>i. \<forall>k>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))
[PROOF STEP]
using assms path_nret_ex_nipd[OF assms]
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<forall>i. \<pi> i \<noteq> local.return
\<forall>i. \<exists>j\<ge>i. \<forall>k>j. \<pi> k \<noteq> ipd (\<pi> j)

goal (1 subgoal):
 1. \<forall>i. \<exists>j\<ge>i. \<forall>k>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))
[PROOF STEP]
by (metis atLeastAtMost_iff ipd_not_self linorder_neqE_nat not_le path_nodes)


[STATEMENT]
lemma path_nret_inf_all_cd: assumes \<open>is_path \<pi>\<close> \<open>\<forall> i. \<pi> i \<noteq> return\<close> shows \<open>\<not> finite {j. \<forall> k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}
[PROOF STEP]
using unbounded_nat_set_infinite path_nret_ex_all_cd[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>j\<ge>i. j \<in> ?A \<Longrightarrow> infinite ?A
\<forall>i. \<exists>j\<ge>i. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. infinite {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}
[PROOF STEP]
by auto


[STATEMENT]
lemma path_nret_inf_icd_seq: assumes path: \<open>is_path \<pi>\<close> and nret: \<open>\<forall> i. \<pi> i \<noteq> return\<close>
obtains f where \<open>\<forall> i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i\<close> \<open>range f = {i. \<forall> j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}\<close> \<open>\<not> (\<exists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note path_nret_inf_all_cd[OF assms]
[PROOF STATE]
proof (state)
this:
infinite {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}
[PROOF STEP]
obtain f where ran: \<open>range f = {j. \<forall> k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}\<close> and asc: \<open>\<forall> i. f i < f (Suc i)\<close>
[PROOF STATE]
proof (prove)
using this:
infinite {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infinite_ascending
[PROOF STATE]
proof (prove)
using this:
infinite {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}
\<lbrakk>infinite ?A; \<And>f. \<lbrakk>range f = ?A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have mono: \<open>\<forall> i j. i < j \<longrightarrow> f i < f j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i < j \<longrightarrow> f i < f j
[PROOF STEP]
using asc
[PROOF STATE]
proof (prove)
using this:
\<forall>i. f i < f (Suc i)

goal (1 subgoal):
 1. \<forall>i j. i < j \<longrightarrow> f i < f j
[PROOF STEP]
by (metis lift_Suc_mono_less)
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < j \<longrightarrow> f i < f j

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

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have cd: \<open>f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> f i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> f i
[PROOF STEP]
using ran asc
[PROOF STATE]
proof (prove)
using this:
range f = {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}
\<forall>i. f i < f (Suc i)

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

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i\<close>
[PROOF STATE]
proof (state)
this:
\<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i

goal (1 subgoal):
 1. \<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i
[PROOF STEP]
obtain m where  im: \<open>f i < m\<close> and mi: \<open> m < f (Suc i)\<close> and cdm: \<open>f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i

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

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>f i < m; m < f (Suc i); f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) cd
[PROOF STATE]
proof (prove)
using this:
\<not> (is_path \<pi> \<and> f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> f i \<and> (\<forall>m\<in>{f i<..<f (Suc i)}. \<not> f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> m))
is_path \<pi>
f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> f i

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

goal (1 subgoal):
 1. \<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i \<Longrightarrow> False
[PROOF STEP]
have \<open>\<forall> k>m. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k>m. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
proof (rule,rule,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>m < k; ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>k. \<lbrakk>m < k; \<not> ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>m < k; ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>k. \<lbrakk>m < k; \<not> ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
assume \<open>f (Suc i) < k\<close>
[PROOF STATE]
proof (state)
this:
f (Suc i) < k

goal (2 subgoals):
 1. \<And>k. \<lbrakk>m < k; ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>k. \<lbrakk>m < k; \<not> ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
hence \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> f (Suc i)\<close>
[PROOF STATE]
proof (prove)
using this:
f (Suc i) < k

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

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

goal (2 subgoals):
 1. \<And>k. \<lbrakk>m < k; ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>k. \<lbrakk>m < k; \<not> ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> f (Suc i)

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using cdm cd_trans
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> f (Suc i)
f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
\<lbrakk>?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i; ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j\<rbrakk> \<Longrightarrow> ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i

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

goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f (Suc i) < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f (Suc i) < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f (Suc i) < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
assume mk: \<open>m < k\<close> and \<open>\<not> f (Suc i) < k\<close>
[PROOF STATE]
proof (state)
this:
m < k
\<not> f (Suc i) < k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f (Suc i) < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
hence ik: \<open>k \<le> f (Suc i)\<close>
[PROOF STATE]
proof (prove)
using this:
m < k
\<not> f (Suc i) < k

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

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

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using cdm
[PROOF STATE]
proof (prove)
using this:
k \<le> f (Suc i)
f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

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

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

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

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

goal (1 subgoal):
 1. \<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> range f
[PROOF STEP]
obtain j where m: \<open>m = f j\<close>
[PROOF STATE]
proof (prove)
using this:
m \<in> range f

goal (1 subgoal):
 1. (\<And>j. m = f j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m = f j

goal (1 subgoal):
 1. \<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using im mi mono
[PROOF STATE]
proof (prove)
using this:
f i < m
m < f (Suc i)
\<forall>i j. i < j \<longrightarrow> f i < f j

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding m
[PROOF STATE]
proof (prove)
using this:
f i < f j
f j < f (Suc i)
\<forall>i j. i < j \<longrightarrow> f i < f j

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis Suc_lessI le_less not_le)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i

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

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

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

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

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<forall> k>m. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k>m. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
proof (rule,rule,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>m < k; ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>k. \<lbrakk>m < k; \<not> ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>m < k; ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>k. \<lbrakk>m < k; \<not> ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
assume \<open>f 0 < k\<close>
[PROOF STATE]
proof (state)
this:
f 0 < k

goal (2 subgoals):
 1. \<And>k. \<lbrakk>m < k; ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>k. \<lbrakk>m < k; \<not> ?P4 k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
hence \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> f 0\<close>
[PROOF STATE]
proof (prove)
using this:
f 0 < k

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

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

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

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using cdm cd_trans
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> f 0
f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
\<lbrakk>?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i; ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j\<rbrakk> \<Longrightarrow> ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i

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

goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f 0 < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f 0 < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f 0 < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
assume mk: \<open>m < k\<close> and \<open>\<not> f 0 < k\<close>
[PROOF STATE]
proof (state)
this:
m < k
\<not> f 0 < k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f 0 < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
hence ik: \<open>k \<le> f 0\<close>
[PROOF STATE]
proof (prove)
using this:
m < k
\<not> f 0 < k

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

goal (1 subgoal):
 1. \<And>k. \<lbrakk>m < k; \<not> f 0 < k\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
k \<le> f 0

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using cdm
[PROOF STATE]
proof (prove)
using this:
k \<le> f 0
f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

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

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>m \<in> range f\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>k>m. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

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

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> range f
[PROOF STEP]
obtain j where m: \<open>m = f j\<close>
[PROOF STATE]
proof (prove)
using this:
m \<in> range f

goal (1 subgoal):
 1. (\<And>j. m = f j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m = f j

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence fj0: \<open>f j < f 0\<close>
[PROOF STATE]
proof (prove)
using this:
m = f j

goal (1 subgoal):
 1. f j < f 0
[PROOF STEP]
using cdm m is_cdi_def
[PROOF STATE]
proof (prove)
using this:
m = f j
f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
m = f 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. f j < f 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f j < f 0

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

goal (1 subgoal):
 1. 0 < j
[PROOF STEP]
by (metis less_irrefl neq0_conv)
[PROOF STATE]
proof (state)
this:
0 < j

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using fj0 mono
[PROOF STATE]
proof (prove)
using this:
0 < j
f j < f 0
\<forall>i j. i < j \<longrightarrow> f i < f j

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

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

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<forall>i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i; range f = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (Suc ?i3) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f ?i3
f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m3 \<Longrightarrow> False
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
f (Suc ?i3) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f ?i3
f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m3 \<Longrightarrow> False

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that ran
[PROOF STATE]
proof (prove)
using this:
f (Suc ?i3) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f ?i3
f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m3 \<Longrightarrow> False
\<lbrakk>\<forall>i. ?f1 (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?f1 i; range ?f1 = {i. \<forall>j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}; \<nexists>i. ?f1 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> thesis
range f = {j. \<forall>k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cdi_iff_no_strict_pd: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longleftrightarrow> is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> return \<and> (\<forall> j \<in> {k..i}. \<not> (\<pi> k, \<pi> j) \<in> pdt)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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> k, \<pi> j) \<notin> pdt))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)
 2. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
assume cd:\<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (state)
this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)
 2. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have 1: \<open>is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return
[PROOF STEP]
using cd
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
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> \<and> k < i \<and> \<pi> i \<noteq> local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)
 2. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have 2: \<open>\<forall> j \<in> {k..i}. \<not> (\<pi> k, \<pi> j) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> False
[PROOF STEP]
assume \<open> \<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)\<close>
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)

goal (1 subgoal):
 1. \<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)
[PROOF STEP]
obtain j where \<open>j \<in> {k..i}\<close> and \<open>(\<pi> k, \<pi> j) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<in> {k..i}; (\<pi> k, \<pi> j) \<in> pdt\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<in> {k..i}
(\<pi> k, \<pi> j) \<in> pdt

goal (1 subgoal):
 1. \<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<pi> j \<noteq> \<pi> k\<close> and \<open>\<pi> j pd\<rightarrow> \<pi> k\<close>
[PROOF STATE]
proof (prove)
using this:
j \<in> {k..i}
(\<pi> k, \<pi> j) \<in> pdt

goal (1 subgoal):
 1. \<pi> j \<noteq> \<pi> k &&& \<pi> j pd\<rightarrow> \<pi> k
[PROOF STEP]
unfolding pdt_def
[PROOF STATE]
proof (prove)
using this:
j \<in> {k..i}
(\<pi> k, \<pi> j) \<in> {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}

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

goal (1 subgoal):
 1. \<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> j \<noteq> \<pi> k
\<pi> j pd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. False
[PROOF STEP]
using path_pd_ipd
[PROOF STATE]
proof (prove)
using this:
\<pi> j \<noteq> \<pi> k
\<pi> j pd\<rightarrow> \<pi> k
\<lbrakk>is_path ?\<pi>; ?\<pi> ?k \<noteq> local.return; ?\<pi> ?n \<noteq> ?\<pi> ?k; ?\<pi> ?n pd\<rightarrow> ?\<pi> ?k; ?k < ?n; \<And>l. \<lbrakk>?k < l; l \<le> ?n; ?\<pi> l = ipd (?\<pi> ?k)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis \<open>j \<in> {k..i}\<close> atLeastAtMost_iff cd cd_not_pd cdi_prefix le_eq_less_or_eq)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)
 2. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
show \<open>is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> return \<and> (\<forall> j \<in> {k..i}. \<not> (\<pi> k, \<pi> j) \<in> pdt)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return
\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt

goal (1 subgoal):
 1. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)

goal (1 subgoal):
 1. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
assume \<open>is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> return \<and> (\<forall> j \<in> {k..i}. \<not> (\<pi> k, \<pi> j) \<in> pdt)\<close>
[PROOF STATE]
proof (state)
this:
is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)

goal (1 subgoal):
 1. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt) \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
thus \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis ipd_in_pdt term_path_stable less_or_eq_imp_le not_cd_impl_ipd path_nodes)
[PROOF STATE]
proof (state)
this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma last_cs: \<open>last (cs\<^bsup>\<pi>\<^esup> i) = \<pi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (cs\<^bsup>\<pi>\<^esup> i) = \<pi> i
[PROOF STEP]
by auto


[STATEMENT]
lemma cs_not_nil: \<open>cs\<^bsup>\<pi>\<^esup> n \<noteq> []\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n \<noteq> []
[PROOF STEP]
by (auto)


[STATEMENT]
lemma cs_return: assumes \<open>\<pi> n = return\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> n = [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = [\<pi> n]
[PROOF STEP]
by (metis assms cs.elims icd_imp_cd ret_no_cd)


[STATEMENT]
lemma cs_0[simp]: \<open>cs\<^bsup>\<pi>\<^esup> 0 = [\<pi> 0]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> 0 = [\<pi> 0]
[PROOF STEP]
using is_icdi_def is_cdi_def
[PROOF STATE]
proof (prove)
using this:
(?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. cs\<^bsup>\<pi>\<^esup> 0 = [\<pi> 0]
[PROOF STEP]
by auto