[STATEMENT]
lemma shifted_cs_eq_is_eq: assumes \<open>is_path \<pi>\<close> and \<open>is_path \<pi>'\<close> and \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close> and \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> n = cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> n'\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> (k+n) = cs\<^bsup>\<pi>'\<^esup> (k'+n')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>'\<^esup> (k' + n')
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
note path = assms(1,2)
[PROOF STATE]
proof (state)
this:
is_path \<pi>
is_path \<pi>'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
note csk = assms(3)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
note csn = assms(4)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
assume ne: \<open>cs\<^bsup>\<pi>\<^esup> (k+n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k'+n')\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n')

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have nretkn:\<open>\<pi> (k+n) \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (k + n) \<noteq> local.return
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> (k + n) = local.return \<Longrightarrow> False
[PROOF STEP]
assume 1:\<open>\<pi> (k+n) = return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> (k + n) = local.return

goal (1 subgoal):
 1. \<pi> (k + n) = local.return \<Longrightarrow> False
[PROOF STEP]
hence \<open>(\<pi>\<guillemotleft>k) n = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + n) = local.return

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

goal (1 subgoal):
 1. \<pi> (k + n) = local.return \<Longrightarrow> False
[PROOF STEP]
hence \<open>(\<pi>'\<guillemotleft>k') n' = return\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) n = local.return

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

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

goal (1 subgoal):
 1. \<pi> (k + n) = local.return \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<pi>' (k' + n') = return\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi>' \<guillemotleft> k') n' = local.return

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

goal (1 subgoal):
 1. \<pi> (k + n) = local.return \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k' + n') = local.return

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> (k + n) \<noteq> local.return

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

goal (1 subgoal):
 1. \<pi> k \<noteq> local.return
[PROOF STEP]
using term_path_stable[OF assms(1), of \<open>k\<close> \<open>k +n\<close>]
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + n) \<noteq> local.return
\<lbrakk>\<pi> k = local.return; k \<le> k + n\<rbrakk> \<Longrightarrow> \<pi> (k + n) = local.return

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have nretkn': \<open>\<pi>' (k'+n') \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (k' + n') \<noteq> local.return
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi>' (k' + n') = local.return \<Longrightarrow> False
[PROOF STEP]
assume 1:\<open>\<pi>' (k'+n') = return\<close>
[PROOF STATE]
proof (state)
this:
\<pi>' (k' + n') = local.return

goal (1 subgoal):
 1. \<pi>' (k' + n') = local.return \<Longrightarrow> False
[PROOF STEP]
hence \<open>(\<pi>'\<guillemotleft>k') n' = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k' + n') = local.return

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

goal (1 subgoal):
 1. \<pi>' (k' + n') = local.return \<Longrightarrow> False
[PROOF STEP]
hence \<open>(\<pi>\<guillemotleft>k) n = return\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi>' \<guillemotleft> k') n' = local.return

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

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

goal (1 subgoal):
 1. \<pi>' (k' + n') = local.return \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<pi> (k + n) = return\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) n = local.return

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

goal (1 subgoal):
 1. \<pi>' (k' + n') = local.return \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + n) = local.return

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi>' (k' + n') \<noteq> local.return

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

goal (1 subgoal):
 1. \<pi>' k' \<noteq> local.return
[PROOF STEP]
using term_path_stable[OF assms(2), of \<open>k'\<close> \<open>k' +n'\<close>]
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k' + n') \<noteq> local.return
\<lbrakk>\<pi>' k' = local.return; k' \<le> k' + n'\<rbrakk> \<Longrightarrow> \<pi>' (k' + n') = local.return

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have n0:\<open>n > 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> False
[PROOF STEP]
assume *: \<open>\<not> 0 < n\<close>
[PROOF STATE]
proof (state)
this:
\<not> 0 < n

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> 0 = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
using assms(3,4)
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < n
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>\<guillemotleft>k) 0 = (\<pi>'\<guillemotleft>k') 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) 0 = (\<pi>' \<guillemotleft> k') 0
[PROOF STEP]
using assms(3) last_cs path_shift_def
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i
?\<pi> \<guillemotleft> ?m = (\<lambda>n. ?\<pi> (?m + n))

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) 0 = (\<pi>' \<guillemotleft> k') 0
[PROOF STEP]
by (metis monoid_add_class.add.right_neutral)
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) 0 = (\<pi>' \<guillemotleft> k') 0

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 0 = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
using 1 cs_0
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) 0 = (\<pi>' \<guillemotleft> k') 0
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> 0 = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
cs\<^bsup>?\<pi>\<^esup> 0 = [?\<pi> 0]

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

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

goal (1 subgoal):
 1. n' = 0
[PROOF STEP]
using cs_inj[of \<open>\<pi>'\<guillemotleft>k'\<close> \<open>0\<close> \<open>n'\<close> ] * assms(2)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 0 = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
\<lbrakk>is_path (\<pi>' \<guillemotleft> k'); (\<pi>' \<guillemotleft> k') 0 \<noteq> local.return; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 0 = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'\<rbrakk> \<Longrightarrow> 0 = n'
\<not> 0 < n
is_path \<pi>'

goal (1 subgoal):
 1. n' = 0
[PROOF STEP]
by (metis path_shift_def assms(4) last_cs nretkn path_path_shift)
[PROOF STATE]
proof (state)
this:
n' = 0

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using ne * assms(3)
[PROOF STATE]
proof (prove)
using this:
n' = 0
cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n')
\<not> 0 < n
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have n0':\<open>n' > 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < n' \<Longrightarrow> False
[PROOF STEP]
assume *: \<open>\<not> 0 < n'\<close>
[PROOF STATE]
proof (state)
this:
\<not> 0 < n'

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 0 = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
[PROOF STEP]
using assms(3,4)
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < n'
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

goal (1 subgoal):
 1. \<not> 0 < n' \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>'\<guillemotleft>k') 0 = (\<pi>\<guillemotleft>k) 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>' \<guillemotleft> k') 0 = (\<pi> \<guillemotleft> k) 0
[PROOF STEP]
using assms(3) last_cs path_shift_def
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i
?\<pi> \<guillemotleft> ?m = (\<lambda>n. ?\<pi> (?m + n))

goal (1 subgoal):
 1. (\<pi>' \<guillemotleft> k') 0 = (\<pi> \<guillemotleft> k) 0
[PROOF STEP]
by (metis monoid_add_class.add.right_neutral)
[PROOF STATE]
proof (state)
this:
(\<pi>' \<guillemotleft> k') 0 = (\<pi> \<guillemotleft> k) 0

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> 0 = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
[PROOF STEP]
using 1 cs_0
[PROOF STATE]
proof (prove)
using this:
(\<pi>' \<guillemotleft> k') 0 = (\<pi> \<guillemotleft> k) 0
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 0 = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
cs\<^bsup>?\<pi>\<^esup> 0 = [?\<pi> 0]

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

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

goal (1 subgoal):
 1. n = 0
[PROOF STEP]
using cs_inj[of \<open>\<pi>\<guillemotleft>k\<close> \<open>0\<close> \<open>n\<close> ] * assms(1)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> 0 = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
\<lbrakk>is_path (\<pi> \<guillemotleft> k); (\<pi> \<guillemotleft> k) 0 \<noteq> local.return; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> 0 = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n\<rbrakk> \<Longrightarrow> 0 = n
\<not> 0 < n'
is_path \<pi>

goal (1 subgoal):
 1. n = 0
[PROOF STEP]
by (metis path_shift_def assms(4) last_cs nretkn path_path_shift)
[PROOF STATE]
proof (state)
this:
n = 0

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using ne * assms(3)
[PROOF STATE]
proof (prove)
using this:
n = 0
cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n')
\<not> 0 < n'
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < n'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have cdleswap': \<open>\<forall> j'<k'. (k'+n') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<longrightarrow> (\<exists>j<k. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<longrightarrow> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
[PROOF STEP]
proof (rule,rule,rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix j'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume jk': \<open>j'<k'\<close> and ncdj': \<open>(k'+n') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'\<close> and ne: \<open>\<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (state)
this:
j' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence kcdj': \<open>k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'\<close>
[PROOF STATE]
proof (prove)
using this:
j' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
[PROOF STEP]
using cr_wn'
[PROOF STATE]
proof (prove)
using this:
j' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
\<lbrakk>?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m; \<not> ?m' cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m; ?m < ?m'\<rbrakk> \<Longrightarrow> ?n < ?m'

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
[PROOF STEP]
obtain j where kcdj: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> and csj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
using this:
k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using csk cs_path_swap_cd path
[PROOF STATE]
proof (prove)
using this:
k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>'\<^esup> ?n'; ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; \<And>k'. \<lbrakk>?n' cd\<^bsup>?\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
is_path \<pi>
is_path \<pi>'

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence jk: \<open>j < k\<close>
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

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

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ncdn: \<open>\<not> (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
using ne csj jk
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
j < k

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain l' where lnocd': \<open>l' = n' \<or> n' cd\<^bsup>\<pi>'\<guillemotleft>k'\<^esup>\<rightarrow> l'\<close> and cslsing': \<open>cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> l' = [(\<pi>'\<guillemotleft>k') l']\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> n' = [(\<pi>'\<guillemotleft>k') n']\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [(\<pi>' \<guillemotleft> k') n']

goal (2 subgoals):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [(\<pi>' \<guillemotleft> k') n']

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of \<open>n'\<close>]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [(\<pi>' \<guillemotleft> k') n']
\<lbrakk>n' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> n'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [(\<pi>' \<guillemotleft> k') n']\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<noteq> [(\<pi>' \<guillemotleft> k') n']\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<noteq> [(\<pi>' \<guillemotleft> k') n']\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume *: \<open>cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> n' \<noteq> [(\<pi>'\<guillemotleft>k') n']\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<noteq> [(\<pi>' \<guillemotleft> k') n']

goal (1 subgoal):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<noteq> [(\<pi>' \<guillemotleft> k') n']\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<noteq> [(\<pi>' \<guillemotleft> k') n']
[PROOF STEP]
obtain x ys where \<open>cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> n' = [x]@ys@[(\<pi>'\<guillemotleft>k') n']\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<noteq> [(\<pi>' \<guillemotleft> k') n']

goal (1 subgoal):
 1. (\<And>x ys. cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [x] @ ys @ [(\<pi>' \<guillemotleft> k') n'] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_Cons append_Nil cs_length_g_one cs_length_one(1) neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [x] @ ys @ [(\<pi>' \<guillemotleft> k') n']

goal (1 subgoal):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<noteq> [(\<pi>' \<guillemotleft> k') n']\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [x] @ ys @ [(\<pi>' \<guillemotleft> k') n']
[PROOF STEP]
obtain l' where \<open>cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> l' = [x]\<close> and cdl': \<open>n' cd\<^bsup>\<pi>'\<guillemotleft>k'\<^esup>\<rightarrow> l'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [x] @ ys @ [(\<pi>' \<guillemotleft> k') n']

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [x]; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_split[of \<open>\<pi>'\<guillemotleft>k'\<close> \<open>n'\<close> \<open>Nil\<close> \<open>x\<close> \<open>ys\<close>]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [x] @ ys @ [(\<pi>' \<guillemotleft> k') n']
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' = [] @ [x] @ ys @ [(\<pi>' \<guillemotleft> k') n'] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> m = [] @ [x] \<and> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> m

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<noteq> [(\<pi>' \<guillemotleft> k') n']\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that cdl'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']
\<lbrakk>?l'1 = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> ?l'1; cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> ?l'1 = [(\<pi>' \<guillemotleft> k') ?l'1]\<rbrakk> \<Longrightarrow> thesis
n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']

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

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

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

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

goal (1 subgoal):
 1. k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
[PROOF STEP]
using jk' ncdj'
[PROOF STATE]
proof (prove)
using this:
l' \<le> n'
j' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'

goal (1 subgoal):
 1. k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
[PROOF STEP]
by (metis add_le_cancel_left cdi_prefix trans_less_add1)
[PROOF STATE]
proof (state)
this:
k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain l where lnocd: \<open>l = n \<or> n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> l\<close> and csl: \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> l = cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lnocd'
[PROOF STATE]
proof (prove)
using this:
l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; l' = n'\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>l' = n'\<close>
[PROOF STATE]
proof (state)
this:
l' = n'

goal (2 subgoals):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; l' = n'\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
l' = n'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using csn that[of \<open>n\<close>]
[PROOF STATE]
proof (prove)
using this:
l' = n'
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
\<lbrakk>n = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> n; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>n' cd\<^bsup>\<pi>'\<guillemotleft>k'\<^esup>\<rightarrow> l'\<close>
[PROOF STATE]
proof (state)
this:
n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'
[PROOF STEP]
obtain l where \<open>n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> l\<close> \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> l = cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
using this:
n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_path_swap_cd path csn
[PROOF STATE]
proof (prove)
using this:
n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>'\<^esup> ?n'; ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; \<And>k'. \<lbrakk>?n' cd\<^bsup>?\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
is_path \<pi>
is_path \<pi>'
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

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

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'
\<lbrakk>?l1 = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> ?l1; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> ?l1 = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have cslsing: \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> l = [(\<pi>\<guillemotleft>k) l]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]
[PROOF STEP]
using cslsing' last_cs csl last.simps
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'
last (?x # ?xs) = (if ?xs = [] then ?x else last ?xs)

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ln: \<open>l\<le>n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> n
[PROOF STEP]
using lnocd
[PROOF STATE]
proof (prove)
using this:
l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l

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

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence nretkl: \<open>\<pi> (k + l) \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
l \<le> n

goal (1 subgoal):
 1. \<pi> (k + l) \<noteq> local.return
[PROOF STEP]
using term_path_stable[of \<open>\<pi>\<close> \<open>k+l\<close> \<open>k+n\<close>] nretkn path(1)
[PROOF STATE]
proof (prove)
using this:
l \<le> n
\<lbrakk>is_path \<pi>; \<pi> (k + l) = local.return; k + l \<le> k + n\<rbrakk> \<Longrightarrow> \<pi> (k + n) = local.return
\<pi> (k + n) \<noteq> local.return
is_path \<pi>

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have *: \<open>n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> l \<Longrightarrow> k+n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k+l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l \<Longrightarrow> k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + l
[PROOF STEP]
using cd_path_shift[of \<open>k\<close> \<open>k+l\<close> \<open>\<pi>\<close> \<open>k+n\<close>] path(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k \<le> k + l; is_path \<pi>\<rbrakk> \<Longrightarrow> (k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + l) = (k + n - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> k + l - k)
is_path \<pi>

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ncdl: \<open>\<not> (k+l) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
using lnocd
[PROOF STATE]
proof (prove)
using this:
l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> False
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; l = n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using ncdn
[PROOF STATE]
proof (prove)
using this:
\<not> k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (2 subgoals):
 1. \<lbrakk>k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; l = n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using cd_trans ncdn *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i; ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j\<rbrakk> \<Longrightarrow> ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i
\<not> k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l \<Longrightarrow> k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + l

goal (1 subgoal):
 1. \<lbrakk>k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<exists> i\<in> {j..k+l}. \<pi> i = ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> k + l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

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

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<exists> i\<in> {k<..k+l}. \<pi> i = ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>{j..k + l}. \<pi> i = ipd (\<pi> j)

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

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

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<in>{k<..k + l}. \<pi> i = ipd (\<pi> j)
[PROOF STEP]
obtain i where ki: \<open>k < i\<close> and il: \<open>i \<le> k+l\<close> and ipdi: \<open>\<pi> i = ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>{k<..k + l}. \<pi> i = ipd (\<pi> j)

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

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

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

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

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) l pd\<rightarrow> ipd (\<pi> j)
[PROOF STEP]
using cs_single_pd_intermed[OF _ cslsing] path(1) path_path_shift
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) (i - k) = ipd (\<pi> j)
i - k \<le> l
\<lbrakk>is_path (\<pi> \<guillemotleft> k); ?k \<le> l\<rbrakk> \<Longrightarrow> (\<pi> \<guillemotleft> k) l pd\<rightarrow> (\<pi> \<guillemotleft> k) ?k
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) l pd\<rightarrow> ipd (\<pi> j)

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>\<guillemotleft>k) l = \<pi>' (k' + l')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) l = \<pi>' (k' + l')
[PROOF STEP]
using csl last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) l = \<pi>' (k' + l')

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> j = \<pi>' j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j = \<pi>' j'
[PROOF STEP]
using csj last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> k) l pd\<rightarrow> ipd (\<pi> j)
(\<pi> \<guillemotleft> k) l = \<pi>' (k' + l')
\<pi> j = \<pi>' j'
[PROOF STEP]
have \<open>\<pi>' (k'+l') pd\<rightarrow> ipd (\<pi>' j')\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) l pd\<rightarrow> ipd (\<pi> j)
(\<pi> \<guillemotleft> k) l = \<pi>' (k' + l')
\<pi> j = \<pi>' j'

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>' (k' + l') pd\<rightarrow> ipd (\<pi>' j')

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>ipd (\<pi>' j') pd\<rightarrow> \<pi>' (k'+l')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi>' j') pd\<rightarrow> \<pi>' (k' + l')
[PROOF STEP]
using ipd_pd_cd[OF lcdj']
[PROOF STATE]
proof (prove)
using this:
ipd (\<pi>' j') pd\<rightarrow> \<pi>' (k' + l')

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

goal (1 subgoal):
 1. \<And>j'. \<lbrakk>j' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi>' (k' + l') pd\<rightarrow> ipd (\<pi>' j')
ipd (\<pi>' j') pd\<rightarrow> \<pi>' (k' + l')
[PROOF STEP]
have \<open>\<pi>' (k'+l') = ipd (\<pi>' j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k' + l') pd\<rightarrow> ipd (\<pi>' j')
ipd (\<pi>' j') pd\<rightarrow> \<pi>' (k' + l')

goal (1 subgoal):
 1. \<pi>' (k' + l') = ipd (\<pi>' j')
[PROOF STEP]
using pd_antisym
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k' + l') pd\<rightarrow> ipd (\<pi>' j')
ipd (\<pi>' j') pd\<rightarrow> \<pi>' (k' + l')
\<lbrakk>?x pd\<rightarrow> ?y; ?y pd\<rightarrow> ?x\<rbrakk> \<Longrightarrow> ?x = ?y

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed

  \<comment> \<open>Symmetric version of the above statement\<close>
[PROOF STATE]
proof (state)
this:
\<forall>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<longrightarrow> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have cdleswap: \<open>\<forall> j<k. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> (\<exists>j'<k'. (k'+n') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
[PROOF STEP]
proof (rule,rule,rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume jk: \<open>j<k\<close> and ncdj: \<open>(k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> and ne: \<open>\<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (state)
this:
j < k
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
\<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence kcdj: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
using this:
j < k
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
\<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
using cr_wn'
[PROOF STATE]
proof (prove)
using this:
j < k
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
\<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
\<lbrakk>?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m; \<not> ?m' cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m; ?m < ?m'\<rbrakk> \<Longrightarrow> ?n < ?m'

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
obtain j' where kcdj': \<open>k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'\<close> and csj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using csk cs_path_swap_cd path
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>'\<^esup> ?n'; ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; \<And>k'. \<lbrakk>?n' cd\<^bsup>?\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
is_path \<pi>
is_path \<pi>'

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence jk': \<open>j' < k'\<close>
[PROOF STATE]
proof (prove)
using this:
k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

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

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ncdn': \<open>\<not> (k'+n') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
[PROOF STEP]
using ne csj jk'
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
j' < k'

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain l where lnocd: \<open>l = n \<or> n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> l\<close> and cslsing: \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> l = [(\<pi>\<guillemotleft>k) l]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> n = [(\<pi>\<guillemotleft>k) n]\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [(\<pi> \<guillemotleft> k) n]

goal (2 subgoals):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [(\<pi> \<guillemotleft> k) n]

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of \<open>n\<close>]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [(\<pi> \<guillemotleft> k) n]
\<lbrakk>n = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> n; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [(\<pi> \<guillemotleft> k) n]\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> [(\<pi> \<guillemotleft> k) n]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> [(\<pi> \<guillemotleft> k) n]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume *: \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> n \<noteq> [(\<pi>\<guillemotleft>k) n]\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> [(\<pi> \<guillemotleft> k) n]

goal (1 subgoal):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> [(\<pi> \<guillemotleft> k) n]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> [(\<pi> \<guillemotleft> k) n]
[PROOF STEP]
obtain x ys where \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> n = [x]@ys@[(\<pi>\<guillemotleft>k) n]\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> [(\<pi> \<guillemotleft> k) n]

goal (1 subgoal):
 1. (\<And>x ys. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [x] @ ys @ [(\<pi> \<guillemotleft> k) n] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_Cons append_Nil cs_length_g_one cs_length_one(1) neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [x] @ ys @ [(\<pi> \<guillemotleft> k) n]

goal (1 subgoal):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> [(\<pi> \<guillemotleft> k) n]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [x] @ ys @ [(\<pi> \<guillemotleft> k) n]
[PROOF STEP]
obtain l where \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> l = [x]\<close> and cdl: \<open>n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [x] @ ys @ [(\<pi> \<guillemotleft> k) n]

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [x]; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_split[of \<open>\<pi>\<guillemotleft>k\<close> \<open>n\<close> \<open>Nil\<close> \<open>x\<close> \<open>ys\<close>]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [x] @ ys @ [(\<pi> \<guillemotleft> k) n]
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = [] @ [x] @ ys @ [(\<pi> \<guillemotleft> k) n] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> m = [] @ [x] \<and> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> m

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]
[PROOF STEP]
using last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [x]
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

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

goal (1 subgoal):
 1. \<lbrakk>\<And>l. \<lbrakk>l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> [(\<pi> \<guillemotleft> k) n]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that cdl
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]
\<lbrakk>?l1 = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> ?l1; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> ?l1 = [(\<pi> \<guillemotleft> k) ?l1]\<rbrakk> \<Longrightarrow> thesis
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain l' where lnocd': \<open>l' = n' \<or> n' cd\<^bsup>\<pi>'\<guillemotleft>k'\<^esup>\<rightarrow> l'\<close> and csl: \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> l = cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lnocd
[PROOF STATE]
proof (prove)
using this:
l = n \<or> n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; l = n\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>l = n\<close>
[PROOF STATE]
proof (state)
this:
l = n

goal (2 subgoals):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; l = n\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
l = n

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using csn that[of \<open>n'\<close>]
[PROOF STATE]
proof (prove)
using this:
l = n
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
\<lbrakk>n' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> n'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>n cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (state)
this:
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. \<lbrakk>\<And>l'. \<lbrakk>l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis; n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l
[PROOF STEP]
obtain l' where \<open>n' cd\<^bsup>\<pi>'\<guillemotleft>k'\<^esup>\<rightarrow> l'\<close> \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> l = cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_path_swap_cd path csn
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> l
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>'\<^esup> ?n'; ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; \<And>k'. \<lbrakk>?n' cd\<^bsup>?\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
is_path \<pi>
is_path \<pi>'
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

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

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'
\<lbrakk>?l'1 = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> ?l'1; cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> ?l'1\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have cslsing': \<open>cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> l' = [(\<pi>'\<guillemotleft>k') l']\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l' = [(\<pi>' \<guillemotleft> k') l']
[PROOF STEP]
using cslsing last_cs csl last.simps
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = [(\<pi> \<guillemotleft> k) l]
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'
last (?x # ?xs) = (if ?xs = [] then ?x else last ?xs)

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ln': \<open>l'\<le>n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' \<le> n'
[PROOF STEP]
using lnocd'
[PROOF STATE]
proof (prove)
using this:
l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'

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

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence nretkl': \<open>\<pi>' (k' + l') \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
l' \<le> n'

goal (1 subgoal):
 1. \<pi>' (k' + l') \<noteq> local.return
[PROOF STEP]
using term_path_stable[of \<open>\<pi>'\<close> \<open>k'+l'\<close> \<open>k'+n'\<close>] nretkn' path(2)
[PROOF STATE]
proof (prove)
using this:
l' \<le> n'
\<lbrakk>is_path \<pi>'; \<pi>' (k' + l') = local.return; k' + l' \<le> k' + n'\<rbrakk> \<Longrightarrow> \<pi>' (k' + n') = local.return
\<pi>' (k' + n') \<noteq> local.return
is_path \<pi>'

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have *: \<open>n' cd\<^bsup>\<pi>'\<guillemotleft>k'\<^esup>\<rightarrow> l' \<Longrightarrow> k'+n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'+l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l' \<Longrightarrow> k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' + l'
[PROOF STEP]
using cd_path_shift[of \<open>k'\<close> \<open>k'+l'\<close> \<open>\<pi>'\<close> \<open>k'+n'\<close>] path(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k' \<le> k' + l'; is_path \<pi>'\<rbrakk> \<Longrightarrow> (k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' + l') = (k' + n' - k' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> k' + l' - k')
is_path \<pi>'

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ncdl': \<open>\<not> (k'+l') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<Longrightarrow> False
[PROOF STEP]
using lnocd'
[PROOF STATE]
proof (prove)
using this:
l' = n' \<or> n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<Longrightarrow> False
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; l' = n'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using ncdn'
[PROOF STATE]
proof (prove)
using this:
\<not> k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'

goal (2 subgoals):
 1. \<lbrakk>k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; l' = n'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using cd_trans ncdn' *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i; ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j\<rbrakk> \<Longrightarrow> ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?i
\<not> k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l' \<Longrightarrow> k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k' + l'

goal (1 subgoal):
 1. \<lbrakk>k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; n' cd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<exists> i'\<in> {j'..k'+l'}. \<pi>' i' = ipd (\<pi>' j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> k' + l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'

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

goal (1 subgoal):
 1. \<exists>i'\<in>{j'..k' + l'}. \<pi>' i' = ipd (\<pi>' j')
[PROOF STEP]
using path(2) jk' nretkl'
[PROOF STATE]
proof (prove)
using this:
\<not> (is_path \<pi>' \<and> j' < k' + l' \<and> \<pi>' (k' + l') \<noteq> local.return \<and> (\<forall>j\<in>{j'..k' + l'}. \<pi>' j \<noteq> ipd (\<pi>' j')))
is_path \<pi>'
j' < k'
\<pi>' (k' + l') \<noteq> local.return

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<exists> i'\<in> {k'<..k'+l'}. \<pi>' i' = ipd (\<pi>' j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>i'\<in>{j'..k' + l'}. \<pi>' i' = ipd (\<pi>' j')

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

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

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i'\<in>{k'<..k' + l'}. \<pi>' i' = ipd (\<pi>' j')
[PROOF STEP]
obtain i' where ki': \<open>k' < i'\<close> and il': \<open>i' \<le> k'+l'\<close> and ipdi: \<open>\<pi>' i' = ipd (\<pi>' j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>i'\<in>{k'<..k' + l'}. \<pi>' i' = ipd (\<pi>' j')

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

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

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

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

goal (1 subgoal):
 1. (\<pi>' \<guillemotleft> k') l' pd\<rightarrow> ipd (\<pi>' j')
[PROOF STEP]
using cs_single_pd_intermed[OF _ cslsing'] path(2) path_path_shift
[PROOF STATE]
proof (prove)
using this:
(\<pi>' \<guillemotleft> k') (i' - k') = ipd (\<pi>' j')
i' - k' \<le> l'
\<lbrakk>is_path (\<pi>' \<guillemotleft> k'); ?k \<le> l'\<rbrakk> \<Longrightarrow> (\<pi>' \<guillemotleft> k') l' pd\<rightarrow> (\<pi>' \<guillemotleft> k') ?k
is_path \<pi>'
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi>' \<guillemotleft> k') l' pd\<rightarrow> ipd (\<pi>' j')

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>'\<guillemotleft>k') l' = \<pi> (k + l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>' \<guillemotleft> k') l' = \<pi> (k + l)
[PROOF STEP]
using csl last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> l = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> l'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi>' \<guillemotleft> k') l' = \<pi> (k + l)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi>' j' = \<pi> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' j' = \<pi> j
[PROOF STEP]
using csj last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<pi>' \<guillemotleft> k') l' pd\<rightarrow> ipd (\<pi>' j')
(\<pi>' \<guillemotleft> k') l' = \<pi> (k + l)
\<pi>' j' = \<pi> j
[PROOF STEP]
have \<open>\<pi> (k+l) pd\<rightarrow> ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi>' \<guillemotleft> k') l' pd\<rightarrow> ipd (\<pi>' j')
(\<pi>' \<guillemotleft> k') l' = \<pi> (k + l)
\<pi>' j' = \<pi> j

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> (k + l) pd\<rightarrow> ipd (\<pi> j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>ipd (\<pi> j) pd\<rightarrow> \<pi> (k+l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> j) pd\<rightarrow> \<pi> (k + l)
[PROOF STEP]
using ipd_pd_cd[OF lcdj]
[PROOF STATE]
proof (prove)
using this:
ipd (\<pi> j) pd\<rightarrow> \<pi> (k + l)

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; \<not> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> (k + l) pd\<rightarrow> ipd (\<pi> j)
ipd (\<pi> j) pd\<rightarrow> \<pi> (k + l)
[PROOF STEP]
have \<open>\<pi> (k+l) = ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + l) pd\<rightarrow> ipd (\<pi> j)
ipd (\<pi> j) pd\<rightarrow> \<pi> (k + l)

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

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

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

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

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

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have cdle: \<open>\<exists>j. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k\<close> (is \<open>\<exists> j. ?P j\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> (\<exists>j. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k

goal (1 subgoal):
 1. \<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k \<Longrightarrow> False
[PROOF STEP]
hence allge: \<open>\<forall>j. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> k \<le> j\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k

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

goal (1 subgoal):
 1. \<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k \<Longrightarrow> False
[PROOF STEP]
have allge': \<open>\<forall>j'. (k'+n') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<longrightarrow> k' \<le> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<longrightarrow> k' \<le> j'
[PROOF STEP]
proof (rule, rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> k' \<le> j'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix j'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<not> k' \<le> j'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume *: \<open>k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'\<close> and \<open>\<not> k' \<le> j'\<close>
[PROOF STATE]
proof (state)
this:
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<not> k' \<le> j'

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

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j < k; k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cdleswap'
[PROOF STATE]
proof (prove)
using this:
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<not> k' \<le> j'
\<forall>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<longrightarrow> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using allge
[PROOF STATE]
proof (prove)
using this:
j < k
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
\<forall>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> k \<le> j

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

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

goal (1 subgoal):
 1. \<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k \<Longrightarrow> False
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
[PROOF STEP]
using cs_split_shift_nocd[OF assms(1) _ allge] n0
[PROOF STATE]
proof (prove)
using this:
k < k + n \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (k + n - k)
0 < n

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

goal (1 subgoal):
 1. \<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n

goal (1 subgoal):
 1. \<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k \<Longrightarrow> False
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
using cs_split_shift_nocd[OF assms(2) _ allge'] n0'
[PROOF STATE]
proof (prove)
using this:
k' < k' + n' \<Longrightarrow> cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> (k' + n' - k')
0 < n'

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

goal (1 subgoal):
 1. \<nexists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

goal (1 subgoal):
 1. False
[PROOF STEP]
using ne assms(4)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n')
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
define j where  \<open>j == GREATEST j. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k\<close>
[PROOF STATE]
proof (state)
this:
j \<equiv> GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have cdj:\<open>(k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> and jk: \<open>j < k\<close> and jge:\<open>\<forall> j'< k. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j &&& j < k &&& \<forall>j'<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
 2. j < k
 3. \<forall>j'<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j
[PROOF STEP]
have bound: \<open>\<forall> y. ?P y \<longrightarrow> y \<le> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> y < k \<longrightarrow> y \<le> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> y < k \<longrightarrow> y \<le> k

goal (3 subgoals):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
 2. j < k
 3. \<forall>j'<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j
[PROOF STEP]
show \<open>(k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
using GreatestI_nat[of \<open>?P\<close>] j_def bound cdle
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k \<and> ?k < k; \<And>y. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> y < k \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k) \<and> (GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k) < k
j \<equiv> GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k
\<forall>y. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> y < k \<longrightarrow> y \<le> k
\<exists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k

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

goal (2 subgoals):
 1. j < k
 2. \<forall>j'<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j
[PROOF STEP]
show \<open>j < k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < k
[PROOF STEP]
using GreatestI_nat[of \<open>?P\<close>] bound j_def cdle
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k \<and> ?k < k; \<And>y. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> y < k \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k) \<and> (GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k) < k
\<forall>y. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> y < k \<longrightarrow> y \<le> k
j \<equiv> GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k
\<exists>j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k

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

goal (1 subgoal):
 1. \<forall>j'<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j
[PROOF STEP]
show \<open>\<forall> j'< k. (k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j'<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j
[PROOF STEP]
using Greatest_le_nat[of \<open>?P\<close>] bound j_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k \<and> ?k < k; \<And>y. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> y < k \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> ?k \<le> (GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k)
\<forall>y. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> y < k \<longrightarrow> y \<le> k
j \<equiv> GREATEST j. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> j < k

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
obtain j' where cdj':\<open>(k'+n') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'\<close> and csj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close>  and jk': \<open>j' < k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'; j' < k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cdleswap cdj jk
[PROOF STATE]
proof (prove)
using this:
\<forall>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> (\<exists>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
j < k

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have jge':\<open>\<forall> i'< k'. (k'+n') cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i' \<longrightarrow> i' \<le> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i' \<longrightarrow> i' \<le> j'
[PROOF STEP]
proof(rule,rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> i' \<le> j'
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> i' \<le> j'
[PROOF STEP]
assume ik': \<open>i' < k'\<close> and cdi': \<open>k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<close>
[PROOF STATE]
proof (state)
this:
i' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> i' \<le> j'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'
[PROOF STEP]
obtain i where cdi:\<open>(k+n) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> and csi: \<open> cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> i\<close> and ik: \<open>i<k\<close>
[PROOF STATE]
proof (prove)
using this:
i' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i; cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> i; i < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cdleswap'
[PROOF STATE]
proof (prove)
using this:
i' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'
\<forall>j'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<longrightarrow> (\<exists>j<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

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

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> i' \<le> j'
[PROOF STEP]
have ij: \<open>i \<le> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j
[PROOF STEP]
using jge cdi ik
[PROOF STATE]
proof (prove)
using this:
\<forall>j'<k. k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
i < k

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

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' < k'; k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> i' \<le> j'
[PROOF STEP]
show \<open>i' \<le> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<le> j'
[PROOF STEP]
using cs_order_le[OF assms(1,2) csi[symmetric] csj _ ij] cd_not_ret[OF cdi]
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return \<Longrightarrow> i' \<le> j'
\<pi> i \<noteq> local.return

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i'<k'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i' \<longrightarrow> i' \<le> j'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
[PROOF STEP]
using  cs_split_shift_cd[OF cdj jk _ jge] n0
[PROOF STATE]
proof (prove)
using this:
k < k + n \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (k + n - k)
0 < n

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>'\<^esup> j' @ cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>'\<^esup> j' @ cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
using  cs_split_shift_cd[OF cdj' jk' _ jge'] n0'
[PROOF STATE]
proof (prove)
using this:
k' < k' + n' \<Longrightarrow> cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>'\<^esup> j' @ cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> (k' + n' - k')
0 < n'

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n') \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>'\<^esup> j' @ cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> (k+n) = cs\<^bsup>\<pi>'\<^esup> (k'+n')\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>'\<^esup> j' @ cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>'\<^esup> (k' + n')
[PROOF STEP]
using csj assms(4)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n
cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>'\<^esup> j' @ cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using ne
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>'\<^esup> (k' + n')
cs\<^bsup>\<pi>\<^esup> (k + n) \<noteq> cs\<^bsup>\<pi>'\<^esup> (k' + n')

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

goal:
No subgoals!
[PROOF STEP]
qed