[STATEMENT]
theorem obs_neq_some_contradicts: fixes \<sigma> \<sigma>' defines \<pi>: \<open>\<pi> \<equiv> path \<sigma>\<close> and \<pi>': \<open>\<pi>' \<equiv> path \<sigma>'\<close>
assumes obsne: \<open>obs \<sigma> k \<noteq> obs \<sigma>' k\<close> and not_none: \<open>obs \<sigma> k \<noteq> None\<close> \<open>obs \<sigma>' k \<noteq> None\<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]
proof -
[PROOF STATE]
proof (state)
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]
obtain i where iki: \<open>is_kth_obs \<pi> k i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. is_kth_obs \<pi> k i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using not_none(1)
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> k \<noteq> None

goal (1 subgoal):
 1. (\<And>i. is_kth_obs \<pi> k i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<pi> obs_some_kth_obs)
[PROOF STATE]
proof (state)
this:
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]
obtain i' where iki': \<open>is_kth_obs \<pi>' k i'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i'. is_kth_obs \<pi>' k i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using not_none(2)
[PROOF STATE]
proof (prove)
using this:
obs \<sigma>' k \<noteq> None

goal (1 subgoal):
 1. (\<And>i'. is_kth_obs \<pi>' k i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<pi>' obs_some_kth_obs)
[PROOF STATE]
proof (state)
this:
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]
have \<open>obsp \<sigma> i = obs \<sigma> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obsp \<sigma> i = obs \<sigma> k
[PROOF STEP]
by (metis \<pi> iki kth_obs_unique obs_def the_equality)
[PROOF STATE]
proof (state)
this:
obsp \<sigma> i = obs \<sigma> k

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]
moreover
[PROOF STATE]
proof (state)
this:
obsp \<sigma> i = obs \<sigma> k

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]
have \<open>obsp \<sigma>' i' = obs \<sigma>' k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obsp \<sigma>' i' = obs \<sigma>' k
[PROOF STEP]
by (metis \<pi>' iki' kth_obs_unique obs_def the_equality)
[PROOF STATE]
proof (state)
this:
obsp \<sigma>' i' = obs \<sigma>' k

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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
obsp \<sigma> i = obs \<sigma> k
obsp \<sigma>' i' = obs \<sigma>' k
[PROOF STEP]
have obspne: \<open>obsp \<sigma> i \<noteq> obsp \<sigma>' i'\<close>
[PROOF STATE]
proof (prove)
using this:
obsp \<sigma> i = obs \<sigma> k
obsp \<sigma>' i' = obs \<sigma>' k

goal (1 subgoal):
 1. obsp \<sigma> i \<noteq> obsp \<sigma>' i'
[PROOF STEP]
using obsne
[PROOF STATE]
proof (prove)
using this:
obsp \<sigma> i = obs \<sigma> k
obsp \<sigma>' i' = obs \<sigma>' k
obs \<sigma> k \<noteq> obs \<sigma>' k

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 (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]
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 obs_neq_some_contradicts'[OF _ iki[unfolded \<pi>] iki'[unfolded \<pi>']]
[PROOF STATE]
proof (prove)
using this:
obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>path \<sigma>\<^esup> i \<noteq> cs\<^bsup>path \<sigma>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' 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]
using obspne \<pi> \<pi>'
[PROOF STATE]
proof (prove)
using this:
obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<or> cs\<^bsup>path \<sigma>\<^esup> i \<noteq> cs\<^bsup>path \<sigma>'\<^esup> i' \<Longrightarrow> \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att
obsp \<sigma> i \<noteq> obsp \<sigma>' i'
\<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 metis
[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


[STATEMENT]
theorem obs_neq_ret_contradicts: fixes \<sigma> \<sigma>' defines \<pi>: \<open>\<pi> \<equiv> path \<sigma>\<close> and \<pi>': \<open>\<pi>' \<equiv> path \<sigma>'\<close>
assumes ret: \<open>\<pi> n = return\<close> and obsne: \<open>obs \<sigma>' i \<noteq> obs \<sigma> i\<close> and obs:\<open>obs \<sigma>' i \<noteq> None\<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]
proof (cases \<open>\<exists> j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists> k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k')\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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 True
[PROOF STATE]
proof (state)
this:
\<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k')

goal (2 subgoals):
 1. \<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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 l k' where jk': \<open>is_kth_obs \<pi>' l k'\<close> and unmatched: \<open>(\<nexists> k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l k'. \<lbrakk>is_kth_obs \<pi>' l k'; \<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
\<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k')

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

goal (2 subgoals):
 1. \<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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]
using \<pi> \<pi>' path0
[PROOF STATE]
proof (prove)
using this:
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
path ?\<sigma> 0 = local.entry

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

goal (2 subgoals):
 1. \<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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 j j' where csj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close> and cd: \<open>k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow>j'\<close> and suc: \<open>\<pi> (Suc j) \<noteq> \<pi>' (Suc j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j j'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'; k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'; \<pi> (Suc j) \<noteq> \<pi>' (Suc j')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using converged_cd_diverge_return[of \<open>\<pi>'\<close> \<open>\<pi>\<close> \<open>k'\<close> \<open>n\<close>] ret unmatched path_is_path \<pi> \<pi>' \<pi>0
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path \<pi>'; is_path \<pi>; \<pi>' 0 = \<pi> 0; \<nexists>l'. cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> l'; \<pi> n = local.return; \<And>k k'a. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>\<^esup> k'a; k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k; \<pi>' (Suc k) \<noteq> \<pi> (Suc k'a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<pi> n = local.return
\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
is_path (path ?\<sigma>)
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
\<pi> 0 = \<pi>' 0

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

goal (2 subgoals):
 1. \<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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>(\<sigma>, j) \<cc> (\<sigma>' ,k')\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<pi> (Suc j) \<noteq> \<pi>' (Suc j')

goal (1 subgoal):
 1. (\<sigma>, j) \<cc> (\<sigma>', k')
[PROOF STEP]
using contradicts.intros(1)[of \<open>\<pi>\<close> \<open>j\<close> \<open>\<pi>'\<close> \<open>k'\<close> \<open>\<sigma>'\<close> \<open>\<sigma>\<close>, unfolded csj] \<pi> \<pi>'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<pi> (Suc j) \<noteq> \<pi>' (Suc j')
\<lbrakk>cs\<^bsup>\<pi>'\<^esup> j' \<prec> cs\<^bsup>\<pi>'\<^esup> k'; \<pi>' = path \<sigma>'; \<pi> = path \<sigma>; \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>'\<^esup> j')) \<noteq> \<pi> (Suc j)\<rbrakk> \<Longrightarrow> (\<sigma>, j) \<cc> (\<sigma>', k')
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'

goal (1 subgoal):
 1. (\<sigma>, j) \<cc> (\<sigma>', k')
[PROOF STEP]
using cd_is_cs_less cd_not_ret cs_select_id
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
k' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j'
\<pi> (Suc j) \<noteq> \<pi>' (Suc j')
\<lbrakk>cs\<^bsup>\<pi>'\<^esup> j' \<prec> cs\<^bsup>\<pi>'\<^esup> k'; \<pi>' = path \<sigma>'; \<pi> = path \<sigma>; \<pi>' (Suc (\<pi>' \<exclamdown> cs\<^bsup>\<pi>'\<^esup> j')) \<noteq> \<pi> (Suc j)\<rbrakk> \<Longrightarrow> (\<sigma>, j) \<cc> (\<sigma>', k')
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
?l cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k \<prec> cs\<^bsup>?\<pi>\<^esup> ?l
?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k \<Longrightarrow> ?\<pi> ?k \<noteq> local.return
\<lbrakk>is_path ?\<pi>; ?\<pi> ?k \<noteq> local.return\<rbrakk> \<Longrightarrow> (?\<pi> \<exclamdown> cs\<^bsup>?\<pi>\<^esup> ?k) = ?k

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

goal (2 subgoals):
 1. \<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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>\<pi>' k' \<in> dom(att)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' k' \<in> dom local.att
[PROOF STEP]
using jk'
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' l k'

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

goal (2 subgoals):
 1. \<exists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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:
\<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]
using *
[PROOF STATE]
proof (prove)
using this:
\<pi>' k' \<in> dom local.att
(\<sigma>, j) \<cc> (\<sigma>', k')

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. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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 False
[PROOF STATE]
proof (state)
this:
\<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k')

goal (1 subgoal):
 1. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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>\<And> j k'. is_kth_obs \<pi>' j k' \<Longrightarrow> \<exists> k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k')

goal (1 subgoal):
 1. \<And>j k'. is_kth_obs \<pi>' j k' \<Longrightarrow> \<exists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi>' ?j1 ?k'1 \<Longrightarrow> \<exists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> ?k'1

goal (1 subgoal):
 1. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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 k' where k': \<open>is_kth_obs \<pi>' i k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. is_kth_obs \<pi>' i k' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obs \<pi>' obs_some_kth_obs
[PROOF STATE]
proof (prove)
using this:
obs \<sigma>' i \<noteq> None
\<pi>' \<equiv> path \<sigma>'
\<lbrakk>obs ?\<sigma> ?k \<noteq> None; \<And>i. is_kth_obs (path ?\<sigma>) ?k i \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>k'. is_kth_obs \<pi>' i k' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi>' i k'

goal (1 subgoal):
 1. \<nexists>j k'. is_kth_obs \<pi>' j k' \<and> (\<nexists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k') \<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 l where \<open>is_kth_obs \<pi> i l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. is_kth_obs \<pi> i l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using * \<pi> \<pi>' k' no_kth_obs_missing_cs path_is_path
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' ?j1 ?k'1 \<Longrightarrow> \<exists>k. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> ?k'1
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
is_kth_obs \<pi>' i k'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; is_kth_obs ?\<pi> ?k ?i; \<nexists>i'. is_kth_obs ?\<pi>' ?k i'; \<And>l j. \<lbrakk>is_kth_obs ?\<pi> l j; \<nexists>j'. cs\<^bsup>?\<pi>\<^esup> j = cs\<^bsup>?\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
is_path (path ?\<sigma>)

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

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

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 \<pi> \<pi>' obs obs_neq_some_contradicts obs_none_no_kth_obs obsne
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> i l
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'
obs \<sigma>' i \<noteq> None
\<lbrakk>obs ?\<sigma> ?k \<noteq> obs ?\<sigma>' ?k; obs ?\<sigma> ?k \<noteq> None; obs ?\<sigma>' ?k \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>k k'. (?\<sigma>', k') \<cc> (?\<sigma>, k) \<and> path ?\<sigma> k \<in> dom local.att \<or> (?\<sigma>, k) \<cc> (?\<sigma>', k') \<and> path ?\<sigma>' k' \<in> dom local.att
obs ?\<sigma> ?k = None \<Longrightarrow> \<nexists>i. is_kth_obs (path ?\<sigma>) ?k i
obs \<sigma>' i \<noteq> obs \<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]
by metis
[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