[STATEMENT]
theorem cop_iff_contradicting: \<open>((\<sigma>,k),(\<sigma>',k')) \<in> cop \<longleftrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>',k') \<cc> (\<sigma>,k) \<and> path \<sigma> k \<in> dom att\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<sigma>, k), \<sigma>', k') \<in> cop) = (\<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
 2. \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<Longrightarrow> ((\<sigma>, k), \<sigma>', k') \<in> cop
[PROOF STEP]
assume \<open>\<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom att\<close>
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att

goal (2 subgoals):
 1. ((\<sigma>, k), \<sigma>', k') \<in> cop \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
 2. \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att \<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> =\<^sub>L \<sigma>' \<and> (\<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 contradicting_in_cop
[PROOF STATE]
proof (prove)
using this:
\<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
\<lbrakk>?\<sigma> =\<^sub>L ?\<sigma>'; (?\<sigma>', ?k') \<cc> (?\<sigma>, ?k); path ?\<sigma> ?k \<in> dom local.att\<rbrakk> \<Longrightarrow> ((?\<sigma>, ?k), ?\<sigma>', ?k') \<in> cop

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

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

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

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
proof (cases rule: cop.cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; path \<sigma> k \<in> dom local.att\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
 2. \<And>ka. \<lbrakk>((\<sigma>, ka), \<sigma>', k') \<in> cp; k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> ka; path \<sigma> (Suc ka) \<noteq> path \<sigma>' (Suc k'); path \<sigma> k \<in> dom local.att\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
((\<sigma>, k), \<sigma>', k') \<in> cp
path \<sigma> k \<in> dom local.att

goal (2 subgoals):
 1. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; path \<sigma> k \<in> dom local.att\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
 2. \<And>ka. \<lbrakk>((\<sigma>, ka), \<sigma>', k') \<in> cp; k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> ka; path \<sigma> (Suc ka) \<noteq> path \<sigma>' (Suc k'); path \<sigma> k \<in> dom local.att\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, k), \<sigma>', k') \<in> cp
path \<sigma> k \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp
path \<sigma> k \<in> dom local.att

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
using cp_iff_reads_contradict contradicts.simps
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp
path \<sigma> k \<in> dom local.att
(((?\<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))
(?a1.0 \<cc> ?a2.0) = ((\<exists>\<pi>' k' \<pi> k \<sigma> \<sigma>'. ?a1.0 = (\<sigma>', k') \<and> ?a2.0 = (\<sigma>, k) \<and> cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k \<and> \<pi> = path \<sigma> \<and> \<pi>' = path \<sigma>' \<and> \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')) \<or> (\<exists>\<pi>' k' \<pi> k \<sigma> \<sigma>'. ?a1.0 = (\<sigma>', k') \<and> ?a2.0 = (\<sigma>, k) \<and> cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k \<and> \<pi> = path \<sigma> \<and> \<pi>' = path \<sigma>' \<and> \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)))

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
by (metis (full_types) reads_restrict1)
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att

goal (1 subgoal):
 1. \<And>ka. \<lbrakk>((\<sigma>, ka), \<sigma>', k') \<in> cp; k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> ka; path \<sigma> (Suc ka) \<noteq> path \<sigma>' (Suc k'); path \<sigma> k \<in> dom local.att\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>((\<sigma>, ka), \<sigma>', k') \<in> cp; k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> ka; path \<sigma> (Suc ka) \<noteq> path \<sigma>' (Suc k'); path \<sigma> k \<in> dom local.att\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
case (2 k)
[PROOF STATE]
proof (state)
this:
((\<sigma>, k), \<sigma>', k') \<in> cp
k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k
path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k')
path \<sigma> k \<in> dom local.att

goal (1 subgoal):
 1. \<And>ka. \<lbrakk>((\<sigma>, ka), \<sigma>', k') \<in> cp; k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> ka; path \<sigma> (Suc ka) \<noteq> path \<sigma>' (Suc k'); path \<sigma> k \<in> dom local.att\<rbrakk> \<Longrightarrow> \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, k), \<sigma>', k') \<in> cp
k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k
path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k')
path \<sigma> k \<in> dom local.att
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp
k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k
path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k')
path \<sigma> k \<in> dom local.att

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
using cp_iff_reads_contradict contradicts.simps
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp
k cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k
path \<sigma> (Suc k) \<noteq> path \<sigma>' (Suc k')
path \<sigma> k \<in> dom local.att
(((?\<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))
(?a1.0 \<cc> ?a2.0) = ((\<exists>\<pi>' k' \<pi> k \<sigma> \<sigma>'. ?a1.0 = (\<sigma>', k') \<and> ?a2.0 = (\<sigma>, k) \<and> cs\<^bsup>\<pi>'\<^esup> k' \<prec> cs\<^bsup>\<pi>\<^esup> k \<and> \<pi> = path \<sigma> \<and> \<pi>' = path \<sigma>' \<and> \<pi> (Suc (\<pi> \<exclamdown> cs\<^bsup>\<pi>'\<^esup> k')) \<noteq> \<pi>' (Suc k')) \<or> (\<exists>\<pi>' k' \<pi> k \<sigma> \<sigma>'. ?a1.0 = (\<sigma>', k') \<and> ?a2.0 = (\<sigma>, k) \<and> cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>\<^esup> k \<and> \<pi> = path \<sigma> \<and> \<pi>' = path \<sigma>' \<and> \<sigma>\<^bsup>k\<^esup> \<restriction> local.reads (\<pi> k) \<noteq> \<sigma>'\<^bsup>k'\<^esup> \<restriction> local.reads (\<pi> k)))

goal (1 subgoal):
 1. \<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att
[PROOF STEP]
by (metis cd_is_cs_less cd_not_ret contradicts.intros(1) cs_select_id path_is_path)
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>' \<and> (\<sigma>', k') \<cc> (\<sigma>, k) \<and> path \<sigma> k \<in> dom local.att

goal:
No subgoals!
[PROOF STEP]
qed