[STATEMENT]
lemma ta_seq_consist_most_recent_write_for:
  assumes sc: "ta_seq_consist P Map.empty (lmap snd E)"
  and read: "r \<in> read_actions E"
  and new_actions_for_fun: "\<And>adal a a'. \<lbrakk> a \<in> new_actions_for P E adal; a' \<in> new_actions_for P E adal \<rbrakk> \<Longrightarrow> a = a'"
  shows "\<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
from read
[PROOF STATE]
proof (chain)
picking this:
r \<in> read_actions E
[PROOF STEP]
obtain t v ad al
    where nth_r: "lnth E r = (t, NormalAction (ReadMem ad al v))"
    and r: "enat r < llength E"
[PROOF STATE]
proof (prove)
using this:
r \<in> read_actions E

goal (1 subgoal):
 1. (\<And>t ad al v. \<lbrakk>lnth E r = (t, NormalAction (ReadMem ad al v)); enat r < llength E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases)(cases "lnth E r", auto simp add: action_obs_def actions_def)
[PROOF STATE]
proof (state)
this:
lnth E r = (t, NormalAction (ReadMem ad al v))
enat r < llength E

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
from nth_r r
[PROOF STATE]
proof (chain)
picking this:
lnth E r = (t, NormalAction (ReadMem ad al v))
enat r < llength E
[PROOF STEP]
have E_unfold: "E = lappend (ltake (enat r) E) (LCons (t, NormalAction (ReadMem ad al v)) (ldropn (Suc r) E))"
[PROOF STATE]
proof (prove)
using this:
lnth E r = (t, NormalAction (ReadMem ad al v))
enat r < llength E

goal (1 subgoal):
 1. E = lappend (ltake (enat r) E) (LCons (t, NormalAction (ReadMem ad al v)) (ldropn (Suc r) E))
[PROOF STEP]
by (metis lappend_ltake_enat_ldropn ldropn_Suc_conv_ldropn)
[PROOF STATE]
proof (state)
this:
E = lappend (ltake (enat r) E) (LCons (t, NormalAction (ReadMem ad al v)) (ldropn (Suc r) E))

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
from sc
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P Map.empty (lmap snd E)
[PROOF STEP]
obtain b where sc': "ta_seq_consist P Map.empty (ltake (enat r) (lmap snd E))"
    and mrw': "mrw_values P Map.empty (map snd (list_of (ltake (enat r) E))) (ad, al) = \<lfloor>(v, b)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P Map.empty (lmap snd E)

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>ta_seq_consist P Map.empty (ltake (enat r) (lmap snd E)); mrw_values P Map.empty (map snd (list_of (ltake (enat r) E))) (ad, al) = \<lfloor>(v, b)\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(subst (asm) (3) E_unfold)(auto simp add: ta_seq_consist_lappend lmap_lappend_distrib)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P Map.empty (ltake (enat r) (lmap snd E))
mrw_values P Map.empty (map snd (list_of (ltake (enat r) E))) (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
from mrw_values_mrw[OF mrw', of t] r
[PROOF STATE]
proof (chain)
picking this:
(None = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (map snd (list_of (ltake (enat r) E))) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)) \<Longrightarrow> \<exists>i<length (list_of (ltake (enat r) E)). P,llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length (list_of (ltake (enat r) E)) \<leadsto>mrw i \<and> value_written P (llist_of (list_of (ltake (enat r) E))) i (ad, al) = v
enat r < llength E
[PROOF STEP]
obtain E' w'
    where E': "E' = llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))])"
    and v: "v = value_written P (ltake (enat r) E) w' (ad, al)"
    and mrw'': "P,E' \<turnstile> r \<leadsto>mrw w'"
    and w': "w' < r"
[PROOF STATE]
proof (prove)
using this:
(None = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (map snd (list_of (ltake (enat r) E))) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)) \<Longrightarrow> \<exists>i<length (list_of (ltake (enat r) E)). P,llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length (list_of (ltake (enat r) E)) \<leadsto>mrw i \<and> value_written P (llist_of (list_of (ltake (enat r) E))) i (ad, al) = v
enat r < llength E

goal (1 subgoal):
 1. (\<And>E' w'. \<lbrakk>E' = llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))]); v = value_written P (ltake (enat r) E) w' (ad, al); P,E' \<turnstile> r \<leadsto>mrw w'; w' < r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce simp add: length_list_of_conv_the_enat min_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
E' = llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))])
v = value_written P (ltake (enat r) E) w' (ad, al)
P,E' \<turnstile> r \<leadsto>mrw w'
w' < r

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
from E' r
[PROOF STATE]
proof (chain)
picking this:
E' = llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))])
enat r < llength E
[PROOF STEP]
have sim: "ltake (enat (Suc r)) E' [\<approx>] ltake (enat (Suc r)) E"
[PROOF STATE]
proof (prove)
using this:
E' = llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))])
enat r < llength E

goal (1 subgoal):
 1. ltake (enat (Suc r)) E' [\<approx>] ltake (enat (Suc r)) E
[PROOF STEP]
by(subst E_unfold)(simp add: ltake_lappend llist_of_list_of_append min_def, auto simp add: eSuc_enat[symmetric] zero_enat_def[symmetric] eq_into_sim_actions)
[PROOF STATE]
proof (state)
this:
ltake (enat (Suc r)) E' [\<approx>] ltake (enat (Suc r)) E

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
from nth_r
[PROOF STATE]
proof (chain)
picking this:
lnth E r = (t, NormalAction (ReadMem ad al v))
[PROOF STEP]
have adal_r: "(ad, al) \<in> action_loc P E r"
[PROOF STATE]
proof (prove)
using this:
lnth E r = (t, NormalAction (ReadMem ad al v))

goal (1 subgoal):
 1. (ad, al) \<in> action_loc P E r
[PROOF STEP]
by(simp add: action_obs_def)
[PROOF STATE]
proof (state)
this:
(ad, al) \<in> action_loc P E r

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
from E' r
[PROOF STATE]
proof (chain)
picking this:
E' = llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))])
enat r < llength E
[PROOF STEP]
have nth_r': "lnth E' r = (t, NormalAction (ReadMem ad al v))"
[PROOF STATE]
proof (prove)
using this:
E' = llist_of (list_of (ltake (enat r) E) @ [(t, NormalAction (ReadMem ad al v))])
enat r < llength E

goal (1 subgoal):
 1. lnth E' r = (t, NormalAction (ReadMem ad al v))
[PROOF STEP]
by(auto simp add: nth_append length_list_of_conv_the_enat min_def)
[PROOF STATE]
proof (state)
this:
lnth E' r = (t, NormalAction (ReadMem ad al v))

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
with mrw'' w' r adal_r
[PROOF STATE]
proof (chain)
picking this:
P,E' \<turnstile> r \<leadsto>mrw w'
w' < r
enat r < llength E
(ad, al) \<in> action_loc P E r
lnth E' r = (t, NormalAction (ReadMem ad al v))
[PROOF STEP]
obtain "E \<turnstile> w' \<le>a r" "w' \<in> write_actions E" "(ad, al) \<in> action_loc P E w'"
[PROOF STATE]
proof (prove)
using this:
P,E' \<turnstile> r \<leadsto>mrw w'
w' < r
enat r < llength E
(ad, al) \<in> action_loc P E r
lnth E' r = (t, NormalAction (ReadMem ad al v))

goal (1 subgoal):
 1. (\<lbrakk>E \<turnstile> w' \<le>a r; w' \<in> write_actions E; (ad, al) \<in> action_loc P E w'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases(fastforce simp add: action_obs_def action_loc_change_prefix[OF sim[symmetric], simplified action_obs_def] intro: action_order_change_prefix[OF _ sim] write_actions_change_prefix[OF _ sim])
[PROOF STATE]
proof (state)
this:
E \<turnstile> w' \<le>a r
w' \<in> write_actions E
(ad, al) \<in> action_loc P E w'

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
with read adal_r
[PROOF STATE]
proof (chain)
picking this:
r \<in> read_actions E
(ad, al) \<in> action_loc P E r
E \<turnstile> w' \<le>a r
w' \<in> write_actions E
(ad, al) \<in> action_loc P E w'
[PROOF STEP]
have "P,E \<turnstile> r \<leadsto>mrw w'"
[PROOF STATE]
proof (prove)
using this:
r \<in> read_actions E
(ad, al) \<in> action_loc P E r
E \<turnstile> w' \<le>a r
w' \<in> write_actions E
(ad, al) \<in> action_loc P E w'

goal (1 subgoal):
 1. P,E \<turnstile> r \<leadsto>mrw w'
[PROOF STEP]
proof(rule most_recent_write_for.intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>wa'. \<lbrakk>wa' \<in> write_actions E; (ad, al) \<in> action_loc P E wa'\<rbrakk> \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
fix wa'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>wa'. \<lbrakk>wa' \<in> write_actions E; (ad, al) \<in> action_loc P E wa'\<rbrakk> \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
assume write': "wa' \<in> write_actions E"
      and adal_wa': "(ad, al) \<in> action_loc P E wa'"
[PROOF STATE]
proof (state)
this:
wa' \<in> write_actions E
(ad, al) \<in> action_loc P E wa'

goal (1 subgoal):
 1. \<And>wa'. \<lbrakk>wa' \<in> write_actions E; (ad, al) \<in> action_loc P E wa'\<rbrakk> \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
show "E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
proof(cases "r \<le> wa'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
 2. \<not> r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
assume "r \<le> wa'"
[PROOF STATE]
proof (state)
this:
r \<le> wa'

goal (2 subgoals):
 1. r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
 2. \<not> r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
proof(cases "is_new_action (action_obs E wa')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
 2. \<not> is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_new_action (action_obs E wa')

goal (2 subgoals):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
 2. \<not> is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
with \<open>r \<le> wa'\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<le> wa'
\<not> is_new_action (action_obs E wa')
[PROOF STEP]
have "E \<turnstile> r \<le>a wa'"
[PROOF STATE]
proof (prove)
using this:
r \<le> wa'
\<not> is_new_action (action_obs E wa')

goal (1 subgoal):
 1. E \<turnstile> r \<le>a wa'
[PROOF STEP]
using read write'
[PROOF STATE]
proof (prove)
using this:
r \<le> wa'
\<not> is_new_action (action_obs E wa')
r \<in> read_actions E
wa' \<in> write_actions E

goal (1 subgoal):
 1. E \<turnstile> r \<le>a wa'
[PROOF STEP]
by(auto simp add: action_order_def elim!: read_actions.cases)
[PROOF STATE]
proof (state)
this:
E \<turnstile> r \<le>a wa'

goal (2 subgoals):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
 2. \<not> is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> r \<le>a wa'

goal (1 subgoal):
 1. E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'

goal (1 subgoal):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_new_action (action_obs E wa')

goal (1 subgoal):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
with write' adal_wa'
[PROOF STATE]
proof (chain)
picking this:
wa' \<in> write_actions E
(ad, al) \<in> action_loc P E wa'
is_new_action (action_obs E wa')
[PROOF STEP]
have "wa' \<in> new_actions_for P E (ad, al)"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> write_actions E
(ad, al) \<in> action_loc P E wa'
is_new_action (action_obs E wa')

goal (1 subgoal):
 1. wa' \<in> new_actions_for P E (ad, al)
[PROOF STEP]
by(simp add: new_actions_for_def)
[PROOF STATE]
proof (state)
this:
wa' \<in> new_actions_for P E (ad, al)

goal (1 subgoal):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
hence "w' \<notin> new_actions_for P E (ad, al)"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> new_actions_for P E (ad, al)

goal (1 subgoal):
 1. w' \<notin> new_actions_for P E (ad, al)
[PROOF STEP]
using r w' \<open>r \<le> wa'\<close>
[PROOF STATE]
proof (prove)
using this:
wa' \<in> new_actions_for P E (ad, al)
enat r < llength E
w' < r
r \<le> wa'

goal (1 subgoal):
 1. w' \<notin> new_actions_for P E (ad, al)
[PROOF STEP]
by(auto dest: new_actions_for_fun)
[PROOF STATE]
proof (state)
this:
w' \<notin> new_actions_for P E (ad, al)

goal (1 subgoal):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
with \<open>w' \<in> write_actions E\<close> \<open>(ad, al) \<in> action_loc P E w'\<close>
[PROOF STATE]
proof (chain)
picking this:
w' \<in> write_actions E
(ad, al) \<in> action_loc P E w'
w' \<notin> new_actions_for P E (ad, al)
[PROOF STEP]
have "\<not> is_new_action (action_obs E w')"
[PROOF STATE]
proof (prove)
using this:
w' \<in> write_actions E
(ad, al) \<in> action_loc P E w'
w' \<notin> new_actions_for P E (ad, al)

goal (1 subgoal):
 1. \<not> is_new_action (action_obs E w')
[PROOF STEP]
by(simp add: new_actions_for_def)
[PROOF STATE]
proof (state)
this:
\<not> is_new_action (action_obs E w')

goal (1 subgoal):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
with write' True \<open>w' \<in> write_actions E\<close>
[PROOF STATE]
proof (chain)
picking this:
wa' \<in> write_actions E
is_new_action (action_obs E wa')
w' \<in> write_actions E
\<not> is_new_action (action_obs E w')
[PROOF STEP]
have "E \<turnstile> wa' \<le>a w'"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> write_actions E
is_new_action (action_obs E wa')
w' \<in> write_actions E
\<not> is_new_action (action_obs E w')

goal (1 subgoal):
 1. E \<turnstile> wa' \<le>a w'
[PROOF STEP]
by(simp add: action_order_def)
[PROOF STATE]
proof (state)
this:
E \<turnstile> wa' \<le>a w'

goal (1 subgoal):
 1. is_new_action (action_obs E wa') \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> wa' \<le>a w'

goal (1 subgoal):
 1. E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'

goal (1 subgoal):
 1. \<not> r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
assume "\<not> r \<le> wa'"
[PROOF STATE]
proof (state)
this:
\<not> r \<le> wa'

goal (1 subgoal):
 1. \<not> r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
hence "wa' < r"
[PROOF STATE]
proof (prove)
using this:
\<not> r \<le> wa'

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

goal (1 subgoal):
 1. \<not> r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
with write' adal_wa'
[PROOF STATE]
proof (chain)
picking this:
wa' \<in> write_actions E
(ad, al) \<in> action_loc P E wa'
wa' < r
[PROOF STEP]
have "wa' \<in> write_actions E'" "(ad, al) \<in> action_loc P E' wa'"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> write_actions E
(ad, al) \<in> action_loc P E wa'
wa' < r

goal (1 subgoal):
 1. wa' \<in> write_actions E' &&& (ad, al) \<in> action_loc P E' wa'
[PROOF STEP]
by(auto intro: write_actions_change_prefix[OF _ sim[symmetric]] simp add: action_loc_change_prefix[OF sim])
[PROOF STATE]
proof (state)
this:
wa' \<in> write_actions E'
(ad, al) \<in> action_loc P E' wa'

goal (1 subgoal):
 1. \<not> r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
from most_recent_write_recent[OF mrw'' _ this] nth_r'
[PROOF STATE]
proof (chain)
picking this:
(ad, al) \<in> action_loc P E' r \<Longrightarrow> E' \<turnstile> wa' \<le>a w' \<or> E' \<turnstile> r \<le>a wa'
lnth E' r = (t, NormalAction (ReadMem ad al v))
[PROOF STEP]
have "E' \<turnstile> wa' \<le>a w' \<or> E' \<turnstile> r \<le>a wa'"
[PROOF STATE]
proof (prove)
using this:
(ad, al) \<in> action_loc P E' r \<Longrightarrow> E' \<turnstile> wa' \<le>a w' \<or> E' \<turnstile> r \<le>a wa'
lnth E' r = (t, NormalAction (ReadMem ad al v))

goal (1 subgoal):
 1. E' \<turnstile> wa' \<le>a w' \<or> E' \<turnstile> r \<le>a wa'
[PROOF STEP]
by(simp add: action_obs_def)
[PROOF STATE]
proof (state)
this:
E' \<turnstile> wa' \<le>a w' \<or> E' \<turnstile> r \<le>a wa'

goal (1 subgoal):
 1. \<not> r \<le> wa' \<Longrightarrow> E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
E' \<turnstile> wa' \<le>a w' \<or> E' \<turnstile> r \<le>a wa'

goal (1 subgoal):
 1. E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
using \<open>wa' < r\<close> w'
[PROOF STATE]
proof (prove)
using this:
E' \<turnstile> wa' \<le>a w' \<or> E' \<turnstile> r \<le>a wa'
wa' < r
w' < r

goal (1 subgoal):
 1. E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'
[PROOF STEP]
by(auto 4 3 del: disjCI intro: disjI1 disjI2 action_order_change_prefix[OF _ sim])
[PROOF STATE]
proof (state)
this:
E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E \<turnstile> wa' \<le>a w' \<or> E \<turnstile> r \<le>a wa'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> r \<leadsto>mrw w'

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
with w'
[PROOF STATE]
proof (chain)
picking this:
w' < r
P,E \<turnstile> r \<leadsto>mrw w'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w' < r
P,E \<turnstile> r \<leadsto>mrw w'

goal (1 subgoal):
 1. \<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i. P,E \<turnstile> r \<leadsto>mrw i \<and> i < r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_seq_consist_mrw_before:
  assumes sc: "ta_seq_consist P Map.empty (lmap snd E)"
  and new_actions_for_fun: "\<And>adal a a'. \<lbrakk> a \<in> new_actions_for P E adal; a' \<in> new_actions_for P E adal \<rbrakk> \<Longrightarrow> a = a'"
  and mrw: "P,E \<turnstile> r \<leadsto>mrw w"
  shows "w < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w < r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w < r
[PROOF STEP]
from mrw
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> r \<leadsto>mrw w
[PROOF STEP]
have "r \<in> read_actions E"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> r \<leadsto>mrw w

goal (1 subgoal):
 1. r \<in> read_actions E
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
r \<in> read_actions E

goal (1 subgoal):
 1. w < r
[PROOF STEP]
with sc new_actions_for_fun
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P Map.empty (lmap snd E)
\<lbrakk>?a \<in> new_actions_for P E ?adal; ?a' \<in> new_actions_for P E ?adal\<rbrakk> \<Longrightarrow> ?a = ?a'
r \<in> read_actions E
[PROOF STEP]
obtain w' where "P,E \<turnstile> r \<leadsto>mrw w'" "w' < r"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P Map.empty (lmap snd E)
\<lbrakk>?a \<in> new_actions_for P E ?adal; ?a' \<in> new_actions_for P E ?adal\<rbrakk> \<Longrightarrow> ?a = ?a'
r \<in> read_actions E

goal (1 subgoal):
 1. (\<And>w'. \<lbrakk>P,E \<turnstile> r \<leadsto>mrw w'; w' < r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest: ta_seq_consist_most_recent_write_for)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> r \<leadsto>mrw w'
w' < r

goal (1 subgoal):
 1. w < r
[PROOF STEP]
with mrw
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> r \<leadsto>mrw w
P,E \<turnstile> r \<leadsto>mrw w'
w' < r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> r \<leadsto>mrw w
P,E \<turnstile> r \<leadsto>mrw w'
w' < r

goal (1 subgoal):
 1. w < r
[PROOF STEP]
by(auto dest: most_recent_write_for_fun)
[PROOF STATE]
proof (state)
this:
w < r

goal:
No subgoals!
[PROOF STEP]
qed