[STATEMENT]
lemma mrw_values_no_write_unchanged:
  assumes no_write: "\<And>w. \<lbrakk> w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w \<rbrakk>
  \<Longrightarrow> case vs adal of None \<Rightarrow> False | Some (v, b) \<Rightarrow> b \<and> is_new_action w"
  shows "mrw_values P vs obs adal = vs adal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mrw_values P vs obs adal = vs adal
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?w \<in> set obs; is_write_action ?w; adal \<in> action_loc_aux P ?w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ?w

goal (1 subgoal):
 1. mrw_values P vs obs adal = vs adal
[PROOF STEP]
proof(induct obs arbitrary: vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs. (\<And>w. \<lbrakk>w \<in> set []; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs [] adal = vs adal
 2. \<And>a obs vs. \<lbrakk>\<And>vs. (\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs obs adal = vs adal; \<And>w. \<lbrakk>w \<in> set (a # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w\<rbrakk> \<Longrightarrow> mrw_values P vs (a # obs) adal = vs adal
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w \<in> set []; is_write_action ?w; adal \<in> action_loc_aux P ?w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ?w

goal (2 subgoals):
 1. \<And>vs. (\<And>w. \<lbrakk>w \<in> set []; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs [] adal = vs adal
 2. \<And>a obs vs. \<lbrakk>\<And>vs. (\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs obs adal = vs adal; \<And>w. \<lbrakk>w \<in> set (a # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w\<rbrakk> \<Longrightarrow> mrw_values P vs (a # obs) adal = vs adal
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mrw_values P vs [] adal = vs adal
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mrw_values P vs [] adal = vs adal

goal (1 subgoal):
 1. \<And>a obs vs. \<lbrakk>\<And>vs. (\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs obs adal = vs adal; \<And>w. \<lbrakk>w \<in> set (a # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w\<rbrakk> \<Longrightarrow> mrw_values P vs (a # obs) adal = vs adal
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a obs vs. \<lbrakk>\<And>vs. (\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs obs adal = vs adal; \<And>w. \<lbrakk>w \<in> set (a # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w\<rbrakk> \<Longrightarrow> mrw_values P vs (a # obs) adal = vs adal
[PROOF STEP]
case (Cons ob obs)
[PROOF STATE]
proof (state)
this:
(\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case ?vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P ?vs obs adal = ?vs adal
\<lbrakk>?w \<in> set (ob # obs); is_write_action ?w; adal \<in> action_loc_aux P ?w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ?w

goal (1 subgoal):
 1. \<And>a obs vs. \<lbrakk>\<And>vs. (\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs obs adal = vs adal; \<And>w. \<lbrakk>w \<in> set (a # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w\<rbrakk> \<Longrightarrow> mrw_values P vs (a # obs) adal = vs adal
[PROOF STEP]
from Cons.prems[of ob]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob
[PROOF STEP]
have "mrw_value P vs ob adal = vs adal"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob

goal (1 subgoal):
 1. mrw_value P vs ob adal = vs adal
[PROOF STEP]
apply(cases adal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
[PROOF STEP]
apply(cases ob rule: mrw_value_cases, fastforce+)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>a b ad hT. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (NewHeapElem ad hT)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 2. \<And>a b ad M vs v. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (ExternalCall ad M vs v)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 3. \<And>a b ad al v. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 4. \<And>a b t. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (ThreadStart t)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 5. \<And>a b t. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (ThreadJoin t)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 6. \<And>a b ad. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (SyncLock ad)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 7. \<And>a b ad. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (SyncUnlock ad)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 8. \<And>a b t. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (ObsInterrupt t)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 9. \<And>a b t. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = NormalAction (ObsInterrupted t)\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
 10. \<And>a b. \<lbrakk>\<lbrakk>ob \<in> set (ob # obs); is_write_action ob; adal \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action ob; adal = (a, b); ob = InitialThreadAction\<rbrakk> \<Longrightarrow> mrw_value P vs ob adal = vs adal
A total of 11 subgoals...
[PROOF STEP]
apply(auto simp add: addr_locs_def split: htype.split_asm)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a x1 D F fm T. \<lbrakk>\<exists>T fm. P \<turnstile> x1 has F:T (fm) in D \<Longrightarrow> False; adal = (a, CField D F); ob = NormalAction (NewHeapElem a (Class_type x1)); vs (a, CField D F) = None; P \<turnstile> x1 has F:T (fm) in D\<rbrakk> \<Longrightarrow> False
 2. \<And>a x21 x22 F fm T. \<lbrakk>\<exists>T fm. P \<turnstile> Object has F:T (fm) in Object \<Longrightarrow> False; adal = (a, CField Object F); ob = NormalAction (NewHeapElem a (Array_type x21 x22)); vs (a, CField Object F) = None; P \<turnstile> Object has F:T (fm) in Object\<rbrakk> \<Longrightarrow> False
 3. \<And>a aa ba x1 D F fm T. \<lbrakk>\<not> ba; \<exists>T fm. P \<turnstile> x1 has F:T (fm) in D \<Longrightarrow> False; adal = (a, CField D F); ob = NormalAction (NewHeapElem a (Class_type x1)); vs (a, CField D F) = \<lfloor>(aa, False)\<rfloor>; P \<turnstile> x1 has F:T (fm) in D\<rbrakk> \<Longrightarrow> default_val T = aa
 4. \<And>a aa ba x21 x22 F fm T. \<lbrakk>\<not> ba; \<exists>T fm. P \<turnstile> Object has F:T (fm) in Object \<Longrightarrow> False; adal = (a, CField Object F); ob = NormalAction (NewHeapElem a (Array_type x21 x22)); vs (a, CField Object F) = \<lfloor>(aa, False)\<rfloor>; P \<turnstile> Object has F:T (fm) in Object\<rbrakk> \<Longrightarrow> default_val T = aa
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mrw_value P vs ob adal = vs adal

goal (1 subgoal):
 1. \<And>a obs vs. \<lbrakk>\<And>vs. (\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs obs adal = vs adal; \<And>w. \<lbrakk>w \<in> set (a # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w\<rbrakk> \<Longrightarrow> mrw_values P vs (a # obs) adal = vs adal
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mrw_value P vs ob adal = vs adal

goal (1 subgoal):
 1. \<And>a obs vs. \<lbrakk>\<And>vs. (\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs obs adal = vs adal; \<And>w. \<lbrakk>w \<in> set (a # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w\<rbrakk> \<Longrightarrow> mrw_values P vs (a # obs) adal = vs adal
[PROOF STEP]
have "mrw_values P (mrw_value P vs ob) obs adal = mrw_value P vs ob adal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mrw_values P (mrw_value P vs ob) obs adal = mrw_value P vs ob adal
[PROOF STEP]
proof(rule Cons.hyps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P vs ob adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P vs ob adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
assume "w \<in> set obs" "is_write_action w" "adal \<in> action_loc_aux P w"
[PROOF STATE]
proof (state)
this:
w \<in> set obs
is_write_action w
adal \<in> action_loc_aux P w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P vs ob adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
with Cons.prems[of w] \<open>mrw_value P vs ob adal = vs adal\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>w \<in> set (ob # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
mrw_value P vs ob adal = vs adal
w \<in> set obs
is_write_action w
adal \<in> action_loc_aux P w
[PROOF STEP]
show "case mrw_value P vs ob adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>w \<in> set (ob # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
mrw_value P vs ob adal = vs adal
w \<in> set obs
is_write_action w
adal \<in> action_loc_aux P w

goal (1 subgoal):
 1. case mrw_value P vs ob adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
case mrw_value P vs ob adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mrw_values P (mrw_value P vs ob) obs adal = mrw_value P vs ob adal

goal (1 subgoal):
 1. \<And>a obs vs. \<lbrakk>\<And>vs. (\<And>w. \<lbrakk>w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w) \<Longrightarrow> mrw_values P vs obs adal = vs adal; \<And>w. \<lbrakk>w \<in> set (a # obs); is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case vs adal of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w\<rbrakk> \<Longrightarrow> mrw_values P vs (a # obs) adal = vs adal
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mrw_value P vs ob adal = vs adal
mrw_values P (mrw_value P vs ob) obs adal = mrw_value P vs ob adal
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mrw_value P vs ob adal = vs adal
mrw_values P (mrw_value P vs ob) obs adal = mrw_value P vs ob adal

goal (1 subgoal):
 1. mrw_values P vs (ob # obs) adal = vs adal
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mrw_values P vs (ob # obs) adal = vs adal

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_seq_consist_lappend:
  assumes "lfinite obs"
  shows "ta_seq_consist P vs (lappend obs obs') \<longleftrightarrow>
         ta_seq_consist P vs obs \<and> ta_seq_consist P (mrw_values P vs (list_of obs)) obs'"
  (is "?concl vs obs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P vs (lappend obs obs') = (ta_seq_consist P vs obs \<and> ta_seq_consist P (mrw_values P vs (list_of obs)) obs')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lfinite obs

goal (1 subgoal):
 1. ta_seq_consist P vs (lappend obs obs') = (ta_seq_consist P vs obs \<and> ta_seq_consist P (mrw_values P vs (list_of obs)) obs')
[PROOF STEP]
proof(induct arbitrary: vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs. ta_seq_consist P vs (lappend LNil obs') = (ta_seq_consist P vs LNil \<and> ta_seq_consist P (mrw_values P vs (list_of LNil)) obs')
 2. \<And>xs x vs. \<lbrakk>lfinite xs; \<And>vs. ta_seq_consist P vs (lappend xs obs') = (ta_seq_consist P vs xs \<and> ta_seq_consist P (mrw_values P vs (list_of xs)) obs')\<rbrakk> \<Longrightarrow> ta_seq_consist P vs (lappend (LCons x xs) obs') = (ta_seq_consist P vs (LCons x xs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons x xs))) obs')
[PROOF STEP]
case lfinite_LNil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>vs. ta_seq_consist P vs (lappend LNil obs') = (ta_seq_consist P vs LNil \<and> ta_seq_consist P (mrw_values P vs (list_of LNil)) obs')
 2. \<And>xs x vs. \<lbrakk>lfinite xs; \<And>vs. ta_seq_consist P vs (lappend xs obs') = (ta_seq_consist P vs xs \<and> ta_seq_consist P (mrw_values P vs (list_of xs)) obs')\<rbrakk> \<Longrightarrow> ta_seq_consist P vs (lappend (LCons x xs) obs') = (ta_seq_consist P vs (LCons x xs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons x xs))) obs')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P vs (lappend LNil obs') = (ta_seq_consist P vs LNil \<and> ta_seq_consist P (mrw_values P vs (list_of LNil)) obs')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (lappend LNil obs') = (ta_seq_consist P vs LNil \<and> ta_seq_consist P (mrw_values P vs (list_of LNil)) obs')

goal (1 subgoal):
 1. \<And>xs x vs. \<lbrakk>lfinite xs; \<And>vs. ta_seq_consist P vs (lappend xs obs') = (ta_seq_consist P vs xs \<and> ta_seq_consist P (mrw_values P vs (list_of xs)) obs')\<rbrakk> \<Longrightarrow> ta_seq_consist P vs (lappend (LCons x xs) obs') = (ta_seq_consist P vs (LCons x xs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons x xs))) obs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs x vs. \<lbrakk>lfinite xs; \<And>vs. ta_seq_consist P vs (lappend xs obs') = (ta_seq_consist P vs xs \<and> ta_seq_consist P (mrw_values P vs (list_of xs)) obs')\<rbrakk> \<Longrightarrow> ta_seq_consist P vs (lappend (LCons x xs) obs') = (ta_seq_consist P vs (LCons x xs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons x xs))) obs')
[PROOF STEP]
case (lfinite_LConsI obs ob)
[PROOF STATE]
proof (state)
this:
lfinite obs
ta_seq_consist P ?vs (lappend obs obs') = (ta_seq_consist P ?vs obs \<and> ta_seq_consist P (mrw_values P ?vs (list_of obs)) obs')

goal (1 subgoal):
 1. \<And>xs x vs. \<lbrakk>lfinite xs; \<And>vs. ta_seq_consist P vs (lappend xs obs') = (ta_seq_consist P vs xs \<and> ta_seq_consist P (mrw_values P vs (list_of xs)) obs')\<rbrakk> \<Longrightarrow> ta_seq_consist P vs (lappend (LCons x xs) obs') = (ta_seq_consist P vs (LCons x xs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons x xs))) obs')
[PROOF STEP]
have "?concl (mrw_value P vs ob) obs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P (mrw_value P vs ob) (lappend obs obs') = (ta_seq_consist P (mrw_value P vs ob) obs \<and> ta_seq_consist P (mrw_values P (mrw_value P vs ob) (list_of obs)) obs')
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
ta_seq_consist P (mrw_value P vs ob) (lappend obs obs') = (ta_seq_consist P (mrw_value P vs ob) obs \<and> ta_seq_consist P (mrw_values P (mrw_value P vs ob) (list_of obs)) obs')

goal (1 subgoal):
 1. \<And>xs x vs. \<lbrakk>lfinite xs; \<And>vs. ta_seq_consist P vs (lappend xs obs') = (ta_seq_consist P vs xs \<and> ta_seq_consist P (mrw_values P vs (list_of xs)) obs')\<rbrakk> \<Longrightarrow> ta_seq_consist P vs (lappend (LCons x xs) obs') = (ta_seq_consist P vs (LCons x xs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons x xs))) obs')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P (mrw_value P vs ob) (lappend obs obs') = (ta_seq_consist P (mrw_value P vs ob) obs \<and> ta_seq_consist P (mrw_values P (mrw_value P vs ob) (list_of obs)) obs')

goal (1 subgoal):
 1. ta_seq_consist P vs (lappend (LCons ob obs) obs') = (ta_seq_consist P vs (LCons ob obs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons ob obs))) obs')
[PROOF STEP]
using \<open>lfinite obs\<close>
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P (mrw_value P vs ob) (lappend obs obs') = (ta_seq_consist P (mrw_value P vs ob) obs \<and> ta_seq_consist P (mrw_values P (mrw_value P vs ob) (list_of obs)) obs')
lfinite obs

goal (1 subgoal):
 1. ta_seq_consist P vs (lappend (LCons ob obs) obs') = (ta_seq_consist P vs (LCons ob obs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons ob obs))) obs')
[PROOF STEP]
by(simp split: action.split add: list_of_LCons)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (lappend (LCons ob obs) obs') = (ta_seq_consist P vs (LCons ob obs) \<and> ta_seq_consist P (mrw_values P vs (list_of (LCons ob obs))) obs')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_seq_consist_coinduct_append [consumes 1, case_names ta_seq_consist, case_conclusion ta_seq_consist LNil lappend]:
  assumes major: "X vs obs"
  and step: "\<And>vs obs. X vs obs
    \<Longrightarrow> obs = LNil \<or>
       (\<exists>obs' obs''. obs = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and>
                    (lfinite obs' \<longrightarrow> (X (mrw_values P vs (list_of obs')) obs'' \<or>
                                       ta_seq_consist P (mrw_values P vs (list_of obs')) obs'')))"
    (is "\<And>vs obs. _ \<Longrightarrow> _ \<or> ?step vs obs")
  shows "ta_seq_consist P vs obs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
from major
[PROOF STATE]
proof (chain)
picking this:
X vs obs
[PROOF STEP]
have "\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P vs (llist_of obs') \<and>
                     X (mrw_values P vs obs') obs''"
[PROOF STATE]
proof (prove)
using this:
X vs obs

goal (1 subgoal):
 1. \<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P vs (llist_of obs') \<and> X (mrw_values P vs obs') obs''
[PROOF STEP]
by(auto intro: exI[where x="[]"])
[PROOF STATE]
proof (state)
this:
\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P vs (llist_of obs') \<and> X (mrw_values P vs obs') obs''

goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P vs (llist_of obs') \<and> X (mrw_values P vs obs') obs''

goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
proof(coinduct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. \<exists>obs' obs''. x2 = lappend (llist_of obs') obs'' \<and> ta_seq_consist P x1 (llist_of obs') \<and> X (mrw_values P x1 obs') obs'' \<Longrightarrow> (\<exists>vs. x1 = vs \<and> x2 = LNil) \<or> (\<exists>ob vs obs. x1 = vs \<and> x2 = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
case (ta_seq_consist vs obs)
[PROOF STATE]
proof (state)
this:
\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P vs (llist_of obs') \<and> X (mrw_values P vs obs') obs''

goal (1 subgoal):
 1. \<And>x1 x2. \<exists>obs' obs''. x2 = lappend (llist_of obs') obs'' \<and> ta_seq_consist P x1 (llist_of obs') \<and> X (mrw_values P x1 obs') obs'' \<Longrightarrow> (\<exists>vs. x1 = vs \<and> x2 = LNil) \<or> (\<exists>ob vs obs. x1 = vs \<and> x2 = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P vs (llist_of obs') \<and> X (mrw_values P vs obs') obs''
[PROOF STEP]
obtain obs' obs''
      where obs: "obs = lappend (llist_of obs') obs''"
      and sc_obs': "ta_seq_consist P vs (llist_of obs')"
      and X: "X (mrw_values P vs obs') obs''"
[PROOF STATE]
proof (prove)
using this:
\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P vs (llist_of obs') \<and> X (mrw_values P vs obs') obs''

goal (1 subgoal):
 1. (\<And>obs' obs''. \<lbrakk>obs = lappend (llist_of obs') obs''; ta_seq_consist P vs (llist_of obs'); X (mrw_values P vs obs') obs''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
obs = lappend (llist_of obs') obs''
ta_seq_consist P vs (llist_of obs')
X (mrw_values P vs obs') obs''

goal (1 subgoal):
 1. \<And>x1 x2. \<exists>obs' obs''. x2 = lappend (llist_of obs') obs'' \<and> ta_seq_consist P x1 (llist_of obs') \<and> X (mrw_values P x1 obs') obs'' \<Longrightarrow> (\<exists>vs. x1 = vs \<and> x2 = LNil) \<or> (\<exists>ob vs obs. x1 = vs \<and> x2 = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
proof(cases obs')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. obs' = [] \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
obs' = []

goal (2 subgoals):
 1. obs' = [] \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
with X
[PROOF STATE]
proof (chain)
picking this:
X (mrw_values P vs obs') obs''
obs' = []
[PROOF STEP]
have "X vs obs''"
[PROOF STATE]
proof (prove)
using this:
X (mrw_values P vs obs') obs''
obs' = []

goal (1 subgoal):
 1. X vs obs''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X vs obs''

goal (2 subgoals):
 1. obs' = [] \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
from step[OF this]
[PROOF STATE]
proof (chain)
picking this:
obs'' = LNil \<or> (\<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
obs'' = LNil \<or> (\<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a))

goal (1 subgoal):
 1. (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. obs'' = LNil \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
assume "obs'' = LNil"
[PROOF STATE]
proof (state)
this:
obs'' = LNil

goal (2 subgoals):
 1. obs'' = LNil \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
with Nil obs
[PROOF STATE]
proof (chain)
picking this:
obs' = []
obs = lappend (llist_of obs') obs''
obs'' = LNil
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
obs' = []
obs = lappend (llist_of obs') obs''
obs'' = LNil

goal (1 subgoal):
 1. (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal (1 subgoal):
 1. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
assume "?step vs obs''"
[PROOF STATE]
proof (state)
this:
\<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a)

goal (1 subgoal):
 1. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a)
[PROOF STEP]
obtain obs''' obs''''
          where obs'': "obs'' = lappend obs''' obs''''" and "obs''' \<noteq> LNil"
          and sc_obs''': "ta_seq_consist P vs obs'''"
          and fin: "lfinite obs''' \<Longrightarrow> X (mrw_values P vs (list_of obs''')) obs'''' \<or>
                                      ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''"
[PROOF STATE]
proof (prove)
using this:
\<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a)

goal (1 subgoal):
 1. (\<And>obs''' obs''''. \<lbrakk>obs'' = lappend obs''' obs''''; obs''' \<noteq> LNil; ta_seq_consist P vs obs'''; lfinite obs''' \<Longrightarrow> X (mrw_values P vs (list_of obs''')) obs'''' \<or> ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
obs'' = lappend obs''' obs''''
obs''' \<noteq> LNil
ta_seq_consist P vs obs'''
lfinite obs''' \<Longrightarrow> X (mrw_values P vs (list_of obs''')) obs'''' \<or> ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''

goal (1 subgoal):
 1. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
from \<open>obs''' \<noteq> LNil\<close>
[PROOF STATE]
proof (chain)
picking this:
obs''' \<noteq> LNil
[PROOF STEP]
obtain ob obs''''' where obs''': "obs''' = LCons ob obs'''''"
[PROOF STATE]
proof (prove)
using this:
obs''' \<noteq> LNil

goal (1 subgoal):
 1. (\<And>ob obs'''''. obs''' = LCons ob obs''''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding neq_LNil_conv
[PROOF STATE]
proof (prove)
using this:
\<exists>x xs'. obs''' = LCons x xs'

goal (1 subgoal):
 1. (\<And>ob obs'''''. obs''' = LCons ob obs''''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
obs''' = LCons ob obs'''''

goal (1 subgoal):
 1. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
with Nil obs'' obs
[PROOF STATE]
proof (chain)
picking this:
obs' = []
obs'' = lappend obs''' obs''''
obs = lappend (llist_of obs') obs''
obs''' = LCons ob obs'''''
[PROOF STEP]
have concl1: "obs = LCons ob (lappend obs''''' obs'''')"
[PROOF STATE]
proof (prove)
using this:
obs' = []
obs'' = lappend obs''' obs''''
obs = lappend (llist_of obs') obs''
obs''' = LCons ob obs'''''

goal (1 subgoal):
 1. obs = LCons ob (lappend obs''''' obs'''')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
obs = LCons ob (lappend obs''''' obs'''')

goal (1 subgoal):
 1. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
have concl2: "case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | _ \<Rightarrow> True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
[PROOF STEP]
using sc_obs''' obs'''
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs obs'''
obs''' = LCons ob obs'''''

goal (1 subgoal):
 1. case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True

goal (1 subgoal):
 1. \<exists>obs' obs''a. obs'' = lappend obs' obs''a \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> X (mrw_values P vs (list_of obs')) obs''a \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''a) \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
proof(cases "lfinite obs'''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<not> lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> lfinite obs'''

goal (2 subgoals):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<not> lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
hence "lappend obs''''' obs'''' = obs'''''"
[PROOF STATE]
proof (prove)
using this:
\<not> lfinite obs'''

goal (1 subgoal):
 1. lappend obs''''' obs'''' = obs'''''
[PROOF STEP]
using obs'''
[PROOF STATE]
proof (prove)
using this:
\<not> lfinite obs'''
obs''' = LCons ob obs'''''

goal (1 subgoal):
 1. lappend obs''''' obs'''' = obs'''''
[PROOF STEP]
by(simp add: lappend_inf)
[PROOF STATE]
proof (state)
this:
lappend obs''''' obs'''' = obs'''''

goal (2 subgoals):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<not> lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
hence "ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')"
[PROOF STATE]
proof (prove)
using this:
lappend obs''''' obs'''' = obs'''''

goal (1 subgoal):
 1. ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')
[PROOF STEP]
using sc_obs''' obs'''
[PROOF STATE]
proof (prove)
using this:
lappend obs''''' obs'''' = obs'''''
ta_seq_consist P vs obs'''
obs''' = LCons ob obs'''''

goal (1 subgoal):
 1. ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')

goal (2 subgoals):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<not> lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
with concl1 concl2
[PROOF STATE]
proof (chain)
picking this:
obs = LCons ob (lappend obs''''' obs'''')
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')
[PROOF STEP]
have ?LCons
[PROOF STATE]
proof (prove)
using this:
obs = LCons ob (lappend obs''''' obs'''')
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')

goal (1 subgoal):
 1. \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)

goal (2 subgoals):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<not> lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)

goal (1 subgoal):
 1. (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal (1 subgoal):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
lfinite obs'''

goal (1 subgoal):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
with obs'''
[PROOF STATE]
proof (chain)
picking this:
obs''' = LCons ob obs'''''
lfinite obs'''
[PROOF STEP]
obtain obs'''''' where obs''''': "obs''''' = llist_of obs''''''"
[PROOF STATE]
proof (prove)
using this:
obs''' = LCons ob obs'''''
lfinite obs'''

goal (1 subgoal):
 1. (\<And>obs''''''. obs''''' = llist_of obs'''''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp(auto simp add: lfinite_eq_range_llist_of)
[PROOF STATE]
proof (state)
this:
obs''''' = llist_of obs''''''

goal (1 subgoal):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
from fin[OF True]
[PROOF STATE]
proof (chain)
picking this:
X (mrw_values P vs (list_of obs''')) obs'''' \<or> ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''
[PROOF STEP]
have "?LCons"
[PROOF STATE]
proof (prove)
using this:
X (mrw_values P vs (list_of obs''')) obs'''' \<or> ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''

goal (1 subgoal):
 1. \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
 2. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
assume X: "X (mrw_values P vs (list_of obs''')) obs''''"
[PROOF STATE]
proof (state)
this:
X (mrw_values P vs (list_of obs''')) obs''''

goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
 2. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
hence "X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''"
[PROOF STATE]
proof (prove)
using this:
X (mrw_values P vs (list_of obs''')) obs''''

goal (1 subgoal):
 1. X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''
[PROOF STEP]
using obs''''' obs'''
[PROOF STATE]
proof (prove)
using this:
X (mrw_values P vs (list_of obs''')) obs''''
obs''''' = llist_of obs''''''
obs''' = LCons ob obs'''''

goal (1 subgoal):
 1. X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''

goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
 2. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''

goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
 2. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
from obs'''''
[PROOF STATE]
proof (chain)
picking this:
obs''''' = llist_of obs''''''
[PROOF STEP]
have "lappend obs''''' obs'''' = lappend (llist_of obs'''''') obs''''"
[PROOF STATE]
proof (prove)
using this:
obs''''' = llist_of obs''''''

goal (1 subgoal):
 1. lappend obs''''' obs'''' = lappend (llist_of obs'''''') obs''''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lappend obs''''' obs'''' = lappend (llist_of obs'''''') obs''''

goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
 2. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lappend obs''''' obs'''' = lappend (llist_of obs'''''') obs''''

goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
 2. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
have "ta_seq_consist P (mrw_value P vs ob) (llist_of obs'''''')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P (mrw_value P vs ob) (llist_of obs'''''')
[PROOF STEP]
using sc_obs''' obs''' obs'''''
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs obs'''
obs''' = LCons ob obs'''''
obs''''' = llist_of obs''''''

goal (1 subgoal):
 1. ta_seq_consist P (mrw_value P vs ob) (llist_of obs'''''')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ta_seq_consist P (mrw_value P vs ob) (llist_of obs'''''')

goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
 2. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''
lappend obs''''' obs'''' = lappend (llist_of obs'''''') obs''''
ta_seq_consist P (mrw_value P vs ob) (llist_of obs'''''')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''
lappend obs''''' obs'''' = lappend (llist_of obs'''''') obs''''
ta_seq_consist P (mrw_value P vs ob) (llist_of obs'''''')

goal (1 subgoal):
 1. \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
using concl1 concl2
[PROOF STATE]
proof (prove)
using this:
X (mrw_values P (mrw_value P vs ob) obs'''''') obs''''
lappend obs''''' obs'''' = lappend (llist_of obs'''''') obs''''
ta_seq_consist P (mrw_value P vs ob) (llist_of obs'''''')
obs = LCons ob (lappend obs''''' obs'''')
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True

goal (1 subgoal):
 1. \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)

goal (1 subgoal):
 1. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
assume "ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''"
[PROOF STATE]
proof (state)
this:
ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''

goal (1 subgoal):
 1. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
with sc_obs''' obs''''' obs'''
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P vs obs'''
obs''''' = llist_of obs''''''
obs''' = LCons ob obs'''''
ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''
[PROOF STEP]
have "ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs obs'''
obs''''' = llist_of obs''''''
obs''' = LCons ob obs'''''
ta_seq_consist P (mrw_values P vs (list_of obs''')) obs''''

goal (1 subgoal):
 1. ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')
[PROOF STEP]
by(simp add: ta_seq_consist_lappend)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')

goal (1 subgoal):
 1. ta_seq_consist P (mrw_values P vs (list_of obs''')) obs'''' \<Longrightarrow> \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
with concl1 concl2
[PROOF STATE]
proof (chain)
picking this:
obs = LCons ob (lappend obs''''' obs'''')
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
obs = LCons ob (lappend obs''''' obs'''')
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
ta_seq_consist P (mrw_value P vs ob) (lappend obs''''' obs'''')

goal (1 subgoal):
 1. \<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)

goal (1 subgoal):
 1. lfinite obs''' \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs)

goal (1 subgoal):
 1. (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal (1 subgoal):
 1. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
case (Cons ob obs''')
[PROOF STATE]
proof (state)
this:
obs' = ob # obs'''

goal (1 subgoal):
 1. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
hence "obs = LCons ob (lappend (llist_of obs''') obs'')"
[PROOF STATE]
proof (prove)
using this:
obs' = ob # obs'''

goal (1 subgoal):
 1. obs = LCons ob (lappend (llist_of obs''') obs'')
[PROOF STEP]
using obs
[PROOF STATE]
proof (prove)
using this:
obs' = ob # obs'''
obs = lappend (llist_of obs') obs''

goal (1 subgoal):
 1. obs = LCons ob (lappend (llist_of obs''') obs'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
obs = LCons ob (lappend (llist_of obs''') obs'')

goal (1 subgoal):
 1. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
obs = LCons ob (lappend (llist_of obs''') obs'')

goal (1 subgoal):
 1. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
from sc_obs' Cons
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P vs (llist_of obs')
obs' = ob # obs'''
[PROOF STEP]
have "case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | _ \<Rightarrow> True"
        and "ta_seq_consist P (mrw_value P vs ob) (llist_of obs''')"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs (llist_of obs')
obs' = ob # obs'''

goal (1 subgoal):
 1. case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True &&& ta_seq_consist P (mrw_value P vs ob) (llist_of obs''')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
ta_seq_consist P (mrw_value P vs ob) (llist_of obs''')

goal (1 subgoal):
 1. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
ta_seq_consist P (mrw_value P vs ob) (llist_of obs''')

goal (1 subgoal):
 1. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
from X Cons
[PROOF STATE]
proof (chain)
picking this:
X (mrw_values P vs obs') obs''
obs' = ob # obs'''
[PROOF STEP]
have "X (mrw_values P (mrw_value P vs ob) obs''') obs''"
[PROOF STATE]
proof (prove)
using this:
X (mrw_values P vs obs') obs''
obs' = ob # obs'''

goal (1 subgoal):
 1. X (mrw_values P (mrw_value P vs ob) obs''') obs''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X (mrw_values P (mrw_value P vs ob) obs''') obs''

goal (1 subgoal):
 1. \<And>a list. obs' = a # list \<Longrightarrow> (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
obs = LCons ob (lappend (llist_of obs''') obs'')
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
ta_seq_consist P (mrw_value P vs ob) (llist_of obs''')
X (mrw_values P (mrw_value P vs ob) obs''') obs''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
obs = LCons ob (lappend (llist_of obs''') obs'')
case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True
ta_seq_consist P (mrw_value P vs ob) (llist_of obs''')
X (mrw_values P (mrw_value P vs ob) obs''') obs''

goal (1 subgoal):
 1. (\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>vs. vs = vs \<and> obs = LNil) \<or> (\<exists>ob vs obs. vs = vs \<and> obs = LCons ob obs \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>obs' obs''. obs = lappend (llist_of obs') obs'' \<and> ta_seq_consist P (mrw_value P vs ob) (llist_of obs') \<and> X (mrw_values P (mrw_value P vs ob) obs') obs'') \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs obs

goal:
No subgoals!
[PROOF STEP]
qed