[STATEMENT]
lemma cs_eq_is_eq_shifted: 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>\<^esup> (k+n) = cs\<^bsup>\<pi>'\<^esup> (k'+n')\<close> shows \<open>cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> n = cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<Longrightarrow> False
[PROOF STEP]
assume ne: \<open>cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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 2:\<open>\<pi>' (k'+n') = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + n) = local.return

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

goal (1 subgoal):
 1. \<pi>' (k' + n') = local.return
[PROOF STEP]
by metis
[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> \<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 &&& (\<pi>' \<guillemotleft> k') n' = local.return
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k' + n') = local.return
\<pi> (k + n) = local.return

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

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

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

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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 2:\<open>\<pi> (k+n) = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k' + n') = local.return

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

goal (1 subgoal):
 1. \<pi> (k + n) = local.return
[PROOF STEP]
by metis
[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> \<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 &&& (\<pi>' \<guillemotleft> k') n' = local.return
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + n) = local.return
\<pi>' (k' + n') = local.return

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

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

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

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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 \<open>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> (k'+ n')\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < n

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> (k' + 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>\<^esup> (k + n) = cs\<^bsup>\<pi>'\<^esup> (k' + n')

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

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

goal (1 subgoal):
 1. n = 0 &&& n' = 0
[PROOF STEP]
using cs_inj[OF assms(2) nretkn', of \<open>k'\<close>] *
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> (k' + n')
cs\<^bsup>\<pi>'\<^esup> (k' + n') = cs\<^bsup>\<pi>'\<^esup> k' \<Longrightarrow> k' + n' = k'
\<not> 0 < n

goal (1 subgoal):
 1. n = 0 &&& n' = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = 0
n' = 0

goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> False
[PROOF STEP]
have \<open>cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
unfolding n0 cs_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(\<pi> \<guillemotleft> k) 0] = [(\<pi>' \<guillemotleft> k') 0]
[PROOF STEP]
by (auto , metis last_cs assms(3))
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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 \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> (k+ n)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < n'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> (k + 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>\<^esup> (k + n) = cs\<^bsup>\<pi>'\<^esup> (k' + n')

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

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

goal (1 subgoal):
 1. n = 0 &&& n' = 0
[PROOF STEP]
using cs_inj[OF assms(1) nretkn, of \<open>k\<close>] *
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> (k + n)
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>\<^esup> k \<Longrightarrow> k + n = k
\<not> 0 < n'

goal (1 subgoal):
 1. n = 0 &&& n' = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = 0
n' = 0

goal (1 subgoal):
 1. \<not> 0 < n' \<Longrightarrow> False
[PROOF STEP]
have \<open>cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
unfolding n0 cs_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(\<pi> \<guillemotleft> k) 0] = [(\<pi>' \<guillemotleft> k') 0]
[PROOF STEP]
by (auto , metis last_cs assms(3))
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<Longrightarrow> k' \<le> j'
[PROOF STEP]
fix j'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<Longrightarrow> k' \<le> j'
[PROOF STEP]
assume *: \<open>k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'\<close>
[PROOF STATE]
proof (state)
this:
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'

goal (1 subgoal):
 1. \<And>j'. k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' \<Longrightarrow> k' \<le> j'
[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>
[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'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_path_swap_cd[OF assms(2,1) assms(4)[symmetric] *]
[PROOF STATE]
proof (prove)
using this:
(\<And>k'. \<lbrakk>k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k'; cs\<^bsup>\<pi>'\<^esup> j' = cs\<^bsup>\<pi>\<^esup> k'\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

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

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

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

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

goal (1 subgoal):
 1. k' \<le> j'
[PROOF STEP]
using cs_order_le[OF assms(1,2,3) csj nretk]
[PROOF STATE]
proof (prove)
using this:
k \<le> j
k \<le> j \<Longrightarrow> k' \<le> j'

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

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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>'\<^esup> (k' + 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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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>] 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. 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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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>
[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'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_path_swap_cd assms cdj
[PROOF STATE]
proof (prove)
using this:
\<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>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
cs\<^bsup>\<pi>\<^esup> (k + n) = cs\<^bsup>\<pi>'\<^esup> (k' + n')
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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>
[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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_path_swap_cd[OF assms(2,1) assms(4)[symmetric]]
[PROOF STATE]
proof (prove)
using this:
i' < k'
k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'
\<lbrakk>k' + n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?k; \<And>k'. \<lbrakk>k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k'; cs\<^bsup>\<pi>'\<^esup> ?k = cs\<^bsup>\<pi>\<^esup> k'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k + n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> 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]
have nreti': \<open>\<pi>' i' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return
[PROOF STEP]
by (metis cd_not_ret cdi')
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<noteq> local.return

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 ik: \<open>i < k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < k
[PROOF STEP]
using cs_order[OF assms(2,1) csi _ nreti' ik'] assms(3)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> ?j' \<Longrightarrow> i < ?j'
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'

goal (1 subgoal):
 1. i < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<Longrightarrow> False
[PROOF STEP]
have jk': \<open>j' < k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j' < k'
[PROOF STEP]
using cs_order[OF assms(1,2) csj assms(3) cd_not_ret[OF cdj] jk]
[PROOF STATE]
proof (prove)
using this:
j' < k'

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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>\<guillemotleft>k\<^esup> n = cs\<^bsup>\<pi>'\<guillemotleft>k'\<^esup> 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> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> 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>\<^esup> (k + n) = cs\<^bsup>\<pi>'\<^esup> (k' + n')

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'
[PROOF STEP]
by auto
[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> \<guillemotleft> k\<^esup> n \<noteq> cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n' \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> n = cs\<^bsup>\<pi>' \<guillemotleft> k'\<^esup> n'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma converged_cd_diverge_cs: assumes \<open>is_path \<pi>\<close> and \<open>is_path \<pi>'\<close> and \<open>cs\<^bsup>\<pi>\<^esup> j  = cs\<^bsup>\<pi>'\<^esup> j'\<close> and \<open>j<l\<close> and \<open>\<not> (\<exists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l')\<close> and \<open>l < m\<close> and \<open>cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<close>
obtains k k' where \<open>j\<le>k\<close> \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close> and \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>is_path (\<pi>\<guillemotleft>j)\<close> \<open>is_path (\<pi>'\<guillemotleft>j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> j) &&& is_path (\<pi>' \<guillemotleft> j')
[PROOF STEP]
using assms(1,2) path_path_shift
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)

goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> j) &&& is_path (\<pi>' \<guillemotleft> j')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> j)
is_path (\<pi>' \<guillemotleft> j')

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> j)
is_path (\<pi>' \<guillemotleft> j')

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>(\<pi>\<guillemotleft>j) 0 = (\<pi>'\<guillemotleft>j') 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> j) 0 = (\<pi>' \<guillemotleft> j') 0
[PROOF STEP]
using assms(3) 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> \<guillemotleft> j) 0 = (\<pi>' \<guillemotleft> j') 0
[PROOF STEP]
by (metis path_shift_def add.right_neutral)
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> j) 0 = (\<pi>' \<guillemotleft> j') 0

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> j) 0 = (\<pi>' \<guillemotleft> j') 0

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<not>(\<exists>l'. cs\<^bsup>\<pi>\<guillemotleft>j\<^esup> (l-j) = cs\<^bsup>\<pi>'\<guillemotleft>j'\<^esup> l')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l' \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<exists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'\<close>
[PROOF STATE]
proof (state)
this:
\<exists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'
[PROOF STEP]
obtain l' where csl: \<open>cs\<^bsup>\<pi>\<guillemotleft>j\<^esup> (l - j) = cs\<^bsup>\<pi>'\<guillemotleft>j'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'

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

goal (1 subgoal):
 1. \<exists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l' \<Longrightarrow> False
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> (j' + l')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> (j' + l')
[PROOF STEP]
using shifted_cs_eq_is_eq[OF assms(1,2,3) csl] assms(4)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (j + (l - j)) = cs\<^bsup>\<pi>'\<^esup> (j' + l')
j < l

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> (j' + l')
\<nexists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nexists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>l-j < m-j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l - j < m - j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
j < l
\<nexists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'

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

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l - j < m - j

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<pi> j \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j \<noteq> local.return
[PROOF STEP]
using cs_return assms(1-5) term_path_stable
[PROOF STATE]
proof (prove)
using this:
?\<pi> ?n = local.return \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?n = [?\<pi> ?n]
is_path \<pi>
is_path \<pi>'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
j < l
\<nexists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?\<pi> ?j = local.return

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

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

goal (1 subgoal):
 1. j' < m'
[PROOF STEP]
using cs_order[OF assms(1,2,3,7)] assms
[PROOF STATE]
proof (prove)
using this:
\<pi> j \<noteq> local.return
\<lbrakk>\<pi> j \<noteq> local.return; j < m\<rbrakk> \<Longrightarrow> j' < m'
is_path \<pi>
is_path \<pi>'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
j < l
\<nexists>l'. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (m - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> (m' - j')
[PROOF STEP]
using cs_eq_is_eq_shifted[OF assms(1,2,3),of \<open>m-j\<close> \<open>m'-j'\<close>] assms(4,6,7)
[PROOF STATE]
proof (prove)
using this:
j' < m'
cs\<^bsup>\<pi>\<^esup> (j + (m - j)) = cs\<^bsup>\<pi>'\<^esup> (j' + (m' - j')) \<Longrightarrow> cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (m - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> (m' - j')
j < l
l < m
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'

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

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> \<guillemotleft> j)
is_path (\<pi>' \<guillemotleft> j')
(\<pi> \<guillemotleft> j) 0 = (\<pi>' \<guillemotleft> j') 0
\<nexists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'
l - j < m - j
cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (m - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> (m' - j')
[PROOF STEP]
obtain k k' where csk: \<open>cs\<^bsup>\<pi>\<guillemotleft>j\<^esup> k = cs\<^bsup>\<pi>'\<guillemotleft>j'\<^esup> k'\<close> and lcdk: \<open>l-j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> k\<close> and suc:\<open>(\<pi>\<guillemotleft>j) (Suc k) \<noteq> (\<pi>'\<guillemotleft>j') (Suc k')\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> j)
is_path (\<pi>' \<guillemotleft> j')
(\<pi> \<guillemotleft> j) 0 = (\<pi>' \<guillemotleft> j') 0
\<nexists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'
l - j < m - j
cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (m - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> (m' - j')

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> k = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> k'; l - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k; (\<pi> \<guillemotleft> j) (Suc k) \<noteq> (\<pi>' \<guillemotleft> j') (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using converged_cd_diverge
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> j)
is_path (\<pi>' \<guillemotleft> j')
(\<pi> \<guillemotleft> j) 0 = (\<pi>' \<guillemotleft> j') 0
\<nexists>l'. cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (l - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> l'
l - j < m - j
cs\<^bsup>\<pi> \<guillemotleft> j\<^esup> (m - j) = cs\<^bsup>\<pi>' \<guillemotleft> j'\<^esup> (m' - j')
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> 0 = ?\<pi>' 0; \<nexists>l'. cs\<^bsup>?\<pi>\<^esup> ?l = cs\<^bsup>?\<pi>'\<^esup> l'; ?l < ?m; cs\<^bsup>?\<pi>\<^esup> ?m = cs\<^bsup>?\<pi>'\<^esup> ?m'; \<And>k k'. \<lbrakk>cs\<^bsup>?\<pi>\<^esup> k = cs\<^bsup>?\<pi>'\<^esup> k'; ?l cd\<^bsup>?\<pi>\<^esup>\<rightarrow> k; ?\<pi> (Suc k) \<noteq> ?\<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> (j+k) = cs\<^bsup>\<pi>'\<^esup> (j'+k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (j + k) = cs\<^bsup>\<pi>'\<^esup> (j' + k')
[PROOF STEP]
using shifted_cs_eq_is_eq[OF assms(1-3) csk]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (j + k) = cs\<^bsup>\<pi>'\<^esup> (j' + k')

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

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

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j+k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j + k
[PROOF STEP]
using lcdk assms(1,2,4)
[PROOF STATE]
proof (prove)
using this:
l - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k
is_path \<pi>
is_path \<pi>'
j < l

goal (1 subgoal):
 1. l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j + k
[PROOF STEP]
by (metis add.commute add_diff_cancel_right' cd_path_shift le_add1)
[PROOF STATE]
proof (state)
this:
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j + k

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

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

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

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

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>j \<le> j+k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> j + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<le> j + k

goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>j \<le> k; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'; l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<pi> (Suc k) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> (j + k) = cs\<^bsup>\<pi>'\<^esup> (j' + k')
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j + k
\<pi> (Suc (j + k)) \<noteq> \<pi>' (Suc (j' + k'))
j \<le> j + k
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (j + k) = cs\<^bsup>\<pi>'\<^esup> (j' + k')
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> j + k
\<pi> (Suc (j + k)) \<noteq> \<pi>' (Suc (j' + k'))
j \<le> j + k

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_ipd_conv: assumes csk: \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close> and ipd: \<open>\<pi> l = ipd (\<pi> k)\<close> \<open>\<pi>' l' = ipd(\<pi>' k')\<close>
  and nipd: \<open>\<forall>n\<in>{k..<l}. \<pi> n \<noteq> ipd (\<pi> k)\<close> \<open>\<forall>n'\<in>{k'..<l'}. \<pi>' n' \<noteq> ipd (\<pi>' k')\<close> and kl: \<open>k < l\<close> \<open>k' < l'\<close>
shows \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
using cs_ipd[OF ipd(1) nipd(1) kl(1)] cs_ipd[OF ipd(2) nipd(2) kl(2)] csk ipd
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> l = filter (\<lambda>n. ipd n \<noteq> \<pi> l) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> l]
cs\<^bsup>\<pi>'\<^esup> l' = filter (\<lambda>n. ipd n \<noteq> \<pi>' l') (cs\<^bsup>\<pi>'\<^esup> k') @ [\<pi>' l']
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
\<pi> l = ipd (\<pi> k)
\<pi>' l' = ipd (\<pi>' k')

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
by (metis (no_types) last_cs)


[STATEMENT]
lemma cp_eq_cs: assumes \<open>((\<sigma>,k),(\<sigma>',k'))\<in>cp\<close> shows \<open>cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
[PROOF STEP]
apply(induction rule: cp.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> \<sigma>' n n' h. \<lbrakk>\<sigma> =\<^sub>L \<sigma>'; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; h \<in> local.reads (path \<sigma> n); (\<sigma>\<^bsup>n\<^esup>) h \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) h; \<forall>k<n. h \<notin> local.writes (path \<sigma> k); \<forall>k'<n'. h \<notin> local.writes (path \<sigma>' k')\<rbrakk> \<Longrightarrow> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'; n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k; n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k'; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v\<rbrakk> \<Longrightarrow> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'; n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'\<rbrakk> \<Longrightarrow> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'\<rbrakk> \<Longrightarrow> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cd_cs_swap: assumes \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>'\<^esup> l'\<close> \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close> shows \<open>l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
have \<open>\<exists> i. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
using assms(1) excd_impl_exicd
[PROOF STATE]
proof (prove)
using this:
l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<exists>k. ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> \<exists>k. ?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> k

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
from cd_in_cs[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ ns @ [\<pi> l]
[PROOF STEP]
obtain ys where csl: \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ ys @ [\<pi> l]\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>ns. cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ ns @ [\<pi> l]

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

goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
obtain xs where csk: \<open>cs\<^bsup>\<pi>\<^esup> k = xs@[\<pi> k]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. cs\<^bsup>\<pi>\<^esup> k = xs @ [\<pi> k] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_butlast_last_id cs_not_nil last_cs)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = xs @ [\<pi> k]

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

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

goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
have csl': \<open>cs\<^bsup>\<pi>'\<^esup> l' = xs@[\<pi> k]@ys@[\<pi>' l']\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> l' = xs @ [\<pi> k] @ ys @ [\<pi>' l']
[PROOF STEP]
by (metis \<pi>l append_eq_appendI assms(2) csk csl)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> l' = xs @ [\<pi> k] @ ys @ [\<pi>' l']

goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
from cs_split[of \<open>\<pi>'\<close> \<open>l'\<close> \<open>xs\<close> \<open>\<pi> k\<close> \<open>ys\<close>]
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>'\<^esup> l' = xs @ [\<pi> k] @ ys @ [\<pi>' l'] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>'\<^esup> m = xs @ [\<pi> k] \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m
[PROOF STEP]
obtain m where csm: \<open>cs\<^bsup>\<pi>'\<^esup> m = xs @ [\<pi> k]\<close> and lcdm: \<open>l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> l' = xs @ [\<pi> k] @ ys @ [\<pi>' l'] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>'\<^esup> m = xs @ [\<pi> k] \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m

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

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

goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
have csm': \<open>cs\<^bsup>\<pi>'\<^esup> m = cs\<^bsup>\<pi>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> m = cs\<^bsup>\<pi>'\<^esup> k'
[PROOF STEP]
by (metis assms(3) csk csm)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> m = cs\<^bsup>\<pi>'\<^esup> k'

goal (1 subgoal):
 1. l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
[PROOF STEP]
have \<open>\<pi>' m \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' m \<noteq> local.return
[PROOF STEP]
using lcdm
[PROOF STATE]
proof (prove)
using this:
l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m

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

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

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

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

goal (1 subgoal):
 1. m = k'
[PROOF STEP]
using cs_inj path' csm'
[PROOF STATE]
proof (prove)
using this:
\<pi>' m \<noteq> local.return
\<lbrakk>is_path ?\<pi>; ?\<pi> ?n \<noteq> local.return; cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>\<^esup> ?n'\<rbrakk> \<Longrightarrow> ?n = ?n'
is_path \<pi>'
cs\<^bsup>\<pi>'\<^esup> m = cs\<^bsup>\<pi>'\<^esup> k'

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kth_obs_not_none: assumes \<open>is_kth_obs (path \<sigma>) k i\<close> obtains a where \<open>obsp \<sigma> i = Some a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. obsp \<sigma> i = Some a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_kth_obs (path \<sigma>) k i

goal (1 subgoal):
 1. (\<And>a. obsp \<sigma> i = Some a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_kth_obs_def obsp_def
[PROOF STATE]
proof (prove)
using this:
card (obs_ids (path \<sigma>) \<inter> {..<i}) = k \<and> local.att (path \<sigma> i) \<noteq> None

goal (1 subgoal):
 1. (\<And>a. (case local.att (path \<sigma> i) of None \<Rightarrow> None | Some f \<Rightarrow> Some (f (\<sigma>\<^bsup>i\<^esup>))) = Some a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma kth_obs_unique: \<open>is_kth_obs \<pi> k i \<Longrightarrow> is_kth_obs \<pi> k j \<Longrightarrow> i = j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_kth_obs \<pi> k i; is_kth_obs \<pi> k j\<rbrakk> \<Longrightarrow> i = j
[PROOF STEP]
proof (induction \<open>i\<close> \<open>j\<close> rule: nat_sym_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
 2. \<And>a. \<lbrakk>is_kth_obs \<pi> k a; is_kth_obs \<pi> k a\<rbrakk> \<Longrightarrow> a = a
 3. \<And>a b. \<lbrakk>\<lbrakk>is_kth_obs \<pi> k b; is_kth_obs \<pi> k a\<rbrakk> \<Longrightarrow> b = a; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
case sym
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> k a_
is_kth_obs \<pi> k a_

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
 2. \<And>a. \<lbrakk>is_kth_obs \<pi> k a; is_kth_obs \<pi> k a\<rbrakk> \<Longrightarrow> a = a
 3. \<And>a b. \<lbrakk>\<lbrakk>is_kth_obs \<pi> k b; is_kth_obs \<pi> k a\<rbrakk> \<Longrightarrow> b = a; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> k a_
is_kth_obs \<pi> k a_

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

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
 2. \<And>a b. \<lbrakk>\<lbrakk>is_kth_obs \<pi> k b; is_kth_obs \<pi> k a\<rbrakk> \<Longrightarrow> b = a; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
 2. \<And>a b. \<lbrakk>\<lbrakk>is_kth_obs \<pi> k b; is_kth_obs \<pi> k a\<rbrakk> \<Longrightarrow> b = a; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
case eq
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_kth_obs \<pi> k b_; is_kth_obs \<pi> k a_\<rbrakk> \<Longrightarrow> b_ = a_
is_kth_obs \<pi> k a_
is_kth_obs \<pi> k b_

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
 2. \<And>a b. \<lbrakk>\<lbrakk>is_kth_obs \<pi> k b; is_kth_obs \<pi> k a\<rbrakk> \<Longrightarrow> b = a; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_kth_obs \<pi> k b_; is_kth_obs \<pi> k a_\<rbrakk> \<Longrightarrow> b_ = a_
is_kth_obs \<pi> k a_
is_kth_obs \<pi> k b_

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
case (less i j)
[PROOF STATE]
proof (state)
this:
i < j
is_kth_obs \<pi> k i
is_kth_obs \<pi> k j

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
have \<open>obs_ids \<pi> \<inter> {..<i} \<subseteq> obs_ids \<pi> \<inter> {..<j}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_ids \<pi> \<inter> {..<i} \<subseteq> obs_ids \<pi> \<inter> {..<j}
[PROOF STEP]
using less(1)
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. obs_ids \<pi> \<inter> {..<i} \<subseteq> obs_ids \<pi> \<inter> {..<j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
obs_ids \<pi> \<inter> {..<i} \<subseteq> obs_ids \<pi> \<inter> {..<j}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
obs_ids \<pi> \<inter> {..<i} \<subseteq> obs_ids \<pi> \<inter> {..<j}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
have \<open>i \<in> obs_ids \<pi> \<inter> {..<j}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> obs_ids \<pi> \<inter> {..<j}
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
i < j
is_kth_obs \<pi> k i
is_kth_obs \<pi> k j

goal (1 subgoal):
 1. i \<in> obs_ids \<pi> \<inter> {..<j}
[PROOF STEP]
unfolding is_kth_obs_def obs_ids_def
[PROOF STATE]
proof (prove)
using this:
i < j
card ({k. local.att (\<pi> k) \<noteq> None} \<inter> {..<i}) = k \<and> local.att (\<pi> i) \<noteq> None
card ({k. local.att (\<pi> k) \<noteq> None} \<inter> {..<j}) = k \<and> local.att (\<pi> j) \<noteq> None

goal (1 subgoal):
 1. i \<in> {k. local.att (\<pi> k) \<noteq> None} \<inter> {..<j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> obs_ids \<pi> \<inter> {..<j}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<in> obs_ids \<pi> \<inter> {..<j}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
have \<open>i \<notin> obs_ids \<pi> \<inter> {..<i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<notin> obs_ids \<pi> \<inter> {..<i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<notin> obs_ids \<pi> \<inter> {..<i}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<notin> obs_ids \<pi> \<inter> {..<i}

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
have \<open>card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<j})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> k i
is_kth_obs \<pi> k j

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
unfolding is_kth_obs_def
[PROOF STATE]
proof (prove)
using this:
card (obs_ids \<pi> \<inter> {..<i}) = k \<and> local.att (\<pi> i) \<noteq> None
card (obs_ids \<pi> \<inter> {..<j}) = k \<and> local.att (\<pi> j) \<noteq> None

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<j})

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<j})

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
have \<open>finite (obs_ids \<pi> \<inter> {..<i})\<close> \<open>finite (obs_ids \<pi> \<inter> {..<j})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (obs_ids \<pi> \<inter> {..<i}) &&& finite (obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (obs_ids \<pi> \<inter> {..<i})
finite (obs_ids \<pi> \<inter> {..<j})

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
obs_ids \<pi> \<inter> {..<i} \<subseteq> obs_ids \<pi> \<inter> {..<j}
i \<in> obs_ids \<pi> \<inter> {..<j}
i \<notin> obs_ids \<pi> \<inter> {..<i}
card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<j})
finite (obs_ids \<pi> \<inter> {..<i})
finite (obs_ids \<pi> \<inter> {..<j})
[PROOF STEP]
have \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
obs_ids \<pi> \<inter> {..<i} \<subseteq> obs_ids \<pi> \<inter> {..<j}
i \<in> obs_ids \<pi> \<inter> {..<j}
i \<notin> obs_ids \<pi> \<inter> {..<i}
card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<j})
finite (obs_ids \<pi> \<inter> {..<i})
finite (obs_ids \<pi> \<inter> {..<j})

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a < b; is_kth_obs \<pi> k a; is_kth_obs \<pi> k b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. i = j
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i = j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obs_none_no_kth_obs: assumes \<open>obs \<sigma> k = None\<close> shows \<open>\<not> (\<exists> i. is_kth_obs (path \<sigma>) k i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>i. is_kth_obs (path \<sigma>) k i
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. is_kth_obs (path \<sigma>) k i \<Longrightarrow> False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> k = None

goal (1 subgoal):
 1. \<exists>i. is_kth_obs (path \<sigma>) k i \<Longrightarrow> False
[PROOF STEP]
unfolding obs_def obsp_def
[PROOF STATE]
proof (prove)
using this:
(if Ex (is_kth_obs (path \<sigma>) k) then case local.att (path \<sigma> (The (is_kth_obs (path \<sigma>) k))) of None \<Rightarrow> None | Some f \<Rightarrow> Some (f (\<sigma>\<^bsup>The (is_kth_obs (path \<sigma>) k)\<^esup>)) else None) = None

goal (1 subgoal):
 1. \<exists>i. is_kth_obs (path \<sigma>) k i \<Longrightarrow> False
[PROOF STEP]
apply (auto split: option.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>local.att (path \<sigma> (The (is_kth_obs (path \<sigma>) k))) = None; is_kth_obs (path \<sigma>) k i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis assms kth_obs_not_none kth_obs_unique obs_def option.distinct(2) the_equality)


[STATEMENT]
lemma obs_some_kth_obs : assumes \<open>obs \<sigma> k \<noteq> None\<close> obtains i where \<open>is_kth_obs (path \<sigma>) k i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. is_kth_obs (path \<sigma>) k i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obs_def assms)


[STATEMENT]
lemma not_none_is_obs: assumes \<open>att(\<pi> i) \<noteq> None\<close> shows \<open>is_kth_obs \<pi> (card (obs_ids \<pi> \<inter> {..<i})) i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_kth_obs \<pi> (card (obs_ids \<pi> \<inter> {..<i})) i
[PROOF STEP]
unfolding is_kth_obs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<i}) \<and> local.att (\<pi> i) \<noteq> None
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
local.att (\<pi> i) \<noteq> None

goal (1 subgoal):
 1. card (obs_ids \<pi> \<inter> {..<i}) = card (obs_ids \<pi> \<inter> {..<i}) \<and> local.att (\<pi> i) \<noteq> None
[PROOF STEP]
by auto


[STATEMENT]
lemma in_obs_ids_is_kth_obs: assumes \<open>i \<in> obs_ids \<pi>\<close> obtains k where \<open>is_kth_obs \<pi> k i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. is_kth_obs \<pi> k i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k. is_kth_obs \<pi> k i \<Longrightarrow> thesis) \<Longrightarrow> is_kth_obs \<pi> ?k4 i
[PROOF STEP]
have \<open>att (\<pi> i) \<noteq> None\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.att (\<pi> i) \<noteq> None
[PROOF STEP]
using assms obs_ids_def
[PROOF STATE]
proof (prove)
using this:
i \<in> obs_ids \<pi>
obs_ids ?\<pi> = {k. local.att (?\<pi> k) \<noteq> None}

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

goal (1 subgoal):
 1. (\<And>k. is_kth_obs \<pi> k i \<Longrightarrow> thesis) \<Longrightarrow> is_kth_obs \<pi> ?k4 i
[PROOF STEP]
thus \<open>is_kth_obs \<pi> (card (obs_ids \<pi> \<inter> {..<i})) i\<close>
[PROOF STATE]
proof (prove)
using this:
local.att (\<pi> i) \<noteq> None

goal (1 subgoal):
 1. is_kth_obs \<pi> (card (obs_ids \<pi> \<inter> {..<i})) i
[PROOF STEP]
using not_none_is_obs
[PROOF STATE]
proof (prove)
using this:
local.att (\<pi> i) \<noteq> None
local.att (?\<pi> ?i) \<noteq> None \<Longrightarrow> is_kth_obs ?\<pi> (card (obs_ids ?\<pi> \<inter> {..<?i})) ?i

goal (1 subgoal):
 1. is_kth_obs \<pi> (card (obs_ids \<pi> \<inter> {..<i})) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> (card (obs_ids \<pi> \<inter> {..<i})) i

goal:
No subgoals!
[PROOF STEP]
qed