[STATEMENT]
lemma compat_low_eq:
  assumes compat: "makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems"
  assumes modes_eq: "map snd cms\<^sub>1 = map snd cms\<^sub>2"
  assumes x_low: "dma x = Low"
  assumes x_readable: "\<forall> i < length cms\<^sub>1. x \<notin> snd (cms\<^sub>1 ! i) AsmNoRead"
  shows "mem\<^sub>1 x = mem\<^sub>2 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
let ?X = "\<lambda> i. differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
from compat
[PROOF STATE]
proof (chain)
picking this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
[PROOF STEP]
have "(length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2) \<or>
                    (\<forall> x. \<exists> j. j < length cms\<^sub>1 \<and> x \<notin> ?X j)"
[PROOF STATE]
proof (prove)
using this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems

goal (1 subgoal):
 1. length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j)

goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
thus "mem\<^sub>1 x = mem\<^sub>2 x"
[PROOF STATE]
proof (prove)
using this:
length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j)

goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
 2. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
assume "length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2"
[PROOF STATE]
proof (state)
this:
length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2

goal (2 subgoals):
 1. length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
 2. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
with x_low
[PROOF STATE]
proof (chain)
picking this:
dma x = Low
length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dma x = Low
length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2

goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
by (simp add: low_eq_def)
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 x = mem\<^sub>2 x

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
assume "\<forall> x. \<exists> j. j < length cms\<^sub>1 \<and> x \<notin> ?X j"
[PROOF STATE]
proof (state)
this:
\<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
[PROOF STEP]
obtain j where j_prop: "j < length cms\<^sub>1 \<and> x \<notin> ?X j"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. (\<And>j. j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
let ?mems\<^sub>1j = "fst (mems ! j)" and
        ?mems\<^sub>2j = "snd (mems ! j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
obtain \<sigma> :: "'Var \<rightharpoonup> 'Val" where "dom \<sigma> = ?X j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma>. dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis dom_restrict_total)
[PROOF STATE]
proof (state)
this:
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
with compat and j_prop
[PROOF STATE]
proof (chain)
picking this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
[PROOF STEP]
have "(cms\<^sub>1 ! j, ?mems\<^sub>1j [\<mapsto> \<sigma>]) \<approx> (cms\<^sub>2 ! j, ?mems\<^sub>2j [\<mapsto> \<sigma>])"
[PROOF STATE]
proof (prove)
using this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. (cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
have "snd (cms\<^sub>1 ! j) = snd (cms\<^sub>2 ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (cms\<^sub>1 ! j) = snd (cms\<^sub>2 ! j)
[PROOF STEP]
using modes_eq
[PROOF STATE]
proof (prove)
using this:
map snd cms\<^sub>1 = map snd cms\<^sub>2

goal (1 subgoal):
 1. snd (cms\<^sub>1 ! j) = snd (cms\<^sub>2 ! j)
[PROOF STEP]
by (metis j_prop length_map nth_map)
[PROOF STATE]
proof (state)
this:
snd (cms\<^sub>1 ! j) = snd (cms\<^sub>2 ! j)

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))
snd (cms\<^sub>1 ! j) = snd (cms\<^sub>2 ! j)
[PROOF STEP]
have "?mems\<^sub>1j [\<mapsto> \<sigma>] =\<^bsub>snd (cms\<^sub>1 ! j)\<^esub>\<^sup>l ?mems\<^sub>2j [\<mapsto> \<sigma>]"
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))
snd (cms\<^sub>1 ! j) = snd (cms\<^sub>2 ! j)

goal (1 subgoal):
 1. subst \<sigma> (fst (mems ! j)) =\<^bsub>snd (cms\<^sub>1 ! j)\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))
[PROOF STEP]
using modes_eq j_prop
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))
snd (cms\<^sub>1 ! j) = snd (cms\<^sub>2 ! j)
map snd cms\<^sub>1 = map snd cms\<^sub>2
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. subst \<sigma> (fst (mems ! j)) =\<^bsub>snd (cms\<^sub>1 ! j)\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))
[PROOF STEP]
by (metis prod.collapse mm_equiv_low_eq)
[PROOF STATE]
proof (state)
this:
subst \<sigma> (fst (mems ! j)) =\<^bsub>snd (cms\<^sub>1 ! j)\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
hence "?mems\<^sub>1j x = ?mems\<^sub>2j x"
[PROOF STATE]
proof (prove)
using this:
subst \<sigma> (fst (mems ! j)) =\<^bsub>snd (cms\<^sub>1 ! j)\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))

goal (1 subgoal):
 1. fst (mems ! j) x = snd (mems ! j) x
[PROOF STEP]
using x_low x_readable j_prop \<open>dom \<sigma> = ?X j\<close>
[PROOF STATE]
proof (prove)
using this:
subst \<sigma> (fst (mems ! j)) =\<^bsub>snd (cms\<^sub>1 ! j)\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))
dma x = Low
\<forall>i<length cms\<^sub>1. x \<notin> snd (cms\<^sub>1 ! i) AsmNoRead
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. fst (mems ! j) x = snd (mems ! j) x
[PROOF STEP]
unfolding low_mds_eq_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. dma x = Low \<and> x \<notin> snd (cms\<^sub>1 ! j) AsmNoRead \<longrightarrow> subst \<sigma> (fst (mems ! j)) x = subst \<sigma> (snd (mems ! j)) x
dma x = Low
\<forall>i<length cms\<^sub>1. x \<notin> snd (cms\<^sub>1 ! i) AsmNoRead
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. fst (mems ! j) x = snd (mems ! j) x
[PROOF STEP]
by (metis subst_not_in_dom)
[PROOF STATE]
proof (state)
this:
fst (mems ! j) x = snd (mems ! j) x

goal (1 subgoal):
 1. \<forall>x. \<exists>j<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fst (mems ! j) x = snd (mems ! j) x

goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
using j_prop
[PROOF STATE]
proof (prove)
using this:
fst (mems ! j) x = snd (mems ! j) x
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
by (metis compat_different_vars)
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 x = mem\<^sub>2 x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 x = mem\<^sub>2 x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loc_reach_subset:
  assumes eval: "\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>"
  shows "loc_reach \<langle>c', mds', mem'\<rangle> \<subseteq> loc_reach \<langle>c, mds, mem\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. loc_reach \<langle>c', mds', mem'\<rangle> \<subseteq> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b ba. \<langle>a, b, ba\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle> \<Longrightarrow> \<langle>a, b, ba\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
fix c'' mds'' mem''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b ba. \<langle>a, b, ba\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle> \<Longrightarrow> \<langle>a, b, ba\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
from eval
[PROOF STATE]
proof (chain)
picking this:
\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>
[PROOF STEP]
have "\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>

goal (1 subgoal):
 1. \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
by (metis loc_reach.refl loc_reach.step surjective_pairing)
[PROOF STATE]
proof (state)
this:
\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>

goal (1 subgoal):
 1. \<And>a b ba. \<langle>a, b, ba\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle> \<Longrightarrow> \<langle>a, b, ba\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
assume "\<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle>"
[PROOF STATE]
proof (state)
this:
\<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle>

goal (1 subgoal):
 1. \<And>a b ba. \<langle>a, b, ba\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle> \<Longrightarrow> \<langle>a, b, ba\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
thus "\<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle>

goal (1 subgoal):
 1. \<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<langle>fst (fst \<langle>c', mds', mem'\<rangle>), snd (fst \<langle>c', mds', mem'\<rangle>), snd \<langle>c', mds', mem'\<rangle>\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
 2. \<And>c'a mds'a mem'a c'' mds'' mem''. \<lbrakk>\<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle>; \<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>; \<langle>c'a, mds'a, mem'a\<rangle> \<leadsto> \<langle>c'', mds'', mem''\<rangle>\<rbrakk> \<Longrightarrow> \<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
 3. \<And>c'a mds'a mem'a mem''. \<lbrakk>\<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle>; \<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>; \<forall>x\<in>mds'a AsmNoWrite. mem'a x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c'a, mds'a, mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
apply (metis \<open>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>\<close> surjective_pairing)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c'a mds'a mem'a c'' mds'' mem''. \<lbrakk>\<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle>; \<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>; \<langle>c'a, mds'a, mem'a\<rangle> \<leadsto> \<langle>c'', mds'', mem''\<rangle>\<rbrakk> \<Longrightarrow> \<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
 2. \<And>c'a mds'a mem'a mem''. \<lbrakk>\<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle>; \<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>; \<forall>x\<in>mds'a AsmNoWrite. mem'a x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c'a, mds'a, mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
apply (metis loc_reach.step)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c'a mds'a mem'a mem''. \<lbrakk>\<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle>; \<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>; \<forall>x\<in>mds'a AsmNoWrite. mem'a x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c'a, mds'a, mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
by (metis loc_reach.mem_diff)
[PROOF STATE]
proof (state)
this:
\<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma locally_sound_modes_invariant:
  assumes sound_modes: "locally_sound_mode_use \<langle>c, mds, mem\<rangle>"
  assumes eval: "\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>"
  shows "locally_sound_mode_use \<langle>c', mds', mem'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. locally_sound_mode_use \<langle>c', mds', mem'\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. locally_sound_mode_use \<langle>c', mds', mem'\<rangle>
[PROOF STEP]
from eval
[PROOF STATE]
proof (chain)
picking this:
\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>
[PROOF STEP]
have "\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>

goal (1 subgoal):
 1. \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
[PROOF STEP]
by (metis fst_conv loc_reach.refl loc_reach.step snd_conv)
[PROOF STATE]
proof (state)
this:
\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>

goal (1 subgoal):
 1. locally_sound_mode_use \<langle>c', mds', mem'\<rangle>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>

goal (1 subgoal):
 1. locally_sound_mode_use \<langle>c', mds', mem'\<rangle>
[PROOF STEP]
using sound_modes
[PROOF STATE]
proof (prove)
using this:
\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
locally_sound_mode_use \<langle>c, mds, mem\<rangle>

goal (1 subgoal):
 1. locally_sound_mode_use \<langle>c', mds', mem'\<rangle>
[PROOF STEP]
unfolding locally_sound_mode_use_def
[PROOF STATE]
proof (prove)
using this:
\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle>
\<forall>c' mds' mem'. \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<rangle> \<longrightarrow> (\<forall>x. (x \<in> mds' GuarNoRead \<longrightarrow> doesnt_read c' x) \<and> (x \<in> mds' GuarNoWrite \<longrightarrow> doesnt_modify c' x))

goal (1 subgoal):
 1. \<forall>c'a mds'a mem'a. \<langle>c'a, mds'a, mem'a\<rangle> \<in> loc_reach \<langle>c', mds', mem'\<rangle> \<longrightarrow> (\<forall>x. (x \<in> mds'a GuarNoRead \<longrightarrow> doesnt_read c'a x) \<and> (x \<in> mds'a GuarNoWrite \<longrightarrow> doesnt_modify c'a x))
[PROOF STEP]
by (metis (no_types) Collect_empty_eq eval loc_reach_subset subsetD)
[PROOF STATE]
proof (state)
this:
locally_sound_mode_use \<langle>c', mds', mem'\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachable_modes_subset:
  assumes eval: "(cms, mem) \<rightarrow> (cms', mem')"
  shows "reachable_mode_states (cms', mem') \<subseteq> reachable_mode_states (cms, mem)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_mode_states (cms', mem') \<subseteq> reachable_mode_states (cms, mem)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> reachable_mode_states (cms', mem') \<Longrightarrow> x \<in> reachable_mode_states (cms, mem)
[PROOF STEP]
fix mdss
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> reachable_mode_states (cms', mem') \<Longrightarrow> x \<in> reachable_mode_states (cms, mem)
[PROOF STEP]
assume "mdss \<in> reachable_mode_states (cms', mem')"
[PROOF STATE]
proof (state)
this:
mdss \<in> reachable_mode_states (cms', mem')

goal (1 subgoal):
 1. \<And>x. x \<in> reachable_mode_states (cms', mem') \<Longrightarrow> x \<in> reachable_mode_states (cms, mem)
[PROOF STEP]
thus "mdss \<in> reachable_mode_states (cms, mem)"
[PROOF STATE]
proof (prove)
using this:
mdss \<in> reachable_mode_states (cms', mem')

goal (1 subgoal):
 1. mdss \<in> reachable_mode_states (cms, mem)
[PROOF STEP]
using reachable_mode_states_def
[PROOF STATE]
proof (prove)
using this:
mdss \<in> reachable_mode_states (cms', mem')
reachable_mode_states ?gc = {mdss. \<exists>cms' mem'. ?gc \<rightarrow>\<^sup>* (cms', mem') \<and> map snd cms' = mdss}

goal (1 subgoal):
 1. mdss \<in> reachable_mode_states (cms, mem)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cms'a mem'a. \<lbrakk>\<And>a b. reachable_mode_states (a, b) = {mdss. \<exists>cms'. (\<exists>mem'. (a, b) \<rightarrow>\<^sup>* (cms', mem')) \<and> map snd cms' = mdss}; mdss = map snd cms'a; (cms', mem') \<rightarrow>\<^sup>* (cms'a, mem'a)\<rbrakk> \<Longrightarrow> \<exists>cms'. (\<exists>mem'. (cms, mem) \<rightarrow>\<^sup>* (cms', mem')) \<and> map snd cms' = map snd cms'a
[PROOF STEP]
by (metis (opaque_lifting, no_types) assms converse_rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
mdss \<in> reachable_mode_states (cms, mem)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma globally_sound_modes_invariant:
  assumes globally_sound: "globally_sound_mode_use (cms, mem)"
  assumes eval: "(cms, mem) \<rightarrow> (cms', mem')"
  shows "globally_sound_mode_use (cms', mem')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. globally_sound_mode_use (cms', mem')
[PROOF STEP]
using assms reachable_modes_subset
[PROOF STATE]
proof (prove)
using this:
globally_sound_mode_use (cms, mem)
(cms, mem) \<rightarrow> (cms', mem')
(?cms, ?mem) \<rightarrow> (?cms', ?mem') \<Longrightarrow> reachable_mode_states (?cms', ?mem') \<subseteq> reachable_mode_states (?cms, ?mem)

goal (1 subgoal):
 1. globally_sound_mode_use (cms', mem')
[PROOF STEP]
unfolding globally_sound_mode_use_def
[PROOF STATE]
proof (prove)
using this:
\<forall>mdss. mdss \<in> reachable_mode_states (cms, mem) \<longrightarrow> compatible_modes mdss
(cms, mem) \<rightarrow> (cms', mem')
(?cms, ?mem) \<rightarrow> (?cms', ?mem') \<Longrightarrow> reachable_mode_states (?cms', ?mem') \<subseteq> reachable_mode_states (?cms, ?mem)

goal (1 subgoal):
 1. \<forall>mdss. mdss \<in> reachable_mode_states (cms', mem') \<longrightarrow> compatible_modes mdss
[PROOF STEP]
by (metis (no_types) subsetD)


[STATEMENT]
lemma loc_reach_mem_diff_subset:
  assumes mem_diff: "\<forall> x. x \<in> mds AsmNoWrite \<longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x"
  shows "\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle> \<Longrightarrow> \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle> \<Longrightarrow> \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle> \<Longrightarrow> \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
let ?lc = "\<langle>c', mds', mem'\<rangle>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle> \<Longrightarrow> \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
assume "?lc \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>"
[PROOF STATE]
proof (state)
this:
\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>

goal (1 subgoal):
 1. \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle> \<Longrightarrow> \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>

goal (1 subgoal):
 1. \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<langle>fst (fst \<langle>c, mds, mem\<^sub>1\<rangle>), snd (fst \<langle>c, mds, mem\<^sub>1\<rangle>), snd \<langle>c, mds, mem\<^sub>1\<rangle>\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
 2. \<And>c' mds' mem' c'' mds'' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<langle>c', mds', mem'\<rangle> \<leadsto> \<langle>c'', mds'', mem''\<rangle>\<rbrakk> \<Longrightarrow> \<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
 3. \<And>c' mds' mem' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<forall>x\<in>mds' AsmNoWrite. mem' x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c', mds', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<langle>fst (fst \<langle>c, mds, mem\<^sub>1\<rangle>), snd (fst \<langle>c, mds, mem\<^sub>1\<rangle>), snd \<langle>c, mds, mem\<^sub>1\<rangle>\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
 2. \<And>c' mds' mem' c'' mds'' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<langle>c', mds', mem'\<rangle> \<leadsto> \<langle>c'', mds'', mem''\<rangle>\<rbrakk> \<Longrightarrow> \<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
 3. \<And>c' mds' mem' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<forall>x\<in>mds' AsmNoWrite. mem' x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c', mds', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>fst (fst \<langle>c, mds, mem\<^sub>1\<rangle>), snd (fst \<langle>c, mds, mem\<^sub>1\<rangle>), snd \<langle>c, mds, mem\<^sub>1\<rangle>\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
by (metis fst_conv loc_reach.mem_diff loc_reach.refl mem_diff snd_conv)
[PROOF STATE]
proof (state)
this:
\<langle>fst (fst \<langle>c, mds, mem\<^sub>1\<rangle>), snd (fst \<langle>c, mds, mem\<^sub>1\<rangle>), snd \<langle>c, mds, mem\<^sub>1\<rangle>\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>

goal (2 subgoals):
 1. \<And>c' mds' mem' c'' mds'' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<langle>c', mds', mem'\<rangle> \<leadsto> \<langle>c'', mds'', mem''\<rangle>\<rbrakk> \<Longrightarrow> \<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
 2. \<And>c' mds' mem' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<forall>x\<in>mds' AsmNoWrite. mem' x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c', mds', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c' mds' mem' c'' mds'' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<langle>c', mds', mem'\<rangle> \<leadsto> \<langle>c'', mds'', mem''\<rangle>\<rbrakk> \<Longrightarrow> \<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
 2. \<And>c' mds' mem' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<forall>x\<in>mds' AsmNoWrite. mem' x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c', mds', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
case step
[PROOF STATE]
proof (state)
this:
\<langle>c'_, mds'_, mem'_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>
\<langle>c'_, mds'_, mem'_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
\<langle>c'_, mds'_, mem'_\<rangle> \<leadsto> \<langle>c''_, mds''_, mem''_\<rangle>

goal (2 subgoals):
 1. \<And>c' mds' mem' c'' mds'' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<langle>c', mds', mem'\<rangle> \<leadsto> \<langle>c'', mds'', mem''\<rangle>\<rbrakk> \<Longrightarrow> \<langle>c'', mds'', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
 2. \<And>c' mds' mem' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<forall>x\<in>mds' AsmNoWrite. mem' x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c', mds', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<langle>c'_, mds'_, mem'_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>
\<langle>c'_, mds'_, mem'_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
\<langle>c'_, mds'_, mem'_\<rangle> \<leadsto> \<langle>c''_, mds''_, mem''_\<rangle>

goal (1 subgoal):
 1. \<langle>c''_, mds''_, mem''_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
by (metis loc_reach.step)
[PROOF STATE]
proof (state)
this:
\<langle>c''_, mds''_, mem''_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. \<And>c' mds' mem' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<forall>x\<in>mds' AsmNoWrite. mem' x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c', mds', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c' mds' mem' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<forall>x\<in>mds' AsmNoWrite. mem' x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c', mds', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
case mem_diff
[PROOF STATE]
proof (state)
this:
\<langle>c'_, mds'_, mem'_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>
\<langle>c'_, mds'_, mem'_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
\<forall>x\<in>mds'_ AsmNoWrite. mem'_ x = mem''_ x

goal (1 subgoal):
 1. \<And>c' mds' mem' mem''. \<lbrakk>\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>; \<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>; \<forall>x\<in>mds' AsmNoWrite. mem' x = mem'' x\<rbrakk> \<Longrightarrow> \<langle>c', mds', mem''\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<langle>c'_, mds'_, mem'_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>1\<rangle>
\<langle>c'_, mds'_, mem'_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
\<forall>x\<in>mds'_ AsmNoWrite. mem'_ x = mem''_ x

goal (1 subgoal):
 1. \<langle>c'_, mds'_, mem''_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
by (metis loc_reach.mem_diff)
[PROOF STATE]
proof (state)
this:
\<langle>c'_, mds'_, mem''_\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c', mds', mem'\<rangle> \<in> loc_reach \<langle>c, mds, mem\<^sub>2\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loc_reach_mem_diff_eq:
  assumes mem_diff: "\<forall> x. x \<in> mds AsmNoWrite \<longrightarrow> mem' x = mem x"
  shows "loc_reach \<langle>c, mds, mem\<rangle> = loc_reach \<langle>c, mds, mem'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. loc_reach \<langle>c, mds, mem\<rangle> = loc_reach \<langle>c, mds, mem'\<rangle>
[PROOF STEP]
using assms loc_reach_mem_diff_subset
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> mds AsmNoWrite \<longrightarrow> mem' x = mem x
\<lbrakk>\<forall>x. x \<in> ?mds AsmNoWrite \<longrightarrow> ?mem\<^sub>1 x = ?mem\<^sub>2 x; \<langle>?c', ?mds', ?mem'\<rangle> \<in> loc_reach \<langle>?c, ?mds, ?mem\<^sub>1\<rangle>\<rbrakk> \<Longrightarrow> \<langle>?c', ?mds', ?mem'\<rangle> \<in> loc_reach \<langle>?c, ?mds, ?mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. loc_reach \<langle>c, mds, mem\<rangle> = loc_reach \<langle>c, mds, mem'\<rangle>
[PROOF STEP]
by (auto, metis)


[STATEMENT]
lemma sound_modes_invariant:
  assumes sound_modes: "sound_mode_use (cms, mem)"
  assumes eval: "(cms, mem) \<rightarrow> (cms', mem')"
  shows "sound_mode_use (cms', mem')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
from sound_modes and eval
[PROOF STATE]
proof (chain)
picking this:
sound_mode_use (cms, mem)
(cms, mem) \<rightarrow> (cms', mem')
[PROOF STEP]
have "globally_sound_mode_use (cms', mem')"
[PROOF STATE]
proof (prove)
using this:
sound_mode_use (cms, mem)
(cms, mem) \<rightarrow> (cms', mem')

goal (1 subgoal):
 1. globally_sound_mode_use (cms', mem')
[PROOF STEP]
by (metis globally_sound_modes_invariant sound_mode_use.simps)
[PROOF STATE]
proof (state)
this:
globally_sound_mode_use (cms', mem')

goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
globally_sound_mode_use (cms', mem')

goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
from sound_modes
[PROOF STATE]
proof (chain)
picking this:
sound_mode_use (cms, mem)
[PROOF STEP]
have loc_sound: "\<forall> i < length cms. locally_sound_mode_use (cms ! i, mem)"
[PROOF STATE]
proof (prove)
using this:
sound_mode_use (cms, mem)

goal (1 subgoal):
 1. \<forall>i<length cms. locally_sound_mode_use (cms ! i, mem)
[PROOF STEP]
unfolding sound_mode_use_def
[PROOF STATE]
proof (prove)
using this:
case (cms, mem) of (cms, mem) \<Rightarrow> list_all (\<lambda>cm. locally_sound_mode_use (cm, mem)) cms \<and> globally_sound_mode_use (cms, mem)

goal (1 subgoal):
 1. \<forall>i<length cms. locally_sound_mode_use (cms ! i, mem)
[PROOF STEP]
by simp (metis list_all_length)
[PROOF STATE]
proof (state)
this:
\<forall>i<length cms. locally_sound_mode_use (cms ! i, mem)

goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
from eval
[PROOF STATE]
proof (chain)
picking this:
(cms, mem) \<rightarrow> (cms', mem')
[PROOF STEP]
obtain k cms\<^sub>k' where
    ev: "(cms ! k, mem) \<leadsto> (cms\<^sub>k', mem') \<and> k < length cms \<and> cms' = cms [k := cms\<^sub>k']"
[PROOF STATE]
proof (prove)
using this:
(cms, mem) \<rightarrow> (cms', mem')

goal (1 subgoal):
 1. (\<And>k cms\<^sub>k'. (cms ! k, mem) \<leadsto> (cms\<^sub>k', mem') \<and> k \<sqsubset> length cms \<and> cms' = cms[k := cms\<^sub>k'] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis meval_elim)
[PROOF STATE]
proof (state)
this:
(cms ! k, mem) \<leadsto> (cms\<^sub>k', mem') \<and> k \<sqsubset> length cms \<and> cms' = cms[k := cms\<^sub>k']

goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
hence "length cms = length cms'"
[PROOF STATE]
proof (prove)
using this:
(cms ! k, mem) \<leadsto> (cms\<^sub>k', mem') \<and> k \<sqsubset> length cms \<and> cms' = cms[k := cms\<^sub>k']

goal (1 subgoal):
 1. length cms = length cms'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length cms = length cms'

goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
have "\<And> i. i < length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<sqsubset> length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<sqsubset> length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<sqsubset> length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
assume i_le: "i < length cms'"
[PROOF STATE]
proof (state)
this:
i \<sqsubset> length cms'

goal (1 subgoal):
 1. \<And>i. i \<sqsubset> length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
thus "?thesis i"
[PROOF STATE]
proof (prove)
using this:
i \<sqsubset> length cms'

goal (1 subgoal):
 1. locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
proof (cases "i = k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<sqsubset> length cms'; i = k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
 2. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
assume "i = k"
[PROOF STATE]
proof (state)
this:
i = k

goal (2 subgoals):
 1. \<lbrakk>i \<sqsubset> length cms'; i = k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
 2. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i = k

goal (1 subgoal):
 1. locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
using i_le ev loc_sound
[PROOF STATE]
proof (prove)
using this:
i = k
i \<sqsubset> length cms'
(cms ! k, mem) \<leadsto> (cms\<^sub>k', mem') \<and> k \<sqsubset> length cms \<and> cms' = cms[k := cms\<^sub>k']
\<forall>i<length cms. locally_sound_mode_use (cms ! i, mem)

goal (1 subgoal):
 1. locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
by (metis (opaque_lifting, no_types) locally_sound_modes_invariant nth_list_update surj_pair)
[PROOF STATE]
proof (state)
this:
locally_sound_mode_use (cms' ! i, mem')

goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
assume "i \<noteq> k"
[PROOF STATE]
proof (state)
this:
i \<noteq> k

goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
hence "cms' ! i = cms ! i"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> k

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

goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
from sound_modes
[PROOF STATE]
proof (chain)
picking this:
sound_mode_use (cms, mem)
[PROOF STEP]
have "compatible_modes (map snd cms)"
[PROOF STATE]
proof (prove)
using this:
sound_mode_use (cms, mem)

goal (1 subgoal):
 1. compatible_modes (map snd cms)
[PROOF STEP]
unfolding sound_mode_use.simps
[PROOF STATE]
proof (prove)
using this:
list_all (\<lambda>cm. locally_sound_mode_use (cm, mem)) cms \<and> globally_sound_mode_use (cms, mem)

goal (1 subgoal):
 1. compatible_modes (map snd cms)
[PROOF STEP]
by (metis globally_sound_modes_compatible)
[PROOF STATE]
proof (state)
this:
compatible_modes (map snd cms)

goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
hence "\<And> x. x \<in> snd (cms ! i) AsmNoWrite \<Longrightarrow> x \<in> snd (cms ! k) GuarNoWrite"
[PROOF STATE]
proof (prove)
using this:
compatible_modes (map snd cms)

goal (1 subgoal):
 1. \<And>x. x \<in> snd (cms ! i) AsmNoWrite \<Longrightarrow> x \<in> snd (cms ! k) GuarNoWrite
[PROOF STEP]
unfolding compatible_modes_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i x. i \<sqsubset> length (map snd cms) \<longrightarrow> (x \<in> (map snd cms ! i) AsmNoRead \<longrightarrow> (\<forall>j<length (map snd cms). j \<noteq> i \<longrightarrow> x \<in> (map snd cms ! j) GuarNoRead)) \<and> (x \<in> (map snd cms ! i) AsmNoWrite \<longrightarrow> (\<forall>j<length (map snd cms). j \<noteq> i \<longrightarrow> x \<in> (map snd cms ! j) GuarNoWrite))

goal (1 subgoal):
 1. \<And>x. x \<in> snd (cms ! i) AsmNoWrite \<Longrightarrow> x \<in> snd (cms ! k) GuarNoWrite
[PROOF STEP]
by (metis (no_types) \<open>i \<noteq> k\<close> \<open>length cms = length cms'\<close> ev i_le length_map nth_map)
[PROOF STATE]
proof (state)
this:
?x5 \<in> snd (cms ! i) AsmNoWrite \<Longrightarrow> ?x5 \<in> snd (cms ! k) GuarNoWrite

goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
hence "\<And> x. x \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> doesnt_modify (fst (cms ! k)) x"
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> snd (cms ! i) AsmNoWrite \<Longrightarrow> ?x5 \<in> snd (cms ! k) GuarNoWrite

goal (1 subgoal):
 1. \<And>x. x \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> doesnt_modify (fst (cms ! k)) x
[PROOF STEP]
using ev loc_sound
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> snd (cms ! i) AsmNoWrite \<Longrightarrow> ?x5 \<in> snd (cms ! k) GuarNoWrite
(cms ! k, mem) \<leadsto> (cms\<^sub>k', mem') \<and> k \<sqsubset> length cms \<and> cms' = cms[k := cms\<^sub>k']
\<forall>i<length cms. locally_sound_mode_use (cms ! i, mem)

goal (1 subgoal):
 1. \<And>x. x \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> doesnt_modify (fst (cms ! k)) x
[PROOF STEP]
unfolding locally_sound_mode_use_def
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> snd (cms ! i) AsmNoWrite \<Longrightarrow> ?x5 \<in> snd (cms ! k) GuarNoWrite
(cms ! k, mem) \<leadsto> (cms\<^sub>k', mem') \<and> k \<sqsubset> length cms \<and> cms' = cms[k := cms\<^sub>k']
\<forall>i<length cms. \<forall>c' mds' mem'. \<langle>c', mds', mem'\<rangle> \<in> loc_reach (cms ! i, mem) \<longrightarrow> (\<forall>x. (x \<in> mds' GuarNoRead \<longrightarrow> doesnt_read c' x) \<and> (x \<in> mds' GuarNoWrite \<longrightarrow> doesnt_modify c' x))

goal (1 subgoal):
 1. \<And>x. x \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> doesnt_modify (fst (cms ! k)) x
[PROOF STEP]
by (metis loc_reach.refl surjective_pairing)
[PROOF STATE]
proof (state)
this:
?x5 \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> doesnt_modify (fst (cms ! k)) ?x5

goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
with eval
[PROOF STATE]
proof (chain)
picking this:
(cms, mem) \<rightarrow> (cms', mem')
?x5 \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> doesnt_modify (fst (cms ! k)) ?x5
[PROOF STEP]
have "\<And> x. x \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> mem x = mem' x"
[PROOF STATE]
proof (prove)
using this:
(cms, mem) \<rightarrow> (cms', mem')
?x5 \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> doesnt_modify (fst (cms ! k)) ?x5

goal (1 subgoal):
 1. \<And>x. x \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> mem x = mem' x
[PROOF STEP]
by (metis (no_types) doesnt_modify_def ev prod.collapse)
[PROOF STATE]
proof (state)
this:
?x5 \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> mem ?x5 = mem' ?x5

goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x5 \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> mem ?x5 = mem' ?x5
[PROOF STEP]
have "loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)"
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> snd (cms ! i) AsmNoWrite \<longrightarrow> mem ?x5 = mem' ?x5

goal (1 subgoal):
 1. loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)
[PROOF STEP]
by (metis loc_reach_mem_diff_eq prod.collapse)
[PROOF STATE]
proof (state)
this:
loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)

goal (1 subgoal):
 1. \<lbrakk>i \<sqsubset> length cms'; i \<noteq> k\<rbrakk> \<Longrightarrow> locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)

goal (1 subgoal):
 1. locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
using loc_sound i_le \<open>length cms = length cms'\<close>
[PROOF STATE]
proof (prove)
using this:
loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)
\<forall>i<length cms. locally_sound_mode_use (cms ! i, mem)
i \<sqsubset> length cms'
length cms = length cms'

goal (1 subgoal):
 1. locally_sound_mode_use (cms' ! i, mem')
[PROOF STEP]
unfolding locally_sound_mode_use_def
[PROOF STATE]
proof (prove)
using this:
loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)
\<forall>i<length cms. \<forall>c' mds' mem'. \<langle>c', mds', mem'\<rangle> \<in> loc_reach (cms ! i, mem) \<longrightarrow> (\<forall>x. (x \<in> mds' GuarNoRead \<longrightarrow> doesnt_read c' x) \<and> (x \<in> mds' GuarNoWrite \<longrightarrow> doesnt_modify c' x))
i \<sqsubset> length cms'
length cms = length cms'

goal (1 subgoal):
 1. \<forall>c' mds' mem'a. \<langle>c', mds', mem'a\<rangle> \<in> loc_reach (cms' ! i, mem') \<longrightarrow> (\<forall>x. (x \<in> mds' GuarNoRead \<longrightarrow> doesnt_read c' x) \<and> (x \<in> mds' GuarNoWrite \<longrightarrow> doesnt_modify c' x))
[PROOF STEP]
by (metis \<open>cms' ! i = cms ! i\<close>)
[PROOF STATE]
proof (state)
this:
locally_sound_mode_use (cms' ! i, mem')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
locally_sound_mode_use (cms' ! i, mem')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i5 \<sqsubset> length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! ?i5, mem')

goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
globally_sound_mode_use (cms', mem')
?i5 \<sqsubset> length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! ?i5, mem')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
globally_sound_mode_use (cms', mem')
?i5 \<sqsubset> length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! ?i5, mem')

goal (1 subgoal):
 1. sound_mode_use (cms', mem')
[PROOF STEP]
unfolding sound_mode_use.simps
[PROOF STATE]
proof (prove)
using this:
globally_sound_mode_use (cms', mem')
?i5 \<sqsubset> length cms' \<Longrightarrow> locally_sound_mode_use (cms' ! ?i5, mem')

goal (1 subgoal):
 1. list_all (\<lambda>cm. locally_sound_mode_use (cm, mem')) cms' \<and> globally_sound_mode_use (cms', mem')
[PROOF STEP]
by (metis (no_types) list_all_length)
[PROOF STATE]
proof (state)
this:
sound_mode_use (cms', mem')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma makes_compatible_eval_k:
  assumes compat: "makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems"
  assumes modes_eq: "map snd cms\<^sub>1 = map snd cms\<^sub>2"
  assumes sound_modes: "sound_mode_use (cms\<^sub>1, mem\<^sub>1)" "sound_mode_use (cms\<^sub>2, mem\<^sub>2)"
  assumes eval: "(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')"
  shows "\<exists> cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and>
                              sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and>
                              map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and>
                              (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and>
                              makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
(* cms\<^sub>1' and mem\<^sub>1' need to be arbitrary so
     that the induction hypothesis is sufficiently general. *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
from eval
[PROOF STATE]
proof (chain)
picking this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
proof (induct "k" arbitrary: cms\<^sub>1' mem\<^sub>1')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
 2. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>1', mem\<^sub>1')

goal (2 subgoals):
 1. \<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
 2. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
hence "cms\<^sub>1' = cms\<^sub>1 \<and> mem\<^sub>1' = mem\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. cms\<^sub>1' = cms\<^sub>1 \<and> mem\<^sub>1' = mem\<^sub>1
[PROOF STEP]
by (metis prod.inject meval_k.simps(1))
[PROOF STATE]
proof (state)
this:
cms\<^sub>1' = cms\<^sub>1 \<and> mem\<^sub>1' = mem\<^sub>1

goal (2 subgoals):
 1. \<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
 2. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
cms\<^sub>1' = cms\<^sub>1 \<and> mem\<^sub>1' = mem\<^sub>1

goal (1 subgoal):
 1. \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
by (metis compat meval_k.simps(1) modes_eq sound_modes)
[PROOF STATE]
proof (state)
this:
\<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>0\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'

goal (1 subgoal):
 1. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (?cms\<^sub>1'5, ?mem\<^sub>1'5) \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (?cms\<^sub>1'5, ?mem\<^sub>1'5) \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd ?cms\<^sub>1'5 = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (?cms\<^sub>1'5, ?mem\<^sub>1'5) (cms\<^sub>2', mem\<^sub>2') mems'
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (?cms\<^sub>1'5, ?mem\<^sub>1'5) \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (?cms\<^sub>1'5, ?mem\<^sub>1'5) \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd ?cms\<^sub>1'5 = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (?cms\<^sub>1'5, ?mem\<^sub>1'5) (cms\<^sub>2', mem\<^sub>2') mems'
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')
[PROOF STEP]
obtain cms\<^sub>1'' mem\<^sub>1'' where eval'':
      "(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1'', mem\<^sub>1'') \<and> (cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')"
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (?cms\<^sub>1'5, ?mem\<^sub>1'5) \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (?cms\<^sub>1'5, ?mem\<^sub>1'5) \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd ?cms\<^sub>1'5 = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (?cms\<^sub>1'5, ?mem\<^sub>1'5) (cms\<^sub>2', mem\<^sub>2') mems'
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. (\<And>cms\<^sub>1''' mem\<^sub>1'''. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1''', mem\<^sub>1''') \<and> (cms\<^sub>1''', mem\<^sub>1''') \<rightarrow> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis meval_k.simps(2) prod_cases3 snd_conv)
[PROOF STATE]
proof (state)
this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1'', mem\<^sub>1'') \<and> (cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
hence "(cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')"
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1'', mem\<^sub>1'') \<and> (cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. (cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
from eval''
[PROOF STATE]
proof (chain)
picking this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1'', mem\<^sub>1'') \<and> (cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')
[PROOF STEP]
obtain cms\<^sub>2'' mem\<^sub>2'' mems'' where IH:
      "sound_mode_use (cms\<^sub>1'', mem\<^sub>1'') \<and>
       sound_mode_use (cms\<^sub>2'', mem\<^sub>2'') \<and>
       map snd cms\<^sub>1'' = map snd cms\<^sub>2'' \<and>
       (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2'', mem\<^sub>2'') \<and>
       makes_compatible (cms\<^sub>1'', mem\<^sub>1'') (cms\<^sub>2'', mem\<^sub>2'') mems''"
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1'', mem\<^sub>1'') \<and> (cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. (\<And>cms\<^sub>2'' mem\<^sub>2'' mems''. sound_mode_use (cms\<^sub>1'', mem\<^sub>1'') \<and> sound_mode_use (cms\<^sub>2'', mem\<^sub>2'') \<and> map snd cms\<^sub>1'' = map snd cms\<^sub>2'' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2'', mem\<^sub>2'') \<and> makes_compatible (cms\<^sub>1'', mem\<^sub>1'') (cms\<^sub>2'', mem\<^sub>2'') mems'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1'', mem\<^sub>1'') \<and> (cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (?cms\<^sub>1'5, ?mem\<^sub>1'5) \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (?cms\<^sub>1'5, ?mem\<^sub>1'5) \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd ?cms\<^sub>1'5 = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (?cms\<^sub>1'5, ?mem\<^sub>1'5) (cms\<^sub>2', mem\<^sub>2') mems'
(cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. (\<And>cms\<^sub>2'' mem\<^sub>2'' mems''. sound_mode_use (cms\<^sub>1'', mem\<^sub>1'') \<and> sound_mode_use (cms\<^sub>2'', mem\<^sub>2'') \<and> map snd cms\<^sub>1'' = map snd cms\<^sub>2'' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2'', mem\<^sub>2'') \<and> makes_compatible (cms\<^sub>1'', mem\<^sub>1'') (cms\<^sub>2'', mem\<^sub>2'') mems'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sound_mode_use (cms\<^sub>1'', mem\<^sub>1'') \<and> sound_mode_use (cms\<^sub>2'', mem\<^sub>2'') \<and> map snd cms\<^sub>1'' = map snd cms\<^sub>2'' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2'', mem\<^sub>2'') \<and> makes_compatible (cms\<^sub>1'', mem\<^sub>1'') (cms\<^sub>2'', mem\<^sub>2'') mems''

goal (1 subgoal):
 1. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')
sound_mode_use (cms\<^sub>1'', mem\<^sub>1'') \<and> sound_mode_use (cms\<^sub>2'', mem\<^sub>2'') \<and> map snd cms\<^sub>1'' = map snd cms\<^sub>2'' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2'', mem\<^sub>2'') \<and> makes_compatible (cms\<^sub>1'', mem\<^sub>1'') (cms\<^sub>2'', mem\<^sub>2'') mems''
[PROOF STEP]
obtain cms\<^sub>2' mem\<^sub>2' mems' where
      "map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and>
       (cms\<^sub>2'', mem\<^sub>2'') \<rightarrow> (cms\<^sub>2', mem\<^sub>2') \<and>
       makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'"
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')
sound_mode_use (cms\<^sub>1'', mem\<^sub>1'') \<and> sound_mode_use (cms\<^sub>2'', mem\<^sub>2'') \<and> map snd cms\<^sub>1'' = map snd cms\<^sub>2'' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2'', mem\<^sub>2'') \<and> makes_compatible (cms\<^sub>1'', mem\<^sub>1'') (cms\<^sub>2'', mem\<^sub>2'') mems''

goal (1 subgoal):
 1. (\<And>cms\<^sub>2' mem\<^sub>2' mems'. map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2'', mem\<^sub>2'') \<rightarrow> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using makes_compatible_invariant
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1'', mem\<^sub>1'') \<rightarrow> (cms\<^sub>1', mem\<^sub>1')
sound_mode_use (cms\<^sub>1'', mem\<^sub>1'') \<and> sound_mode_use (cms\<^sub>2'', mem\<^sub>2'') \<and> map snd cms\<^sub>1'' = map snd cms\<^sub>2'' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2'', mem\<^sub>2'') \<and> makes_compatible (cms\<^sub>1'', mem\<^sub>1'') (cms\<^sub>2'', mem\<^sub>2'') mems''
\<lbrakk>sound_mode_use (?cms\<^sub>1, ?mem\<^sub>1); sound_mode_use (?cms\<^sub>2, ?mem\<^sub>2); makes_compatible (?cms\<^sub>1, ?mem\<^sub>1) (?cms\<^sub>2, ?mem\<^sub>2) ?mems; map snd ?cms\<^sub>1 = map snd ?cms\<^sub>2; (?cms\<^sub>1, ?mem\<^sub>1) \<rightarrow> (?cms\<^sub>1', ?mem\<^sub>1'); \<And>cms\<^sub>2' mem\<^sub>2' mems'. map snd ?cms\<^sub>1' = map snd cms\<^sub>2' \<and> (?cms\<^sub>2, ?mem\<^sub>2) \<rightarrow> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (?cms\<^sub>1', ?mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>cms\<^sub>2' mem\<^sub>2' mems'. map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2'', mem\<^sub>2'') \<rightarrow> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2'', mem\<^sub>2'') \<rightarrow> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'

goal (1 subgoal):
 1. \<And>k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>\<And>cms\<^sub>1' mem\<^sub>1'. (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'; (cms\<^sub>1, mem\<^sub>1) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2'', mem\<^sub>2'') \<rightarrow> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'

goal (1 subgoal):
 1. \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
[PROOF STEP]
by (metis IH eval'' meval_k.simps(2) sound_modes_invariant)
[PROOF STATE]
proof (state)
this:
\<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>Suc k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (cms\<^sub>1', mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (cms\<^sub>2, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma differing_vars_initially_empty:
  "i < n \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (zip (replicate n mem\<^sub>1) (replicate n mem\<^sub>2)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<sqsubset> n \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (zip (replicate n mem\<^sub>1) (replicate n mem\<^sub>2)) i
[PROOF STEP]
unfolding differing_vars_lists_def differing_vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<sqsubset> n \<Longrightarrow> x \<notin> {x. mem\<^sub>1 x \<noteq> fst (zip (replicate n mem\<^sub>1) (replicate n mem\<^sub>2) ! i) x} \<union> {x. mem\<^sub>2 x \<noteq> snd (zip (replicate n mem\<^sub>1) (replicate n mem\<^sub>2) ! i) x}
[PROOF STEP]
by auto