[STATEMENT]
lemma converged_ipd_same_icd: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and  converge: \<open>l < m\<close> \<open>cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<close>
and csk: \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close> and icd: \<open>l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and suc: \<open>\<pi> (Suc k) = \<pi>' (Suc k')\<close>
and ipd: \<open>\<pi>' m' = ipd (\<pi> k)\<close> \<open>\<forall> n \<in> {k'..<m'}. \<pi>' n \<noteq> ipd (\<pi> k)\<close>
shows \<open>\<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
assume l: \<open>l = Suc k\<close>
[PROOF STATE]
proof (state)
this:
l = Suc k

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence \<open>\<pi> (Suc k) \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
Suc k cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence \<open>\<pi>' (Suc k') \<noteq> ipd (\<pi>' k')\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc k) \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. \<pi>' (Suc k') \<noteq> ipd (\<pi>' k')
[PROOF STEP]
by (metis csk last_cs suc)
[PROOF STATE]
proof (state)
this:
\<pi>' (Suc k') \<noteq> ipd (\<pi>' k')

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>' (Suc k') \<noteq> ipd (\<pi>' k')

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>\<pi>' (Suc k') \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (Suc k') \<noteq> local.return
[PROOF STEP]
by (metis \<open>Suc k cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> ret_no_cd suc)
[PROOF STATE]
proof (state)
this:
\<pi>' (Suc k') \<noteq> local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi>' (Suc k') \<noteq> ipd (\<pi>' k')
\<pi>' (Suc k') \<noteq> local.return
[PROOF STEP]
have \<open>Suc k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (Suc k') \<noteq> ipd (\<pi>' k')
\<pi>' (Suc k') \<noteq> local.return

goal (1 subgoal):
 1. Suc k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
\<pi>' (Suc k') \<noteq> ipd (\<pi>' k')
\<pi>' (Suc k') \<noteq> local.return

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

goal (1 subgoal):
 1. is_path \<pi>' \<and> k' < Suc k' \<and> \<pi>' (Suc k') \<noteq> local.return \<and> (\<forall>j\<in>{k'..Suc k'}. \<pi>' j \<noteq> ipd (\<pi>' k'))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<pi>' (Suc k') \<noteq> ipd (\<pi>' k'); \<pi>' (Suc k') \<noteq> local.return; is_path \<pi>'; \<pi>' j = ipd (\<pi>' k'); k' \<le> j; j \<le> Suc k'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis ipd_not_self le_Suc_eq le_antisym path_nodes term_path_stable)
[PROOF STATE]
proof (state)
this:
Suc k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

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

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

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

goal (1 subgoal):
 1. is_path \<pi>' \<and> Suc k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<and> (\<forall>m\<in>{k'<..<Suc k'}. \<not> Suc k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Suc k' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> Suc k' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' (Suc k')]
[PROOF STEP]
using icd_cs
[PROOF STATE]
proof (prove)
using this:
Suc k' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
?l icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?l = cs\<^bsup>?\<pi>\<^esup> ?k @ [?\<pi> ?l]

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> Suc k' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' (Suc k')]

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<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]
using icd icd_cs
[PROOF STATE]
proof (prove)
using this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
?l icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?l = cs\<^bsup>?\<pi>\<^esup> ?k @ [?\<pi> ?l]

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 (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>'\<^esup> Suc k' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' (Suc k')]
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> l]
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> (Suc k')\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> Suc k' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' (Suc k')]
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> l]

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<not> ?P \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> Suc k'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
assume nsuck: \<open>l \<noteq> Suc k\<close>
[PROOF STATE]
proof (state)
this:
l \<noteq> Suc k

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have kk'[simp]: \<open>\<pi>' k' = \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' k' = \<pi> k
[PROOF STEP]
by (metis csk last_cs)
[PROOF STATE]
proof (state)
this:
\<pi>' k' = \<pi> k

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have kl: \<open>k < l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < l
[PROOF STEP]
using icd
[PROOF STATE]
proof (prove)
using this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence skl: \<open>Suc k < l\<close>
[PROOF STATE]
proof (prove)
using this:
k < l

goal (1 subgoal):
 1. Suc k < l
[PROOF STEP]
by (metis Suc_lessI nsuck)
[PROOF STATE]
proof (state)
this:
Suc k < l

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence lpd: \<open>\<pi> l pd\<rightarrow> \<pi> (Suc k)\<close>
[PROOF STATE]
proof (prove)
using this:
Suc k < l

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> (Suc k)
[PROOF STEP]
using icd icd_pd_intermediate
[PROOF STATE]
proof (prove)
using this:
Suc k < l
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; ?k < ?j; ?j \<le> ?i\<rbrakk> \<Longrightarrow> ?\<pi> ?i pd\<rightarrow> ?\<pi> ?j

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have km: \<open>k < m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < m
[PROOF STEP]
by (metis converge(1) kl order.strict_trans)
[PROOF STATE]
proof (state)
this:
k < m

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have lcd: \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using icd is_icdi_def
[PROOF STATE]
proof (prove)
using this:
l icd\<^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. l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence ipdk_pdl: \<open>ipd (\<pi> k) pd\<rightarrow> (\<pi> l)\<close>
[PROOF STATE]
proof (prove)
using this:
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have *: \<open>ipd (\<pi> k) \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> k) \<in> local.nodes
[PROOF STEP]
by (metis ipdk_pdl pd_node1)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> k) \<in> local.nodes

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have nretk: \<open>\<pi> k \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k \<noteq> local.return
[PROOF STEP]
by (metis kl lcd path(1) ret_no_cd term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
\<pi> k \<noteq> local.return

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have **: \<open>\<not> (\<pi> l) pd\<rightarrow> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<pi> l pd\<rightarrow> ipd (\<pi> k)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> ipd (\<pi> k) \<Longrightarrow> False
[PROOF STEP]
assume a: \<open>\<pi> l pd\<rightarrow> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (state)
this:
\<pi> l pd\<rightarrow> ipd (\<pi> k)

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

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi> k
[PROOF STEP]
by (metis is_ipd_def \<open>k < l\<close> ipd_is_ipd ipdk_pdl path(1) path_nodes pd_antisym term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
\<pi> l pd\<rightarrow> \<pi> k

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

goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> ipd (\<pi> k) \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> l \<noteq> (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> l \<noteq> \<pi> k
[PROOF STEP]
by (metis "*" a ipd_not_self ipdk_pdl lcd pd_antisym ret_no_cd)
[PROOF STATE]
proof (state)
this:
\<pi> l \<noteq> \<pi> k

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using lcd cd_not_pd
[PROOF STATE]
proof (prove)
using this:
\<pi> l pd\<rightarrow> \<pi> k
\<pi> l \<noteq> \<pi> k
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<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. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have km': \<open>k' < m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < m'
[PROOF STEP]
using cs_order[OF path csk converge(2) nretk km]
[PROOF STATE]
proof (prove)
using this:
k' < m'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
obtain \<pi>'' n'' where path'': \<open>is_path \<pi>''\<close>  and \<pi>''0: \<open>\<pi>'' 0 = ipd (\<pi> k)\<close> and \<pi>''n: \<open>\<pi>'' n'' = return\<close> and not\<pi>l: \<open>\<forall> i\<le>n''. \<pi>'' i \<noteq> \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>'' n''. \<lbrakk>is_path \<pi>''; \<pi>'' 0 = ipd (\<pi> k); \<pi>'' n'' = local.return; \<forall>i\<le>n''. \<pi>'' i \<noteq> \<pi> l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using no_pd_path[OF * **]
[PROOF STATE]
proof (prove)
using this:
(\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi>' 0 = ipd (\<pi> k); \<pi>' n = local.return; \<forall>k\<le>n. \<pi>' k \<noteq> \<pi> l\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
let \<open>?\<pi>'\<close> = \<open>(\<pi>' @\<^bsup>m'\<^esup> \<pi>'') \<guillemotleft> Suc k'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>is_path ?\<pi>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi>' @\<^bsup>m'\<^esup> \<pi>'' \<guillemotleft> Suc k')
[PROOF STEP]
by (metis \<pi>''0 ipd(1) path'' path(2) path_cons path_path_shift)
[PROOF STATE]
proof (state)
this:
is_path (\<pi>' @\<^bsup>m'\<^esup> \<pi>'' \<guillemotleft> Suc k')

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi>' @\<^bsup>m'\<^esup> \<pi>'' \<guillemotleft> Suc k')

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>?\<pi>' 0 = \<pi> (Suc k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>' @\<^bsup>m'\<^esup> \<pi>'' \<guillemotleft> Suc k') 0 = \<pi> (Suc k)
[PROOF STEP]
using km' suc
[PROOF STATE]
proof (prove)
using this:
k' < m'
\<pi> (Suc k) = \<pi>' (Suc k')

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi>' @\<^bsup>m'\<^esup> \<pi>'' \<guillemotleft> Suc k') 0 = \<pi> (Suc k)

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>?\<pi>' (m' - Suc k' + n'') = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>' @\<^bsup>m'\<^esup> \<pi>'' \<guillemotleft> Suc k') (m' - Suc k' + n'') = local.return
[PROOF STEP]
using \<pi>''n km' \<pi>''0 ipd(1)
[PROOF STATE]
proof (prove)
using this:
\<pi>'' n'' = local.return
k' < m'
\<pi>'' 0 = ipd (\<pi> k)
\<pi>' m' = ipd (\<pi> k)

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

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

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

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

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have l''m: \<open>l'' \<le> m' - Suc k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l'' \<le> m' - Suc k'
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l'' \<le> m' - Suc k' \<Longrightarrow> False
[PROOF STEP]
using l'' not\<pi>l km'
[PROOF STATE]
proof (prove)
using this:
l'' \<le> m' - Suc k' + n''
(\<pi>' @\<^bsup>m'\<^esup> \<pi>'' \<guillemotleft> Suc k') l'' = \<pi> l
\<forall>i\<le>n''. \<pi>'' i \<noteq> \<pi> l
k' < m'

goal (1 subgoal):
 1. \<not> l'' \<le> m' - Suc k' \<Longrightarrow> False
[PROOF STEP]
by (cases \<open>Suc (k' + l'') \<le> m'\<close>, auto)
[PROOF STATE]
proof (state)
this:
l'' \<le> m' - Suc k'

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
let \<open>?l'\<close> = \<open>Suc ( k' + l'')\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have lm': \<open>?l' \<le> m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (k' + l'') \<le> m'
[PROOF STEP]
using l''m km'
[PROOF STATE]
proof (prove)
using this:
l'' \<le> m' - Suc k'
k' < m'

goal (1 subgoal):
 1. Suc (k' + l'') \<le> m'
[PROOF STEP]
by auto

  \<comment> \<open>Now we have found our desired l'\<close>
[PROOF STATE]
proof (state)
this:
Suc (k' + l'') \<le> m'

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have 1: \<open>\<pi>' ?l' = \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (Suc (k' + l'')) = \<pi> l
[PROOF STEP]
using  l'' l''m lm'
[PROOF STATE]
proof (prove)
using this:
l'' \<le> m' - Suc k' + n''
(\<pi>' @\<^bsup>m'\<^esup> \<pi>'' \<guillemotleft> Suc k') l'' = \<pi> l
l'' \<le> m' - Suc k'
Suc (k' + l'') \<le> m'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have 2: \<open>k' < ?l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < Suc (k' + l'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k' < Suc (k' + l'')

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have 3: \<open>?l' < m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (k' + l'') < m'
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Suc (k' + l'') < m' \<Longrightarrow> False
[PROOF STEP]
using lm'
[PROOF STATE]
proof (prove)
using this:
Suc (k' + l'') \<le> m'

goal (1 subgoal):
 1. \<not> Suc (k' + l'') < m' \<Longrightarrow> False
[PROOF STEP]
by (simp, metis "**" 1 ipd(1) ipdk_pdl)

  \<comment> \<open>Need the least such l'\<close>
[PROOF STATE]
proof (state)
this:
Suc (k' + l'') < m'

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
let \<open>?P\<close> = \<open>\<lambda> l'. \<pi>' l' = \<pi> l \<and> k' < l' \<and> l' < m'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have *: \<open>?P ?l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (Suc (k' + l'')) = \<pi> l \<and> k' < Suc (k' + l'') \<and> Suc (k' + l'') < m'
[PROOF STEP]
using 1 2 3
[PROOF STATE]
proof (prove)
using this:
\<pi>' (Suc (k' + l'')) = \<pi> l
k' < Suc (k' + l'')
Suc (k' + l'') < m'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
define l' where l': \<open>l' == LEAST l'. ?P l'\<close>
[PROOF STATE]
proof (state)
this:
l' \<equiv> LEAST l'. \<pi>' l' = \<pi> l \<and> k' < l' \<and> l' < m'

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<pi>l': \<open>\<pi>' l' = \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' l' = \<pi> l
[PROOF STEP]
using l' 1 2 3 LeastI[of \<open>?P\<close>]
[PROOF STATE]
proof (prove)
using this:
l' \<equiv> LEAST l'. \<pi>' l' = \<pi> l \<and> k' < l' \<and> l' < m'
\<pi>' (Suc (k' + l'')) = \<pi> l
k' < Suc (k' + l'')
Suc (k' + l'') < m'
\<pi>' ?k = \<pi> l \<and> k' < ?k \<and> ?k < m' \<Longrightarrow> \<pi>' (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') = \<pi> l \<and> k' < (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') \<and> (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') < m'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have kl': \<open>k' < l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < l'
[PROOF STEP]
using l' 1 2 3 LeastI[of \<open>?P\<close>]
[PROOF STATE]
proof (prove)
using this:
l' \<equiv> LEAST l'. \<pi>' l' = \<pi> l \<and> k' < l' \<and> l' < m'
\<pi>' (Suc (k' + l'')) = \<pi> l
k' < Suc (k' + l'')
Suc (k' + l'') < m'
\<pi>' ?k = \<pi> l \<and> k' < ?k \<and> ?k < m' \<Longrightarrow> \<pi>' (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') = \<pi> l \<and> k' < (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') \<and> (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') < m'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have lm': \<open>l' < m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' < m'
[PROOF STEP]
using l' 1 2 3 LeastI[of \<open>?P\<close>]
[PROOF STATE]
proof (prove)
using this:
l' \<equiv> LEAST l'. \<pi>' l' = \<pi> l \<and> k' < l' \<and> l' < m'
\<pi>' (Suc (k' + l'')) = \<pi> l
k' < Suc (k' + l'')
Suc (k' + l'') < m'
\<pi>' ?k = \<pi> l \<and> k' < ?k \<and> ?k < m' \<Longrightarrow> \<pi>' (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') = \<pi> l \<and> k' < (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') \<and> (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') < m'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have nretl': \<open>\<pi>' l' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' l' \<noteq> local.return
[PROOF STEP]
by (metis \<pi>''n \<pi>l' le_refl not\<pi>l)
[PROOF STATE]
proof (state)
this:
\<pi>' l' \<noteq> local.return

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have nipd': \<open>\<forall> j \<in> {k'..l'}. \<pi>' j \<noteq> ipd (\<pi>' k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{k'..l'}. \<pi>' j \<noteq> ipd (\<pi>' k')
[PROOF STEP]
using lm' kk' ipd(2) kl'
[PROOF STATE]
proof (prove)
using this:
l' < m'
\<pi>' k' = \<pi> k
\<forall>n\<in>{k'..<m'}. \<pi>' n \<noteq> ipd (\<pi> k)
k' < l'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have lcd': \<open>l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
by (metis is_cdi_def kl' nipd' nretl' path(2))
[PROOF STATE]
proof (state)
this:
l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have licd: \<open>l' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
have \<open>\<forall> m \<in> {k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> (\<forall> m \<in> {k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m)\<close>
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m)

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

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

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<Longrightarrow> False
[PROOF STEP]
have jm': \<open>j'<m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j' < m'
[PROOF STEP]
by (metis jl' lm' order.strict_trans)
[PROOF STATE]
proof (state)
this:
j' < m'

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi>' j' \<noteq> \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' j' \<noteq> \<pi> l
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<pi>' j' \<noteq> \<pi> l \<Longrightarrow> False
[PROOF STEP]
using l' kj' jm' jl' Least_le[of \<open>?P\<close> \<open>j'\<close>]
[PROOF STATE]
proof (prove)
using this:
l' \<equiv> LEAST l'. \<pi>' l' = \<pi> l \<and> k' < l' \<and> l' < m'
k' < j'
j' < m'
j' < l'
\<pi>' j' = \<pi> l \<and> k' < j' \<and> j' < m' \<Longrightarrow> (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') \<le> j'

goal (1 subgoal):
 1. \<not> \<pi>' j' \<noteq> \<pi> l \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>' j' \<noteq> \<pi> l

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

goal (1 subgoal):
 1. \<not> \<pi>' l' pd\<rightarrow> \<pi>' j'
[PROOF STEP]
using cd_not_pd lcdj' \<pi>l'
[PROOF STATE]
proof (prove)
using this:
\<pi>' j' \<noteq> \<pi> l
\<lbrakk>?l cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; ?\<pi> ?l \<noteq> ?\<pi> ?k\<rbrakk> \<Longrightarrow> \<not> ?\<pi> ?l pd\<rightarrow> ?\<pi> ?k
l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<pi>' l' = \<pi> l

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

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

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi>' j' \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' j' \<in> local.nodes
[PROOF STEP]
using path(2) 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>' j' \<in> local.nodes
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>' j' \<in> local.nodes

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> \<pi>' l' pd\<rightarrow> \<pi>' j'
\<pi>' j' \<in> local.nodes
[PROOF STEP]
obtain \<pi>\<^sub>1 n\<^sub>1 where path\<^sub>1: \<open>is_path \<pi>\<^sub>1\<close> and \<pi>0\<^sub>1: \<open>\<pi>\<^sub>1 0 = \<pi>' j'\<close> and \<pi>n\<^sub>1: \<open>\<pi>\<^sub>1 n\<^sub>1 = return\<close> and nl': \<open>\<forall> l \<le>n\<^sub>1. \<pi>\<^sub>1 l \<noteq> \<pi>' l'\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> \<pi>' l' pd\<rightarrow> \<pi>' j'
\<pi>' j' \<in> local.nodes

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<Longrightarrow> False
[PROOF STEP]
have \<open>?\<pi>'' 0 = \<pi> (Suc k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>' @\<^bsup>j'\<^esup> \<pi>\<^sub>1 \<guillemotleft> Suc k') 0 = \<pi> (Suc k)
[PROOF STEP]
by (simp, metis kj' less_eq_Suc_le suc)
[PROOF STATE]
proof (state)
this:
(\<pi>' @\<^bsup>j'\<^esup> \<pi>\<^sub>1 \<guillemotleft> Suc k') 0 = \<pi> (Suc k)

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

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<Longrightarrow> False
[PROOF STEP]
have kj': \<open>Suc k' \<le> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k' \<le> j'
[PROOF STEP]
by (metis kj' less_eq_Suc_le)
[PROOF STATE]
proof (state)
this:
Suc k' \<le> j'

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<Longrightarrow> False
[PROOF STEP]
hence \<open>?\<pi>'' (j' - Suc k' + n\<^sub>1) = return\<close>
[PROOF STATE]
proof (prove)
using this:
Suc k' \<le> j'

goal (1 subgoal):
 1. (\<pi>' @\<^bsup>j'\<^esup> \<pi>\<^sub>1 \<guillemotleft> Suc k') (j' - Suc k' + n\<^sub>1) = local.return
[PROOF STEP]
by (simp, metis \<pi>0\<^sub>1 \<pi>n\<^sub>1)
[PROOF STATE]
proof (state)
this:
(\<pi>' @\<^bsup>j'\<^esup> \<pi>\<^sub>1 \<guillemotleft> Suc k') (j' - Suc k' + n\<^sub>1) = local.return

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

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

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

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m) \<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 a: \<open>l'' \<le> j' - Suc k'\<close>
[PROOF STATE]
proof (state)
this:
l'' \<le> j' - Suc k'

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

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

goal (1 subgoal):
 1. \<pi>' (l'' + Suc k') = \<pi> l
[PROOF STEP]
by(simp, metis Nat.le_diff_conv2 add_Suc diff_add_inverse le_add1 le_add_diff_inverse2)
[PROOF STATE]
proof (state)
this:
\<pi>' (l'' + Suc k') = \<pi> l

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
have \<open>l'' + Suc k' < l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l'' + Suc k' < l'
[PROOF STEP]
by (metis a jl' add_diff_cancel_right' kj' le_add_diff_inverse less_imp_diff_less ordered_cancel_comm_monoid_diff_class.le_diff_conv2)
[PROOF STATE]
proof (state)
this:
l'' + Suc k' < l'

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

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
have \<open>k' < l'' + Suc k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < l'' + Suc k'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k' < l'' + Suc k'

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using Least_le[of \<open>?P\<close> \<open>l'' + Suc k'\<close>] l'
[PROOF STATE]
proof (prove)
using this:
\<pi>' (l'' + Suc k') = \<pi> l
l'' + Suc k' < l'
l'' + Suc k' < m'
k' < l'' + Suc k'
\<pi>' (l'' + Suc k') = \<pi> l \<and> k' < l'' + Suc k' \<and> l'' + Suc k' < m' \<Longrightarrow> (LEAST x. \<pi>' x = \<pi> l \<and> k' < x \<and> x < m') \<le> l'' + Suc k'
l' \<equiv> LEAST l'. \<pi>' l' = \<pi> l \<and> k' < l' \<and> l' < m'

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

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

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

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

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

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

goal (1 subgoal):
 1. \<pi>\<^sub>1 (Suc (k' + l'') - j') = \<pi> l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>1 (Suc (k' + l'') - j') = \<pi> l

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

goal (1 subgoal):
 1. \<not> l'' \<le> j' - Suc k' \<Longrightarrow> False
[PROOF STEP]
have \<open>Suc (k' + l'') - j' \<le> n\<^sub>1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (k' + l'') - j' \<le> n\<^sub>1
[PROOF STEP]
using ** kj'
[PROOF STATE]
proof (prove)
using this:
l'' \<le> j' - Suc k' + n\<^sub>1
Suc k' \<le> j'

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using nl'
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^sub>1 (Suc (k' + l'') - j') = \<pi> l
Suc (k' + l'') - j' \<le> n\<^sub>1
\<forall>l\<le>n\<^sub>1. \<pi>\<^sub>1 l \<noteq> \<pi>' l'

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis \<pi>l')
[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:
\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. l' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m

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

goal (1 subgoal):
 1. is_path \<pi>' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<and> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m)
[PROOF STEP]
using lcd' path(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m
l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
is_path \<pi>'

goal (1 subgoal):
 1. is_path \<pi>' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' \<and> (\<forall>m\<in>{k'<..<l'}. \<not> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' l']\<close>
[PROOF STATE]
proof (prove)
using this:
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 (metis icd_cs)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' l']

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<pi>\<^esup> l\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' l']

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

goal (1 subgoal):
 1. l \<noteq> Suc k \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<pi>\<^esup> l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma converged_same_icd: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and converge: \<open>l < n\<close> \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'\<close>
and csk: \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close> and icd: \<open>l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and suc: \<open>\<pi> (Suc k) = \<pi>' (Suc k')\<close>
shows \<open>\<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[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]
using icd
[PROOF STATE]
proof (prove)
using this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<pi> k \<noteq> local.return
[PROOF STEP]
using term_path_stable less_imp_le
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> (is_path \<pi> \<and> k < l \<and> \<pi> l \<noteq> local.return \<and> (\<forall>j\<in>{k..l}. \<pi> j \<noteq> ipd (\<pi> k))) \<and> (\<forall>m\<in>{k<..<l}. \<not> (is_path \<pi> \<and> m < l \<and> \<pi> l \<noteq> local.return \<and> (\<forall>j\<in>{m..l}. \<pi> j \<noteq> ipd (\<pi> m))))
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?\<pi> ?j = local.return
?x < ?y \<Longrightarrow> ?x \<le> ?y

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have kl: \<open>k < l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < l
[PROOF STEP]
using icd
[PROOF STATE]
proof (prove)
using this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have kn: \<open>k < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n
[PROOF STEP]
using converge kl
[PROOF STATE]
proof (prove)
using this:
l < n
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
k < l

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
from path_ipd_swap[OF path(1) nret kn]
[PROOF STATE]
proof (chain)
picking this:
(\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<rho> m where path\<rho>: \<open>is_path \<rho>\<close> and \<pi>\<rho>: \<open>\<pi> =\<^bsub>n\<^esub>  \<rho>\<close> and km: \<open>k < m\<close> and ipd: \<open>\<rho> m = ipd (\<rho> k)\<close> \<open>\<forall> l \<in> {k..<m}. \<rho> l \<noteq> ipd (\<rho> k)\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<rho> m. \<lbrakk>is_path \<rho>; \<pi> =\<^bsub>n\<^esub> \<rho>; k < m; \<rho> m = ipd (\<rho> k); \<forall>l\<in>{k..<m}. \<rho> l \<noteq> ipd (\<rho> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_path \<rho>
\<pi> =\<^bsub>n\<^esub> \<rho>
k < m
\<rho> m = ipd (\<rho> k)
\<forall>l\<in>{k..<m}. \<rho> l \<noteq> ipd (\<rho> k)

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csk1: \<open>cs\<^bsup>\<rho>\<^esup> k = cs\<^bsup>\<pi>\<^esup> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<rho>\<^esup> k = cs\<^bsup>\<pi>\<^esup> k
[PROOF STEP]
using cs_path_swap_le path path\<rho> \<pi>\<rho> kn
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> =\<^bsub>?n\<^esub> ?\<pi>'; ?k \<le> ?n\<rbrakk> \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k
is_path \<pi>
is_path \<pi>'
is_path \<rho>
\<pi> =\<^bsub>n\<^esub> \<rho>
k < n

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have suc\<rho>: \<open>\<rho> (Suc k) = \<pi> (Suc k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> (Suc k) = \<pi> (Suc k)
[PROOF STEP]
by (metis \<pi>\<rho> eq_up_to_def kn less_eq_Suc_le)
[PROOF STATE]
proof (state)
this:
\<rho> (Suc k) = \<pi> (Suc k)

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[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 csk last_cs nret)
[PROOF STATE]
proof (state)
this:
\<pi>' k' \<noteq> local.return

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have kn': \<open>k' < n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < n'
[PROOF STEP]
using cs_order[OF path csk converge(2) nret kn]
[PROOF STATE]
proof (prove)
using this:
k' < n'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
from path_ipd_swap[OF path(2) nret' kn']
[PROOF STATE]
proof (chain)
picking this:
(\<And>\<pi>'' m. \<lbrakk>is_path \<pi>''; \<pi>' =\<^bsub>n'\<^esub> \<pi>''; k' < m; \<pi>'' m = ipd (\<pi>'' k'); \<forall>l\<in>{k'..<m}. \<pi>'' l \<noteq> ipd (\<pi>'' k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<rho>' m' where path\<rho>': \<open>is_path \<rho>'\<close> and \<pi>\<rho>': \<open>\<pi>' =\<^bsub>n'\<^esub> \<rho>'\<close> and km': \<open>k' < m'\<close> and ipd': \<open>\<rho>' m' = ipd (\<rho>' k')\<close> \<open>\<forall> l \<in> {k'..<m'}. \<rho>' l \<noteq> ipd (\<rho>' k')\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>\<pi>'' m. \<lbrakk>is_path \<pi>''; \<pi>' =\<^bsub>n'\<^esub> \<pi>''; k' < m; \<pi>'' m = ipd (\<pi>'' k'); \<forall>l\<in>{k'..<m}. \<pi>'' l \<noteq> ipd (\<pi>'' k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<rho>' m'. \<lbrakk>is_path \<rho>'; \<pi>' =\<^bsub>n'\<^esub> \<rho>'; k' < m'; \<rho>' m' = ipd (\<rho>' k'); \<forall>l\<in>{k'..<m'}. \<rho>' l \<noteq> ipd (\<rho>' k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_path \<rho>'
\<pi>' =\<^bsub>n'\<^esub> \<rho>'
k' < m'
\<rho>' m' = ipd (\<rho>' k')
\<forall>l\<in>{k'..<m'}. \<rho>' l \<noteq> ipd (\<rho>' k')

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csk1': \<open>cs\<^bsup>\<rho>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<rho>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> k'
[PROOF STEP]
using cs_path_swap_le path path\<rho>' \<pi>\<rho>' kn'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> =\<^bsub>?n\<^esub> ?\<pi>'; ?k \<le> ?n\<rbrakk> \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k
is_path \<pi>
is_path \<pi>'
is_path \<rho>'
\<pi>' =\<^bsub>n'\<^esub> \<rho>'
k' < n'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have suc\<rho>': \<open>\<rho>' (Suc k') = \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho>' (Suc k') = \<pi>' (Suc k')
[PROOF STEP]
by (metis \<pi>\<rho>' eq_up_to_def kn' less_eq_Suc_le)
[PROOF STATE]
proof (state)
this:
\<rho>' (Suc k') = \<pi>' (Suc k')

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have icd\<rho>: \<open>l icd\<^bsup>\<rho>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l icd\<^bsup>\<rho>\<^esup>\<rightarrow> k
[PROOF STEP]
using icdi_path_swap_le[OF path\<rho> icd \<pi>\<rho>] converge
[PROOF STATE]
proof (prove)
using this:
l \<le> n \<Longrightarrow> l icd\<^bsup>\<rho>\<^esup>\<rightarrow> k
l < n
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have lm: \<open>l < m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < m
[PROOF STEP]
using ipd(1) icd\<rho> km
[PROOF STATE]
proof (prove)
using this:
\<rho> m = ipd (\<rho> k)
l icd\<^bsup>\<rho>\<^esup>\<rightarrow> k
k < m

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

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csk': \<open>cs\<^bsup>\<rho>\<^esup> k = cs\<^bsup>\<rho>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<rho>\<^esup> k = cs\<^bsup>\<rho>'\<^esup> k'
[PROOF STEP]
using csk1 csk1' csk
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<rho>\<^esup> k = cs\<^bsup>\<pi>\<^esup> k
cs\<^bsup>\<rho>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> k'
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence kk': \<open>\<rho>' k' = \<rho> k\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<rho>\<^esup> k = cs\<^bsup>\<rho>'\<^esup> k'

goal (1 subgoal):
 1. \<rho>' k' = \<rho> k
[PROOF STEP]
using last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<rho>\<^esup> k = cs\<^bsup>\<rho>'\<^esup> k'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

goal (1 subgoal):
 1. \<rho>' k' = \<rho> k
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<rho>' k' = \<rho> k

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have suc': \<open>\<rho> (Suc k) = \<rho>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> (Suc k) = \<rho>' (Suc k')
[PROOF STEP]
using suc suc\<rho> suc\<rho>'
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc k) = \<pi>' (Suc k')
\<rho> (Suc k) = \<pi> (Suc k)
\<rho>' (Suc k') = \<pi>' (Suc k')

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have mm': \<open>\<rho>' m' = \<rho> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho>' m' = \<rho> m
[PROOF STEP]
using ipd(1) ipd'(1) kk'
[PROOF STATE]
proof (prove)
using this:
\<rho> m = ipd (\<rho> k)
\<rho>' m' = ipd (\<rho>' k')
\<rho>' k' = \<rho> k

goal (1 subgoal):
 1. \<rho>' m' = \<rho> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<rho>' m' = \<rho> m

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
from cs_ipd[OF ipd km] cs_ipd[OF ipd' km',unfolded mm', folded csk']
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<rho>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<rho> m) (cs\<^bsup>\<rho>\<^esup> k) @ [\<rho> m]
cs\<^bsup>\<rho>'\<^esup> m' = filter (\<lambda>n. ipd n \<noteq> \<rho> m) (cs\<^bsup>\<rho>\<^esup> k) @ [\<rho> m]
[PROOF STEP]
have csm: \<open>cs\<^bsup>\<rho>\<^esup> m = cs\<^bsup>\<rho>'\<^esup> m'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<rho>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<rho> m) (cs\<^bsup>\<rho>\<^esup> k) @ [\<rho> m]
cs\<^bsup>\<rho>'\<^esup> m' = filter (\<lambda>n. ipd n \<noteq> \<rho> m) (cs\<^bsup>\<rho>\<^esup> k) @ [\<rho> m]

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
from converged_ipd_same_icd[OF path\<rho> path\<rho>' lm  csm csk' icd\<rho> suc' ipd'[unfolded kk']]
[PROOF STATE]
proof (chain)
picking this:
\<exists>l'. cs\<^bsup>\<rho>\<^esup> l = cs\<^bsup>\<rho>'\<^esup> l'
[PROOF STEP]
obtain l' where csl: \<open>cs\<^bsup>\<rho>\<^esup> l = cs\<^bsup>\<rho>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. cs\<^bsup>\<rho>\<^esup> l = cs\<^bsup>\<rho>'\<^esup> l'

goal (1 subgoal):
 1. (\<And>l'. cs\<^bsup>\<rho>\<^esup> l = cs\<^bsup>\<rho>'\<^esup> l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<rho>\<^esup> l = cs\<^bsup>\<rho>'\<^esup> l'

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csl\<rho>: \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<rho>\<^esup> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<rho>\<^esup> l
[PROOF STEP]
using \<pi>\<rho> converge(1) cs_path_swap_le less_imp_le_nat path(1) path\<rho>
[PROOF STATE]
proof (prove)
using this:
\<pi> =\<^bsub>n\<^esub> \<rho>
l < n
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> =\<^bsub>?n\<^esub> ?\<pi>'; ?k \<le> ?n\<rbrakk> \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k
?m < ?n \<Longrightarrow> ?m \<le> ?n
is_path \<pi>
is_path \<rho>

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have nretl: \<open>\<rho> l \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> l \<noteq> local.return
[PROOF STEP]
by (metis icd\<rho> icd_imp_cd ret_no_cd)
[PROOF STATE]
proof (state)
this:
\<rho> l \<noteq> local.return

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csn': \<open>cs\<^bsup>\<rho>\<^esup> n = cs\<^bsup>\<rho>'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<rho>\<^esup> n = cs\<^bsup>\<rho>'\<^esup> n'
[PROOF STEP]
using converge(2) cs_path_swap path path\<rho> path\<rho>' \<pi>\<rho> \<pi>\<rho>'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> =\<^bsub>?k\<^esub> ?\<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k
is_path \<pi>
is_path \<pi>'
is_path \<rho>
is_path \<rho>'
\<pi> =\<^bsub>n\<^esub> \<rho>
\<pi>' =\<^bsub>n'\<^esub> \<rho>'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have ln': \<open>l' < n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' < n'
[PROOF STEP]
using cs_order[OF path\<rho> path\<rho>' csl csn' nretl converge(1)]
[PROOF STATE]
proof (prove)
using this:
l' < n'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csl\<rho>': \<open>cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<rho>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<rho>'\<^esup> l'
[PROOF STEP]
using cs_path_swap_le[OF path(2) path\<rho>' \<pi>\<rho>'] ln'
[PROOF STATE]
proof (prove)
using this:
?k \<le> n' \<Longrightarrow> cs\<^bsup>\<pi>'\<^esup> ?k = cs\<^bsup>\<rho>'\<^esup> ?k
l' < n'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csl': \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
using csl\<rho> csl\<rho>' csl
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<rho>\<^esup> l
cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<rho>'\<^esup> l'
cs\<^bsup>\<rho>\<^esup> l = cs\<^bsup>\<rho>'\<^esup> l'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_is_cs_less: assumes \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> k \<prec> cs\<^bsup>\<pi>\<^esup> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k \<prec> cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k \<prec> cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
obtain xs where csl: \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ xs @[\<pi> l]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ xs @ [\<pi> l] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cd_in_cs[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>ns. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ ns @ [\<pi> l]

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k \<prec> cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
hence len: \<open>length(cs\<^bsup>\<pi>\<^esup> k) < length (cs\<^bsup>\<pi>\<^esup> l)\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ xs @ [\<pi> l]

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k \<prec> cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
have take: \<open>take (length (cs\<^bsup>\<pi>\<^esup> k)) (cs\<^bsup>\<pi>\<^esup> l) = cs\<^bsup>\<pi>\<^esup> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length (cs\<^bsup>\<pi>\<^esup> k)) (cs\<^bsup>\<pi>\<^esup> l) = cs\<^bsup>\<pi>\<^esup> k
[PROOF STEP]
using csl
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ xs @ [\<pi> l]

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k \<prec> cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k \<prec> cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
using cs_less.intros[OF len take]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k \<prec> cs\<^bsup>\<pi>\<^esup> l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_select_id: assumes \<open>is_path \<pi>\<close> \<open>\<pi> k \<noteq> return\<close> shows \<open>\<pi>\<exclamdown>cs\<^bsup>\<pi>\<^esup> k = k\<close> (is \<open>?k = k\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<exclamdown> cs\<^bsup>\<pi>\<^esup> k) = k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<pi> \<exclamdown> cs\<^bsup>\<pi>\<^esup> k) = k
[PROOF STEP]
have *: \<open>\<And> i . cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k  \<Longrightarrow> i = k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> i = k
[PROOF STEP]
using cs_inj[OF assms]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> ?n' \<Longrightarrow> k = ?n'

goal (1 subgoal):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> i = k
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> ?i1 = k

goal (1 subgoal):
 1. (\<pi> \<exclamdown> cs\<^bsup>\<pi>\<^esup> k) = k
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> ?k = cs\<^bsup>\<pi>\<^esup> k\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> ?i1 = k

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> cs\<^bsup>\<pi>\<^esup> k) = cs\<^bsup>\<pi>\<^esup> k
[PROOF STEP]
unfolding cs_select_def
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> ?i1 = k

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (THE ka. cs\<^bsup>\<pi>\<^esup> ka = cs\<^bsup>\<pi>\<^esup> k) = cs\<^bsup>\<pi>\<^esup> k
[PROOF STEP]
using theI[of \<open>\<lambda> i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k\<close> \<open>k\<close>]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> ?i1 = k
\<lbrakk>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> k; \<And>x. cs\<^bsup>\<pi>\<^esup> x = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> x = k\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> (THE x. cs\<^bsup>\<pi>\<^esup> x = cs\<^bsup>\<pi>\<^esup> k) = cs\<^bsup>\<pi>\<^esup> k

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

goal (1 subgoal):
 1. (\<pi> \<exclamdown> cs\<^bsup>\<pi>\<^esup> k) = k
[PROOF STEP]
thus \<open>?k = k\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> cs\<^bsup>\<pi>\<^esup> k) = cs\<^bsup>\<pi>\<^esup> k

goal (1 subgoal):
 1. (\<pi> \<exclamdown> cs\<^bsup>\<pi>\<^esup> k) = k
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> cs\<^bsup>\<pi>\<^esup> k) = cs\<^bsup>\<pi>\<^esup> k
cs\<^bsup>\<pi>\<^esup> ?i1 = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> ?i1 = k

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_single_nocd: assumes \<open>cs\<^bsup>\<pi>\<^esup> i = [x]\<close> shows \<open>\<forall> k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have \<open>\<not> (\<exists> k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
using assms cs_not_nil
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = [x]
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

goal (1 subgoal):
 1. \<not> (\<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
hence \<open>\<not> (\<exists> k. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_single_pd_intermed: assumes \<open>is_path \<pi>\<close> \<open>cs\<^bsup>\<pi>\<^esup> n = [\<pi> n]\<close> \<open>k \<le> n\<close> shows \<open>\<pi> n pd\<rightarrow> \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> n pd\<rightarrow> \<pi> k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> n pd\<rightarrow> \<pi> k
[PROOF STEP]
have \<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 assms(2) cs_single_nocd icd_imp_cd)
[PROOF STATE]
proof (state)
this:
\<forall>l. \<not> n icd\<^bsup>\<pi>\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. \<pi> n pd\<rightarrow> \<pi> k
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>l. \<not> n icd\<^bsup>\<pi>\<^esup>\<rightarrow> l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_first_pd:  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>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 cs_cases first first_pd_no_cd icd_imp_cd path pd)


[STATEMENT]
lemma converged_pd_cs_single: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and  converge: \<open>l < m\<close> \<open>cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<close>
and \<pi>0: \<open>\<pi> 0 = \<pi>' 0\<close> and mpdl: \<open>\<pi> m pd\<rightarrow> \<pi> l\<close> and csl: \<open>cs\<^bsup>\<pi>\<^esup> l = [\<pi> l]\<close>
shows \<open>\<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have *: \<open>\<pi> l pd\<rightarrow> \<pi>' 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> l pd\<rightarrow> \<pi>' 0
[PROOF STEP]
using cs_single_pd_intermed[OF path(1) csl] \<pi>0[symmetric]
[PROOF STATE]
proof (prove)
using this:
?k \<le> l \<Longrightarrow> \<pi> l pd\<rightarrow> \<pi> ?k
\<pi>' 0 = \<pi> 0

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<pi>m: \<open>\<pi> m = \<pi>' m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> m = \<pi>' m'
[PROOF STEP]
by (metis converge(2) last_cs)
[PROOF STATE]
proof (state)
this:
\<pi> m = \<pi>' m'

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence **: \<open>\<pi>' m' pd\<rightarrow> \<pi> l\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> m = \<pi>' m'

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

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
obtain l' where lm': \<open>l' \<le> m'\<close> and \<pi>l:  \<open>\<pi>' l' = \<pi> l\<close> (is \<open>?P l'\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' \<le> m'; \<pi>' l' = \<pi> l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using path_pd_pd0[OF path(2) ** *]
[PROOF STATE]
proof (prove)
using this:
(\<And>k. \<lbrakk>k \<le> m'; \<pi>' k = \<pi> l\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
let \<open>?l\<close> = \<open>(LEAST l'. \<pi>' l' = \<pi> l)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<pi>l': \<open>\<pi>' ?l = \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l
[PROOF STEP]
using LeastI[of \<open>?P\<close>,OF \<pi>l]
[PROOF STATE]
proof (prove)
using this:
\<pi>' (LEAST x. \<pi>' x = \<pi> l) = \<pi> l

goal (1 subgoal):
 1. \<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>\<forall> i <?l. \<pi>' i \<noteq> \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi> l
[PROOF STEP]
using Least_le[of \<open>?P\<close>]
[PROOF STATE]
proof (prove)
using this:
\<pi>' ?k = \<pi> l \<Longrightarrow> (LEAST x. \<pi>' x = \<pi> l) \<le> ?k

goal (1 subgoal):
 1. \<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi> l
[PROOF STEP]
by (metis not_less)
[PROOF STATE]
proof (state)
this:
\<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi> l

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence \<open>\<forall> i <?l. \<pi>' i \<noteq> \<pi>' ?l\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi> l

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

goal (1 subgoal):
 1. \<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi>' (LEAST l'. \<pi>' l' = \<pi> l)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi>' (LEAST l'. \<pi>' l' = \<pi> l)

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi>' (LEAST l'. \<pi>' l' = \<pi> l)

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>\<pi>' ?l pd\<rightarrow> \<pi>' 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (LEAST l'. \<pi>' l' = \<pi> l) pd\<rightarrow> \<pi>' 0
[PROOF STEP]
using * \<pi>l'
[PROOF STATE]
proof (prove)
using this:
\<pi> l pd\<rightarrow> \<pi>' 0
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l

goal (1 subgoal):
 1. \<pi>' (LEAST l'. \<pi>' l' = \<pi> l) pd\<rightarrow> \<pi>' 0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) pd\<rightarrow> \<pi>' 0

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l
\<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi>' (LEAST l'. \<pi>' l' = \<pi> l)
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) pd\<rightarrow> \<pi>' 0
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>'\<^esup> ?l = [\<pi>' ?l]\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l
\<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi>' (LEAST l'. \<pi>' l' = \<pi> l)
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) pd\<rightarrow> \<pi>' 0

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> (LEAST l'. \<pi>' l' = \<pi> l) = [\<pi>' (LEAST l'. \<pi>' l' = \<pi> l)]
[PROOF STEP]
using cs_first_pd[OF path(2)]
[PROOF STATE]
proof (prove)
using this:
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l
\<forall>i<LEAST l'. \<pi>' l' = \<pi> l. \<pi>' i \<noteq> \<pi>' (LEAST l'. \<pi>' l' = \<pi> l)
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) pd\<rightarrow> \<pi>' 0
\<lbrakk>\<pi>' ?n pd\<rightarrow> \<pi>' 0; \<forall>l<?n. \<pi>' l \<noteq> \<pi>' ?n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>'\<^esup> ?n = [\<pi>' ?n]

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> (LEAST l'. \<pi>' l' = \<pi> l) = [\<pi>' (LEAST l'. \<pi>' l' = \<pi> l)]

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
using csl \<pi>l'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> (LEAST l'. \<pi>' l' = \<pi> l) = [\<pi>' (LEAST l'. \<pi>' l' = \<pi> l)]
cs\<^bsup>\<pi>\<^esup> l = [\<pi> l]
\<pi>' (LEAST l'. \<pi>' l' = \<pi> l) = \<pi> l

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

goal:
No subgoals!
[PROOF STEP]
qed