[STATEMENT]
theorem cp_in_scp: assumes \<open>((\<sigma>,k),(\<sigma>',k'))\<in>cp\<close> shows \<open>(path \<sigma>,k)\<in>scp \<and> (path \<sigma>',k')\<in>scp\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cp

goal (1 subgoal):
 1. (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
proof(induction \<open>\<sigma>\<close> \<open>k\<close> \<open>\<sigma>'\<close> \<open>k'\<close> rule:cp.induct[case_names read_high dd dcd sym])
[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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
case (read_high \<sigma> \<sigma>' k k' h)
[PROOF STATE]
proof (state)
this:
\<sigma> =\<^sub>L \<sigma>'
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
h \<in> local.reads (path \<sigma> k)
(\<sigma>\<^bsup>k\<^esup>) h \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) h
\<forall>k<k. h \<notin> local.writes (path \<sigma> k)
\<forall>k'<k'. 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
have \<open>\<sigma> h = (\<sigma>\<^bsup>k\<^esup>) h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> h = (\<sigma>\<^bsup>k\<^esup>) h
[PROOF STEP]
using read_high(5)
[PROOF STATE]
proof (prove)
using this:
\<forall>k<k. h \<notin> local.writes (path \<sigma> k)

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

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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<sigma> h = (\<sigma>\<^bsup>k\<^esup>) h

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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
have \<open>\<sigma>' h = (\<sigma>'\<^bsup>k'\<^esup>) h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' h = (\<sigma>'\<^bsup>k'\<^esup>) h
[PROOF STEP]
using read_high(6)
[PROOF STATE]
proof (prove)
using this:
\<forall>k'<k'. h \<notin> local.writes (path \<sigma>' k')

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

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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<sigma> h = (\<sigma>\<^bsup>k\<^esup>) h
\<sigma>' h = (\<sigma>'\<^bsup>k'\<^esup>) h
[PROOF STEP]
have \<open>\<sigma> h \<noteq> \<sigma>' h\<close>
[PROOF STATE]
proof (prove)
using this:
\<sigma> h = (\<sigma>\<^bsup>k\<^esup>) h
\<sigma>' h = (\<sigma>'\<^bsup>k'\<^esup>) h

goal (1 subgoal):
 1. \<sigma> h \<noteq> \<sigma>' h
[PROOF STEP]
using read_high(4)
[PROOF STATE]
proof (prove)
using this:
\<sigma> h = (\<sigma>\<^bsup>k\<^esup>) h
\<sigma>' h = (\<sigma>'\<^bsup>k'\<^esup>) h
(\<sigma>\<^bsup>k\<^esup>) h \<noteq> (\<sigma>'\<^bsup>k'\<^esup>) h

goal (1 subgoal):
 1. \<sigma> h \<noteq> \<sigma>' h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma> h \<noteq> \<sigma>' h

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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
hence *: \<open>h\<in>hvars\<close>
[PROOF STATE]
proof (prove)
using this:
\<sigma> h \<noteq> \<sigma>' h

goal (1 subgoal):
 1. h \<in> local.hvars
[PROOF STEP]
using read_high(1)
[PROOF STATE]
proof (prove)
using this:
\<sigma> h \<noteq> \<sigma>' h
\<sigma> =\<^sub>L \<sigma>'

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

goal (1 subgoal):
 1. h \<in> local.hvars
[PROOF STEP]
by (metis Compl_iff IFC_def.restrict_def)
[PROOF STATE]
proof (state)
this:
h \<in> local.hvars

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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
have 1: \<open>(path \<sigma>,k)\<in>scp\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma>, k) \<in> scp
[PROOF STEP]
using scp.intros(1) read_high(3,5) *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?h \<in> local.hvars; ?h \<in> local.reads (path ?\<sigma> ?n); \<forall>k<?n. ?h \<notin> local.writes (path ?\<sigma> k)\<rbrakk> \<Longrightarrow> (path ?\<sigma>, ?n) \<in> scp
h \<in> local.reads (path \<sigma> k)
\<forall>k<k. h \<notin> local.writes (path \<sigma> k)
h \<in> local.hvars

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

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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
have \<open>path \<sigma> k = path \<sigma>' k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma> k = path \<sigma>' k'
[PROOF STEP]
using read_high(2)
[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 (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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
hence \<open>(path \<sigma>',k')\<in>scp\<close>
[PROOF STATE]
proof (prove)
using this:
path \<sigma> k = path \<sigma>' k'

goal (1 subgoal):
 1. (path \<sigma>', k') \<in> scp
[PROOF STEP]
using scp.intros(1) read_high(3,6) *
[PROOF STATE]
proof (prove)
using this:
path \<sigma> k = path \<sigma>' k'
\<lbrakk>?h \<in> local.hvars; ?h \<in> local.reads (path ?\<sigma> ?n); \<forall>k<?n. ?h \<notin> local.writes (path ?\<sigma> k)\<rbrakk> \<Longrightarrow> (path ?\<sigma>, ?n) \<in> scp
h \<in> local.reads (path \<sigma> k)
\<forall>k'<k'. h \<notin> local.writes (path \<sigma>' k')
h \<in> local.hvars

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

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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 4. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
(path \<sigma>', k') \<in> scp

goal (1 subgoal):
 1. (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(path \<sigma>', k') \<in> scp
(path \<sigma>, k) \<in> scp

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

goal (3 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[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; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
case dd
[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_
(path \<sigma>_, k_) \<in> scp \<and> (path \<sigma>'_, k'_) \<in> scp

goal (3 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 3. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma>_, n_) \<in> scp \<and> (path \<sigma>'_, n'_) \<in> scp
[PROOF STEP]
using scp.intros(3) dd
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?\<pi>, ?m) \<in> scp; ?n dd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?m\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp
((\<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_
(path \<sigma>_, k_) \<in> scp \<and> (path \<sigma>'_, k'_) \<in> scp

goal (1 subgoal):
 1. (path \<sigma>_, n_) \<in> scp \<and> (path \<sigma>'_, n'_) \<in> scp
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(path \<sigma>_, n_) \<in> scp \<and> (path \<sigma>'_, n'_) \<in> scp

goal (2 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[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; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
case sym
[PROOF STATE]
proof (state)
this:
((\<sigma>_, k_), \<sigma>'_, k'_) \<in> cp
(path \<sigma>_, k_) \<in> scp \<and> (path \<sigma>'_, k'_) \<in> scp

goal (2 subgoals):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp\<rbrakk> \<Longrightarrow> (path \<sigma>', k') \<in> scp \<and> (path \<sigma>, k) \<in> scp
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
((\<sigma>_, k_), \<sigma>'_, k'_) \<in> cp
(path \<sigma>_, k_) \<in> scp \<and> (path \<sigma>'_, k'_) \<in> scp

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

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
case (dcd \<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')
(path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
note scp.intros(4) is_dcdi_via_def cd_cs_swap cs_ipd
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?\<pi>, ?m) \<in> scp; (?\<pi>', ?m') \<in> scp; ?n dcd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?m via ?\<pi>' ?m'\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp
(?n dcd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?m via ?\<pi>' ?m') = (is_path ?\<pi> \<and> ?m < ?n \<and> (\<exists>l' n'. cs\<^bsup>?\<pi>\<^esup> ?m = cs\<^bsup>?\<pi>'\<^esup> ?m' \<and> cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>'\<^esup> n' \<and> n' dd\<^bsup>?\<pi>',?v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>?\<pi>'\<^esup>\<rightarrow> ?m') \<and> (\<forall>l\<in>{?m..<?n}. ?v \<notin> local.writes (?\<pi> l)))
\<lbrakk>?l cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; cs\<^bsup>?\<pi>\<^esup> ?l = cs\<^bsup>?\<pi>'\<^esup> ?l'; cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k'\<rbrakk> \<Longrightarrow> ?l' cd\<^bsup>?\<pi>'\<^esup>\<rightarrow> ?k'
\<lbrakk>?\<pi> ?m = ipd (?\<pi> ?k); \<forall>n\<in>{?k..<?m}. ?\<pi> n \<noteq> ipd (?\<pi> ?k); ?k < ?m\<rbrakk> \<Longrightarrow> cs\<^bsup>?\<pi>\<^esup> ?m = filter (\<lambda>n. ipd n \<noteq> ?\<pi> ?m) (cs\<^bsup>?\<pi>\<^esup> ?k) @ [?\<pi> ?m]

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have 1: \<open>(path \<sigma>, n)\<in>scp\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma>, n) \<in> scp
[PROOF STEP]
using dcd.IH dcd.hyps(2) dcd.hyps(3) scp.intros(2) scp.intros(3)
[PROOF STATE]
proof (prove)
using this:
(path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp
n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l
l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k
\<lbrakk>(?\<pi>, ?m) \<in> scp; ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp
\<lbrakk>(?\<pi>, ?m) \<in> scp; ?n dd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?m\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp

goal (1 subgoal):
 1. (path \<sigma>, n) \<in> scp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(path \<sigma>, n) \<in> scp

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have csk: \<open>cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
[PROOF STEP]
using cp_eq_cs[OF dcd(1)]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
[PROOF STEP]
.
[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' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have kn: \<open>k<n\<close> and kl: \<open>k<l\<close> and ln: \<open>l<n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n &&& k < l &&& l < n
[PROOF STEP]
using dcd(2,3)
[PROOF STATE]
proof (prove)
using this:
n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l
l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. k < n &&& k < l &&& l < n
[PROOF STEP]
unfolding is_ddi_def is_cdi_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))
is_path (path \<sigma>) \<and> k < l \<and> path \<sigma> l \<noteq> local.return \<and> (\<forall>j\<in>{k..l}. path \<sigma> j \<noteq> ipd (path \<sigma> k))

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

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have nret: \<open>path \<sigma> k \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma> k \<noteq> local.return
[PROOF STEP]
using cd_not_ret dcd.hyps(3)
[PROOF STATE]
proof (prove)
using this:
?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k \<Longrightarrow> ?\<pi> ?k \<noteq> local.return
l cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have \<open>k' < n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < n'
[PROOF STEP]
using kn csk dcd(4) cs_order nret path_is_path last_cs
[PROOF STATE]
proof (prove)
using this:
k < n
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; cs\<^bsup>?\<pi>\<^esup> ?i = cs\<^bsup>?\<pi>'\<^esup> ?i'; cs\<^bsup>?\<pi>\<^esup> ?j = cs\<^bsup>?\<pi>'\<^esup> ?j'; ?\<pi> ?i \<noteq> local.return; ?i < ?j\<rbrakk> \<Longrightarrow> ?i' < ?j'
path \<sigma> k \<noteq> local.return
is_path (path ?\<sigma>)
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

goal (1 subgoal):
 1. k' < n'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k' < n'

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have 2: \<open>(path \<sigma>', n')\<in>scp\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
assume j'ex: \<open>\<exists>j'\<in>{k'..<n'}. v \<in> writes (path \<sigma>' j')\<close>
[PROOF STATE]
proof (state)
this:
\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j')

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence \<open>\<exists>j'. j'\<in>{k'..<n'} \<and> v \<in> writes (path \<sigma>' j')\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j')

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
note * = GreatestI_ex_nat[OF this]
[PROOF STATE]
proof (state)
this:
(\<And>y. y \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' y) \<Longrightarrow> y \<le> ?b) \<Longrightarrow> (GREATEST j'. j' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' j')) \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' (GREATEST j'. j' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' j')))

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
define j' where \<open>j' == GREATEST j'. j'\<in>{k'..<n'} \<and> v \<in> writes (path \<sigma>' j')\<close>
[PROOF STATE]
proof (state)
this:
j' \<equiv> GREATEST j'. j' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' j')

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
note ** = *[of \<open>j'\<close>,folded j'_def]
[PROOF STATE]
proof (state)
this:
(\<And>y. y \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' y) \<Longrightarrow> y \<le> j') \<Longrightarrow> j' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' j')

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have \<open>k' \<le> j'\<close> \<open>j'<n'\<close> and j'write: \<open>v \<in> writes (path \<sigma>' j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k' \<le> j' &&& j' < n') &&& v \<in> local.writes (path \<sigma>' j')
[PROOF STEP]
using "*" atLeastLessThan_iff j'_def nat_less_le
[PROOF STATE]
proof (prove)
using this:
(\<And>y. y \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' y) \<Longrightarrow> y \<le> ?b) \<Longrightarrow> (GREATEST j'. j' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' j')) \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' (GREATEST j'. j' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' j')))
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
j' \<equiv> GREATEST j'. j' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' j')
(?m < ?n) = (?m \<le> ?n \<and> ?m \<noteq> ?n)

goal (1 subgoal):
 1. (k' \<le> j' &&& j' < n') &&& v \<in> local.writes (path \<sigma>' j')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' \<le> j'
j' < n'
v \<in> local.writes (path \<sigma>' j')

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have nowrite: \<open>\<forall> i'\<in>{j'<..<n'}. v \<notin> writes(path \<sigma>' i')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i'\<in>{j'<..<n'}. v \<notin> local.writes (path \<sigma>' i')
[PROOF STEP]
proof (rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {j'<..<n'}; \<not> v \<notin> local.writes (path \<sigma>' i')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {j'<..<n'}; \<not> v \<notin> local.writes (path \<sigma>' i')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>i' \<in> {j'<..<n'}\<close> \<open>\<not> v \<notin> local.writes (path \<sigma>' i')\<close>
[PROOF STATE]
proof (state)
this:
i' \<in> {j'<..<n'}
\<not> v \<notin> local.writes (path \<sigma>' i')

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {j'<..<n'}; \<not> v \<notin> local.writes (path \<sigma>' i')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>i' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' i')\<close>
[PROOF STATE]
proof (prove)
using this:
i' \<in> {j'<..<n'}
\<not> v \<notin> local.writes (path \<sigma>' i')

goal (1 subgoal):
 1. i' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' i')
[PROOF STEP]
using \<open>k' \<le> j'\<close>
[PROOF STATE]
proof (prove)
using this:
i' \<in> {j'<..<n'}
\<not> v \<notin> local.writes (path \<sigma>' i')
k' \<le> j'

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

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {j'<..<n'}; \<not> v \<notin> local.writes (path \<sigma>' i')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>i' \<le> j'\<close>
[PROOF STATE]
proof (prove)
using this:
i' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' i')

goal (1 subgoal):
 1. i' \<le> j'
[PROOF STEP]
using Greatest_le_nat
[PROOF STATE]
proof (prove)
using this:
i' \<in> {k'..<n'} \<and> v \<in> local.writes (path \<sigma>' i')
\<lbrakk>?P ?k; \<And>y. ?P y \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> ?k \<le> Greatest ?P

goal (1 subgoal):
 1. i' \<le> j'
[PROOF STEP]
by (metis (no_types, lifting) atLeastLessThan_iff j'_def nat_less_le)
[PROOF STATE]
proof (state)
this:
i' \<le> j'

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {j'<..<n'}; \<not> v \<notin> local.writes (path \<sigma>' i')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
i' \<le> j'

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>i' \<in> {j'<..<n'}\<close>
[PROOF STATE]
proof (prove)
using this:
i' \<le> j'
i' \<in> {j'<..<n'}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i'\<in>{j'<..<n'}. v \<notin> local.writes (path \<sigma>' i')

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have \<open>path \<sigma>' n' = path \<sigma> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma>' n' = path \<sigma> n
[PROOF STEP]
using dcd(4) last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence \<open>v\<in>reads(path \<sigma>' n')\<close>
[PROOF STATE]
proof (prove)
using this:
path \<sigma>' n' = path \<sigma> n

goal (1 subgoal):
 1. v \<in> local.reads (path \<sigma>' n')
[PROOF STEP]
using dcd(2)
[PROOF STATE]
proof (prove)
using this:
path \<sigma>' n' = path \<sigma> n
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:
path \<sigma>' n' = path \<sigma> n
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. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence nddj': \<open>n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> j'\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma>' n')

goal (1 subgoal):
 1. n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> j'
[PROOF STEP]
using dcd(2)
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma>' n')
n dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> j'
[PROOF STEP]
unfolding is_ddi_def
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma>' n')
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. is_path (path \<sigma>') \<and> j' < n' \<and> v \<in> local.reads (path \<sigma>' n') \<inter> local.writes (path \<sigma>' j') \<and> (\<forall>l\<in>{j'<..<n'}. v \<notin> local.writes (path \<sigma>' l))
[PROOF STEP]
using nowrite \<open>j'<n'\<close> j'write
[PROOF STATE]
proof (prove)
using this:
v \<in> local.reads (path \<sigma>' n')
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))
\<forall>i'\<in>{j'<..<n'}. v \<notin> local.writes (path \<sigma>' i')
j' < n'
v \<in> local.writes (path \<sigma>' j')

goal (1 subgoal):
 1. is_path (path \<sigma>') \<and> j' < n' \<and> v \<in> local.reads (path \<sigma>' n') \<inter> local.writes (path \<sigma>' j') \<and> (\<forall>l\<in>{j'<..<n'}. v \<notin> local.writes (path \<sigma>' l))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> j'

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
assume \<open>j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (state)
this:
j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
thus \<open>(path \<sigma>',n') \<in> scp\<close>
[PROOF STATE]
proof (prove)
using this:
j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
using scp.intros(2) scp.intros(3) dcd.IH nddj'
[PROOF STATE]
proof (prove)
using this:
j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'
\<lbrakk>(?\<pi>, ?m) \<in> scp; ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp
\<lbrakk>(?\<pi>, ?m) \<in> scp; ?n dd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?m\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp
(path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp
n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> j'

goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(path \<sigma>', n') \<in> scp

goal (1 subgoal):
 1. \<not> j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
assume jcdk': \<open>\<not> j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (state)
this:
\<not> j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. \<not> j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
assume \<open>j' = k'\<close>
[PROOF STATE]
proof (state)
this:
j' = k'

goal (2 subgoals):
 1. ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
 2. \<not> ?P \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
j' = k'

goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
using scp.intros(3) dcd.IH nddj'
[PROOF STATE]
proof (prove)
using this:
j' = k'
\<lbrakk>(?\<pi>, ?m) \<in> scp; ?n dd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?m\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp
(path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp
n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> j'

goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(path \<sigma>', n') \<in> scp

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
assume \<open>j' \<noteq> k'\<close>
[PROOF STATE]
proof (state)
this:
j' \<noteq> k'

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence \<open>k' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
j' \<noteq> k'

goal (1 subgoal):
 1. k' < j'
[PROOF STEP]
using \<open>k' \<le> j'\<close>
[PROOF STATE]
proof (prove)
using this:
j' \<noteq> k'
k' \<le> j'

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have \<open>path \<sigma>' j' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma>' j' \<noteq> local.return
[PROOF STEP]
using j'write writes_return
[PROOF STATE]
proof (prove)
using this:
v \<in> local.writes (path \<sigma>' j')
local.writes local.return = {}

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence ipdex':\<open>\<exists>j. j \<in>{k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k') \<close>
[PROOF STATE]
proof (prove)
using this:
path \<sigma>' j' \<noteq> local.return

goal (1 subgoal):
 1. \<exists>j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')
[PROOF STEP]
using path_is_path \<open>k' < j'\<close> jcdk' is_cdi_def
[PROOF STATE]
proof (prove)
using this:
path \<sigma>' j' \<noteq> local.return
is_path (path ?\<sigma>)
k' < j'
\<not> j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'
(?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (is_path ?\<pi> \<and> ?k < ?i \<and> ?\<pi> ?i \<noteq> local.return \<and> (\<forall>j\<in>{?k..?i}. ?\<pi> j \<noteq> ipd (?\<pi> ?k)))

goal (1 subgoal):
 1. \<exists>j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
define i' where \<open>i' == LEAST j. j\<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')\<close>
[PROOF STATE]
proof (state)
this:
i' \<equiv> LEAST j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have iipd': \<open>i'\<in> {k'..j'}\<close> \<open>path \<sigma>' i' = ipd (path \<sigma>' k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<in> {k'..j'} &&& path \<sigma>' i' = ipd (path \<sigma>' k')
[PROOF STEP]
unfolding i'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')) \<in> {k'..j'} &&& path \<sigma>' (LEAST j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')) = ipd (path \<sigma>' k')
[PROOF STEP]
using LeastI_ex[OF ipdex']
[PROOF STATE]
proof (prove)
using this:
(LEAST j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')) \<in> {k'..j'} \<and> path \<sigma>' (LEAST j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')) = ipd (path \<sigma>' k')

goal (1 subgoal):
 1. (LEAST j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')) \<in> {k'..j'} &&& path \<sigma>' (LEAST j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')) = ipd (path \<sigma>' k')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
i' \<in> {k'..j'}
path \<sigma>' i' = ipd (path \<sigma>' k')

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have *:\<open>\<forall> i \<in> {k'..<i'}. path \<sigma>' i \<noteq> ipd (path \<sigma>' k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{k'..<i'}. path \<sigma>' i \<noteq> ipd (path \<sigma>' k')
[PROOF STEP]
proof (rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> {k'..<i'}; \<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> {k'..<i'}; \<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume  *: \<open>i \<in> {k'..<i'}\<close> \<open>\<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')\<close>
[PROOF STATE]
proof (state)
this:
i \<in> {k'..<i'}
\<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> {k'..<i'}; \<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence **: \<open>i \<in>{k'..j'} \<and> path \<sigma>' i = ipd (path \<sigma>' k')\<close> (is \<open>?P i\<close>)
[PROOF STATE]
proof (prove)
using this:
i \<in> {k'..<i'}
\<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')

goal (1 subgoal):
 1. i \<in> {k'..j'} \<and> path \<sigma>' i = ipd (path \<sigma>' k')
[PROOF STEP]
using iipd'(1)
[PROOF STATE]
proof (prove)
using this:
i \<in> {k'..<i'}
\<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')
i' \<in> {k'..j'}

goal (1 subgoal):
 1. i \<in> {k'..j'} \<and> path \<sigma>' i = ipd (path \<sigma>' k')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> {k'..j'} \<and> path \<sigma>' i = ipd (path \<sigma>' k')

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> {k'..<i'}; \<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {k'..j'} \<and> path \<sigma>' i = ipd (path \<sigma>' k')

goal (1 subgoal):
 1. False
[PROOF STEP]
using Least_le[of \<open>?P\<close> \<open>i\<close>] i'_def *
[PROOF STATE]
proof (prove)
using this:
i \<in> {k'..j'} \<and> path \<sigma>' i = ipd (path \<sigma>' k')
i \<in> {k'..j'} \<and> path \<sigma>' i = ipd (path \<sigma>' k') \<Longrightarrow> (LEAST x. x \<in> {k'..j'} \<and> path \<sigma>' x = ipd (path \<sigma>' k')) \<le> i
i' \<equiv> LEAST j. j \<in> {k'..j'} \<and> path \<sigma>' j = ipd (path \<sigma>' k')
i \<in> {k'..<i'}
\<not> path \<sigma>' i \<noteq> ipd (path \<sigma>' k')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{k'..<i'}. path \<sigma>' i \<noteq> ipd (path \<sigma>' k')

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have \<open>i' \<noteq> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<noteq> k'
[PROOF STEP]
using iipd'(2)
[PROOF STATE]
proof (prove)
using this:
path \<sigma>' i' = ipd (path \<sigma>' k')

goal (1 subgoal):
 1. i' \<noteq> k'
[PROOF STEP]
by (metis csk last_cs nret path_in_nodes ipd_not_self)
[PROOF STATE]
proof (state)
this:
i' \<noteq> k'

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence \<open>k'<i'\<close>
[PROOF STATE]
proof (prove)
using this:
i' \<noteq> k'

goal (1 subgoal):
 1. k' < i'
[PROOF STEP]
using iipd'(1)
[PROOF STATE]
proof (prove)
using this:
i' \<noteq> k'
i' \<in> {k'..j'}

goal (1 subgoal):
 1. k' < i'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k' < i'

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence csi': \<open>cs\<^bsup>path \<sigma>'\<^esup> i' = [n\<leftarrow>cs\<^bsup>path \<sigma>'\<^esup> k' . ipd n \<noteq> path \<sigma>' i'] @ [path \<sigma>' i']\<close>
[PROOF STATE]
proof (prove)
using this:
k' < i'

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>'\<^esup> i' = filter (\<lambda>n. ipd n \<noteq> path \<sigma>' i') (cs\<^bsup>path \<sigma>'\<^esup> k') @ [path \<sigma>' i']
[PROOF STEP]
using cs_ipd[OF iipd'(2) *]
[PROOF STATE]
proof (prove)
using this:
k' < i'
k' < i' \<Longrightarrow> cs\<^bsup>path \<sigma>'\<^esup> i' = filter (\<lambda>n. ipd n \<noteq> path \<sigma>' i') (cs\<^bsup>path \<sigma>'\<^esup> k') @ [path \<sigma>' i']

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>'\<^esup> i' = filter (\<lambda>n. ipd n \<noteq> path \<sigma>' i') (cs\<^bsup>path \<sigma>'\<^esup> k') @ [path \<sigma>' i']
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>path \<sigma>'\<^esup> i' = filter (\<lambda>n. ipd n \<noteq> path \<sigma>' i') (cs\<^bsup>path \<sigma>'\<^esup> k') @ [path \<sigma>' i']

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have ncdk': \<open>\<not> n' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'
[PROOF STEP]
using \<open>j' < n'\<close> \<open>k' < j'\<close> cdi_prefix jcdk' less_imp_le_nat
[PROOF STATE]
proof (prove)
using this:
j' < n'
k' < j'
\<lbrakk>?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m; ?m < ?n'; ?n' \<le> ?n\<rbrakk> \<Longrightarrow> ?n' cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m
\<not> j' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'
?m < ?n \<Longrightarrow> ?m \<le> ?n

goal (1 subgoal):
 1. \<not> n' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> n' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence ncdk: \<open>\<not> n cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> n' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. \<not> n cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k
[PROOF STEP]
using cd_cs_swap csk dcd(4)
[PROOF STATE]
proof (prove)
using this:
\<not> n' cd\<^bsup>path \<sigma>'\<^esup>\<rightarrow> k'
\<lbrakk>?l cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; cs\<^bsup>?\<pi>\<^esup> ?l = cs\<^bsup>?\<pi>'\<^esup> ?l'; cs\<^bsup>?\<pi>\<^esup> ?k = cs\<^bsup>?\<pi>'\<^esup> ?k'\<rbrakk> \<Longrightarrow> ?l' cd\<^bsup>?\<pi>'\<^esup>\<rightarrow> ?k'
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
cs\<^bsup>path \<sigma>\<^esup> n = cs\<^bsup>path \<sigma>'\<^esup> n'

goal (1 subgoal):
 1. \<not> n cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> n cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have ipdex: \<open>\<exists>i. i\<in>{k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)\<close> (is \<open>\<exists>i. ?P i\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
 2. \<not> ?P \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
assume *:\<open>path \<sigma> n = return\<close>
[PROOF STATE]
proof (state)
this:
path \<sigma> n = local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
 2. \<not> ?P \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
from path_ret_ipd[of \<open>path \<sigma>\<close> \<open>k\<close> \<open>n\<close>,OF path_is_path nret *]
[PROOF STATE]
proof (chain)
picking this:
(\<And>l. \<lbrakk>k < l; l \<le> n; path \<sigma> l = ipd (path \<sigma> k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain i where \<open>?P i\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>l. \<lbrakk>k < l; l \<le> n; path \<sigma> l = ipd (path \<sigma> k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
 2. \<not> ?P \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)

goal (1 subgoal):
 1. \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)

goal (1 subgoal):
 1. path \<sigma> n \<noteq> local.return \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path \<sigma> n \<noteq> local.return \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
assume *:\<open>path \<sigma> n \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
path \<sigma> n \<noteq> local.return

goal (1 subgoal):
 1. path \<sigma> n \<noteq> local.return \<Longrightarrow> \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
using not_cd_impl_ipd [of \<open>path \<sigma>\<close> \<open>k\<close> \<open>n\<close>, OF path_is_path \<open>k<n\<close> ncdk *]
[PROOF STATE]
proof (prove)
using this:
(\<And>j. \<lbrakk>j \<in> {k..n}; path \<sigma> j = ipd (path \<sigma> k)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
define i where  \<open>i == LEAST j. j\<in> {k..n} \<and> path \<sigma> j = ipd (path \<sigma> k)\<close>
[PROOF STATE]
proof (state)
this:
i \<equiv> LEAST j. j \<in> {k..n} \<and> path \<sigma> j = ipd (path \<sigma> k)

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have iipd: \<open>i\<in> {k..n}\<close> \<open>path \<sigma> i = ipd (path \<sigma> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> {k..n} &&& path \<sigma> i = ipd (path \<sigma> k)
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST j. j \<in> {k..n} \<and> path \<sigma> j = ipd (path \<sigma> k)) \<in> {k..n} &&& path \<sigma> (LEAST j. j \<in> {k..n} \<and> path \<sigma> j = ipd (path \<sigma> k)) = ipd (path \<sigma> k)
[PROOF STEP]
using LeastI_ex[OF ipdex]
[PROOF STATE]
proof (prove)
using this:
(LEAST i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)) \<in> {k..n} \<and> path \<sigma> (LEAST i. i \<in> {k..n} \<and> path \<sigma> i = ipd (path \<sigma> k)) = ipd (path \<sigma> k)

goal (1 subgoal):
 1. (LEAST j. j \<in> {k..n} \<and> path \<sigma> j = ipd (path \<sigma> k)) \<in> {k..n} &&& path \<sigma> (LEAST j. j \<in> {k..n} \<and> path \<sigma> j = ipd (path \<sigma> k)) = ipd (path \<sigma> k)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
i \<in> {k..n}
path \<sigma> i = ipd (path \<sigma> k)

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have **:\<open>\<forall> i' \<in> {k..<i}. path \<sigma> i' \<noteq> ipd (path \<sigma> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i'\<in>{k..<i}. path \<sigma> i' \<noteq> ipd (path \<sigma> k)
[PROOF STEP]
proof (rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {k..<i}; \<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {k..<i}; \<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume  *: \<open>i' \<in> {k..<i}\<close> \<open>\<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)\<close>
[PROOF STATE]
proof (state)
this:
i' \<in> {k..<i}
\<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {k..<i}; \<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence **: \<open>i' \<in>{k..n} \<and> path \<sigma> i' = ipd (path \<sigma> k)\<close> (is \<open>?P i'\<close>)
[PROOF STATE]
proof (prove)
using this:
i' \<in> {k..<i}
\<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)

goal (1 subgoal):
 1. i' \<in> {k..n} \<and> path \<sigma> i' = ipd (path \<sigma> k)
[PROOF STEP]
using iipd(1)
[PROOF STATE]
proof (prove)
using this:
i' \<in> {k..<i}
\<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)
i \<in> {k..n}

goal (1 subgoal):
 1. i' \<in> {k..n} \<and> path \<sigma> i' = ipd (path \<sigma> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' \<in> {k..n} \<and> path \<sigma> i' = ipd (path \<sigma> k)

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' \<in> {k..<i}; \<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
i' \<in> {k..n} \<and> path \<sigma> i' = ipd (path \<sigma> k)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Least_le[of \<open>?P\<close> \<open>i'\<close>] i_def *
[PROOF STATE]
proof (prove)
using this:
i' \<in> {k..n} \<and> path \<sigma> i' = ipd (path \<sigma> k)
i' \<in> {k..n} \<and> path \<sigma> i' = ipd (path \<sigma> k) \<Longrightarrow> (LEAST x. x \<in> {k..n} \<and> path \<sigma> x = ipd (path \<sigma> k)) \<le> i'
i \<equiv> LEAST j. j \<in> {k..n} \<and> path \<sigma> j = ipd (path \<sigma> k)
i' \<in> {k..<i}
\<not> path \<sigma> i' \<noteq> ipd (path \<sigma> k)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i'\<in>{k..<i}. path \<sigma> i' \<noteq> ipd (path \<sigma> k)

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have \<open>i \<noteq> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> k
[PROOF STEP]
using iipd(2)
[PROOF STATE]
proof (prove)
using this:
path \<sigma> i = ipd (path \<sigma> k)

goal (1 subgoal):
 1. i \<noteq> k
[PROOF STEP]
by (metis nret path_in_nodes ipd_not_self)
[PROOF STATE]
proof (state)
this:
i \<noteq> k

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence \<open>k<i\<close>
[PROOF STATE]
proof (prove)
using this:
i \<noteq> k

goal (1 subgoal):
 1. k < i
[PROOF STEP]
using iipd(1)
[PROOF STATE]
proof (prove)
using this:
i \<noteq> k
i \<in> {k..n}

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence \<open>cs\<^bsup>path \<sigma>\<^esup> i = [n\<leftarrow>cs\<^bsup>path \<sigma>\<^esup> k . ipd n \<noteq> path \<sigma> i] @ [path \<sigma> i]\<close>
[PROOF STATE]
proof (prove)
using this:
k < i

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> i = filter (\<lambda>n. ipd n \<noteq> path \<sigma> i) (cs\<^bsup>path \<sigma>\<^esup> k) @ [path \<sigma> i]
[PROOF STEP]
using cs_ipd[OF iipd(2) **]
[PROOF STATE]
proof (prove)
using this:
k < i
k < i \<Longrightarrow> cs\<^bsup>path \<sigma>\<^esup> i = filter (\<lambda>n. ipd n \<noteq> path \<sigma> i) (cs\<^bsup>path \<sigma>\<^esup> k) @ [path \<sigma> i]

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> i = filter (\<lambda>n. ipd n \<noteq> path \<sigma> i) (cs\<^bsup>path \<sigma>\<^esup> k) @ [path \<sigma> i]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>path \<sigma>\<^esup> i = filter (\<lambda>n. ipd n \<noteq> path \<sigma> i) (cs\<^bsup>path \<sigma>\<^esup> k) @ [path \<sigma> i]

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence csi: \<open>cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> i = filter (\<lambda>n. ipd n \<noteq> path \<sigma> i) (cs\<^bsup>path \<sigma>\<^esup> k) @ [path \<sigma> i]

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i'
[PROOF STEP]
using csi' csk
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> i = filter (\<lambda>n. ipd n \<noteq> path \<sigma> i) (cs\<^bsup>path \<sigma>\<^esup> k) @ [path \<sigma> i]
cs\<^bsup>path \<sigma>'\<^esup> i' = filter (\<lambda>n. ipd n \<noteq> path \<sigma>' i') (cs\<^bsup>path \<sigma>'\<^esup> k') @ [path \<sigma>' i']
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'

goal (1 subgoal):
 1. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i'
[PROOF STEP]
unfolding iipd'(2) iipd(2)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> i = filter (\<lambda>n. ipd n \<noteq> ipd (path \<sigma> k)) (cs\<^bsup>path \<sigma>\<^esup> k) @ [ipd (path \<sigma> k)]
cs\<^bsup>path \<sigma>'\<^esup> i' = filter (\<lambda>n. ipd n \<noteq> ipd (path \<sigma>' k')) (cs\<^bsup>path \<sigma>'\<^esup> k') @ [ipd (path \<sigma>' k')]
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence \<open>(LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')) \<le> i'\<close> (is \<open>(LEAST x. ?P x) \<le> _\<close>)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i'

goal (1 subgoal):
 1. (LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')) \<le> i'
[PROOF STEP]
using \<open>k' < i'\<close> Least_le[of \<open>?P\<close> \<open>i'\<close>]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i'
k' < i'
k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i') \<Longrightarrow> (LEAST x. k' < x \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> x)) \<le> i'

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence nw: \<open>\<forall>j'\<in>{i'..<n'}. v \<notin> writes (path \<sigma>' j')\<close>
[PROOF STATE]
proof (prove)
using this:
(LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')) \<le> i'

goal (1 subgoal):
 1. \<forall>j'\<in>{i'..<n'}. v \<notin> local.writes (path \<sigma>' j')
[PROOF STEP]
using dcd(7) allB_atLeastLessThan_lower
[PROOF STATE]
proof (prove)
using this:
(LEAST i'. k' < i' \<and> (\<exists>i. cs\<^bsup>path \<sigma>\<^esup> i = cs\<^bsup>path \<sigma>'\<^esup> i')) \<le> i'
\<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')
\<lbrakk>?i \<le> ?j; \<forall>x\<in>{?i..<?n}. ?P x\<rbrakk> \<Longrightarrow> \<forall>x\<in>{?j..<?n}. ?P x

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j'\<in>{i'..<n'}. v \<notin> local.writes (path \<sigma>' j')

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have \<open>v \<in> writes (path \<sigma>' j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> local.writes (path \<sigma>' j')
[PROOF STEP]
using nddj'
[PROOF STATE]
proof (prove)
using this:
n' dd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> j'

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

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> local.writes (path \<sigma>' j')

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
have \<open>i' \<le> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<le> j'
[PROOF STEP]
using iipd'(1)
[PROOF STATE]
proof (prove)
using this:
i' \<in> {k'..j'}

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>j'\<in>{i'..<n'}. v \<notin> local.writes (path \<sigma>' j')
v \<in> local.writes (path \<sigma>' j')
i' \<le> j'
[PROOF STEP]
have \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>j'\<in>{i'..<n'}. v \<notin> local.writes (path \<sigma>' j')
v \<in> local.writes (path \<sigma>' j')
i' \<le> j'

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>j' < n'\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>j'\<in>{i'..<n'}. v \<notin> local.writes (path \<sigma>' j')
v \<in> local.writes (path \<sigma>' j')
i' \<le> j'
j' < n'

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

goal (1 subgoal):
 1. j' \<noteq> k' \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(path \<sigma>', n') \<in> scp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(path \<sigma>', n') \<in> scp

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(path \<sigma>', n') \<in> scp

goal (1 subgoal):
 1. \<not> (\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j')) \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j')) \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
assume \<open>\<not> (\<exists>j'\<in>{k'..<n'}. v \<in> writes (path \<sigma>' j'))\<close>
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j'))

goal (1 subgoal):
 1. \<not> (\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j')) \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
hence \<open>n' dcd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k' via (path \<sigma>) k\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j'))

goal (1 subgoal):
 1. n' dcd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k' via path \<sigma> k
[PROOF STEP]
unfolding is_dcdi_via_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j'))

goal (1 subgoal):
 1. is_path (path \<sigma>') \<and> k' < n' \<and> (\<exists>l' n'a. cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> cs\<^bsup>path \<sigma>'\<^esup> n' = cs\<^bsup>path \<sigma>\<^esup> n'a \<and> n'a dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k) \<and> (\<forall>l\<in>{k'..<n'}. v \<notin> local.writes (path \<sigma>' l))
[PROOF STEP]
using dcd(2-4) csk \<open>k'<n'\<close> path_is_path
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j'))
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'
cs\<^bsup>path \<sigma>\<^esup> k = cs\<^bsup>path \<sigma>'\<^esup> k'
k' < n'
is_path (path ?\<sigma>)

goal (1 subgoal):
 1. is_path (path \<sigma>') \<and> k' < n' \<and> (\<exists>l' n'a. cs\<^bsup>path \<sigma>'\<^esup> k' = cs\<^bsup>path \<sigma>\<^esup> k \<and> cs\<^bsup>path \<sigma>'\<^esup> n' = cs\<^bsup>path \<sigma>\<^esup> n'a \<and> n'a dd\<^bsup>path \<sigma>,v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>path \<sigma>\<^esup>\<rightarrow> k) \<and> (\<forall>l\<in>{k'..<n'}. v \<notin> local.writes (path \<sigma>' l))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
n' dcd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k' via path \<sigma> k

goal (1 subgoal):
 1. \<not> (\<exists>j'\<in>{k'..<n'}. v \<in> local.writes (path \<sigma>' j')) \<Longrightarrow> (path \<sigma>', n') \<in> scp
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
n' dcd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k' via path \<sigma> k

goal (1 subgoal):
 1. (path \<sigma>', n') \<in> scp
[PROOF STEP]
using dcd.IH scp.intros(4)
[PROOF STATE]
proof (prove)
using this:
n' dcd\<^bsup>path \<sigma>',v\<^esup>\<rightarrow> k' via path \<sigma> k
(path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp
\<lbrakk>(?\<pi>, ?m) \<in> scp; (?\<pi>', ?m') \<in> scp; ?n dcd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?m via ?\<pi>' ?m'\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(path \<sigma>', n') \<in> scp

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n v l n'. \<lbrakk>((\<sigma>, k), \<sigma>', k') \<in> cp; (path \<sigma>, k) \<in> scp \<and> (path \<sigma>', k') \<in> scp; 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> (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
(path \<sigma>, n) \<in> scp
(path \<sigma>', n') \<in> scp
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
(path \<sigma>, n) \<in> scp
(path \<sigma>', n') \<in> scp

goal (1 subgoal):
 1. (path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(path \<sigma>, n) \<in> scp \<and> (path \<sigma>', n') \<in> scp

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem cop_in_scop: assumes \<open>((\<sigma>,k),(\<sigma>',k'))\<in>cop\<close> shows \<open>(path \<sigma>,k)\<in>scop \<and> (path \<sigma>',k')\<in>scp\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (path \<sigma>, k) \<in> scop \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, k), \<sigma>', k') \<in> cop

goal (1 subgoal):
 1. (path \<sigma>, k) \<in> scop \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
apply (induct rule: cop.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> n \<sigma>' n'. \<lbrakk>((\<sigma>, n), \<sigma>', n') \<in> cp; path \<sigma> n \<in> dom local.att\<rbrakk> \<Longrightarrow> (path \<sigma>, n) \<in> scop \<and> (path \<sigma>', n') \<in> scp
 2. \<And>\<sigma> k \<sigma>' k' n. \<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> (path \<sigma>, n) \<in> scop \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
apply (simp add: cp_in_scp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> n \<sigma>' n'. \<lbrakk>((\<sigma>, n), \<sigma>', n') \<in> cp; path \<sigma> n \<in> dom local.att\<rbrakk> \<Longrightarrow> (path \<sigma>, n) \<in> scop
 2. \<And>\<sigma> k \<sigma>' k' n. \<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> (path \<sigma>, n) \<in> scop \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
using cp_in_scp scop.intros scp.intros(2)
[PROOF STATE]
proof (prove)
using this:
((?\<sigma>, ?k), ?\<sigma>', ?k') \<in> cp \<Longrightarrow> (path ?\<sigma>, ?k) \<in> scp \<and> (path ?\<sigma>', ?k') \<in> scp
\<lbrakk>(?\<pi>, ?n) \<in> scp; ?\<pi> ?n \<in> dom local.att\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scop
\<lbrakk>(?\<pi>, ?m) \<in> scp; ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp

goal (2 subgoals):
 1. \<And>\<sigma> n \<sigma>' n'. \<lbrakk>((\<sigma>, n), \<sigma>', n') \<in> cp; path \<sigma> n \<in> dom local.att\<rbrakk> \<Longrightarrow> (path \<sigma>, n) \<in> scop
 2. \<And>\<sigma> k \<sigma>' k' n. \<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> (path \<sigma>, n) \<in> scop \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n. \<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> (path \<sigma>, n) \<in> scop \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
using cp_in_scp scop.intros scp.intros(2)
[PROOF STATE]
proof (prove)
using this:
((?\<sigma>, ?k), ?\<sigma>', ?k') \<in> cp \<Longrightarrow> (path ?\<sigma>, ?k) \<in> scp \<and> (path ?\<sigma>', ?k') \<in> scp
\<lbrakk>(?\<pi>, ?n) \<in> scp; ?\<pi> ?n \<in> dom local.att\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scop
\<lbrakk>(?\<pi>, ?m) \<in> scp; ?n cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m\<rbrakk> \<Longrightarrow> (?\<pi>, ?n) \<in> scp

goal (1 subgoal):
 1. \<And>\<sigma> k \<sigma>' k' n. \<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> (path \<sigma>, n) \<in> scop \<and> (path \<sigma>', k') \<in> scp
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem scop_correct: assumes \<open>scop = empty\<close> shows \<open>secure\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
using cop_correct assms cop_in_scop
[PROOF STATE]
proof (prove)
using this:
cop = {} \<Longrightarrow> secure
scop = {}
((?\<sigma>, ?k), ?\<sigma>', ?k') \<in> cop \<Longrightarrow> (path ?\<sigma>, ?k) \<in> scop \<and> (path ?\<sigma>', ?k') \<in> scp

goal (1 subgoal):
 1. secure
[PROOF STEP]
by fast