[STATEMENT]
theorem contradicting_in_cop: assumes \<open>\<sigma> =\<^sub>L \<sigma>'\<close> and \<open>(\<sigma>',k') \<cc> (\<sigma>,k)\<close> and \<open>path \<sigma> k \<in> dom att\<close>
shows \<open>((\<sigma>,k),\<sigma>',k') \<in> cop\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', k') \<cc> (\<sigma>, k)

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
 2. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
case (1 \<pi>' \<pi>)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k
\<pi> = path \<sigma>
\<pi>' = path \<sigma>'
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')

goal (2 subgoals):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
 2. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
define j where \<open>j \<equiv> \<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k'\<close>
[PROOF STATE]
proof (state)
this:
j \<equiv> \<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k'

goal (2 subgoals):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
 2. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
have csj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> k'
[PROOF STEP]
unfolding j_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k') = cs\<^bsup>\<pi>'\<^esup> k'
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k
\<pi> = path \<sigma>
\<pi>' = path \<sigma>'
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')

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

goal (2 subgoals):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
 2. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
have suc: \<open>\<pi> (Suc j) \<noteq> \<pi>' (Suc k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc j) \<noteq> \<pi>' (Suc k')
[PROOF STEP]
using 1 j_def
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k
\<pi> = path \<sigma>
\<pi>' = path \<sigma>'
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')
j \<equiv> \<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k'

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

goal (2 subgoals):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
 2. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
have kcdj: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
by (metis cs_not_nil cs_select_is_cs(2) 1(1,2) j_def path_is_path)
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (2 subgoals):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
 2. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
obtain v where readv: \<open>v\<in>reads(path \<sigma> j)\<close> and vneq: \<open>(\<sigma>\<^bsup>j\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> local.reads (path \<sigma> j); (\<sigma>\<^bsup>j\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using suc csj
[PROOF STATE]
proof (prove)
using this:
\<pi> (Suc j) \<noteq> \<pi>' (Suc k')
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> k'

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> local.reads (path \<sigma> j); (\<sigma>\<^bsup>j\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
using this:
path \<sigma> (Suc j) \<noteq> path \<sigma>' (Suc k')
cs\<^bsup>path \<sigma>\<^esup> j = cs\<^bsup>path \<sigma>'\<^esup> k'

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> local.reads (path \<sigma> j); (\<sigma>\<^bsup>j\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis IFC_def.suc_def 1(2) 1(3) last_cs path_suc reads_restr_suc reads_restrict)
[PROOF STATE]
proof (state)
this:
v \<in> local.reads (path \<sigma> j)
(\<sigma>\<^bsup>j\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v

goal (2 subgoals):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
 2. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
have \<open>((\<sigma>,j),\<sigma>',k') \<in> cp\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<sigma>, j), \<sigma>', k') \<in> cp
[PROOF STEP]
apply (rule contradicting_in_cp[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. cs\<^bsup>path \<sigma>\<^esup> j = cs\<^bsup>path \<sigma>'\<^esup> k'
 2. ?v \<in> local.reads (path \<sigma> j)
 3. (\<sigma>\<^bsup>j\<^esup>) ?v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) ?v
[PROOF STEP]
using readv vneq csj 1
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma> j)
(\<sigma>\<^bsup>j\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> k'
cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k
\<pi> = path \<sigma>
\<pi>' = path \<sigma>'
\<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')

goal (3 subgoals):
 1. cs\<^bsup>path \<sigma>\<^esup> j = cs\<^bsup>path \<sigma>'\<^esup> k'
 2. ?v \<in> local.reads (path \<sigma> j)
 3. (\<sigma>\<^bsup>j\<^esup>) ?v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) ?v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<sigma>, j), \<sigma>', k') \<in> cp

goal (2 subgoals):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
 2. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
thus \<open>((\<sigma>,k),\<sigma>',k') \<in> cop\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, j), \<sigma>', k') \<in> cp

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
using kcdj suc assms(3) cop.intros(2)
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, j), \<sigma>', k') \<in> cp
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
\<pi> (Suc j) \<noteq> \<pi>' (Suc k')
path \<sigma> k \<in> dom local.att
\<lbrakk>((?\<sigma>, ?k), ?\<sigma>', ?k') \<in> cp; ?n cd\<^bsup>path ?\<sigma>\<^esup>\<rightarrow> ?k; path ?\<sigma> (Suc ?k) \<noteq> path ?\<sigma>' (Suc ?k'); path ?\<sigma> ?n \<in> dom local.att\<rbrakk> \<Longrightarrow> ((?\<sigma>, ?n), ?\<sigma>', ?k') \<in> cop

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, j), \<sigma>', k') \<in> cp
k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> j
path \<sigma> (Suc j) \<noteq> path \<sigma>' (Suc k')
path \<sigma> k \<in> dom local.att
\<lbrakk>((?\<sigma>, ?k), ?\<sigma>', ?k') \<in> cp; ?n cd\<^bsup>path ?\<sigma>\<^esup>\<rightarrow> ?k; path ?\<sigma> (Suc ?k) \<noteq> path ?\<sigma>' (Suc ?k'); path ?\<sigma> ?n \<in> dom local.att\<rbrakk> \<Longrightarrow> ((?\<sigma>, ?n), ?\<sigma>', ?k') \<in> cop

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

goal (1 subgoal):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
case (2 \<pi>' \<pi>)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k
\<pi> = path \<sigma>
\<pi>' = path \<sigma>'
\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)

goal (1 subgoal):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
obtain v where readv: \<open>v\<in>reads(path \<sigma> k)\<close> and vneq: \<open>(\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> local.reads (path \<sigma> k); (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2(2-4)
[PROOF STATE]
proof (prove)
using this:
\<pi> = path \<sigma>
\<pi>' = path \<sigma>'
\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> local.reads (path \<sigma> k); (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis reads_restrict)
[PROOF STATE]
proof (state)
this:
v \<in> local.reads (path \<sigma> k)
(\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v

goal (1 subgoal):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
have \<open>((\<sigma>,k),\<sigma>',k') \<in> cp\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cp
[PROOF STEP]
apply (rule contradicting_in_cp[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
 2. ?v \<in> local.reads (path \<sigma> k)
 3. (\<sigma>\<^bsup>k\<^esup>) ?v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) ?v
[PROOF STEP]
using readv vneq 2
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma> k)
(\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v
cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k
\<pi> = path \<sigma>
\<pi>' = path \<sigma>'
\<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)

goal (3 subgoals):
 1. cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
 2. ?v \<in> local.reads (path \<sigma> k)
 3. (\<sigma>\<^bsup>k\<^esup>) ?v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) ?v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<sigma>, k), \<sigma>', k') \<in> cp

goal (1 subgoal):
 1. \<And>\<pi>' \<pi>. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k; \<pi> = path \<sigma>; \<pi>' = path \<sigma>'; \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)\<rbrakk> \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
thus \<open>((\<sigma>,k),\<sigma>',k') \<in> cop\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
using assms(3) cop.intros(1)
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp
path \<sigma> k \<in> dom local.att
\<lbrakk>((?\<sigma>, ?n), ?\<sigma>', ?n') \<in> cp; path ?\<sigma> ?n \<in> dom local.att\<rbrakk> \<Longrightarrow> ((?\<sigma>, ?n), ?\<sigma>', ?n') \<in> cop

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
unfolding 2
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp
path \<sigma> k \<in> dom local.att
\<lbrakk>((?\<sigma>, ?n), ?\<sigma>', ?n') \<in> cp; path ?\<sigma> ?n \<in> dom local.att\<rbrakk> \<Longrightarrow> ((?\<sigma>, ?n), ?\<sigma>', ?n') \<in> cop

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem cop_correct_term: fixes \<sigma> \<sigma>' defines \<pi>: \<open>\<pi> \<equiv> path \<sigma>\<close> and \<pi>': \<open>\<pi>' \<equiv> path \<sigma>'\<close>
assumes ret: \<open>\<pi> n = return\<close> \<open>\<pi>' n' = return\<close> and obsne: \<open>obs \<sigma> \<noteq> obs \<sigma>'\<close> and leq: \<open>\<sigma> =\<^sub>L \<sigma>'\<close>
shows \<open>\<exists> k k'. ((\<sigma>,k),\<sigma>',k')\<in> cop \<or> ((\<sigma>',k'),\<sigma>,k)\<in> cop\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
have *: \<open>\<exists> k k'. ((\<sigma>', k') \<cc> (\<sigma> ,k) \<and> \<pi> k \<in> dom (att)) \<or> ((\<sigma>, k) \<cc> (\<sigma>' ,k') \<and> \<pi>' k' \<in> dom (att))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
using  obs_neq_contradicts_term ret obsne \<pi> \<pi>'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>path ?\<sigma> ?n = local.return; path ?\<sigma>' ?n' = local.return; obs ?\<sigma> \<noteq> obs ?\<sigma>'\<rbrakk> \<Longrightarrow> \<exists>k k'. (?\<sigma>', k') \<cc> (?\<sigma>, k) \<and> path ?\<sigma> k \<in> dom local.att \<or> (?\<sigma>, k) \<cc> (?\<sigma>', k') \<and> path ?\<sigma>' k' \<in> dom local.att
\<pi> n = local.return
\<pi>' n' = local.return
obs \<sigma> \<noteq> obs \<sigma>'
\<pi> \<equiv> path \<sigma>
\<pi>' \<equiv> path \<sigma>'

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

goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
have leq' :\<open>\<sigma>' =\<^sub>L \<sigma>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' =\<^sub>L \<sigma>
[PROOF STEP]
using leq
[PROOF STATE]
proof (prove)
using this:
\<sigma> =\<^sub>L \<sigma>'

goal (1 subgoal):
 1. \<sigma>' =\<^sub>L \<sigma>
[PROOF STEP]
unfolding loweq_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<restriction> (- local.hvars) = \<sigma>' \<restriction> (- local.hvars)

goal (1 subgoal):
 1. \<sigma>' \<restriction> (- local.hvars) = \<sigma> \<restriction> (- local.hvars)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>' =\<^sub>L \<sigma>

goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
from * contradicting_in_cop[OF leq] contradicting_in_cop[OF leq']
[PROOF STATE]
proof (chain)
picking this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
\<lbrakk>(\<sigma>', ?k') \<cc> (\<sigma>, ?k); path \<sigma> ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>, ?k), \<sigma>', ?k') \<in> cop
\<lbrakk>(\<sigma>, ?k') \<cc> (\<sigma>', ?k); path \<sigma>' ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>', ?k), \<sigma>, ?k') \<in> cop
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
\<lbrakk>(\<sigma>', ?k') \<cc> (\<sigma>, ?k); path \<sigma> ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>, ?k), \<sigma>', ?k') \<in> cop
\<lbrakk>(\<sigma>, ?k') \<cc> (\<sigma>', ?k); path \<sigma>' ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>', ?k), \<sigma>, ?k') \<in> cop

goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
unfolding \<pi> \<pi>'
[PROOF STATE]
proof (prove)
using this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att
\<lbrakk>(\<sigma>', ?k') \<cc> (\<sigma>, ?k); path \<sigma> ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>, ?k), \<sigma>', ?k') \<in> cop
\<lbrakk>(\<sigma>, ?k') \<cc> (\<sigma>', ?k); path \<sigma>' ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>', ?k), \<sigma>, ?k') \<in> cop

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem cop_correct_ret: fixes \<sigma> \<sigma>' defines \<pi>: \<open>\<pi> \<equiv> path \<sigma>\<close> and \<pi>': \<open>\<pi>' \<equiv> path \<sigma>'\<close>
assumes ret: \<open>\<pi> n = return\<close> and obsne: \<open>obs \<sigma> i \<noteq> obs \<sigma>' i\<close> and obs: \<open>obs \<sigma>' i \<noteq> None\<close> and leq: \<open>\<sigma> =\<^sub>L \<sigma>'\<close>
shows \<open>\<exists> k k'. ((\<sigma>,k),\<sigma>',k')\<in> cop \<or> ((\<sigma>',k'),\<sigma>,k)\<in> cop\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
have *: \<open>\<exists> k k'. ((\<sigma>', k') \<cc> (\<sigma> ,k) \<and> \<pi> k \<in> dom (att)) \<or> ((\<sigma>, k) \<cc> (\<sigma>' ,k') \<and> \<pi>' k' \<in> dom (att))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
[PROOF STEP]
by (metis (no_types, lifting) \<pi> \<pi>' obs obs_neq_ret_contradicts obsne ret)
[PROOF STATE]
proof (state)
this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att

goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
have leq' :\<open>\<sigma>' =\<^sub>L \<sigma>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' =\<^sub>L \<sigma>
[PROOF STEP]
using leq
[PROOF STATE]
proof (prove)
using this:
\<sigma> =\<^sub>L \<sigma>'

goal (1 subgoal):
 1. \<sigma>' =\<^sub>L \<sigma>
[PROOF STEP]
unfolding loweq_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<restriction> (- local.hvars) = \<sigma>' \<restriction> (- local.hvars)

goal (1 subgoal):
 1. \<sigma>' \<restriction> (- local.hvars) = \<sigma> \<restriction> (- local.hvars)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>' =\<^sub>L \<sigma>

goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
from * contradicting_in_cop[OF leq] contradicting_in_cop[OF leq']
[PROOF STATE]
proof (chain)
picking this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
\<lbrakk>(\<sigma>', ?k') \<cc> (\<sigma>, ?k); path \<sigma> ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>, ?k), \<sigma>', ?k') \<in> cop
\<lbrakk>(\<sigma>, ?k') \<cc> (\<sigma>', ?k); path \<sigma>' ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>', ?k), \<sigma>, ?k') \<in> cop
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> \<pi> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> \<pi>' k' \<in> dom local.att
\<lbrakk>(\<sigma>', ?k') \<cc> (\<sigma>, ?k); path \<sigma> ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>, ?k), \<sigma>', ?k') \<in> cop
\<lbrakk>(\<sigma>, ?k') \<cc> (\<sigma>', ?k); path \<sigma>' ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>', ?k), \<sigma>, ?k') \<in> cop

goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
unfolding \<pi> \<pi>'
[PROOF STATE]
proof (prove)
using this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att
\<lbrakk>(\<sigma>', ?k') \<cc> (\<sigma>, ?k); path \<sigma> ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>, ?k), \<sigma>', ?k') \<in> cop
\<lbrakk>(\<sigma>, ?k') \<cc> (\<sigma>', ?k); path \<sigma>' ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((\<sigma>', ?k), \<sigma>, ?k') \<in> cop

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem cop_correct_nterm: assumes obsne: \<open>obs \<sigma> k \<noteq> obs \<sigma>' k\<close> \<open>obs \<sigma> k \<noteq> None\<close> \<open>obs \<sigma>' k \<noteq> None\<close>
and leq: \<open>\<sigma> =\<^sub>L \<sigma>'\<close>
shows \<open>\<exists> k k'. ((\<sigma>,k),\<sigma>',k')\<in> cop \<or> ((\<sigma>',k'),\<sigma>,k)\<in> cop\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
obtain k k' where \<open>((\<sigma>', k') \<cc> (\<sigma> ,k) \<and> path \<sigma> k \<in> dom att) \<or> ((\<sigma>, k) \<cc> (\<sigma>' ,k') \<and> path \<sigma>' k' \<in> dom att)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' k. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obs_neq_some_contradicts[OF obsne]
[PROOF STATE]
proof (prove)
using this:
\<exists>k k'. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att

goal (1 subgoal):
 1. (\<And>k' k. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<or> (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att

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

goal (1 subgoal):
 1. \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<Longrightarrow> \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
 2. (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att \<Longrightarrow> \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
assume *: \<open>(\<sigma>', k') \<cc> (\<sigma> ,k) \<and> path \<sigma> k \<in> dom att\<close>
[PROOF STATE]
proof (state)
this:
(\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att

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

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
using leq
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
\<sigma> =\<^sub>L \<sigma>'

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

goal (2 subgoals):
 1. (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<Longrightarrow> \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
 2. (\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att \<Longrightarrow> \<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cop

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

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

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

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

goal (1 subgoal):
 1. ((\<sigma>', k'), \<sigma>, k) \<in> cop
[PROOF STEP]
using leq
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, k) \<cc> (\<sigma>', k') \<and> path \<sigma>' k' \<in> dom local.att
\<sigma> =\<^sub>L \<sigma>'

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k k'. ((\<sigma>, k), \<sigma>', k') \<in> cop \<or> ((\<sigma>', k'), \<sigma>, k) \<in> cop

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem cop_correct: assumes \<open>cop = empty\<close> shows \<open>secure\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> secure \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> secure\<close>
[PROOF STATE]
proof (state)
this:
\<not> secure

goal (1 subgoal):
 1. \<not> secure \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> secure
[PROOF STEP]
obtain \<sigma> \<sigma>' where leq: \<open> \<sigma> =\<^sub>L \<sigma>'\<close>
    and **: \<open>\<not> obs \<sigma> \<approx> obs \<sigma>' \<or> (terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> secure

goal (1 subgoal):
 1. (\<And>\<sigma> \<sigma>'. \<lbrakk>\<sigma> =\<^sub>L \<sigma>'; \<not> obs \<sigma> \<approx> obs \<sigma>' \<or> terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding secure_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>\<sigma> \<sigma>'. \<sigma> =\<^sub>L \<sigma>' \<longrightarrow> obs \<sigma> \<approx> obs \<sigma>' \<and> (terminates \<sigma> \<longrightarrow> obs \<sigma>' \<lesssim> obs \<sigma>))

goal (1 subgoal):
 1. (\<And>\<sigma> \<sigma>'. \<lbrakk>\<sigma> =\<^sub>L \<sigma>'; \<not> obs \<sigma> \<approx> obs \<sigma>' \<or> terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>'
\<not> obs \<sigma> \<approx> obs \<sigma>' \<or> terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>

goal (1 subgoal):
 1. \<not> secure \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
\<not> obs \<sigma> \<approx> obs \<sigma>' \<or> terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> obs \<sigma> \<approx> obs \<sigma>' \<Longrightarrow> False
 2. terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> obs \<sigma> \<approx> obs \<sigma>'\<close>
[PROOF STATE]
proof (state)
this:
\<not> obs \<sigma> \<approx> obs \<sigma>'

goal (2 subgoals):
 1. \<not> obs \<sigma> \<approx> obs \<sigma>' \<Longrightarrow> False
 2. terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> obs \<sigma> \<approx> obs \<sigma>'
[PROOF STEP]
obtain k where \<open>obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma> k \<noteq> None \<and> obs \<sigma>' k \<noteq> None\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> obs \<sigma> \<approx> obs \<sigma>'

goal (1 subgoal):
 1. (\<And>k. obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma> k \<noteq> None \<and> obs \<sigma>' k \<noteq> None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding obs_comp_def obs_prefix_def
[PROOF STATE]
proof (prove)
using this:
\<not> ((\<forall>i. obs \<sigma> i \<noteq> None \<longrightarrow> obs \<sigma> i = obs \<sigma>' i) \<or> (\<forall>i. obs \<sigma>' i \<noteq> None \<longrightarrow> obs \<sigma>' i = obs \<sigma> i))

goal (1 subgoal):
 1. (\<And>k. obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma> k \<noteq> None \<and> obs \<sigma>' k \<noteq> None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis kth_obs_stable linorder_neqE_nat obs_none_no_kth_obs obs_some_kth_obs)
[PROOF STATE]
proof (state)
this:
obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma> k \<noteq> None \<and> obs \<sigma>' k \<noteq> None

goal (2 subgoals):
 1. \<not> obs \<sigma> \<approx> obs \<sigma>' \<Longrightarrow> False
 2. terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma> k \<noteq> None \<and> obs \<sigma>' k \<noteq> None

goal (1 subgoal):
 1. False
[PROOF STEP]
using cop_correct_nterm leq assms
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma> k \<noteq> None \<and> obs \<sigma>' k \<noteq> None
\<lbrakk>obs ?\<sigma> ?k \<noteq> obs ?\<sigma>' ?k; obs ?\<sigma> ?k \<noteq> None; obs ?\<sigma>' ?k \<noteq> None; ?\<sigma> =\<^sub>L ?\<sigma>'\<rbrakk> \<Longrightarrow> \<exists>k k'. ((?\<sigma>, k), ?\<sigma>', k') \<in> cop \<or> ((?\<sigma>', k'), ?\<sigma>, k) \<in> cop
\<sigma> =\<^sub>L \<sigma>'
cop = {}

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

goal (1 subgoal):
 1. terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma> \<Longrightarrow> False
[PROOF STEP]
assume *: \<open>terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>\<close>
[PROOF STATE]
proof (state)
this:
terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>

goal (1 subgoal):
 1. terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>
[PROOF STEP]
obtain n where ret: \<open>path \<sigma> n = return\<close>
[PROOF STATE]
proof (prove)
using this:
terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>

goal (1 subgoal):
 1. (\<And>n. path \<sigma> n = local.return \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding terminates_def
[PROOF STATE]
proof (prove)
using this:
(\<exists>i. path \<sigma> i = local.return) \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>

goal (1 subgoal):
 1. (\<And>n. path \<sigma> n = local.return \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path \<sigma> n = local.return

goal (1 subgoal):
 1. terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma> \<Longrightarrow> False
[PROOF STEP]
obtain k where \<open>obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma>' k \<noteq> None\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma>' k \<noteq> None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma>

goal (1 subgoal):
 1. (\<And>k. obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma>' k \<noteq> None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding obs_prefix_def
[PROOF STATE]
proof (prove)
using this:
terminates \<sigma> \<and> \<not> (\<forall>i. obs \<sigma>' i \<noteq> None \<longrightarrow> obs \<sigma>' i = obs \<sigma> i)

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

goal (1 subgoal):
 1. terminates \<sigma> \<and> \<not> obs \<sigma>' \<lesssim> obs \<sigma> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma>' k \<noteq> None

goal (1 subgoal):
 1. False
[PROOF STEP]
using cop_correct_ret ret leq assms
[PROOF STATE]
proof (prove)
using this:
obs \<sigma> k \<noteq> obs \<sigma>' k \<and> obs \<sigma>' k \<noteq> None
\<lbrakk>path ?\<sigma> ?n = local.return; obs ?\<sigma> ?i \<noteq> obs ?\<sigma>' ?i; obs ?\<sigma>' ?i \<noteq> None; ?\<sigma> =\<^sub>L ?\<sigma>'\<rbrakk> \<Longrightarrow> \<exists>k k'. ((?\<sigma>, k), ?\<sigma>', k') \<in> cop \<or> ((?\<sigma>', k'), ?\<sigma>, k) \<in> cop
path \<sigma> n = local.return
\<sigma> =\<^sub>L \<sigma>'
cop = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis empty_iff)
[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]
theorem cp_iff_reads_contradict: \<open>((\<sigma>,k),(\<sigma>',k')) \<in> cp \<longleftrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists> v\<in>reads(path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<sigma>, k), \<sigma>', k') \<in> cp) = (\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cp \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)
 2. \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v) \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cp
[PROOF STEP]
assume \<open>\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<close>
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (2 subgoals):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cp \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)
 2. \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v) \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cp
[PROOF STEP]
thus \<open>((\<sigma>, k), \<sigma>', k') \<in> cp\<close>
[PROOF STATE]
proof (prove)
using this:
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cp
[PROOF STEP]
using contradicting_in_cp
[PROOF STATE]
proof (prove)
using this:
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)
\<lbrakk>?\<sigma> =\<^sub>L ?\<sigma>'; cs\<^bsup>path ?\<sigma>\<^esup> ?k = cs\<^bsup>path ?\<sigma>'\<^esup> ?k'; ?v \<in> local.reads (path ?\<sigma> ?k); (?\<sigma>\<^bsup>?k\<^esup>) ?v \<noteq> (?\<sigma>'\<^bsup>?k'\<^esup>) ?v\<rbrakk> \<Longrightarrow> ((?\<sigma>, ?k), ?\<sigma>', ?k') \<in> cp

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

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cp \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cp \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)
[PROOF STEP]
assume \<open>((\<sigma>, k), \<sigma>', k') \<in> cp\<close>
[PROOF STATE]
proof (state)
this:
((\<sigma>, k), \<sigma>', k') \<in> cp

goal (1 subgoal):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cp \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)
[PROOF STEP]
thus \<open>\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp

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

goal (4 subgoals):
 1. \<And>\<sigma> \<sigma>' n n' h. \<lbrakk>\<sigma> =\<^sub>L \<sigma>'; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; h \<in> local.reads (path \<sigma> n); (\<sigma>\<^bsup>n\<^esup>) h \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) h; \<forall>k<n. h \<notin> local.writes (path \<sigma> k); \<forall>k'<n'. h \<notin> local.writes (path \<sigma>' k')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k; n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k'; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<sigma> =\<^sub>L \<sigma>'
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
h \<in> local.reads (path \<sigma> n)
(\<sigma>\<^bsup>n\<^esup>) h \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) h
\<forall>k<n. h \<notin> local.writes (path \<sigma> k)
\<forall>k'<n'. h \<notin> local.writes (path \<sigma>' k')
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<sigma> =\<^sub>L \<sigma>'
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
h \<in> local.reads (path \<sigma> n)
(\<sigma>\<^bsup>n\<^esup>) h \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) h
\<forall>k<n. h \<notin> local.writes (path \<sigma> k)
\<forall>k'<n'. h \<notin> local.writes (path \<sigma>' k')

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)

goal (3 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k; n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k'; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 3. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k; n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k'; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 3. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
case (2 \<sigma> k \<sigma>' k' n v n')
[PROOF STATE]
proof (state)
this:
((\<sigma>, k), \<sigma>', k') \<in> cp
n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k
n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k'
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
(\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (3 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k; n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k'; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 3. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
have \<open>v\<in>reads (path \<sigma> n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> local.reads (path \<sigma> n)
[PROOF STEP]
using 2(2)
[PROOF STATE]
proof (prove)
using this:
n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. v \<in> local.reads (path \<sigma> n)
[PROOF STEP]
unfolding is_ddi_def
[PROOF STATE]
proof (prove)
using this:
is_path (path \<sigma>) \<and> k < n \<and> v \<in> local.reads (path \<sigma> n) \<inter> local.writes (path \<sigma> k) \<and> (\<forall>l\<in>{k<..<n}. v \<notin> local.writes (path \<sigma> l))

goal (1 subgoal):
 1. v \<in> local.reads (path \<sigma> n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> local.reads (path \<sigma> n)

goal (3 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k; n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k'; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 3. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> local.reads (path \<sigma> n)
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma> n)

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma> n)
((\<sigma>, k), \<sigma>', k') \<in> cp
n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> k
n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k'
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
(\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)

goal (2 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
case (3 \<sigma> k \<sigma>' k' n v l n')
[PROOF STATE]
proof (state)
this:
((\<sigma>, k), \<sigma>', k') \<in> cp
n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l
l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k')
(\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v
\<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (2 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
have \<open>v\<in>reads (path \<sigma> n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> local.reads (path \<sigma> n)
[PROOF STEP]
using 3(2)
[PROOF STATE]
proof (prove)
using this:
n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. v \<in> local.reads (path \<sigma> n)
[PROOF STEP]
unfolding is_ddi_def
[PROOF STATE]
proof (prove)
using this:
is_path (path \<sigma>) \<and> l < n \<and> v \<in> local.reads (path \<sigma> n) \<inter> local.writes (path \<sigma> l) \<and> (\<forall>l\<in>{l<..<n}. v \<notin> local.writes (path \<sigma> l))

goal (1 subgoal):
 1. v \<in> local.reads (path \<sigma> n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> local.reads (path \<sigma> n)

goal (2 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v); n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l; l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k; cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'; path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k'); (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v; \<forall>j'\<in>{LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')..<n'}. v \<notin> local.writes (path \<sigma>' j')\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
 2. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> local.reads (path \<sigma> n)
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma> n)

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
[PROOF STEP]
using 3(4,6,8)
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma> n)
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
(\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n' \<and> (\<exists>v\<in>local.reads (path \<sigma> n). (\<sigma>\<^bsup>n\<^esup>) v \<noteq> (\<sigma>'\<^bsup>n'\<^esup>) v)

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
case (4 \<sigma> k \<sigma>' k')
[PROOF STATE]
proof (state)
this:
((\<sigma>, k), \<sigma>', k') \<in> cp
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
hence \<open>cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

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

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
hence \<open>path \<sigma>' k' = path \<sigma> k\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'

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

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path \<sigma>' k' = path \<sigma> k

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
have \<open>\<sigma>' =\<^sub>L \<sigma>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' =\<^sub>L \<sigma>
[PROOF STEP]
using 4(2)
[PROOF STATE]
proof (prove)
using this:
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (1 subgoal):
 1. \<sigma>' =\<^sub>L \<sigma>
[PROOF STEP]
unfolding loweq_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<restriction> (- local.hvars) = \<sigma>' \<restriction> (- local.hvars) \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (1 subgoal):
 1. \<sigma>' \<restriction> (- local.hvars) = \<sigma> \<restriction> (- local.hvars)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma>' =\<^sub>L \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; \<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)\<rbrakk> \<Longrightarrow> \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path \<sigma>' k' = path \<sigma> k
\<sigma>' =\<^sub>L \<sigma>
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
path \<sigma>' k' = path \<sigma> k
\<sigma>' =\<^sub>L \<sigma>

goal (1 subgoal):
 1. \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
path \<sigma>' k' = path \<sigma> k
\<sigma>' =\<^sub>L \<sigma>
((\<sigma>, k), \<sigma>', k') \<in> cp
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal (1 subgoal):
 1. \<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<sigma>' =\<^sub>L \<sigma> \<and> cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> (\<exists>v\<in>local.reads (path \<sigma>' k'). (\<sigma>'\<^bsup>k'\<^esup>) v \<noteq> (\<sigma>\<^bsup>k\<^esup>) v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k' \<and> (\<exists>v\<in>local.reads (path \<sigma> k). (\<sigma>\<^bsup>k\<^esup>) v \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) v)

goal:
No subgoals!
[PROOF STEP]
qed