[STATEMENT]
lemma obs_neq_some_contradicts': fixes \<sigma> \<sigma>' defines \<pi>: \<open>\<pi> \<equiv> path \<sigma>\<close> and \<pi>': \<open>\<pi>' \<equiv> path \<sigma>'\<close>
assumes obsnecs: \<open>obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'\<close>
and iki: \<open>is_kth_obs \<pi> k i\<close> and iki': \<open>is_kth_obs \<pi>' k i'\<close>
shows \<open>\<exists> k k'. ((\<sigma>', k') \<cc> (\<sigma> ,k) \<and> \<pi> k \<in> dom att) \<or> ((\<sigma>, k) \<cc> (\<sigma>' ,k') \<and> \<pi>' k' \<in> dom att)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using obsnecs iki iki'
[PROOF STATE]
proof (prove)
using this:
obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof (induction \<open>k\<close> arbitrary: \<open>i\<close> \<open>i'\<close> rule: less_induct )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
case (less k i i')
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < k; obsp \<sigma> ?i1 \<noteq> obsp \<sigma>' ?i'1 \<or> cs\<^bsup>\<pi>\<^esup> ?i1 \<noteq> cs\<^bsup>\<pi>'\<^esup> ?i'1; is_kth_obs \<pi> ?y1 ?i1; is_kth_obs \<pi>' ?y1 ?i'1\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
note iki = \<open>is_kth_obs \<pi> k i\<close>
  and iki' = \<open>is_kth_obs \<pi>' k i'\<close>
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have domi: \<open>\<pi> i \<in> dom att\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> i \<in> dom local.att
[PROOF STEP]
by (metis is_kth_obs_def domIff iki)
[PROOF STATE]
proof (state)
this:
\<pi> i \<in> dom local.att

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have domi': \<open>\<pi>' i' \<in> dom att\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' i' \<in> dom local.att
[PROOF STEP]
by (metis is_kth_obs_def domIff iki')
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<in> dom local.att

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
note obsnecs = \<open>obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (state)
this:
obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att; obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'\<rbrakk> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume csi: \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence *: \<open>obsp \<sigma> i \<noteq> obsp \<sigma>' i'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. obsp \<sigma> i \<noteq> obsp \<sigma>' i'
[PROOF STEP]
using obsnecs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. obsp \<sigma> i \<noteq> obsp \<sigma>' i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
obsp \<sigma> i \<noteq> obsp \<sigma>' i'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
note obsp_contradict[OF _ *] csi domi \<pi> \<pi>'
[PROOF STATE]
proof (state)
this:
cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i' \<Longrightarrow> (\<sigma>', i') \<cc> (\<sigma>, i)
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
\<pi> i \<in> dom local.att
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i' \<Longrightarrow> (\<sigma>', i') \<cc> (\<sigma>, i)
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
\<pi> i \<in> dom local.att
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume ncsi: \<open>cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi> &&& is_path \<pi>'
[PROOF STEP]
using \<pi> \<pi>' path_is_path
[PROOF STATE]
proof (prove)
using this:
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
is_path (path ?\<sigma>)

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<pi>0: \<open>\<pi> 0 = \<pi>' 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> 0 = \<pi>' 0
[PROOF STEP]
unfolding \<pi> \<pi>' path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ((local.step ^^ 0) (local.entry, \<sigma>)) = fst ((local.step ^^ 0) (local.entry, \<sigma>'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> 0 = \<pi>' 0

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
note kth_obs_cs_missing_cs[of \<open>\<pi>\<close> \<open>\<pi>'\<close> \<open>k\<close> \<open>i\<close> \<open>i'\<close>] \<pi> \<pi>' path_is_path iki iki' ncsi
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_path \<pi>; is_path \<pi>'; is_kth_obs \<pi> k i; is_kth_obs \<pi>' k i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>l j. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> ?thesis; \<And>l' j'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
is_path (path ?\<sigma>)
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence \<open>(\<exists> l j .j \<le> i \<and> is_kth_obs \<pi> l j \<and> \<not> (\<exists> j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')) \<or> (\<exists> l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> \<not> (\<exists> j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'))\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path \<pi>; is_path \<pi>'; is_kth_obs \<pi> k i; is_kth_obs \<pi>' k i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>l j. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> ?thesis; \<And>l' j'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
is_path (path ?\<sigma>)
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')) \<or> (\<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'))

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume \<open>\<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> \<not> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (state)
this:
\<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (2 subgoals):
 1. \<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
[PROOF STEP]
obtain l j where ji: \<open>j\<le>i\<close> and iobs: \<open>is_kth_obs \<pi> l j\<close> and notin: \<open>\<not> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

goal (1 subgoal):
 1. (\<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>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:
j \<le> i
is_kth_obs \<pi> l j
\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

goal (2 subgoals):
 1. \<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have dom: \<open>\<pi> j \<in> dom att\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j \<in> dom local.att
[PROOF STEP]
using iobs is_kth_obs_def
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> l j
is_kth_obs ?\<pi> ?k ?i = (card (obs_ids ?\<pi> \<inter> {..<?i}) = ?k \<and> local.att (?\<pi> ?i) \<noteq> None)

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

goal (2 subgoals):
 1. \<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
obtain n n' where nj: \<open>n < j\<close> and csn: \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'\<close> and sucn:  \<open>\<pi> (Suc n) \<noteq> \<pi>' (Suc n')\<close> and cdloop: \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<or> (\<forall> j'> n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n n'. \<lbrakk>n < j; cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'; \<pi> (Suc n) \<noteq> \<pi>' (Suc n'); j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<or> (\<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using missing_cd_or_loop[OF path \<pi>0 notin]
[PROOF STATE]
proof (prove)
using this:
(\<And>i i'. \<lbrakk>i < j; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (2 subgoals):
 1. \<exists>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using cdloop
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<or> (\<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n')

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume cdjn: \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close>
[PROOF STATE]
proof (state)
this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

goal (2 subgoals):
 1. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence csnj: \<open>cs\<^bsup>\<pi>'\<^esup> n' \<prec> cs\<^bsup>\<pi>\<^esup> j\<close>
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> n' \<prec> cs\<^bsup>\<pi>\<^esup> j
[PROOF STEP]
using csn
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'

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

goal (2 subgoals):
 1. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have cssel: \<open>\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n')) = \<pi> (Suc n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n')) = \<pi> (Suc n)
[PROOF STEP]
using csn
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'

goal (1 subgoal):
 1. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n')) = \<pi> (Suc n)
[PROOF STEP]
by (metis cdjn cd_not_ret cs_select_id path(1))
[PROOF STATE]
proof (state)
this:
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n')) = \<pi> (Suc n)

goal (2 subgoals):
 1. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>(\<sigma>',n') \<cc> (\<sigma>,j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>', n') \<cc> (\<sigma>, j)
[PROOF STEP]
using csnj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> n' \<prec> cs\<^bsup>\<pi>\<^esup> j

goal (1 subgoal):
 1. (\<sigma>', n') \<cc> (\<sigma>, j)
[PROOF STEP]
apply(rule contradicts.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pi> = path \<sigma>
 2. \<pi>' = path \<sigma>'
 3. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n')) \<noteq> \<pi>' (Suc n')
[PROOF STEP]
using cssel \<pi> \<pi>' sucn
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n')) = \<pi> (Suc n)
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
\<pi> (Suc n) \<noteq> \<pi>' (Suc n')

goal (3 subgoals):
 1. \<pi> = path \<sigma>
 2. \<pi>' = path \<sigma>'
 3. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n')) \<noteq> \<pi>' (Suc n')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>', n') \<cc> (\<sigma>, j)

goal (2 subgoals):
 1. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', n') \<cc> (\<sigma>, j)

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using dom
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', n') \<cc> (\<sigma>, j)
\<pi> j \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume loop: \<open>\<forall> j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (state)
this:
\<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. \<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume in': \<open>i' \<le> n'\<close>
[PROOF STATE]
proof (state)
this:
i' \<le> n'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[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 le_eq_less_or_eq lessI loop not_le path(2) ret_no_cd term_path_stable)
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<noteq> local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume \<open>\<exists> \<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota>\<close>
[PROOF STATE]
proof (state)
this:
\<exists>\<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota>
[PROOF STEP]
obtain \<iota> where cs\<iota>: \<open>cs\<^bsup>\<pi>\<^esup> \<iota> = cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>\<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota>

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<iota>n: \<open>\<iota> \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> \<le> n
[PROOF STEP]
using cs_order_le[OF path(2,1) cs\<iota>[symmetric] csn[symmetric] nreti' in']
[PROOF STATE]
proof (prove)
using this:
\<iota> \<le> n

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence \<iota>i: \<open>\<iota> < i\<close>
[PROOF STATE]
proof (prove)
using this:
\<iota> \<le> n

goal (1 subgoal):
 1. \<iota> < i
[PROOF STEP]
using nj ji
[PROOF STATE]
proof (prove)
using this:
\<iota> \<le> n
n < j
j \<le> i

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have dom\<iota>: \<open>\<pi> \<iota> \<in> dom att\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<iota> \<in> dom local.att
[PROOF STEP]
using domi' cs\<iota> last_cs
[PROOF STATE]
proof (prove)
using this:
\<pi>' i' \<in> dom local.att
cs\<^bsup>\<pi>\<^esup> \<iota> = cs\<^bsup>\<pi>'\<^esup> i'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

goal (1 subgoal):
 1. \<pi> \<iota> \<in> dom local.att
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi> \<iota> \<in> dom local.att

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
obtain \<kappa> where i\<kappa>\<iota>: \<open>is_kth_obs \<pi> \<kappa> \<iota>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<kappa>. is_kth_obs \<pi> \<kappa> \<iota> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dom\<iota>
[PROOF STATE]
proof (prove)
using this:
\<pi> \<iota> \<in> dom local.att

goal (1 subgoal):
 1. (\<And>\<kappa>. is_kth_obs \<pi> \<kappa> \<iota> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis is_kth_obs_def domIff)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> \<kappa> \<iota>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence \<kappa>k: \<open>\<kappa> < k\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> \<kappa> \<iota>

goal (1 subgoal):
 1. \<kappa> < k
[PROOF STEP]
using \<iota>i iki
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> \<kappa> \<iota>
\<iota> < i
is_kth_obs \<pi> k i

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
obtain \<iota>' where i\<kappa>\<iota>': \<open>is_kth_obs \<pi>' \<kappa> \<iota>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<iota>'. is_kth_obs \<pi>' \<kappa> \<iota>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<kappa>k iki'
[PROOF STATE]
proof (prove)
using this:
\<kappa> < k
is_kth_obs \<pi>' k i'

goal (1 subgoal):
 1. (\<And>\<iota>'. is_kth_obs \<pi>' \<kappa> \<iota>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis kth_obs_stable)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi>' \<kappa> \<iota>'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>\<iota>' < i'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota>' < i'
[PROOF STEP]
using \<kappa>k iki' i\<kappa>\<iota>'
[PROOF STATE]
proof (prove)
using this:
\<kappa> < k
is_kth_obs \<pi>' k i'
is_kth_obs \<pi>' \<kappa> \<iota>'

goal (1 subgoal):
 1. \<iota>' < i'
[PROOF STEP]
by (metis kth_obs_le_iff)
[PROOF STATE]
proof (state)
this:
\<iota>' < i'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence cs\<iota>': \<open>cs\<^bsup>\<pi>\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>'\<^esup> \<iota>'\<close>
[PROOF STATE]
proof (prove)
using this:
\<iota>' < i'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>'\<^esup> \<iota>'
[PROOF STEP]
unfolding cs\<iota>
[PROOF STATE]
proof (prove)
using this:
\<iota>' < i'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> i' \<noteq> cs\<^bsup>\<pi>'\<^esup> \<iota>'
[PROOF STEP]
using cs_inj[OF path(2) nreti', of \<open>\<iota>'\<close>]
[PROOF STATE]
proof (prove)
using this:
\<iota>' < i'
cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> \<iota>' \<Longrightarrow> i' = \<iota>'

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>'\<^esup> \<iota>'

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using less(1)[OF \<kappa>k _ i\<kappa>\<iota> i\<kappa>\<iota>']
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>'\<^esup> \<iota>'
obsp \<sigma> \<iota> \<noteq> obsp \<sigma>' \<iota>' \<or> cs\<^bsup>\<pi>\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>'\<^esup> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<nexists>\<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>\<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume notin'': \<open>\<not>(\<exists> \<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota>)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>\<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota>

goal (1 subgoal):
 1. \<nexists>\<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
obtain \<iota> \<iota>' where \<iota>i': \<open>\<iota>' < i'\<close> and cs\<iota>: \<open>cs\<^bsup>\<pi>\<^esup> \<iota> = cs\<^bsup>\<pi>'\<^esup> \<iota>'\<close> and suc\<iota>: \<open>\<pi> (Suc \<iota>) \<noteq> \<pi>' (Suc \<iota>')\<close> and cdloop': \<open>i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>' \<or> (\<forall> j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<iota>' \<iota>. \<lbrakk>\<iota>' < i'; cs\<^bsup>\<pi>\<^esup> \<iota> = cs\<^bsup>\<pi>'\<^esup> \<iota>'; \<pi> (Suc \<iota>) \<noteq> \<pi>' (Suc \<iota>'); i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>' \<or> (\<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using missing_cd_or_loop[OF path(2,1) \<pi>0[symmetric] notin'']
[PROOF STATE]
proof (prove)
using this:
(\<And>i i'. \<lbrakk>i < i'; cs\<^bsup>\<pi>'\<^esup> i = cs\<^bsup>\<pi>\<^esup> i'; \<pi>' (Suc i) \<noteq> \<pi> (Suc i'); i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<nexists>\<iota>. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using cdloop'
[PROOF STATE]
proof (prove)
using this:
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>' \<or> (\<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>)

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume cdjn: \<open>i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>'\<close>
[PROOF STATE]
proof (state)
this:
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>'

goal (2 subgoals):
 1. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence csnj: \<open>cs\<^bsup>\<pi>\<^esup> \<iota> \<prec> cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (prove)
using this:
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> \<iota> \<prec> cs\<^bsup>\<pi>'\<^esup> i'
[PROOF STEP]
using cs\<iota>
[PROOF STATE]
proof (prove)
using this:
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>'
cs\<^bsup>\<pi>\<^esup> \<iota> = cs\<^bsup>\<pi>'\<^esup> \<iota>'

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

goal (2 subgoals):
 1. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have cssel: \<open>\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>)) = \<pi>' (Suc \<iota>')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>)) = \<pi>' (Suc \<iota>')
[PROOF STEP]
using cs\<iota>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> \<iota> = cs\<^bsup>\<pi>'\<^esup> \<iota>'

goal (1 subgoal):
 1. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>)) = \<pi>' (Suc \<iota>')
[PROOF STEP]
by (metis cdjn cd_not_ret cs_select_id path(2))
[PROOF STATE]
proof (state)
this:
\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>)) = \<pi>' (Suc \<iota>')

goal (2 subgoals):
 1. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>(\<sigma>,\<iota>) \<cc> (\<sigma>',i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, \<iota>) \<cc> (\<sigma>', i')
[PROOF STEP]
using csnj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> \<iota> \<prec> cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. (\<sigma>, \<iota>) \<cc> (\<sigma>', i')
[PROOF STEP]
apply(rule contradicts.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pi>' = path \<sigma>'
 2. \<pi> = path \<sigma>
 3. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>)) \<noteq> \<pi> (Suc \<iota>)
[PROOF STEP]
using cssel \<pi> \<pi>' suc\<iota>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>)) = \<pi>' (Suc \<iota>')
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
\<pi> (Suc \<iota>) \<noteq> \<pi>' (Suc \<iota>')

goal (3 subgoals):
 1. \<pi>' = path \<sigma>'
 2. \<pi> = path \<sigma>
 3. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>)) \<noteq> \<pi> (Suc \<iota>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>, \<iota>) \<cc> (\<sigma>', i')

goal (2 subgoals):
 1. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<iota>) \<cc> (\<sigma>', i')

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using domi'
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<iota>) \<cc> (\<sigma>', i')
\<pi>' i' \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume loop': \<open>\<forall> j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>\<close>
[PROOF STATE]
proof (state)
this:
\<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<iota>n': \<open>\<iota>' < n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota>' < n'
[PROOF STEP]
using in' \<iota>i'
[PROOF STATE]
proof (prove)
using this:
i' \<le> n'
\<iota>' < i'

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

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have nret\<iota>': \<open>\<pi>' \<iota>' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' \<iota>' \<noteq> local.return
[PROOF STEP]
by (metis cs\<iota> last_cs le_eq_less_or_eq lessI path(1) path(2) suc\<iota> term_path_stable)
[PROOF STATE]
proof (state)
this:
\<pi>' \<iota>' \<noteq> local.return

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>\<iota> < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> < n
[PROOF STEP]
using cs_order[OF path(2,1) cs\<iota>[symmetric] csn[symmetric] nret\<iota>' \<iota>n']
[PROOF STATE]
proof (prove)
using this:
\<iota> < n

goal (1 subgoal):
 1. \<iota> < n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<iota> < n

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence \<open>\<iota> < i\<close>
[PROOF STATE]
proof (prove)
using this:
\<iota> < n

goal (1 subgoal):
 1. \<iota> < i
[PROOF STEP]
using nj ji
[PROOF STATE]
proof (prove)
using this:
\<iota> < n
n < j
j \<le> i

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

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence cdi\<iota>: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>\<close>
[PROOF STATE]
proof (prove)
using this:
\<iota> < i

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>
[PROOF STEP]
using loop'
[PROOF STATE]
proof (prove)
using this:
\<iota> < i
\<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>

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

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence cs\<iota>i: \<open>cs\<^bsup>\<pi>'\<^esup> \<iota>' \<prec> cs\<^bsup>\<pi>\<^esup> i\<close>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> \<iota>' \<prec> cs\<^bsup>\<pi>\<^esup> i
[PROOF STEP]
using cs\<iota>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>
cs\<^bsup>\<pi>\<^esup> \<iota> = cs\<^bsup>\<pi>'\<^esup> \<iota>'

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

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have cssel: \<open>\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>')) = \<pi> (Suc \<iota>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>')) = \<pi> (Suc \<iota>)
[PROOF STEP]
using cs\<iota>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> \<iota> = cs\<^bsup>\<pi>'\<^esup> \<iota>'

goal (1 subgoal):
 1. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>')) = \<pi> (Suc \<iota>)
[PROOF STEP]
by (metis cdi\<iota> cd_not_ret cs_select_id path(1))
[PROOF STATE]
proof (state)
this:
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>')) = \<pi> (Suc \<iota>)

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>(\<sigma>',\<iota>') \<cc> (\<sigma>,i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>', \<iota>') \<cc> (\<sigma>, i)
[PROOF STEP]
using cs\<iota>i
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> \<iota>' \<prec> cs\<^bsup>\<pi>\<^esup> i

goal (1 subgoal):
 1. (\<sigma>', \<iota>') \<cc> (\<sigma>, i)
[PROOF STEP]
apply(rule contradicts.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pi> = path \<sigma>
 2. \<pi>' = path \<sigma>'
 3. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>')) \<noteq> \<pi>' (Suc \<iota>')
[PROOF STEP]
using cssel \<pi> \<pi>' suc\<iota>
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>')) = \<pi> (Suc \<iota>)
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
\<pi> (Suc \<iota>) \<noteq> \<pi>' (Suc \<iota>')

goal (3 subgoals):
 1. \<pi> = path \<sigma>
 2. \<pi>' = path \<sigma>'
 3. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>')) \<noteq> \<pi>' (Suc \<iota>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>', \<iota>') \<cc> (\<sigma>, i)

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', \<iota>') \<cc> (\<sigma>, i)

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using domi
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', \<iota>') \<cc> (\<sigma>, i)
\<pi> i \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<not> i' \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i' \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume \<open>\<not> i' \<le> n'\<close>
[PROOF STATE]
proof (state)
this:
\<not> i' \<le> n'

goal (1 subgoal):
 1. \<not> i' \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence ni': \<open>n'< i'\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i' \<le> n'

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

goal (1 subgoal):
 1. \<not> i' \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence cdin: \<open>i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (prove)
using this:
n' < i'

goal (1 subgoal):
 1. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'
[PROOF STEP]
using loop
[PROOF STATE]
proof (prove)
using this:
n' < i'
\<forall>j'>n'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

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

goal (1 subgoal):
 1. \<not> i' \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence csni: \<open>cs\<^bsup>\<pi>\<^esup> n \<prec> cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (prove)
using this:
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n \<prec> cs\<^bsup>\<pi>'\<^esup> i'
[PROOF STEP]
using csn
[PROOF STATE]
proof (prove)
using this:
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'

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

goal (1 subgoal):
 1. \<not> i' \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have cssel: \<open>\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n)) = \<pi>' (Suc n')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n)) = \<pi>' (Suc n')
[PROOF STEP]
using csn
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'

goal (1 subgoal):
 1. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n)) = \<pi>' (Suc n')
[PROOF STEP]
by (metis cdin cd_not_ret cs_select_id path(2))
[PROOF STATE]
proof (state)
this:
\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n)) = \<pi>' (Suc n')

goal (1 subgoal):
 1. \<not> i' \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>(\<sigma>,n) \<cc> (\<sigma>',i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, n) \<cc> (\<sigma>', i')
[PROOF STEP]
using csni
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n \<prec> cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. (\<sigma>, n) \<cc> (\<sigma>', i')
[PROOF STEP]
apply(rule contradicts.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pi>' = path \<sigma>'
 2. \<pi> = path \<sigma>
 3. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n)) \<noteq> \<pi> (Suc n)
[PROOF STEP]
using cssel \<pi> \<pi>' sucn
[PROOF STATE]
proof (prove)
using this:
\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n)) = \<pi>' (Suc n')
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
\<pi> (Suc n) \<noteq> \<pi>' (Suc n')

goal (3 subgoals):
 1. \<pi>' = path \<sigma>'
 2. \<pi> = path \<sigma>
 3. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n)) \<noteq> \<pi> (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>, n) \<cc> (\<sigma>', i')

goal (1 subgoal):
 1. \<not> i' \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, n) \<cc> (\<sigma>', i')

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using domi'
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, n) \<cc> (\<sigma>', i')
\<pi>' i' \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
      \<comment> \<open>Symmetric case as above, indices might be messy.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume \<open>\<exists>l j. j \<le> i' \<and> is_kth_obs \<pi>' l j \<and> \<not> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> j)\<close>
[PROOF STATE]
proof (state)
this:
\<exists>l j. j \<le> i' \<and> is_kth_obs \<pi>' l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> j)

goal (1 subgoal):
 1. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l j. j \<le> i' \<and> is_kth_obs \<pi>' l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> j)
[PROOF STEP]
obtain l j where ji': \<open>j\<le>i'\<close> and iobs: \<open>is_kth_obs \<pi>' l j\<close> and notin: \<open>\<not> (\<exists>j'. cs\<^bsup>\<pi>'\<^esup> j = cs\<^bsup>\<pi>\<^esup> j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>l j. j \<le> i' \<and> is_kth_obs \<pi>' l j \<and> (\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> j)

goal (1 subgoal):
 1. (\<And>j l. \<lbrakk>j \<le> i'; is_kth_obs \<pi>' l j; \<nexists>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:
j \<le> i'
is_kth_obs \<pi>' l j
\<nexists>j'. cs\<^bsup>\<pi>'\<^esup> j = cs\<^bsup>\<pi>\<^esup> j'

goal (1 subgoal):
 1. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have dom: \<open>\<pi>' j \<in> dom att\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' j \<in> dom local.att
[PROOF STEP]
using iobs is_kth_obs_def
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' l j
is_kth_obs ?\<pi> ?k ?i = (card (obs_ids ?\<pi> \<inter> {..<?i}) = ?k \<and> local.att (?\<pi> ?i) \<noteq> None)

goal (1 subgoal):
 1. \<pi>' j \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>' j \<in> dom local.att

goal (1 subgoal):
 1. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
obtain n n' where nj: \<open>n < j\<close> and csn: \<open>cs\<^bsup>\<pi>'\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<close> and sucn:  \<open>\<pi>' (Suc n) \<noteq> \<pi> (Suc n')\<close> and cdloop: \<open>j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n \<or> (\<forall> j'> n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n n'. \<lbrakk>n < j; cs\<^bsup>\<pi>'\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'; \<pi>' (Suc n) \<noteq> \<pi> (Suc n'); j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n \<or> (\<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using missing_cd_or_loop[OF path(2,1) \<pi>0[symmetric] ] notin
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<nexists>k'. cs\<^bsup>\<pi>'\<^esup> ?k = cs\<^bsup>\<pi>\<^esup> k'; \<And>i i'. \<lbrakk>i < ?k; cs\<^bsup>\<pi>'\<^esup> i = cs\<^bsup>\<pi>\<^esup> i'; \<pi>' (Suc i) \<noteq> \<pi> (Suc i'); ?k cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<nexists>j'. cs\<^bsup>\<pi>'\<^esup> j = cs\<^bsup>\<pi>\<^esup> j'

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

goal (1 subgoal):
 1. \<exists>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<and> (\<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j') \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using cdloop
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n \<or> (\<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n')

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume cdjn: \<open>j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n\<close>
[PROOF STATE]
proof (state)
this:
j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n

goal (2 subgoals):
 1. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence csnj: \<open>cs\<^bsup>\<pi>\<^esup> n' \<prec> cs\<^bsup>\<pi>'\<^esup> j\<close>
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n' \<prec> cs\<^bsup>\<pi>'\<^esup> j
[PROOF STEP]
using csn
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n
cs\<^bsup>\<pi>'\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

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

goal (2 subgoals):
 1. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have cssel: \<open>\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n')) = \<pi>' (Suc n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n')) = \<pi>' (Suc n)
[PROOF STEP]
using csn
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

goal (1 subgoal):
 1. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n')) = \<pi>' (Suc n)
[PROOF STEP]
by (metis cdjn cd_not_ret cs_select_id path(2))
[PROOF STATE]
proof (state)
this:
\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n')) = \<pi>' (Suc n)

goal (2 subgoals):
 1. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>(\<sigma>,n') \<cc> (\<sigma>',j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, n') \<cc> (\<sigma>', j)
[PROOF STEP]
using csnj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n' \<prec> cs\<^bsup>\<pi>'\<^esup> j

goal (1 subgoal):
 1. (\<sigma>, n') \<cc> (\<sigma>', j)
[PROOF STEP]
apply(rule contradicts.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pi>' = path \<sigma>'
 2. \<pi> = path \<sigma>
 3. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n')) \<noteq> \<pi> (Suc n')
[PROOF STEP]
using cssel \<pi>' \<pi> sucn
[PROOF STATE]
proof (prove)
using this:
\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n')) = \<pi>' (Suc n)
\<pi>' \<equiv> path \<sigma>'
\<pi> \<equiv> path \<sigma>
\<pi>' (Suc n) \<noteq> \<pi> (Suc n')

goal (3 subgoals):
 1. \<pi>' = path \<sigma>'
 2. \<pi> = path \<sigma>
 3. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> n')) \<noteq> \<pi> (Suc n')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>, n') \<cc> (\<sigma>', j)

goal (2 subgoals):
 1. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, n') \<cc> (\<sigma>', j)

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using dom
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, n') \<cc> (\<sigma>', j)
\<pi>' j \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume loop: \<open>\<forall> j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (state)
this:
\<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. \<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume in': \<open>i \<le> n'\<close>
[PROOF STATE]
proof (state)
this:
i \<le> n'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[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 le_eq_less_or_eq lessI loop not_le path(1) ret_no_cd term_path_stable)
[PROOF STATE]
proof (state)
this:
\<pi> i \<noteq> local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume \<open>\<exists> \<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota>\<close>
[PROOF STATE]
proof (state)
this:
\<exists>\<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota>
[PROOF STEP]
obtain \<iota> where cs\<iota>: \<open>cs\<^bsup>\<pi>'\<^esup> \<iota> = cs\<^bsup>\<pi>\<^esup> i\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>\<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota>

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<iota>n: \<open>\<iota> \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> \<le> n
[PROOF STEP]
using cs_order_le[OF path cs\<iota>[symmetric] csn[symmetric] nreti in']
[PROOF STATE]
proof (prove)
using this:
\<iota> \<le> n

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence \<iota>i': \<open>\<iota> < i'\<close>
[PROOF STATE]
proof (prove)
using this:
\<iota> \<le> n

goal (1 subgoal):
 1. \<iota> < i'
[PROOF STEP]
using nj ji'
[PROOF STATE]
proof (prove)
using this:
\<iota> \<le> n
n < j
j \<le> i'

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have dom\<iota>: \<open>\<pi>' \<iota> \<in> dom att\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' \<iota> \<in> dom local.att
[PROOF STEP]
using domi cs\<iota> last_cs
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<in> dom local.att
cs\<^bsup>\<pi>'\<^esup> \<iota> = cs\<^bsup>\<pi>\<^esup> i
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

goal (1 subgoal):
 1. \<pi>' \<iota> \<in> dom local.att
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi>' \<iota> \<in> dom local.att

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
obtain \<kappa> where i\<kappa>\<iota>: \<open>is_kth_obs \<pi>' \<kappa> \<iota>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<kappa>. is_kth_obs \<pi>' \<kappa> \<iota> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dom\<iota>
[PROOF STATE]
proof (prove)
using this:
\<pi>' \<iota> \<in> dom local.att

goal (1 subgoal):
 1. (\<And>\<kappa>. is_kth_obs \<pi>' \<kappa> \<iota> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis is_kth_obs_def domIff)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi>' \<kappa> \<iota>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence \<kappa>k: \<open>\<kappa> < k\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' \<kappa> \<iota>

goal (1 subgoal):
 1. \<kappa> < k
[PROOF STEP]
using \<iota>i' iki'
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' \<kappa> \<iota>
\<iota> < i'
is_kth_obs \<pi>' k i'

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
obtain \<iota>' where i\<kappa>\<iota>': \<open>is_kth_obs \<pi> \<kappa> \<iota>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<iota>'. is_kth_obs \<pi> \<kappa> \<iota>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<kappa>k iki
[PROOF STATE]
proof (prove)
using this:
\<kappa> < k
is_kth_obs \<pi> k i

goal (1 subgoal):
 1. (\<And>\<iota>'. is_kth_obs \<pi> \<kappa> \<iota>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis kth_obs_stable)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> \<kappa> \<iota>'

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>\<iota>' < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota>' < i
[PROOF STEP]
using \<kappa>k iki i\<kappa>\<iota>'
[PROOF STATE]
proof (prove)
using this:
\<kappa> < k
is_kth_obs \<pi> k i
is_kth_obs \<pi> \<kappa> \<iota>'

goal (1 subgoal):
 1. \<iota>' < i
[PROOF STEP]
by (metis kth_obs_le_iff)
[PROOF STATE]
proof (state)
this:
\<iota>' < i

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence cs\<iota>': \<open>cs\<^bsup>\<pi>'\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>\<^esup> \<iota>'\<close>
[PROOF STATE]
proof (prove)
using this:
\<iota>' < i

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>\<^esup> \<iota>'
[PROOF STEP]
unfolding cs\<iota>
[PROOF STATE]
proof (prove)
using this:
\<iota>' < i

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> \<iota>'
[PROOF STEP]
using cs_inj[OF path(1) nreti, of \<open>\<iota>'\<close>]
[PROOF STATE]
proof (prove)
using this:
\<iota>' < i
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> \<iota>' \<Longrightarrow> i = \<iota>'

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<not> ?P \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>\<^esup> \<iota>'

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using less(1)[OF \<kappa>k _ i\<kappa>\<iota>' i\<kappa>\<iota>]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> \<iota> \<noteq> cs\<^bsup>\<pi>\<^esup> \<iota>'
obsp \<sigma> \<iota>' \<noteq> obsp \<sigma>' \<iota> \<or> cs\<^bsup>\<pi>\<^esup> \<iota>' \<noteq> cs\<^bsup>\<pi>'\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<nexists>\<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>\<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume notin'': \<open>\<not>(\<exists> \<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota>)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>\<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota>

goal (1 subgoal):
 1. \<nexists>\<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
obtain \<iota> \<iota>' where \<iota>i: \<open>\<iota>' < i\<close> and cs\<iota>: \<open>cs\<^bsup>\<pi>'\<^esup> \<iota> = cs\<^bsup>\<pi>\<^esup> \<iota>'\<close> and suc\<iota>: \<open>\<pi>' (Suc \<iota>) \<noteq> \<pi> (Suc \<iota>')\<close> and cdloop': \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>' \<or> (\<forall> j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<iota>' \<iota>. \<lbrakk>\<iota>' < i; cs\<^bsup>\<pi>'\<^esup> \<iota> = cs\<^bsup>\<pi>\<^esup> \<iota>'; \<pi>' (Suc \<iota>) \<noteq> \<pi> (Suc \<iota>'); i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>' \<or> (\<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using missing_cd_or_loop[OF path \<pi>0 notin'']
[PROOF STATE]
proof (prove)
using this:
(\<And>i i'. \<lbrakk>i < i; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'; \<pi> (Suc i) \<noteq> \<pi>' (Suc i'); i cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> (\<forall>j'>i'. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<nexists>\<iota>. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using cdloop'
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>' \<or> (\<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>)

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume cdjn: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>'\<close>
[PROOF STATE]
proof (state)
this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>'

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence csnj: \<open>cs\<^bsup>\<pi>'\<^esup> \<iota> \<prec> cs\<^bsup>\<pi>\<^esup> i\<close>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> \<iota> \<prec> cs\<^bsup>\<pi>\<^esup> i
[PROOF STEP]
using cs\<iota>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>'
cs\<^bsup>\<pi>'\<^esup> \<iota> = cs\<^bsup>\<pi>\<^esup> \<iota>'

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

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have cssel: \<open>\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>)) = \<pi> (Suc \<iota>')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>)) = \<pi> (Suc \<iota>')
[PROOF STEP]
using cs\<iota>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> \<iota> = cs\<^bsup>\<pi>\<^esup> \<iota>'

goal (1 subgoal):
 1. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>)) = \<pi> (Suc \<iota>')
[PROOF STEP]
by (metis cdjn cd_not_ret cs_select_id path(1))
[PROOF STATE]
proof (state)
this:
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>)) = \<pi> (Suc \<iota>')

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>(\<sigma>',\<iota>) \<cc> (\<sigma>,i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>', \<iota>) \<cc> (\<sigma>, i)
[PROOF STEP]
using csnj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> \<iota> \<prec> cs\<^bsup>\<pi>\<^esup> i

goal (1 subgoal):
 1. (\<sigma>', \<iota>) \<cc> (\<sigma>, i)
[PROOF STEP]
apply(rule contradicts.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pi> = path \<sigma>
 2. \<pi>' = path \<sigma>'
 3. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>)) \<noteq> \<pi>' (Suc \<iota>)
[PROOF STEP]
using cssel \<pi>' \<pi> suc\<iota>
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>)) = \<pi> (Suc \<iota>')
\<pi>' \<equiv> path \<sigma>'
\<pi> \<equiv> path \<sigma>
\<pi>' (Suc \<iota>) \<noteq> \<pi> (Suc \<iota>')

goal (3 subgoals):
 1. \<pi> = path \<sigma>
 2. \<pi>' = path \<sigma>'
 3. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> \<iota>)) \<noteq> \<pi>' (Suc \<iota>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>', \<iota>) \<cc> (\<sigma>, i)

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> \<iota>' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
 2. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', \<iota>) \<cc> (\<sigma>, i)

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using domi
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', \<iota>) \<cc> (\<sigma>, i)
\<pi> i \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume loop': \<open>\<forall> j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>\<close>
[PROOF STATE]
proof (state)
this:
\<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<iota>n': \<open>\<iota>' < n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota>' < n'
[PROOF STEP]
using in' \<iota>i
[PROOF STATE]
proof (prove)
using this:
i \<le> n'
\<iota>' < i

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

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have nret\<iota>': \<open>\<pi> \<iota>' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<iota>' \<noteq> local.return
[PROOF STEP]
by (metis cs\<iota> last_cs le_eq_less_or_eq lessI path(1) path(2) suc\<iota> term_path_stable)
[PROOF STATE]
proof (state)
this:
\<pi> \<iota>' \<noteq> local.return

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>\<iota> < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> < n
[PROOF STEP]
using cs_order[OF path cs\<iota>[symmetric] csn[symmetric] nret\<iota>' \<iota>n']
[PROOF STATE]
proof (prove)
using this:
\<iota> < n

goal (1 subgoal):
 1. \<iota> < n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<iota> < n

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence \<open>\<iota> < i'\<close>
[PROOF STATE]
proof (prove)
using this:
\<iota> < n

goal (1 subgoal):
 1. \<iota> < i'
[PROOF STEP]
using nj ji'
[PROOF STATE]
proof (prove)
using this:
\<iota> < n
n < j
j \<le> i'

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

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence cdi\<iota>: \<open>i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>\<close>
[PROOF STATE]
proof (prove)
using this:
\<iota> < i'

goal (1 subgoal):
 1. i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>
[PROOF STEP]
using loop'
[PROOF STATE]
proof (prove)
using this:
\<iota> < i'
\<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>

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

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence cs\<iota>i': \<open>cs\<^bsup>\<pi>\<^esup> \<iota>' \<prec> cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (prove)
using this:
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> \<iota>' \<prec> cs\<^bsup>\<pi>'\<^esup> i'
[PROOF STEP]
using cs\<iota>
[PROOF STATE]
proof (prove)
using this:
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota>
cs\<^bsup>\<pi>'\<^esup> \<iota> = cs\<^bsup>\<pi>\<^esup> \<iota>'

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

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have cssel: \<open>\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>')) = \<pi>' (Suc \<iota>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>')) = \<pi>' (Suc \<iota>)
[PROOF STEP]
using cs\<iota>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> \<iota> = cs\<^bsup>\<pi>\<^esup> \<iota>'

goal (1 subgoal):
 1. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>')) = \<pi>' (Suc \<iota>)
[PROOF STEP]
by (metis cdi\<iota> cd_not_ret cs_select_id path(2))
[PROOF STATE]
proof (state)
this:
\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>')) = \<pi>' (Suc \<iota>)

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>(\<sigma>,\<iota>') \<cc> (\<sigma>',i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, \<iota>') \<cc> (\<sigma>', i')
[PROOF STEP]
using cs\<iota>i'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> \<iota>' \<prec> cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. (\<sigma>, \<iota>') \<cc> (\<sigma>', i')
[PROOF STEP]
apply(rule contradicts.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pi>' = path \<sigma>'
 2. \<pi> = path \<sigma>
 3. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>')) \<noteq> \<pi> (Suc \<iota>')
[PROOF STEP]
using cssel \<pi>' \<pi> suc\<iota>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>')) = \<pi>' (Suc \<iota>)
\<pi>' \<equiv> path \<sigma>'
\<pi> \<equiv> path \<sigma>
\<pi>' (Suc \<iota>) \<noteq> \<pi> (Suc \<iota>')

goal (3 subgoals):
 1. \<pi>' = path \<sigma>'
 2. \<pi> = path \<sigma>
 3. \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>\<^esup> \<iota>')) \<noteq> \<pi> (Suc \<iota>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>, \<iota>') \<cc> (\<sigma>', i')

goal (1 subgoal):
 1. \<forall>j>\<iota>. j cd\<^bsup>\<pi>'\<^esup>\<rightarrow> \<iota> \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<iota>') \<cc> (\<sigma>', i')

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using domi'
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<iota>') \<cc> (\<sigma>', i')
\<pi>' i' \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<not> i \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
assume \<open>\<not> i \<le> n'\<close>
[PROOF STATE]
proof (state)
this:
\<not> i \<le> n'

goal (1 subgoal):
 1. \<not> i \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence ni: \<open>n'< i\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i \<le> n'

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

goal (1 subgoal):
 1. \<not> i \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence cdin: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (prove)
using this:
n' < i

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
[PROOF STEP]
using loop
[PROOF STATE]
proof (prove)
using this:
n' < i
\<forall>j'>n'. j' cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'

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

goal (1 subgoal):
 1. \<not> i \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
hence csni': \<open>cs\<^bsup>\<pi>'\<^esup> n \<prec> cs\<^bsup>\<pi>\<^esup> i\<close>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> n \<prec> cs\<^bsup>\<pi>\<^esup> i
[PROOF STEP]
using csn
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
cs\<^bsup>\<pi>'\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

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

goal (1 subgoal):
 1. \<not> i \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have cssel: \<open>\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n)) = \<pi> (Suc n')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n)) = \<pi> (Suc n')
[PROOF STEP]
using csn
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

goal (1 subgoal):
 1. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n)) = \<pi> (Suc n')
[PROOF STEP]
by (metis cdin cd_not_ret cs_select_id path(1))
[PROOF STATE]
proof (state)
this:
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n)) = \<pi> (Suc n')

goal (1 subgoal):
 1. \<not> i \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
have \<open>(\<sigma>',n) \<cc> (\<sigma>,i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>', n) \<cc> (\<sigma>, i)
[PROOF STEP]
using csni'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> n \<prec> cs\<^bsup>\<pi>\<^esup> i

goal (1 subgoal):
 1. (\<sigma>', n) \<cc> (\<sigma>, i)
[PROOF STEP]
apply(rule contradicts.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<pi> = path \<sigma>
 2. \<pi>' = path \<sigma>'
 3. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n)) \<noteq> \<pi>' (Suc n)
[PROOF STEP]
using cssel \<pi>' \<pi> sucn
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n)) = \<pi> (Suc n')
\<pi>' \<equiv> path \<sigma>'
\<pi> \<equiv> path \<sigma>
\<pi>' (Suc n) \<noteq> \<pi> (Suc n')

goal (3 subgoals):
 1. \<pi> = path \<sigma>
 2. \<pi>' = path \<sigma>'
 3. \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> n)) \<noteq> \<pi>' (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<sigma>', n) \<cc> (\<sigma>, i)

goal (1 subgoal):
 1. \<not> i \<le> n' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', n) \<cc> (\<sigma>, i)

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using domi
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', n) \<cc> (\<sigma>, i)
\<pi> i \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed