[STATEMENT]
lemma memory_write_asi_low_equal: 
assumes a1: "low_equal s1 s2 \<and>
Some t1 = memory_write_asi 10 addr bm data s1 \<and>
Some t2 = memory_write_asi 10 addr bm data s2"
shows "low_equal t1 t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. low_equal t1 t2
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
low_equal s1 s2 \<and> Some t1 = memory_write_asi 10 addr bm data s1 \<and> Some t2 = memory_write_asi 10 addr bm data s2

goal (1 subgoal):
 1. low_equal t1 t2
[PROOF STEP]
apply (simp add: memory_write_asi_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. low_equal s1 s2 \<and> Some t1 = store_word_mem (add_data_cache s1 addr data bm) addr data bm 10 \<and> Some t2 = store_word_mem (add_data_cache s2 addr data bm) addr data bm 10 \<Longrightarrow> low_equal t1 t2
[PROOF STEP]
by (meson add_data_cache_low_equal store_word_mem_low_equal)