[STATEMENT]
lemma missing_cs_contradicts: assumes notin: \<open>\<not>(\<exists> k'. cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k')\<close> and converge: \<open>k<n\<close> \<open>cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'\<close> shows \<open>\<exists> j'. (\<sigma>', j') \<cc> (\<sigma>, k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
let \<open>?\<pi>\<close> = \<open>path \<sigma>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
let \<open>?\<pi>'\<close> = \<open>path \<sigma>'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
have init: \<open>?\<pi> 0 = ?\<pi>' 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma> 0 = path \<sigma>' 0
[PROOF STEP]
unfolding 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:
path \<sigma> 0 = path \<sigma>' 0

goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
have path: \<open>is_path ?\<pi>\<close> \<open>is_path ?\<pi>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (path \<sigma>) &&& is_path (path \<sigma>')
[PROOF STEP]
using path_is_path
[PROOF STATE]
proof (prove)
using this:
is_path (path ?\<sigma>)

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

goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[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>path \<sigma>\<^esup> j = cs\<^bsup>path \<sigma>'\<^esup> j'; k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> j; path \<sigma> (Suc j) \<noteq> path \<sigma>' (Suc j')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using converged_cd_diverge[OF path init notin converge]
[PROOF STATE]
proof (prove)
using this:
(\<And>ka k'. \<lbrakk>cs\<^bsup>path \<sigma>\<^esup> ka = cs\<^bsup>path \<sigma>'\<^esup> k'; k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> ka; path \<sigma> (Suc ka) \<noteq> path \<sigma>' (Suc k')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
have less: \<open>cs\<^bsup>?\<pi>\<^esup> j \<prec> cs\<^bsup>?\<pi>\<^esup> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> j \<prec> cs\<^bsup>path \<sigma>\<^esup> k
[PROOF STEP]
using cd cd_is_cs_less
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> j
?l cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?k \<prec> cs\<^bsup>?\<pi>\<^esup> ?l

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> j \<prec> cs\<^bsup>path \<sigma>\<^esup> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>path \<sigma>\<^esup> j \<prec> cs\<^bsup>path \<sigma>\<^esup> k

goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
have nretj: \<open>?\<pi> j \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma> j \<noteq> local.return
[PROOF STEP]
by (metis cd is_cdi_def term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
path \<sigma> j \<noteq> local.return

goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
have cs: \<open>?\<pi> \<exclamdown> cs\<^bsup>?\<pi>'\<^esup> j' = j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma> \<exclamdown> cs\<^bsup>path \<sigma>'\<^esup> j') = j
[PROOF STEP]
using csj cs_select_id nretj path_is_path
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> j = cs\<^bsup>path \<sigma>'\<^esup> j'
\<lbrakk>is_path ?\<pi>; ?\<pi> ?k \<noteq> local.return\<rbrakk> \<Longrightarrow> (?\<pi> \<exclamdown> cs\<^bsup>?\<pi>\<^esup> ?k) = ?k
path \<sigma> j \<noteq> local.return
is_path (path ?\<sigma>)

goal (1 subgoal):
 1. (path \<sigma> \<exclamdown> cs\<^bsup>path \<sigma>'\<^esup> j') = j
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(path \<sigma> \<exclamdown> cs\<^bsup>path \<sigma>'\<^esup> j') = j

goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
have \<open>(\<sigma>',j') \<cc> (\<sigma>,k)\<close>
[PROOF STATE]
proof (prove)
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 cs] less suc csj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cs\<^bsup>path \<sigma>'\<^esup> j' \<prec> cs\<^bsup>path \<sigma>\<^esup> k; path \<sigma> = path \<sigma>; path \<sigma>' = path \<sigma>'; path \<sigma> (Suc j) \<noteq> path \<sigma>' (Suc j')\<rbrakk> \<Longrightarrow> (\<sigma>', j') \<cc> (\<sigma>, k)
cs\<^bsup>path \<sigma>\<^esup> j \<prec> cs\<^bsup>path \<sigma>\<^esup> k
path \<sigma> (Suc j) \<noteq> path \<sigma>' (Suc j')
cs\<^bsup>path \<sigma>\<^esup> j = cs\<^bsup>path \<sigma>'\<^esup> j'

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

goal (1 subgoal):
 1. \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, k)
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', j') \<cc> (\<sigma>, k)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem obs_neq_contradicts_term: 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> \<open>\<pi>' n' = return\<close> and obsne: \<open>obs \<sigma> \<noteq> obs \<sigma>'\<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]
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. \<exists>k k'. (\<sigma>', 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 k1 where neq: \<open>obs \<sigma> k1 \<noteq> obs \<sigma>' k1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k1. obs \<sigma> k1 \<noteq> obs \<sigma>' k1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obsne ext[of \<open>obs \<sigma>\<close> \<open>obs \<sigma>'\<close>]
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> \<noteq> obs \<sigma>'
(\<And>x. obs \<sigma> x = obs \<sigma>' x) \<Longrightarrow> obs \<sigma> = obs \<sigma>'

goal (1 subgoal):
 1. (\<And>k1. obs \<sigma> k1 \<noteq> obs \<sigma>' k1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
obs \<sigma> k1 \<noteq> obs \<sigma>' k1

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]
hence \<open>(\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')
  \<or> (\<exists> k i. is_kth_obs \<pi> k i \<and> \<not> (\<exists> i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
  \<or> (\<exists> k i'. is_kth_obs \<pi>' k i' \<and> \<not> (\<exists> i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))\<close>
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> k1 \<noteq> obs \<sigma>' k1

goal (1 subgoal):
 1. (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
proof(cases rule: option_neq_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = None\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 3. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
case (none2 x)
[PROOF STATE]
proof (state)
this:
obs \<sigma> k1 = Some x
obs \<sigma>' k1 = None

goal (3 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = None\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 3. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
have notin\<pi>': \<open>\<not> (\<exists> l. is_kth_obs \<pi>' k1 l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>l. is_kth_obs \<pi>' k1 l
[PROOF STEP]
using none2(2) \<pi>' obs_none_no_kth_obs
[PROOF STATE]
proof (prove)
using this:
obs \<sigma>' k1 = None
\<pi>' \<equiv> path \<sigma>'
obs ?\<sigma> ?k = None \<Longrightarrow> \<nexists>i. is_kth_obs (path ?\<sigma>) ?k i

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

goal (3 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = None\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 3. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
obtain i where in\<pi>: \<open>is_kth_obs \<pi> k1 i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. is_kth_obs \<pi> k1 i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obs_some_kth_obs[of \<open>\<sigma>\<close> \<open>k1\<close>] none2(1) \<pi>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>obs \<sigma> k1 \<noteq> None; \<And>i. is_kth_obs (path \<sigma>) k1 i \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
obs \<sigma> k1 = Some x
\<pi> \<equiv> path \<sigma>

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

goal (3 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = None\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 3. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
obtain l j where \<open>is_kth_obs \<pi> l j\<close> \<open>\<not> (\<exists> j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<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) \<Longrightarrow> thesis
[PROOF STEP]
using path in\<pi> notin\<pi>'
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
is_kth_obs \<pi> k1 i
\<nexists>l. is_kth_obs \<pi>' k1 l

goal (1 subgoal):
 1. (\<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) \<Longrightarrow> thesis
[PROOF STEP]
by (metis no_kth_obs_missing_cs)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> l j
\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

goal (3 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = None\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 3. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> l j
\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))

goal (2 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
case (none1 x)
[PROOF STATE]
proof (state)
this:
obs \<sigma> k1 = None
obs \<sigma>' k1 = Some x

goal (2 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
have notin\<pi>: \<open>\<not> (\<exists> l. is_kth_obs \<pi> k1 l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>l. is_kth_obs \<pi> k1 l
[PROOF STEP]
using none1(1) \<pi> obs_none_no_kth_obs
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> k1 = None
\<pi> \<equiv> path \<sigma>
obs ?\<sigma> ?k = None \<Longrightarrow> \<nexists>i. is_kth_obs (path ?\<sigma>) ?k i

goal (1 subgoal):
 1. \<nexists>l. is_kth_obs \<pi> k1 l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>l. is_kth_obs \<pi> k1 l

goal (2 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
obtain i' where in\<pi>': \<open>is_kth_obs \<pi>' k1 i'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i'. is_kth_obs \<pi>' k1 i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obs_some_kth_obs[of \<open>\<sigma>'\<close> \<open>k1\<close>] none1(2) \<pi>'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>obs \<sigma>' k1 \<noteq> None; \<And>i. is_kth_obs (path \<sigma>') k1 i \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
obs \<sigma>' k1 = Some x
\<pi>' \<equiv> path \<sigma>'

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

goal (2 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
obtain l j where \<open>is_kth_obs \<pi>' l j\<close> \<open>\<not> (\<exists> j'. cs\<^bsup>\<pi>\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<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) \<Longrightarrow> thesis
[PROOF STEP]
using path in\<pi>' notin\<pi>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
is_kth_obs \<pi>' k1 i'
\<nexists>l. is_kth_obs \<pi> k1 l

goal (1 subgoal):
 1. (\<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) \<Longrightarrow> thesis
[PROOF STEP]
by (metis no_kth_obs_missing_cs)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi>' l j
\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> j

goal (2 subgoals):
 1. \<And>a. \<lbrakk>obs \<sigma> k1 = None; obs \<sigma>' k1 = Some a\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' l j
\<nexists>j'. cs\<^bsup>\<pi>\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> j

goal (1 subgoal):
 1. (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
case (some x y)
[PROOF STATE]
proof (state)
this:
obs \<sigma> k1 = Some x
obs \<sigma>' k1 = Some y
x \<noteq> y

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
obtain i where in\<pi>: \<open>is_kth_obs \<pi> k1 i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. is_kth_obs \<pi> k1 i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obs_some_kth_obs[of \<open>\<sigma>\<close> \<open>k1\<close>] some \<pi>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>obs \<sigma> k1 \<noteq> None; \<And>i. is_kth_obs (path \<sigma>) k1 i \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
obs \<sigma> k1 = Some x
obs \<sigma>' k1 = Some y
x \<noteq> y
\<pi> \<equiv> path \<sigma>

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
obtain i' where in\<pi>': \<open>is_kth_obs \<pi>' k1 i'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i'. is_kth_obs \<pi>' k1 i' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obs_some_kth_obs[of \<open>\<sigma>'\<close> \<open>k1\<close>] some \<pi>'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>obs \<sigma>' k1 \<noteq> None; \<And>i. is_kth_obs (path \<sigma>') k1 i \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
obs \<sigma> k1 = Some x
obs \<sigma>' k1 = Some y
x \<noteq> y
\<pi>' \<equiv> path \<sigma>'

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

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>obs \<sigma> k1 = Some a; obs \<sigma>' k1 = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<not> ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
assume *: \<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 i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<not> ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
have \<open>obsp \<sigma> i = obs \<sigma> k1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obsp \<sigma> i = obs \<sigma> k1
[PROOF STEP]
by (metis obs_def \<pi> in\<pi> kth_obs_unique the_equality)
[PROOF STATE]
proof (state)
this:
obsp \<sigma> i = obs \<sigma> k1

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<not> ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
obsp \<sigma> i = obs \<sigma> k1

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<not> ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
have \<open>obsp \<sigma>' i' = obs \<sigma>' k1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obsp \<sigma>' i' = obs \<sigma>' k1
[PROOF STEP]
by (metis obs_def \<pi>' in\<pi>' kth_obs_unique the_equality)
[PROOF STATE]
proof (state)
this:
obsp \<sigma>' i' = obs \<sigma>' k1

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<not> ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
obsp \<sigma> i = obs \<sigma> k1
obsp \<sigma>' i' = obs \<sigma>' k1
[PROOF STEP]
have \<open>obsp \<sigma> i \<noteq> obsp \<sigma>' i'\<close>
[PROOF STATE]
proof (prove)
using this:
obsp \<sigma> i = obs \<sigma> k1
obsp \<sigma>' i' = obs \<sigma>' k1

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

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 i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
 2. \<not> ?P \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
obsp \<sigma> i \<noteq> obsp \<sigma>' i'

goal (1 subgoal):
 1. (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
using * in\<pi> in\<pi>'
[PROOF STATE]
proof (prove)
using this:
obsp \<sigma> i \<noteq> obsp \<sigma>' i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> k1 i
is_kth_obs \<pi>' k1 i'

goal (1 subgoal):
 1. (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[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 i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
assume *: \<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 i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
note kth_obs_cs_missing_cs[OF path in\<pi> in\<pi>' *]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i' \<Longrightarrow> (\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> 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]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i') \<or> (\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')) \<or> (\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> 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 (cases rule: three_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 3. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
case 1
[PROOF STATE]
proof (state)
this:
\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (3 subgoals):
 1. \<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 3. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
[PROOF STEP]
obtain k i i' where iki: \<open>is_kth_obs \<pi> k i\<close> \<open>is_kth_obs \<pi>' k i'\<close> and obsne: \<open>obsp \<sigma> i \<noteq> obsp \<sigma>' i'\<close> and csi: \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

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

goal (3 subgoals):
 1. \<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 3. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 obsp_contradict[OF csi[unfolded \<pi> \<pi>'] obsne]
[PROOF STATE]
proof (state)
this:
(\<sigma>', i') \<cc> (\<sigma>, i)

goal (3 subgoals):
 1. \<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 3. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>', i') \<cc> (\<sigma>, i)

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

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

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

goal (3 subgoals):
 1. \<exists>k i i'. is_kth_obs \<pi> k i \<and> is_kth_obs \<pi>' k i' \<and> obsp \<sigma> i \<noteq> obsp \<sigma>' i' \<and> cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 3. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>', i') \<cc> (\<sigma>, i)
\<pi> i \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', i') \<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 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 (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')

goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')
[PROOF STEP]
obtain k i where iki: \<open>is_kth_obs \<pi> k i\<close> and notin\<pi>': \<open>\<not> (\<exists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')

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

goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
let \<open>?n\<close> = \<open>Suc (max n i)\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 nn: \<open>n < ?n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < Suc (max n i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < Suc (max n i)

goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 iln: \<open>i < ?n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < Suc (max n i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < Suc (max n i)

goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 retn: \<open>\<pi> ?n = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc (max n i)) = local.return
[PROOF STEP]
using ret term_path_stable path
[PROOF STATE]
proof (prove)
using this:
\<pi> n = local.return
\<pi>' n' = local.return
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?\<pi> ?j = local.return
is_path \<pi>
is_path \<pi>'

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

goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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>cs\<^bsup>\<pi>\<^esup> ?n = cs\<^bsup>\<pi>'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc (max n i)) = local.return

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

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

goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> Suc (max n i) = cs\<^bsup>\<pi>'\<^esup> n'
[PROOF STEP]
obtain i' where \<open>(\<sigma>',i') \<cc> (\<sigma>,i)\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> Suc (max n i) = cs\<^bsup>\<pi>'\<^esup> n'

goal (1 subgoal):
 1. (\<And>i'. (\<sigma>', i') \<cc> (\<sigma>, i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using missing_cs_contradicts[OF notin\<pi>'[unfolded \<pi> \<pi>'] iln] \<pi> \<pi>'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> Suc (max n i) = cs\<^bsup>\<pi>'\<^esup> n'
cs\<^bsup>path \<sigma>\<^esup> Suc (max n i) = cs\<^bsup>path \<sigma>'\<^esup> ?n' \<Longrightarrow> \<exists>j'. (\<sigma>', j') \<cc> (\<sigma>, i)
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'

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

goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>', i') \<cc> (\<sigma>, i)

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

goal (2 subgoals):
 1. \<exists>k i. is_kth_obs \<pi> k i \<and> (\<nexists>i'. cs\<^bsup>\<pi>\<^esup> i = 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
 2. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>', i') \<cc> (\<sigma>, i)
\<pi> i \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', i') \<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 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. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
case 3
[PROOF STATE]
proof (state)
this:
\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')
[PROOF STEP]
obtain k i' where iki: \<open>is_kth_obs \<pi>' k i'\<close> and notin\<pi>': \<open>\<not> (\<exists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i')

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

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
let \<open>?n\<close> = \<open>Suc (max n' i')\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 nn: \<open>n' < ?n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' < Suc (max n' i')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n' < Suc (max n' i')

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 iln: \<open>i' < ?n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < Suc (max n' i')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' < Suc (max n' i')

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 retn: \<open>\<pi>' ?n = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' (Suc (max n' i')) = local.return
[PROOF STEP]
using ret term_path_stable path
[PROOF STATE]
proof (prove)
using this:
\<pi> n = local.return
\<pi>' n' = local.return
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?\<pi> ?j = local.return
is_path \<pi>
is_path \<pi>'

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

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> ?n\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (Suc (max n' i')) = local.return

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

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

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> Suc (max n' i')
[PROOF STEP]
obtain i where \<open>(\<sigma>,i) \<cc> (\<sigma>',i')\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> Suc (max n' i')

goal (1 subgoal):
 1. (\<And>i. (\<sigma>, i) \<cc> (\<sigma>', i') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using missing_cs_contradicts notin\<pi>' iln \<pi> \<pi>'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> Suc (max n' i')
\<lbrakk>\<nexists>k'. cs\<^bsup>path ?\<sigma>\<^esup> ?k = cs\<^bsup>path ?\<sigma>'\<^esup> k'; ?k < ?n; cs\<^bsup>path ?\<sigma>\<^esup> ?n = cs\<^bsup>path ?\<sigma>'\<^esup> ?n'\<rbrakk> \<Longrightarrow> \<exists>j'. (?\<sigma>', j') \<cc> (?\<sigma>, ?k)
\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
i' < Suc (max n' i')
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'

goal (1 subgoal):
 1. (\<And>i. (\<sigma>, i) \<cc> (\<sigma>', i') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<sigma>, i) \<cc> (\<sigma>', i')

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>, i) \<cc> (\<sigma>', i')

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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 \<open>\<pi>' i' \<in> dom att\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' i' \<in> dom local.att
[PROOF STEP]
using iki is_kth_obs_def
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' k i'
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>' i' \<in> dom local.att
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k i'. is_kth_obs \<pi>' k i' \<and> (\<nexists>i. cs\<^bsup>\<pi>\<^esup> i = 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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, i) \<cc> (\<sigma>', i')
\<pi>' i' \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, i) \<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 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:
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