[STATEMENT]
lemma converged_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 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 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 *: \<open>\<pi> l = return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> l = 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]
hence \<open>\<pi> m = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> l = local.return

goal (1 subgoal):
 1. \<pi> m = local.return
[PROOF STEP]
by (metis converge(1) path(1) term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
\<pi> m = 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]
hence \<open>cs\<^bsup>\<pi>\<^esup> m = [return]\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> m = local.return

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> m = [local.return]
[PROOF STEP]
using cs_return
[PROOF STATE]
proof (prove)
using this:
\<pi> m = local.return
?\<pi> ?n = local.return \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?n = [?\<pi> ?n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> m = [local.return]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> m = [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]
hence \<open>cs\<^bsup>\<pi>'\<^esup> m' = [return]\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = [local.return]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> m' = [local.return]
[PROOF STEP]
using converge
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = [local.return]
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> m' = [local.return]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> m' = [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]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> m' = [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]
have \<open>cs\<^bsup>\<pi>\<^esup> l = [return]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = [local.return]
[PROOF STEP]
using * cs_return
[PROOF STATE]
proof (prove)
using this:
\<pi> l = local.return
?\<pi> ?n = local.return \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?n = [?\<pi> ?n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = [local.return]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> l = [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:
cs\<^bsup>\<pi>'\<^esup> m' = [local.return]
cs\<^bsup>\<pi>\<^esup> l = [local.return]
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> m' = [local.return]
cs\<^bsup>\<pi>\<^esup> l = [local.return]

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<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. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
obtain \<pi>\<^sub>1 n where path1: \<open>is_path \<pi>\<^sub>1\<close> and upto: \<open>\<pi> =\<^bsub>m\<^esub> \<pi>\<^sub>1\<close> and \<pi>n: \<open>\<pi>\<^sub>1 n = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>\<^sub>1 n. \<lbrakk>is_path \<pi>\<^sub>1; \<pi> =\<^bsub>m\<^esub> \<pi>\<^sub>1; \<pi>\<^sub>1 n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using path(1) path_swap_ret
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<lbrakk>is_path ?\<pi>; \<And>\<pi>' n. \<lbrakk>is_path \<pi>'; ?\<pi> =\<^bsub>?k\<^esub> \<pi>'; \<pi>' n = local.return\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<pi>\<^sub>1 n. \<lbrakk>is_path \<pi>\<^sub>1; \<pi> =\<^bsub>m\<^esub> \<pi>\<^sub>1; \<pi>\<^sub>1 n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_path \<pi>\<^sub>1
\<pi> =\<^bsub>m\<^esub> \<pi>\<^sub>1
\<pi>\<^sub>1 n = local.return

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
obtain \<pi>\<^sub>1' n' where path1': \<open>is_path \<pi>\<^sub>1'\<close> and upto': \<open>\<pi>' =\<^bsub>m'\<^esub>  \<pi>\<^sub>1'\<close> and \<pi>n': \<open>\<pi>\<^sub>1' n' = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>\<^sub>1' n'. \<lbrakk>is_path \<pi>\<^sub>1'; \<pi>' =\<^bsub>m'\<^esub> \<pi>\<^sub>1'; \<pi>\<^sub>1' n' = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using path(2) path_swap_ret
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>'
\<lbrakk>is_path ?\<pi>; \<And>\<pi>' n. \<lbrakk>is_path \<pi>'; ?\<pi> =\<^bsub>?k\<^esub> \<pi>'; \<pi>' n = local.return\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<pi>\<^sub>1' n'. \<lbrakk>is_path \<pi>\<^sub>1'; \<pi>' =\<^bsub>m'\<^esub> \<pi>\<^sub>1'; \<pi>\<^sub>1' n' = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_path \<pi>\<^sub>1'
\<pi>' =\<^bsub>m'\<^esub> \<pi>\<^sub>1'
\<pi>\<^sub>1' n' = local.return

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<pi>1l: \<open>\<pi>\<^sub>1 l = \<pi> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>1 l = \<pi> l
[PROOF STEP]
using upto converge(1)
[PROOF STATE]
proof (prove)
using this:
\<pi> =\<^bsub>m\<^esub> \<pi>\<^sub>1
l < m

goal (1 subgoal):
 1. \<pi>\<^sub>1 l = \<pi> l
[PROOF STEP]
by (metis eq_up_to_def nat_less_le)
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>1 l = \<pi> l

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have cs1l: \<open>cs\<^bsup>\<pi>\<^sub>1\<^esup> l = cs\<^bsup>\<pi>\<^esup> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^sub>1\<^esup> l = cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
using cs_path_swap_le upto path1 path(1) converge(1)
[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
\<pi> =\<^bsub>m\<^esub> \<pi>\<^sub>1
is_path \<pi>\<^sub>1
is_path \<pi>
l < m

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csl1: \<open>cs\<^bsup>\<pi>\<^sub>1\<^esup> l = [\<pi>\<^sub>1 l]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^sub>1\<^esup> l = [\<pi>\<^sub>1 l]
[PROOF STEP]
by (metis \<pi>1l cs1l csl)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^sub>1\<^esup> l = [\<pi>\<^sub>1 l]

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have converge1: \<open>cs\<^bsup>\<pi>\<^sub>1\<^esup> n = cs\<^bsup>\<pi>\<^sub>1'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^sub>1\<^esup> n = cs\<^bsup>\<pi>\<^sub>1'\<^esup> n'
[PROOF STEP]
using \<pi>n \<pi>n' cs_return
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^sub>1 n = local.return
\<pi>\<^sub>1' n' = local.return
?\<pi> ?n = local.return \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?n = [?\<pi> ?n]

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<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 nret \<pi>n \<pi>1l term_path_stable[OF path1 \<pi>n]
[PROOF STATE]
proof (prove)
using this:
\<pi> l \<noteq> local.return
\<pi>\<^sub>1 n = local.return
\<pi>\<^sub>1 l = \<pi> l
n \<le> ?j \<Longrightarrow> \<pi>\<^sub>1 ?j = local.return

goal (1 subgoal):
 1. l < n
[PROOF STEP]
by (auto, metis linorder_neqE_nat less_imp_le)
[PROOF STATE]
proof (state)
this:
l < n

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<pi>01: \<open>\<pi>\<^sub>1 0 = \<pi>\<^sub>1' 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>1 0 = \<pi>\<^sub>1' 0
[PROOF STEP]
using \<pi>0 eq_up_to_apply[OF upto] eq_up_to_apply[OF upto']
[PROOF STATE]
proof (prove)
using this:
\<pi> 0 = \<pi>' 0
?j \<le> m \<Longrightarrow> \<pi> ?j = \<pi>\<^sub>1 ?j
?j \<le> m' \<Longrightarrow> \<pi>' ?j = \<pi>\<^sub>1' ?j

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have pd: \<open>\<pi>\<^sub>1 n pd\<rightarrow> \<pi>\<^sub>1 l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>1 n pd\<rightarrow> \<pi>\<^sub>1 l
[PROOF STEP]
using \<pi>n
[PROOF STATE]
proof (prove)
using this:
\<pi>\<^sub>1 n = local.return

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
obtain l' where csl: \<open>cs\<^bsup>\<pi>\<^sub>1\<^esup> l = cs\<^bsup>\<pi>\<^sub>1'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. cs\<^bsup>\<pi>\<^sub>1\<^esup> l = cs\<^bsup>\<pi>\<^sub>1'\<^esup> l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using converged_pd_cs_single[OF path1 path1' ln converge1 \<pi>01 pd csl1]
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. cs\<^bsup>\<pi>\<^sub>1\<^esup> l = cs\<^bsup>\<pi>\<^sub>1'\<^esup> l'

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have cs1m: \<open>cs\<^bsup>\<pi>\<^sub>1\<^esup> m = cs\<^bsup>\<pi>\<^esup> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^sub>1\<^esup> m = cs\<^bsup>\<pi>\<^esup> m
[PROOF STEP]
using cs_path_swap upto path1 path(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> =\<^bsub>?k\<^esub> ?\<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k
\<pi> =\<^bsub>m\<^esub> \<pi>\<^sub>1
is_path \<pi>\<^sub>1
is_path \<pi>

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have cs1m': \<open>cs\<^bsup>\<pi>\<^sub>1'\<^esup> m' = cs\<^bsup>\<pi>'\<^esup> m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^sub>1'\<^esup> m' = cs\<^bsup>\<pi>'\<^esup> m'
[PROOF STEP]
using cs_path_swap upto' path1' path(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> =\<^bsub>?k\<^esub> ?\<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k
\<pi>' =\<^bsub>m'\<^esub> \<pi>\<^sub>1'
is_path \<pi>\<^sub>1'
is_path \<pi>'

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^sub>1\<^esup> m = cs\<^bsup>\<pi>\<^sub>1'\<^esup> m'
[PROOF STEP]
using converge(2) cs1m
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^sub>1'\<^esup> m' = cs\<^bsup>\<pi>'\<^esup> m'
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
cs\<^bsup>\<pi>\<^sub>1\<^esup> m = cs\<^bsup>\<pi>\<^esup> m

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have nret1: \<open>\<pi>\<^sub>1 l \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>1 l \<noteq> local.return
[PROOF STEP]
using nret \<pi>1l
[PROOF STATE]
proof (prove)
using this:
\<pi> l \<noteq> local.return
\<pi>\<^sub>1 l = \<pi> l

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<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 cs_order[OF path1 path1' csl converge1 nret1 converge(1)]
[PROOF STATE]
proof (prove)
using this:
l' < m'

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<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>\<^sub>1'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<pi>\<^sub>1'\<^esup> l'
[PROOF STEP]
using cs_path_swap_le[OF path(2) path1' upto'] lm'
[PROOF STATE]
proof (prove)
using this:
?k \<le> m' \<Longrightarrow> cs\<^bsup>\<pi>'\<^esup> ?k = cs\<^bsup>\<pi>\<^sub>1'\<^esup> ?k
l' < m'

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<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> l' = cs\<^bsup>\<pi>\<^sub>1'\<^esup> l'

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<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>\<^sub>1\<^esup> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^sub>1\<^esup> l
[PROOF STEP]
using cs_path_swap_le[OF path(1) path1 upto] converge(1)
[PROOF STATE]
proof (prove)
using this:
?k \<le> m \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> ?k = cs\<^bsup>\<pi>\<^sub>1\<^esup> ?k
l < m

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<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> l' = cs\<^bsup>\<pi>\<^sub>1'\<^esup> l'
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^sub>1\<^esup> l
[PROOF STEP]
have \<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>\<^sub>1'\<^esup> l'
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^sub>1\<^esup> l

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
using csl
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> l' = cs\<^bsup>\<pi>\<^sub>1'\<^esup> l'
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^sub>1\<^esup> l
cs\<^bsup>\<pi>\<^sub>1\<^esup> l = cs\<^bsup>\<pi>\<^sub>1'\<^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. \<pi> l \<noteq> local.return \<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 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 converged_cd_same_suc: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and init: \<open>\<pi> 0 = \<pi>' 0\<close>
and cd_suc: \<open>\<forall> k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')\<close> and converge: \<open>l < m\<close> \<open>cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<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]
using path init cd_suc converge
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
\<pi> 0 = \<pi>' 0
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
proof (induction \<open>\<pi>\<close> \<open>l\<close> rule: cs_induct,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
case (cs \<pi> l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ex (is_icdi l \<pi>); is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi l \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); The (is_icdi l \<pi>) < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> The (is_icdi l \<pi>) = cs\<^bsup>\<pi>'\<^esup> l'
is_path \<pi>
is_path \<pi>'
\<pi> 0 = \<pi>' 0
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
assume *: \<open>\<exists>k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (state)
this:
\<exists>k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
let \<open>?k\<close> = \<open>THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have icd: \<open>l icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
[PROOF STEP]
by (metis "*" icd_is_the_icd)
[PROOF STATE]
proof (state)
this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence lcdk: \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k\<close>
[PROOF STATE]
proof (prove)
using this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

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

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence kl: \<open>?k<l\<close>
[PROOF STATE]
proof (prove)
using this:
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

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

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

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>\<And> j. ?k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
using icd cd_trans is_icdi_def
[PROOF STATE]
proof (prove)
using this:
l icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
\<lbrakk>?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i; ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j\<rbrakk> \<Longrightarrow> ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i
(?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. \<And>j. (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1 \<Longrightarrow> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence suc': \<open>\<forall> j j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j' \<and> ?k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> \<pi> (Suc j) = \<pi>' (Suc j')\<close>
[PROOF STATE]
proof (prove)
using this:
(THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1 \<Longrightarrow> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1

goal (1 subgoal):
 1. \<forall>j j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j' \<and> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> \<pi> (Suc j) = \<pi>' (Suc j')
[PROOF STEP]
using cs.prems(4)
[PROOF STATE]
proof (prove)
using this:
(THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1 \<Longrightarrow> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')

goal (1 subgoal):
 1. \<forall>j j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j' \<and> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> \<pi> (Suc j) = \<pi>' (Suc j')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>j j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j' \<and> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> \<pi> (Suc j) = \<pi>' (Suc j')

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
from cs.IH[OF * cs(2) path(2) cs(4) suc'] cs.prems kl
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>The (is_icdi l \<pi>) < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> The (is_icdi l \<pi>) = cs\<^bsup>\<pi>'\<^esup> l'
is_path \<pi>
is_path \<pi>'
\<pi> 0 = \<pi>' 0
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
(THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) < l
[PROOF STEP]
have \<open>\<exists>k'. cs\<^bsup>\<pi>\<^esup> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = cs\<^bsup>\<pi>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>The (is_icdi l \<pi>) < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> The (is_icdi l \<pi>) = cs\<^bsup>\<pi>'\<^esup> l'
is_path \<pi>
is_path \<pi>'
\<pi> 0 = \<pi>' 0
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
(THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) < l

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

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k'. cs\<^bsup>\<pi>\<^esup> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = cs\<^bsup>\<pi>'\<^esup> k'
[PROOF STEP]
obtain k' where csk: \<open>cs\<^bsup>\<pi>\<^esup> ?k = cs\<^bsup>\<pi>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k'. cs\<^bsup>\<pi>\<^esup> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = cs\<^bsup>\<pi>'\<^esup> k'

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

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have suc2: \<open>\<pi> (Suc ?k) = \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)) = \<pi>' (Suc k')
[PROOF STEP]
using cs.prems(4) lcdk csk
[PROOF STATE]
proof (prove)
using this:
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
cs\<^bsup>\<pi>\<^esup> (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = cs\<^bsup>\<pi>'\<^esup> k'

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

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have km: \<open>?k < m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) < m
[PROOF STEP]
using kl cs.prems(5)
[PROOF STATE]
proof (prove)
using this:
(THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) < l
l < m

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

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<not> ?P7 \<pi>'' n\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
from converged_same_icd[OF cs(2) path(2) cs.prems(5) cs.prems(6) csk icd suc2]
[PROOF STATE]
proof (chain)
picking this:
\<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. 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]
.
[PROOF STATE]
proof (state)
this:
\<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<nexists>k. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<nexists>k. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
case (cs \<pi> l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ex (is_icdi l \<pi>); is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi l \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); The (is_icdi l \<pi>) < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> The (is_icdi l \<pi>) = cs\<^bsup>\<pi>'\<^esup> l'
is_path \<pi>
is_path \<pi>'
\<pi> 0 = \<pi>' 0
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<nexists>k. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
assume \<open>\<not> (\<exists>k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<nexists>k. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> l = [\<pi> l]\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi n \<pi>'') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); The (is_icdi n \<pi>'') < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> l'; is_path \<pi>''; is_path \<pi>'; \<pi>'' 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>''\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> n cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k \<longrightarrow> \<pi>'' (Suc k) = \<pi>' (Suc k'); n < m; cs\<^bsup>\<pi>''\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); l < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'; \<nexists>k. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
with cs converged_cs_single
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Ex (is_icdi l \<pi>); is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi l \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); The (is_icdi l \<pi>) < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> The (is_icdi l \<pi>) = cs\<^bsup>\<pi>'\<^esup> l'
is_path \<pi>
is_path \<pi>'
\<pi> 0 = \<pi>' 0
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?l < ?m; cs\<^bsup>?\<pi>\<^esup> ?m = cs\<^bsup>?\<pi>'\<^esup> ?m'; ?\<pi> 0 = ?\<pi>' 0; cs\<^bsup>?\<pi>\<^esup> ?l = [?\<pi> ?l]\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>?\<pi>\<^esup> ?l = cs\<^bsup>?\<pi>'\<^esup> l'
cs\<^bsup>\<pi>\<^esup> l = [\<pi> l]
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Ex (is_icdi l \<pi>); is_path \<pi>; is_path \<pi>'; \<pi> 0 = \<pi>' 0; \<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> The (is_icdi l \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k'); The (is_icdi l \<pi>) < m; cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> The (is_icdi l \<pi>) = cs\<^bsup>\<pi>'\<^esup> l'
is_path \<pi>
is_path \<pi>'
\<pi> 0 = \<pi>' 0
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?l < ?m; cs\<^bsup>?\<pi>\<^esup> ?m = cs\<^bsup>?\<pi>'\<^esup> ?m'; ?\<pi> 0 = ?\<pi>' 0; cs\<^bsup>?\<pi>\<^esup> ?l = [?\<pi> ?l]\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>?\<pi>\<^esup> ?l = cs\<^bsup>?\<pi>'\<^esup> l'
cs\<^bsup>\<pi>\<^esup> 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


[STATEMENT]
lemma converged_cd_diverge:
assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and init: \<open>\<pi> 0 = \<pi>' 0\<close> and notin: \<open>\<not> (\<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l')\<close> and converge: \<open>l < m\<close> \<open>cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<close>
obtains k k' where \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close> \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>\<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms converged_cd_same_suc
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
\<pi> 0 = \<pi>' 0
\<nexists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> 0 = ?\<pi>' 0; \<forall>k k'. cs\<^bsup>?\<pi>\<^esup> k = cs\<^bsup>?\<pi>'\<^esup> k' \<and> ?l cd\<^bsup>?\<pi>\<^esup>\<rightarrow> k \<longrightarrow> ?\<pi> (Suc k) = ?\<pi>' (Suc k'); ?l < ?m; cs\<^bsup>?\<pi>\<^esup> ?m = cs\<^bsup>?\<pi>'\<^esup> ?m'\<rbrakk> \<Longrightarrow> \<exists>l'. cs\<^bsup>?\<pi>\<^esup> ?l = cs\<^bsup>?\<pi>'\<^esup> l'

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


[STATEMENT]
lemma converged_cd_same_suc_return: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and \<pi>0: \<open>\<pi> 0 = \<pi>' 0\<close>
and cd_suc: \<open>\<forall> k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k')\<close> and ret: \<open>\<pi>' n' = return\<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 \<open>\<pi> l = return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> l = 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]
hence \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> l = local.return

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> n'
[PROOF STEP]
using ret cs_return
[PROOF STATE]
proof (prove)
using this:
\<pi> l = local.return
\<pi>' n' = local.return
?\<pi> ?n = local.return \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?n = [?\<pi> ?n]

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

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> n'

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. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
assume nretl: \<open>\<pi> l \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> l \<noteq> local.return

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>\<pi> l \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> l \<in> local.nodes
[PROOF STEP]
using path path_nodes
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi> l \<in> local.nodes
[PROOF STEP]
obtain \<pi>l n where ipl: \<open>is_path \<pi>l\<close> and \<pi>l:  \<open>\<pi> l = \<pi>l 0\<close> and retn: \<open>\<pi>l n = return\<close> and notl: \<open>\<forall> i>0. \<pi>l i \<noteq> \<pi> l\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> l \<in> local.nodes

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence ip: \<open>is_path (\<pi>@\<^bsup>l\<^esup> \<pi>l)\<close> and l: \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>l) l = \<pi> l\<close> and retl: \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>l) (l + n) = return\<close> and nl: \<open>\<forall> i>l. (\<pi>@\<^bsup>l\<^esup> \<pi>l) i \<noteq> \<pi> l\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>l
\<pi> l = \<pi>l 0
\<pi>l n = local.return
\<forall>i>0. \<pi>l i \<noteq> \<pi> l

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

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<pi>0': \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>l) 0 = \<pi>' 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>l\<^esup> \<pi>l) 0 = \<pi>' 0
[PROOF STEP]
unfolding cs_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>l\<^esup> \<pi>l) 0 = \<pi>' 0
[PROOF STEP]
using  \<pi>l \<pi>0
[PROOF STATE]
proof (prove)
using this:
\<pi> l = \<pi>l 0
\<pi> 0 = \<pi>' 0

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have csn: \<open>cs\<^bsup>\<pi>@\<^bsup>l\<^esup> \<pi>l\<^esup>  (l+n) = cs\<^bsup>\<pi>'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> (l + n) = cs\<^bsup>\<pi>'\<^esup> n'
[PROOF STEP]
using ret retl cs_return
[PROOF STATE]
proof (prove)
using this:
\<pi>' n' = local.return
(\<pi> @\<^bsup>l\<^esup> \<pi>l) (l + n) = local.return
?\<pi> ?n = local.return \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?n = [?\<pi> ?n]

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have eql: \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>l) =\<^bsub>l\<^esub> \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>l\<^esup> \<pi>l) =\<^bsub>l\<^esub> \<pi>
[PROOF STEP]
by (metis path_append_eq_up_to)
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>l\<^esup> \<pi>l) =\<^bsub>l\<^esub> \<pi>

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

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>0 < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
using nretl[unfolded \<pi>l] retn
[PROOF STATE]
proof (prove)
using this:
\<pi>l 0 \<noteq> local.return
\<pi>l n = local.return

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
hence ln: \<open>l < l + n\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have *: \<open>\<forall> k k'. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>  k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k \<longrightarrow> (\<pi> @\<^bsup>l\<^esup> \<pi>l) (Suc k) = \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k k'. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k \<longrightarrow> (\<pi> @\<^bsup>l\<^esup> \<pi>l) (Suc k) = \<pi>' (Suc k')
[PROOF STEP]
proof (rule,rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k k'. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k \<Longrightarrow> (\<pi> @\<^bsup>l\<^esup> \<pi>l) (Suc k) = \<pi>' (Suc k')
[PROOF STEP]
fix k k'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k k'. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k \<Longrightarrow> (\<pi> @\<^bsup>l\<^esup> \<pi>l) (Suc k) = \<pi>' (Suc k')
[PROOF STEP]
assume *: \<open>cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>  k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k

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

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

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using eql * cs_path_swap_le[OF ip path(1) eql,of \<open>k\<close>] cdi_path_swap_le[OF path(1) _ eql,of \<open>l\<close> \<open>k\<close>]
[PROOF STATE]
proof (prove)
using this:
k < l
(\<pi> @\<^bsup>l\<^esup> \<pi>l) =\<^bsub>l\<^esub> \<pi>
cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k
k \<le> l \<Longrightarrow> cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>\<^esup> k
\<lbrakk>l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k; l \<le> l\<rbrakk> \<Longrightarrow> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

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

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

goal (1 subgoal):
 1. \<And>k k'. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k \<Longrightarrow> (\<pi> @\<^bsup>l\<^esup> \<pi>l) (Suc k) = \<pi>' (Suc k')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi> (Suc k) = \<pi>' (Suc k')
[PROOF STEP]
show \<open>(\<pi> @\<^bsup>l\<^esup> \<pi>l) (Suc k) = \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc k) = \<pi>' (Suc k')

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k k'. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>\<rightarrow> k \<longrightarrow> (\<pi> @\<^bsup>l\<^esup> \<pi>l) (Suc k) = \<pi>' (Suc k')

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
obtain l' where \<open>cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup>  l = cs\<^bsup>\<pi>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using converged_cd_same_suc[OF ip path(2) \<pi>0' * ln csn]
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'

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

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>@\<^bsup>l\<^esup> \<pi>l\<^esup>  l = cs\<^bsup>\<pi>\<^esup> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> l = cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
using eql
[PROOF STATE]
proof (prove)
using this:
(\<pi> @\<^bsup>l\<^esup> \<pi>l) =\<^bsub>l\<^esub> \<pi>

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

goal (1 subgoal):
 1. \<pi> l \<noteq> local.return \<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> @\<^bsup>l\<^esup> \<pi>l\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> l = cs\<^bsup>\<pi>\<^esup> l
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
cs\<^bsup>\<pi> @\<^bsup>l\<^esup> \<pi>l\<^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_cd_diverge_return: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and init: \<open>\<pi> 0 = \<pi>' 0\<close>
and notin: \<open>\<not> (\<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l')\<close> and ret: \<open>\<pi>' m' = return\<close>
obtains k k' where \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close> \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>\<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using converged_cd_same_suc_return[OF path init _ ret, of \<open>l\<close>] notin
[PROOF STATE]
proof (prove)
using this:
\<forall>k k'. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k' \<and> l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longrightarrow> \<pi> (Suc k) = \<pi>' (Suc k') \<Longrightarrow> \<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
\<nexists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'

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