[STATEMENT]
lemma kth_obs_cs_missing_cs:  assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and iki: \<open>is_kth_obs \<pi> k i\<close> and iki': \<open>is_kth_obs \<pi>' k i'\<close> and csi: \<open>cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'\<close>
obtains l j where \<open>j \<le> i\<close> \<open>is_kth_obs \<pi> l j\<close> \<open>\<not> (\<exists> j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close> | l' j' where \<open>j' \<le> i'\<close> \<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. \<lbrakk>\<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume nt: \<open>\<not> thesis\<close>
[PROOF STATE]
proof (state)
this:
\<not> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using iki iki' csi that
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
\<lbrakk>?j1 \<le> i; is_kth_obs \<pi> ?l1 ?j1; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> ?j1 = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?j'1 \<le> i'; is_kth_obs \<pi>' ?l'1 ?j'1; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> ?j'1\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof (induction \<open>k\<close> arbitrary: \<open>i\<close> \<open>i'\<close> rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (less k i i')
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < k; is_kth_obs \<pi> ?y1 ?i1; is_kth_obs \<pi>' ?y1 ?i'1; cs\<^bsup>\<pi>\<^esup> ?i1 \<noteq> cs\<^bsup>\<pi>'\<^esup> ?i'1; \<And>j l. \<lbrakk>j \<le> ?i1; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> ?i'1; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
\<lbrakk>?j1 \<le> i; is_kth_obs \<pi> ?l1 ?j1; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> ?j1 = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?j'1 \<le> i'; is_kth_obs \<pi>' ?l'1 ?j'1; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> ?j'1\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence all_in_\<pi>': \<open>\<forall> l j. j\<le>i \<and> is_kth_obs \<pi> l j \<longrightarrow> (\<exists> j' . cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
    and all_in_\<pi>: \<open>\<forall> l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<longrightarrow> (\<exists> j . cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 < k; is_kth_obs \<pi> ?y1 ?i1; is_kth_obs \<pi>' ?y1 ?i'1; cs\<^bsup>\<pi>\<^esup> ?i1 \<noteq> cs\<^bsup>\<pi>'\<^esup> ?i'1; \<And>j l. \<lbrakk>j \<le> ?i1; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> ?i'1; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
\<lbrakk>?j1 \<le> i; is_kth_obs \<pi> ?l1 ?j1; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> ?j1 = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?j'1 \<le> i'; is_kth_obs \<pi>' ?l'1 ?j'1; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> ?j'1\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain j j' where csji: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> i'\<close> and csij: \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j j'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> i'; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using all_in_\<pi> all_in_\<pi>' less
[PROOF STATE]
proof (prove)
using this:
\<forall>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<longrightarrow> (\<exists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
\<forall>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
\<lbrakk>?y1 < k; is_kth_obs \<pi> ?y1 ?i1; is_kth_obs \<pi>' ?y1 ?i'1; cs\<^bsup>\<pi>\<^esup> ?i1 \<noteq> cs\<^bsup>\<pi>'\<^esup> ?i'1; \<And>j l. \<lbrakk>j \<le> ?i1; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> ?i'1; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
\<lbrakk>?j1 \<le> i; is_kth_obs \<pi> ?l1 ?j1; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> ?j1 = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?j'1 \<le> i'; is_kth_obs \<pi>' ?l'1 ?j'1; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> ?j'1\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
obtain l l' where ilj: \<open>is_kth_obs \<pi> l j\<close> and ilj': \<open>is_kth_obs \<pi>' l' j'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> i'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. (\<And>l l'. \<lbrakk>is_kth_obs \<pi> l j; is_kth_obs \<pi>' l' j'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis is_kth_obs_def last_cs less.prems(1,2))
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> l j
is_kth_obs \<pi>' l' j'

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have lnk: \<open>l \<noteq> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> k
[PROOF STEP]
using ilj csji less(2) less(4) kth_obs_unique
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> l j
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> i'
is_kth_obs \<pi> k i
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
\<lbrakk>is_kth_obs ?\<pi> ?k ?i; is_kth_obs ?\<pi> ?k ?j\<rbrakk> \<Longrightarrow> ?i = ?j

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

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have lnk': \<open>l' \<noteq> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' \<noteq> k
[PROOF STEP]
using ilj' csij less(3) less(4) kth_obs_unique
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' l' j'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> j'
is_kth_obs \<pi>' k i'
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
\<lbrakk>is_kth_obs ?\<pi> ?k ?i; is_kth_obs ?\<pi> ?k ?j\<rbrakk> \<Longrightarrow> ?i = ?j

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

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have cseq: \<open>\<forall> l j j'. l < k \<and>  is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
fix t p p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
assume tk: \<open>t < k\<close> and ikp: \<open>is_kth_obs \<pi> t p\<close> and ikp': \<open>is_kth_obs \<pi>' t p'\<close>
[PROOF STATE]
proof (state)
this:
t < k
is_kth_obs \<pi> t p
is_kth_obs \<pi>' t p'

goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
hence pi: \<open>p < i\<close> and pi': \<open>p' < i'\<close>
[PROOF STATE]
proof (prove)
using this:
t < k
is_kth_obs \<pi> t p
is_kth_obs \<pi>' t p'

goal (1 subgoal):
 1. p < i &&& p' < i'
[PROOF STEP]
by (metis kth_obs_mono less.prems(1)) (metis kth_obs_mono less.prems(2) tk ikp')
[PROOF STATE]
proof (state)
this:
p < i
p' < i'

goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
have *: \<open>\<And>j l. j \<le> p \<Longrightarrow> is_kth_obs \<pi> l j \<Longrightarrow> \<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j l. \<lbrakk>j \<le> p; is_kth_obs \<pi> l j\<rbrakk> \<Longrightarrow> \<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
using pi all_in_\<pi>'
[PROOF STATE]
proof (prove)
using this:
p < i
\<forall>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

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

goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
have **: \<open>\<And>j' l'. j' \<le> p' \<Longrightarrow> is_kth_obs \<pi>' l' j' \<Longrightarrow> \<exists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j' l'. \<lbrakk>j' \<le> p'; is_kth_obs \<pi>' l' j'\<rbrakk> \<Longrightarrow> \<exists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
using pi' all_in_\<pi>
[PROOF STATE]
proof (prove)
using this:
p' < i'
\<forall>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<longrightarrow> (\<exists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')

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

goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> p = cs\<^bsup>\<pi>'\<^esup> p'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> p = cs\<^bsup>\<pi>'\<^esup> p'
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> p \<noteq> cs\<^bsup>\<pi>'\<^esup> p' \<Longrightarrow> False
[PROOF STEP]
using less(1)[OF tk ikp ikp'] * **
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cs\<^bsup>\<pi>\<^esup> p \<noteq> cs\<^bsup>\<pi>'\<^esup> p'; \<And>j l. \<lbrakk>j \<le> p; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> p'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
\<lbrakk>?j1 \<le> p; is_kth_obs \<pi> ?l1 ?j1\<rbrakk> \<Longrightarrow> \<exists>j'. cs\<^bsup>\<pi>\<^esup> ?j1 = cs\<^bsup>\<pi>'\<^esup> j'
\<lbrakk>?j'1 \<le> p'; is_kth_obs \<pi>' ?l'1 ?j'1\<rbrakk> \<Longrightarrow> \<exists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> ?j'1

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

goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?t3 < k; is_kth_obs \<pi> ?t3 ?p3; is_kth_obs \<pi>' ?t3 ?p'3\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> ?p3 = cs\<^bsup>\<pi>'\<^esup> ?p'3

goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t3 < k; is_kth_obs \<pi> ?t3 ?p3; is_kth_obs \<pi>' ?t3 ?p'3\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> ?p3 = cs\<^bsup>\<pi>'\<^esup> ?p'3

goal (1 subgoal):
 1. \<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

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

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have ii'nret: \<open>\<pi> i \<noteq> return \<or> \<pi>' i' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> i \<noteq> local.return \<or> \<pi>' i' \<noteq> local.return
[PROOF STEP]
using less cs_return
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 < k; is_kth_obs \<pi> ?y1 ?i1; is_kth_obs \<pi>' ?y1 ?i'1; cs\<^bsup>\<pi>\<^esup> ?i1 \<noteq> cs\<^bsup>\<pi>'\<^esup> ?i'1; \<And>j l. \<lbrakk>j \<le> ?i1; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> ?i'1; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'
\<lbrakk>?j1 \<le> i; is_kth_obs \<pi> ?l1 ?j1; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> ?j1 = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?j'1 \<le> i'; is_kth_obs \<pi>' ?l'1 ?j'1; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> ?j'1\<rbrakk> \<Longrightarrow> thesis
?\<pi> ?n = local.return \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?n = [?\<pi> ?n]

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

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have a: \<open>k < l \<or> k < l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < l \<or> k < l'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (k < l \<or> k < l') \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not>(k < l \<or> k < l')\<close>
[PROOF STATE]
proof (state)
this:
\<not> (k < l \<or> k < l')

goal (1 subgoal):
 1. \<not> (k < l \<or> k < l') \<Longrightarrow> False
[PROOF STEP]
hence *: \<open>l < k\<close> \<open>l' < k\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (k < l \<or> k < l')

goal (1 subgoal):
 1. l < k &&& l' < k
[PROOF STEP]
using lnk lnk'
[PROOF STATE]
proof (prove)
using this:
\<not> (k < l \<or> k < l')
l \<noteq> k
l' \<noteq> k

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

goal (1 subgoal):
 1. \<not> (k < l \<or> k < l') \<Longrightarrow> False
[PROOF STEP]
hence ji: \<open>j < i\<close> and ji': \<open>j' < i'\<close>
[PROOF STATE]
proof (prove)
using this:
l < k
l' < k

goal (1 subgoal):
 1. j < i &&& j' < i'
[PROOF STEP]
using ilj ilj' less(2,3) kth_obs_mono
[PROOF STATE]
proof (prove)
using this:
l < k
l' < k
is_kth_obs \<pi> l j
is_kth_obs \<pi>' l' j'
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
\<lbrakk>is_kth_obs ?\<pi> ?k ?i; is_kth_obs ?\<pi> ?l ?j; ?k < ?l\<rbrakk> \<Longrightarrow> ?i < ?j

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

goal (1 subgoal):
 1. \<not> (k < l \<or> k < l') \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using ii'nret
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return \<or> \<pi>' i' \<noteq> local.return

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<pi> i \<noteq> local.return \<Longrightarrow> False
 2. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
assume nreti: \<open>\<pi> i \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> i \<noteq> local.return

goal (2 subgoals):
 1. \<pi> i \<noteq> local.return \<Longrightarrow> False
 2. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
hence nretj': \<open>\<pi>' j' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return

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

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

goal (2 subgoals):
 1. \<pi> i \<noteq> local.return \<Longrightarrow> False
 2. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using cs_order[OF path(2,1) csij[symmetric] csji[symmetric] nretj' ji'] ji
[PROOF STATE]
proof (prove)
using this:
i < j
j < i

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

goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
assume nreti': \<open>\<pi>' i' \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<noteq> local.return

goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
hence nretj': \<open>\<pi> j \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' i' \<noteq> local.return

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

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

goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using cs_order[OF path csji csij nretj' ji] ji'
[PROOF STATE]
proof (prove)
using this:
i' < j'
j' < i'

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k < l \<or> k < l'

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>l < k \<or> l' < k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < k \<or> l' < k
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (l < k \<or> l' < k) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> (l< k \<or> l' < k)\<close>
[PROOF STATE]
proof (state)
this:
\<not> (l < k \<or> l' < k)

goal (1 subgoal):
 1. \<not> (l < k \<or> l' < k) \<Longrightarrow> False
[PROOF STEP]
hence \<open>k < l\<close> \<open>k < l'\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (l < k \<or> l' < k)

goal (1 subgoal):
 1. k < l &&& k < l'
[PROOF STEP]
using lnk lnk'
[PROOF STATE]
proof (prove)
using this:
\<not> (l < k \<or> l' < k)
l \<noteq> k
l' \<noteq> k

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

goal (1 subgoal):
 1. \<not> (l < k \<or> l' < k) \<Longrightarrow> False
[PROOF STEP]
hence ji: \<open>i < j\<close> and ji': \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
k < l
k < l'

goal (1 subgoal):
 1. i < j &&& i' < j'
[PROOF STEP]
using ilj ilj' less(2,3) kth_obs_mono
[PROOF STATE]
proof (prove)
using this:
k < l
k < l'
is_kth_obs \<pi> l j
is_kth_obs \<pi>' l' j'
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
\<lbrakk>is_kth_obs ?\<pi> ?k ?i; is_kth_obs ?\<pi> ?l ?j; ?k < ?l\<rbrakk> \<Longrightarrow> ?i < ?j

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

goal (1 subgoal):
 1. \<not> (l < k \<or> l' < k) \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using ii'nret
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return \<or> \<pi>' i' \<noteq> local.return

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<pi> i \<noteq> local.return \<Longrightarrow> False
 2. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
assume nreti: \<open>\<pi> i \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> i \<noteq> local.return

goal (2 subgoals):
 1. \<pi> i \<noteq> local.return \<Longrightarrow> False
 2. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using cs_order[OF path csij csji nreti ji]  ji'
[PROOF STATE]
proof (prove)
using this:
j' < i'
i' < j'

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

goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
assume nreti': \<open>\<pi>' i' \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<noteq> local.return

goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using cs_order[OF path(2,1) csji[symmetric] csij[symmetric] nreti' ji'] ji
[PROOF STATE]
proof (prove)
using this:
j < i
i < j

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l < k \<or> l' < k

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>k < l \<and> l' < k \<or> k < l' \<and> l < k\<close>
[PROOF STATE]
proof (prove)
using this:
l < k \<or> l' < k

goal (1 subgoal):
 1. k < l \<and> l' < k \<or> k < l' \<and> l < k
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
l < k \<or> l' < k
k < l \<or> k < l'

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

goal (1 subgoal):
 1. \<And>x i i'. \<lbrakk>\<And>y i i'. \<lbrakk>y < x; is_kth_obs \<pi> y i; is_kth_obs \<pi>' y i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False; is_kth_obs \<pi> x i; is_kth_obs \<pi>' x i'; cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>'\<^esup> i'; \<And>j l. \<lbrakk>j \<le> i; is_kth_obs \<pi> l j; \<nexists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis; \<And>j' l'. \<lbrakk>j' \<le> i'; is_kth_obs \<pi>' l' j'; \<nexists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
k < l \<and> l' < k \<or> k < l' \<and> l < k

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
assume \<open>k < l \<and> l' < k\<close>
[PROOF STATE]
proof (state)
this:
k < l \<and> l' < k

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence kl: \<open>k < l\<close> and lk': \<open>l' < k\<close>
[PROOF STATE]
proof (prove)
using this:
k < l \<and> l' < k

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

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence ij: \<open>i < j\<close> and ji': \<open>j' < i'\<close>
[PROOF STATE]
proof (prove)
using this:
k < l
l' < k

goal (1 subgoal):
 1. i < j &&& j' < i'
[PROOF STEP]
using less(2,3) ilj ilj' kth_obs_mono
[PROOF STATE]
proof (prove)
using this:
k < l
l' < k
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
is_kth_obs \<pi> l j
is_kth_obs \<pi>' l' j'
\<lbrakk>is_kth_obs ?\<pi> ?k ?i; is_kth_obs ?\<pi> ?l ?j; ?k < ?l\<rbrakk> \<Longrightarrow> ?i < ?j

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

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
have nreti: \<open>\<pi> i \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> i \<noteq> local.return
[PROOF STEP]
by (metis csji ii'nret ij last_cs path(1) term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
\<pi> i \<noteq> local.return

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
obtain h where ilh: \<open>is_kth_obs \<pi> l' h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. is_kth_obs \<pi> l' h \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ji' all_in_\<pi> ilj' no_kth_obs_missing_cs path(1) path(2)
[PROOF STATE]
proof (prove)
using this:
j' < i'
\<forall>l' j'. j' \<le> i' \<and> is_kth_obs \<pi>' l' j' \<longrightarrow> (\<exists>j. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
is_kth_obs \<pi>' l' j'
\<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 \<pi>
is_path \<pi>'

goal (1 subgoal):
 1. (\<And>h. is_kth_obs \<pi> l' h \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis kl lk' ilj kth_obs_stable)
[PROOF STATE]
proof (state)
this:
is_kth_obs \<pi> l' h

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> h = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> l' h

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> h = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
using cseq lk' ilj'
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> l' h
\<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
l' < k
is_kth_obs \<pi>' l' j'

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

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> h\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> h = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> h
[PROOF STEP]
using csij
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> h = cs\<^bsup>\<pi>'\<^esup> j'
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> j'

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

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence hi: \<open>h = i\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> h

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

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

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
have \<open>l' = k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' = k
[PROOF STEP]
using less(2) ilh
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> k i
is_kth_obs \<pi> l' h

goal (1 subgoal):
 1. l' = k
[PROOF STEP]
unfolding hi
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi> k i
is_kth_obs \<pi> l' i

goal (1 subgoal):
 1. l' = k
[PROOF STEP]
by (metis is_kth_obs_def)
[PROOF STATE]
proof (state)
this:
l' = k

goal (2 subgoals):
 1. k < l \<and> l' < k \<Longrightarrow> False
 2. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
l' = k

goal (1 subgoal):
 1. False
[PROOF STEP]
using lk'
[PROOF STATE]
proof (prove)
using this:
l' = k
l' < k

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

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
assume \<open>k < l' \<and> l < k\<close>
[PROOF STATE]
proof (state)
this:
k < l' \<and> l < k

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence kl': \<open>k < l'\<close> and lk: \<open>l < k\<close>
[PROOF STATE]
proof (prove)
using this:
k < l' \<and> l < k

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

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence ij': \<open>i' < j'\<close> and ji: \<open>j < i\<close>
[PROOF STATE]
proof (prove)
using this:
k < l'
l < k

goal (1 subgoal):
 1. i' < j' &&& j < i
[PROOF STEP]
using less(2,3) ilj ilj' kth_obs_mono
[PROOF STATE]
proof (prove)
using this:
k < l'
l < k
is_kth_obs \<pi> k i
is_kth_obs \<pi>' k i'
is_kth_obs \<pi> l j
is_kth_obs \<pi>' l' j'
\<lbrakk>is_kth_obs ?\<pi> ?k ?i; is_kth_obs ?\<pi> ?l ?j; ?k < ?l\<rbrakk> \<Longrightarrow> ?i < ?j

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

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
have nreti': \<open>\<pi>' i' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return
[PROOF STEP]
by (metis csij ii'nret ij' last_cs path(2) term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<noteq> local.return

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
obtain h' where ilh': \<open>is_kth_obs \<pi>' l h'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h'. is_kth_obs \<pi>' l h' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using all_in_\<pi>' ilj no_kth_obs_missing_cs path(1) path(2) kl' lk ilj' kth_obs_stable
[PROOF STATE]
proof (prove)
using this:
\<forall>l j. j \<le> i \<and> is_kth_obs \<pi> l j \<longrightarrow> (\<exists>j'. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j')
is_kth_obs \<pi> l j
\<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 \<pi>
is_path \<pi>'
k < l'
l < k
is_kth_obs \<pi>' l' j'
\<lbrakk>is_kth_obs ?\<pi> ?l ?j; ?k < ?l\<rbrakk> \<Longrightarrow> \<exists>i. is_kth_obs ?\<pi> ?k i

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

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> h'\<close>
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' l h'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> h'
[PROOF STEP]
using cseq lk ilj
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' l h'
\<forall>l j j'. l < k \<and> is_kth_obs \<pi> l j \<and> is_kth_obs \<pi>' l j' \<longrightarrow> cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'
l < k
is_kth_obs \<pi> l j

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

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> h'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> h'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> h'
[PROOF STEP]
using csji
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> h'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> i'

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

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
hence hi: \<open>h' = i'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> h'

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

goal (1 subgoal):
 1. h' = i'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
h' = i'

goal (1 subgoal):
 1. k < l' \<and> l < k \<Longrightarrow> False
[PROOF STEP]
have \<open>l = k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = k
[PROOF STEP]
using less(3) ilh'
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' k i'
is_kth_obs \<pi>' l h'

goal (1 subgoal):
 1. l = k
[PROOF STEP]
unfolding hi
[PROOF STATE]
proof (prove)
using this:
is_kth_obs \<pi>' k i'
is_kth_obs \<pi>' l i'

goal (1 subgoal):
 1. l = k
[PROOF STEP]
by (metis is_kth_obs_def)
[PROOF STATE]
proof (state)
this:
l = k

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using lk
[PROOF STATE]
proof (prove)
using this:
l = k
l < k

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reads_restrict1: \<open>\<sigma> \<restriction> (reads n) = \<sigma>' \<restriction> (reads n) \<Longrightarrow> \<forall> x \<in> reads n. \<sigma> x = \<sigma>' x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<restriction> local.reads n = \<sigma>' \<restriction> local.reads n \<Longrightarrow> \<forall>x\<in>local.reads n. \<sigma> x = \<sigma>' x
[PROOF STEP]
by (metis restrict_def)


[STATEMENT]
lemma reads_restrict2: \<open>\<forall> x \<in> reads n. \<sigma> x = \<sigma>' x \<Longrightarrow> \<sigma> \<restriction> (reads n) = \<sigma>' \<restriction> (reads n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>local.reads n. \<sigma> x = \<sigma>' x \<Longrightarrow> \<sigma> \<restriction> local.reads n = \<sigma>' \<restriction> local.reads n
[PROOF STEP]
unfolding restrict_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>local.reads n. \<sigma> x = \<sigma>' x \<Longrightarrow> (\<lambda>na. if na \<in> local.reads n then \<sigma> na else undefined) = (\<lambda>na. if na \<in> local.reads n then \<sigma>' na else undefined)
[PROOF STEP]
by auto


[STATEMENT]
lemma reads_restrict: \<open>(\<sigma> \<restriction> (reads n) = \<sigma>' \<restriction> (reads n)) = (\<forall> x \<in> reads n. \<sigma> x = \<sigma>' x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma> \<restriction> local.reads n = \<sigma>' \<restriction> local.reads n) = (\<forall>x\<in>local.reads n. \<sigma> x = \<sigma>' x)
[PROOF STEP]
using reads_restrict1 reads_restrict2
[PROOF STATE]
proof (prove)
using this:
?\<sigma> \<restriction> local.reads ?n = ?\<sigma>' \<restriction> local.reads ?n \<Longrightarrow> \<forall>x\<in>local.reads ?n. ?\<sigma> x = ?\<sigma>' x
\<forall>x\<in>local.reads ?n. ?\<sigma> x = ?\<sigma>' x \<Longrightarrow> ?\<sigma> \<restriction> local.reads ?n = ?\<sigma>' \<restriction> local.reads ?n

goal (1 subgoal):
 1. (\<sigma> \<restriction> local.reads n = \<sigma>' \<restriction> local.reads n) = (\<forall>x\<in>local.reads n. \<sigma> x = \<sigma>' x)
[PROOF STEP]
by metis


[STATEMENT]
lemma reads_restr_suc: \<open>\<sigma> \<restriction> (reads n) = \<sigma>' \<restriction> (reads n) \<Longrightarrow> suc n \<sigma> = suc n \<sigma>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<restriction> local.reads n = \<sigma>' \<restriction> local.reads n \<Longrightarrow> suc n \<sigma> = suc n \<sigma>'
[PROOF STEP]
by (metis reads_restrict uses_suc)


[STATEMENT]
lemma reads_restr_sem: \<open>\<sigma> \<restriction> (reads n) = \<sigma>' \<restriction> (reads n) \<Longrightarrow> \<forall> v \<in> writes n. sem n \<sigma> v = sem n \<sigma>' v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<restriction> local.reads n = \<sigma>' \<restriction> local.reads n \<Longrightarrow> \<forall>v\<in>local.writes n. sem n \<sigma> v = sem n \<sigma>' v
[PROOF STEP]
by (metis reads_restrict1 uses_writes)


[STATEMENT]
lemma reads_obsp: assumes \<open>path \<sigma> k = path \<sigma>' k'\<close> \<open>\<sigma>\<^bsup>k\<^esup> \<restriction> (reads (path \<sigma> k)) = \<sigma>'\<^bsup>k'\<^esup> \<restriction> (reads (path \<sigma> k))\<close> shows \<open>obsp \<sigma> k = obsp \<sigma>' k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obsp \<sigma> k = obsp \<sigma>' k'
[PROOF STEP]
using assms(2) uses_att
[PROOF STATE]
proof (prove)
using this:
\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (path \<sigma> k) = \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (path \<sigma> k)
\<lbrakk>local.att ?n = Some ?f; \<forall>v\<in>local.reads ?n. ?\<sigma> v = ?\<sigma>' v\<rbrakk> \<Longrightarrow> ?f ?\<sigma> = ?f ?\<sigma>'

goal (1 subgoal):
 1. obsp \<sigma> k = obsp \<sigma>' k'
[PROOF STEP]
unfolding obsp_def assms(1) reads_restrict
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>local.reads (path \<sigma>' k'). (\<sigma>\<^bsup>k\<^esup>) x = (\<sigma>'\<^bsup>k'\<^esup>) x
\<lbrakk>local.att ?n = Some ?f; \<forall>v\<in>local.reads ?n. ?\<sigma> v = ?\<sigma>' v\<rbrakk> \<Longrightarrow> ?f ?\<sigma> = ?f ?\<sigma>'

goal (1 subgoal):
 1. (case local.att (path \<sigma>' k') of None \<Rightarrow> None | Some f \<Rightarrow> Some (f (\<sigma>\<^bsup>k\<^esup>))) = (case local.att (path \<sigma>' k') of None \<Rightarrow> None | Some f \<Rightarrow> Some (f (\<sigma>'\<^bsup>k'\<^esup>)))
[PROOF STEP]
apply (cases \<open>att (path \<sigma>' k')\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>local.reads (path \<sigma>' k'). (\<sigma>\<^bsup>k\<^esup>) x = (\<sigma>'\<^bsup>k'\<^esup>) x; \<And>n f \<sigma> \<sigma>'. \<lbrakk>local.att n = Some f; \<forall>v\<in>local.reads n. \<sigma> v = \<sigma>' v\<rbrakk> \<Longrightarrow> f \<sigma> = f \<sigma>'; local.att (path \<sigma>' k') = None\<rbrakk> \<Longrightarrow> (case local.att (path \<sigma>' k') of None \<Rightarrow> None | Some f \<Rightarrow> Some (f (\<sigma>\<^bsup>k\<^esup>))) = (case local.att (path \<sigma>' k') of None \<Rightarrow> None | Some f \<Rightarrow> Some (f (\<sigma>'\<^bsup>k'\<^esup>)))
 2. \<And>a. \<lbrakk>\<forall>x\<in>local.reads (path \<sigma>' k'). (\<sigma>\<^bsup>k\<^esup>) x = (\<sigma>'\<^bsup>k'\<^esup>) x; \<And>n f \<sigma> \<sigma>'. \<lbrakk>local.att n = Some f; \<forall>v\<in>local.reads n. \<sigma> v = \<sigma>' v\<rbrakk> \<Longrightarrow> f \<sigma> = f \<sigma>'; local.att (path \<sigma>' k') = Some a\<rbrakk> \<Longrightarrow> (case local.att (path \<sigma>' k') of None \<Rightarrow> None | Some f \<Rightarrow> Some (f (\<sigma>\<^bsup>k\<^esup>))) = (case local.att (path \<sigma>' k') of None \<Rightarrow> None | Some f \<Rightarrow> Some (f (\<sigma>'\<^bsup>k'\<^esup>)))
[PROOF STEP]
by auto


[STATEMENT]
lemma no_writes_unchanged0: assumes \<open>\<forall> l<k. v\<notin> writes(path \<sigma> l)\<close> shows \<open>(\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>l<k. v \<notin> local.writes (path \<sigma> l)

goal (1 subgoal):
 1. (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v
[PROOF STEP]
proof (induction \<open>k\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>l<0. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>0\<^esup>) v = \<sigma> v
 2. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>l<0. v \<notin> local.writes (path \<sigma> l)

goal (2 subgoals):
 1. \<forall>l<0. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>0\<^esup>) v = \<sigma> v
 2. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>l<0. v \<notin> local.writes (path \<sigma> l)

goal (1 subgoal):
 1. (\<sigma>\<^bsup>0\<^esup>) v = \<sigma> v
[PROOF STEP]
by(auto simp add: kth_state_def)
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^bsup>0\<^esup>) v = \<sigma> v

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v
\<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
hence \<open>(\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v
\<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)

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

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
have \<open>\<sigma>\<^bsup>Suc k\<^esup>  = snd ( step (path \<sigma> k,\<sigma>\<^bsup>k\<^esup>))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^bsup>Suc k\<^esup> = snd (local.step (path \<sigma> k, \<sigma>\<^bsup>k\<^esup>))
[PROOF STEP]
by (metis kth_state_suc)
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsup>Suc k\<^esup> = snd (local.step (path \<sigma> k, \<sigma>\<^bsup>k\<^esup>))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
hence \<open>\<sigma>\<^bsup>Suc k\<^esup>  = sem (path \<sigma> k) (\<sigma>\<^bsup>k\<^esup>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<sigma>\<^bsup>Suc k\<^esup> = snd (local.step (path \<sigma> k, \<sigma>\<^bsup>k\<^esup>))

goal (1 subgoal):
 1. \<sigma>\<^bsup>Suc k\<^esup> = sem (path \<sigma> k) (\<sigma>\<^bsup>k\<^esup>)
[PROOF STEP]
by (metis step_suc_sem snd_conv)
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsup>Suc k\<^esup> = sem (path \<sigma> k) (\<sigma>\<^bsup>k\<^esup>)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsup>Suc k\<^esup> = sem (path \<sigma> k) (\<sigma>\<^bsup>k\<^esup>)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
have \<open>v \<notin> writes (path \<sigma> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> local.writes (path \<sigma> k)
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
\<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)

goal (1 subgoal):
 1. v \<notin> local.writes (path \<sigma> k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<notin> local.writes (path \<sigma> k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>l<k. v \<notin> local.writes (path \<sigma> l) \<Longrightarrow> (\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v; \<forall>l<Suc k. v \<notin> local.writes (path \<sigma> l)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v
\<sigma>\<^bsup>Suc k\<^esup> = sem (path \<sigma> k) (\<sigma>\<^bsup>k\<^esup>)
v \<notin> local.writes (path \<sigma> k)
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v
\<sigma>\<^bsup>Suc k\<^esup> = sem (path \<sigma> k) (\<sigma>\<^bsup>k\<^esup>)
v \<notin> local.writes (path \<sigma> k)

goal (1 subgoal):
 1. (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
using writes
[PROOF STATE]
proof (prove)
using this:
(\<sigma>\<^bsup>k\<^esup>) v = \<sigma> v
\<sigma>\<^bsup>Suc k\<^esup> = sem (path \<sigma> k) (\<sigma>\<^bsup>k\<^esup>)
v \<notin> local.writes (path \<sigma> k)
\<exists>\<sigma>. \<sigma> ?v \<noteq> sem ?n \<sigma> ?v \<Longrightarrow> ?v \<in> local.writes ?n

goal (1 subgoal):
 1. (\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^bsup>Suc k\<^esup>) v = \<sigma> v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma written_read_dd: assumes \<open>is_path \<pi>\<close> \<open>v \<in> reads (\<pi> k) \<close> \<open>v \<in> writes (\<pi> j)\<close> \<open>j<k\<close> obtains l where \<open>k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let \<open>?l\<close> = \<open>GREATEST l. l < k \<and> v \<in> writes (\<pi> l)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>?l < k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)) < k
[PROOF STEP]
by (metis (no_types, lifting) GreatestI_ex_nat assms(3) assms(4) less_or_eq_imp_le)
[PROOF STATE]
proof (state)
this:
(GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)) < k

goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)) < k

goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>v \<in> writes (\<pi> ?l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))
[PROOF STEP]
by (metis (no_types, lifting) GreatestI_nat assms(3) assms(4) less_or_eq_imp_le)
[PROOF STATE]
proof (state)
this:
v \<in> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))

goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>v \<in> reads (\<pi> k) \<inter> writes (\<pi> ?l)\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))

goal (1 subgoal):
 1. v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
v \<in> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))
v \<in> local.reads (\<pi> k)

goal (1 subgoal):
 1. v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))

goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))

goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note is_ddi_def
[PROOF STATE]
proof (state)
this:
(?n dd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?m) = (is_path ?\<pi> \<and> ?m < ?n \<and> ?v \<in> local.reads (?\<pi> ?n) \<inter> local.writes (?\<pi> ?m) \<and> (\<forall>l\<in>{?m<..<?n}. ?v \<notin> local.writes (?\<pi> l)))

goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<forall> l \<in> {?l<..<k}. v \<notin> writes (\<pi> l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>{GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)<..<k}. v \<notin> local.writes (\<pi> l)
[PROOF STEP]
by (auto, metis (lifting, no_types) Greatest_le_nat le_antisym nat_less_le)
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>{GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)<..<k}. v \<notin> local.writes (\<pi> l)

goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)) < k
v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))
\<forall>l\<in>{GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)<..<k}. v \<notin> local.writes (\<pi> l)
[PROOF STEP]
have \<open>k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> ?l\<close>
[PROOF STATE]
proof (prove)
using this:
(GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)) < k
v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))
\<forall>l\<in>{GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)<..<k}. v \<notin> local.writes (\<pi> l)

goal (1 subgoal):
 1. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)) < k
v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))
\<forall>l\<in>{GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)<..<k}. v \<notin> local.writes (\<pi> l)
is_path \<pi>

goal (1 subgoal):
 1. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l))
[PROOF STEP]
unfolding is_ddi_def
[PROOF STATE]
proof (prove)
using this:
(GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)) < k
v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)))
\<forall>l\<in>{GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)<..<k}. v \<notin> local.writes (\<pi> l)
is_path \<pi>

goal (1 subgoal):
 1. is_path \<pi> \<and> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)) < k \<and> v \<in> local.reads (\<pi> k) \<inter> local.writes (\<pi> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l))) \<and> (\<forall>l\<in>{GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l)<..<k}. v \<notin> local.writes (\<pi> l))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l))

goal (1 subgoal):
 1. (\<And>l. k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> (GREATEST l. l < k \<and> v \<in> local.writes (\<pi> l))
k dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> ?l1 \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_writes_unchanged: assumes \<open>k \<le> l\<close> \<open>\<forall> j \<in> {k..<l}. v\<notin> writes(path \<sigma> j)\<close> shows \<open>(\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<le> l
\<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)

goal (1 subgoal):
 1. (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
proof (induction \<open>l - k\<close> arbitrary: \<open>l\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>0 = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
 2. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = l - k
k \<le> l
\<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)

goal (2 subgoals):
 1. \<And>l. \<lbrakk>0 = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
 2. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
0 = l - k
k \<le> l
\<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)

goal (1 subgoal):
 1. (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
case (Suc lk l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>lk = ?l1 - k; k \<le> ?l1; \<forall>j\<in>{k..<?l1}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>?l1\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
Suc lk = l - k
k \<le> l
\<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
hence kl: \<open>k < l\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>lk = ?l1 - k; k \<le> ?l1; \<forall>j\<in>{k..<?l1}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>?l1\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
Suc lk = l - k
k \<le> l
\<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)

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

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k < l
[PROOF STEP]
obtain l' where lsuc: \<open>l = Suc l'\<close>
[PROOF STATE]
proof (prove)
using this:
k < l

goal (1 subgoal):
 1. (\<And>l'. l = Suc l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lessE
[PROOF STATE]
proof (prove)
using this:
k < l
\<lbrakk>?i < ?k; ?k = Suc ?i \<Longrightarrow> ?P; \<And>j. \<lbrakk>?i < j; ?k = Suc j\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>l'. l = Suc l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l = Suc l'

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
hence \<open>lk = l' - k\<close>
[PROOF STATE]
proof (prove)
using this:
l = Suc l'

goal (1 subgoal):
 1. lk = l' - k
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
l = Suc l'
\<lbrakk>lk = ?l1 - k; k \<le> ?l1; \<forall>j\<in>{k..<?l1}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>?l1\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
Suc lk = l - k
k \<le> l
\<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)

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

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lk = l' - k

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
have \<open>\<forall> j \<in> {k..<l'}. v \<notin> writes (path \<sigma> j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{k..<l'}. v \<notin> local.writes (path \<sigma> j)
[PROOF STEP]
using Suc(4) lsuc
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)
l = Suc l'

goal (1 subgoal):
 1. \<forall>j\<in>{k..<l'}. v \<notin> local.writes (path \<sigma> j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>{k..<l'}. v \<notin> local.writes (path \<sigma> j)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lk = l' - k
\<forall>j\<in>{k..<l'}. v \<notin> local.writes (path \<sigma> j)
[PROOF STEP]
have \<open>(\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v\<close>
[PROOF STATE]
proof (prove)
using this:
lk = l' - k
\<forall>j\<in>{k..<l'}. v \<notin> local.writes (path \<sigma> j)

goal (1 subgoal):
 1. (\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
using Suc(1)[of \<open>l'\<close>] lsuc kl
[PROOF STATE]
proof (prove)
using this:
lk = l' - k
\<forall>j\<in>{k..<l'}. v \<notin> local.writes (path \<sigma> j)
\<lbrakk>lk = l' - k; k \<le> l'; \<forall>j\<in>{k..<l'}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
l = Suc l'
k < l

goal (1 subgoal):
 1. (\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
have \<open>\<sigma>\<^bsup>l\<^esup> = snd ( step (path \<sigma> l',\<sigma>\<^bsup>l'\<^esup>))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^bsup>l\<^esup> = snd (local.step (path \<sigma> l', \<sigma>\<^bsup>l'\<^esup>))
[PROOF STEP]
by (metis kth_state_suc lsuc)
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsup>l\<^esup> = snd (local.step (path \<sigma> l', \<sigma>\<^bsup>l'\<^esup>))

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
hence \<open>\<sigma>\<^bsup>l\<^esup> = sem (path \<sigma> l') (\<sigma>\<^bsup>l'\<^esup>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<sigma>\<^bsup>l\<^esup> = snd (local.step (path \<sigma> l', \<sigma>\<^bsup>l'\<^esup>))

goal (1 subgoal):
 1. \<sigma>\<^bsup>l\<^esup> = sem (path \<sigma> l') (\<sigma>\<^bsup>l'\<^esup>)
[PROOF STEP]
by (metis step_suc_sem snd_conv)
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsup>l\<^esup> = sem (path \<sigma> l') (\<sigma>\<^bsup>l'\<^esup>)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsup>l\<^esup> = sem (path \<sigma> l') (\<sigma>\<^bsup>l'\<^esup>)

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
have \<open>l' < l\<close> \<open>k \<le> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' < l &&& k \<le> l'
[PROOF STEP]
using kl lsuc
[PROOF STATE]
proof (prove)
using this:
k < l
l = Suc l'

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

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
hence \<open>v \<notin> writes (path \<sigma> l')\<close>
[PROOF STATE]
proof (prove)
using this:
l' < l
k \<le> l'

goal (1 subgoal):
 1. v \<notin> local.writes (path \<sigma> l')
[PROOF STEP]
using Suc.prems(2)
[PROOF STATE]
proof (prove)
using this:
l' < l
k \<le> l'
\<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)

goal (1 subgoal):
 1. v \<notin> local.writes (path \<sigma> l')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<notin> local.writes (path \<sigma> l')

goal (1 subgoal):
 1. \<And>x l. \<lbrakk>\<And>l. \<lbrakk>x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v; Suc x = l - k; k \<le> l; \<forall>j\<in>{k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
\<sigma>\<^bsup>l\<^esup> = sem (path \<sigma> l') (\<sigma>\<^bsup>l'\<^esup>)
v \<notin> local.writes (path \<sigma> l')
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
\<sigma>\<^bsup>l\<^esup> = sem (path \<sigma> l') (\<sigma>\<^bsup>l'\<^esup>)
v \<notin> local.writes (path \<sigma> l')

goal (1 subgoal):
 1. (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
[PROOF STEP]
using writes
[PROOF STATE]
proof (prove)
using this:
(\<sigma>\<^bsup>l'\<^esup>) v = (\<sigma>\<^bsup>k\<^esup>) v
\<sigma>\<^bsup>l\<^esup> = sem (path \<sigma> l') (\<sigma>\<^bsup>l'\<^esup>)
v \<notin> local.writes (path \<sigma> l')
\<exists>\<sigma>. \<sigma> ?v \<noteq> sem ?n \<sigma> ?v \<Longrightarrow> ?v \<in> local.writes ?n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ddi_value: assumes \<open>l dd\<^bsup>(path \<sigma>),v\<^esup>\<rightarrow> k\<close> shows \<open>(\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>Suc k\<^esup> ) v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>Suc k\<^esup>) v
[PROOF STEP]
using assms no_writes_unchanged[of \<open>Suc k\<close> \<open>l\<close> \<open>v\<close> \<open>\<sigma>\<close>]
[PROOF STATE]
proof (prove)
using this:
l dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k
\<lbrakk>Suc k \<le> l; \<forall>j\<in>{Suc k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>Suc k\<^esup>) v

goal (1 subgoal):
 1. (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>Suc k\<^esup>) v
[PROOF STEP]
unfolding is_ddi_def
[PROOF STATE]
proof (prove)
using this:
is_path (path \<sigma>) \<and> k < l \<and> v \<in> local.reads (path \<sigma> l) \<inter> local.writes (path \<sigma> k) \<and> (\<forall>l\<in>{k<..<l}. v \<notin> local.writes (path \<sigma> l))
\<lbrakk>Suc k \<le> l; \<forall>j\<in>{Suc k..<l}. v \<notin> local.writes (path \<sigma> j)\<rbrakk> \<Longrightarrow> (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>Suc k\<^esup>) v

goal (1 subgoal):
 1. (\<sigma>\<^bsup>l\<^esup>) v = (\<sigma>\<^bsup>Suc k\<^esup>) v
[PROOF STEP]
by auto


[STATEMENT]
lemma written_value: assumes \<open>path \<sigma> l = path \<sigma>' l'\<close> \<open>\<sigma>\<^bsup>l\<^esup> \<restriction> reads (path \<sigma> l) = \<sigma>'\<^bsup>l'\<^esup> \<restriction> reads (path \<sigma> l)\<close> \<open>v \<in> writes (path \<sigma> l)\<close>
shows \<open>(\<sigma>\<^bsup>Suc l\<^esup> ) v = (\<sigma>'\<^bsup>Suc l'\<^esup> ) v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>\<^bsup>Suc l\<^esup>) v = (\<sigma>'\<^bsup>Suc l'\<^esup>) v
[PROOF STEP]
by (metis assms reads_restr_sem snd_conv step_suc_sem kth_state_suc)


[STATEMENT]
lemma obsp_contradict: assumes csk: \<open>cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'\<close> and obs: \<open>obsp \<sigma> k \<noteq> obsp \<sigma>' k'\<close> shows \<open>(\<sigma>', k') \<cc> (\<sigma>, k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>', k') \<cc> (\<sigma>, k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<sigma>', k') \<cc> (\<sigma>, k)
[PROOF STEP]
have pk: \<open>path \<sigma> k = path \<sigma>' k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma> k = path \<sigma>' k'
[PROOF STEP]
using assms last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
obsp \<sigma> k \<noteq> obsp \<sigma>' k'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

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

goal (1 subgoal):
 1. (\<sigma>', k') \<cc> (\<sigma>, k)
[PROOF STEP]
hence \<open>\<sigma>\<^bsup>k\<^esup>\<restriction>(reads (path \<sigma> k)) \<noteq> \<sigma>'\<^bsup>k'\<^esup>\<restriction>(reads (path \<sigma> k))\<close>
[PROOF STATE]
proof (prove)
using this:
path \<sigma> k = path \<sigma>' k'

goal (1 subgoal):
 1. \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (path \<sigma> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (path \<sigma> k)
[PROOF STEP]
using obs reads_obsp[OF pk]
[PROOF STATE]
proof (prove)
using this:
path \<sigma> k = path \<sigma>' k'
obsp \<sigma> k \<noteq> obsp \<sigma>' k'
\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (path \<sigma> k) = \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (path \<sigma> k) \<Longrightarrow> obsp \<sigma> k = obsp \<sigma>' k'

goal (1 subgoal):
 1. \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (path \<sigma> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (path \<sigma> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (path \<sigma> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (path \<sigma> k)

goal (1 subgoal):
 1. (\<sigma>', k') \<cc> (\<sigma>, k)
[PROOF STEP]
thus \<open>(\<sigma>',k') \<cc> (\<sigma>,k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (path \<sigma> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (path \<sigma> k)

goal (1 subgoal):
 1. (\<sigma>', k') \<cc> (\<sigma>, k)
[PROOF STEP]
using contradicts.intros(2)[OF csk[symmetric]]
[PROOF STATE]
proof (prove)
using this:
\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (path \<sigma> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (path \<sigma> k)
\<lbrakk>path \<sigma> = path ?\<sigma>; path \<sigma>' = path ?\<sigma>'; ?\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (path \<sigma> k) \<noteq> ?\<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (path \<sigma> k)\<rbrakk> \<Longrightarrow> (?\<sigma>', k') \<cc> (?\<sigma>, k)

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

goal:
No subgoals!
[PROOF STEP]
qed