[STATEMENT]
lemma ta_seq_consist_coinduct_append_wf
  [consumes 2, case_names ta_seq_consist, case_conclusion ta_seq_consist LNil lappend]:
  assumes major: "X vs obs a"
  and wf: "wf R"
  and step: "\<And>vs obs a. X vs obs a
    \<Longrightarrow> obs = LNil \<or>
       (\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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''))"
    (is "\<And>vs obs a. _ \<Longrightarrow> _ \<or> ?step vs obs a")
  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]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
fix vs obs a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
assume "X vs obs a"
[PROOF STATE]
proof (state)
this:
X vs obs a

goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf R
X vs obs a
[PROOF STEP]
have "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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or>
                            ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))"
      (is "_ \<or> ?step_concl vs obs")
[PROOF STATE]
proof (prove)
using this:
wf R
X vs obs a

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
proof(induct a arbitrary: vs obs rule: wf_induct[consumes 1, case_names wf])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x vs obs. \<lbrakk>\<forall>y. (y, x) \<in> R \<longrightarrow> (\<forall>x xa. X x xa y \<longrightarrow> xa = LNil \<or> (\<exists>obs' obs''. xa = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P x obs' \<and> (lfinite obs' \<longrightarrow> Ex (X (mrw_values P x (list_of obs')) obs'') \<or> ta_seq_consist P (mrw_values P x (list_of obs')) obs''))); X vs obs x\<rbrakk> \<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> Ex (X (mrw_values P vs (list_of obs')) obs'') \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
case (wf a)
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, a) \<in> R \<longrightarrow> (\<forall>x xa. X x xa y \<longrightarrow> xa = LNil \<or> (\<exists>obs' obs''. xa = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P x obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>a. X (mrw_values P x (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P x (list_of obs')) obs'')))
X vs obs a

goal (1 subgoal):
 1. \<And>x vs obs. \<lbrakk>\<forall>y. (y, x) \<in> R \<longrightarrow> (\<forall>x xa. X x xa y \<longrightarrow> xa = LNil \<or> (\<exists>obs' obs''. xa = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P x obs' \<and> (lfinite obs' \<longrightarrow> Ex (X (mrw_values P x (list_of obs')) obs'') \<or> ta_seq_consist P (mrw_values P x (list_of obs')) obs''))); X vs obs x\<rbrakk> \<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> Ex (X (mrw_values P vs (list_of obs')) obs'') \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
note IH = wf.hyps[rule_format]
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?y, a) \<in> R; X ?x ?xa ?y\<rbrakk> \<Longrightarrow> ?xa = LNil \<or> (\<exists>obs' obs''. ?xa = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P ?x obs' \<and> (lfinite obs' \<longrightarrow> Ex (X (mrw_values P ?x (list_of obs')) obs'') \<or> ta_seq_consist P (mrw_values P ?x (list_of obs')) obs''))

goal (1 subgoal):
 1. \<And>x vs obs. \<lbrakk>\<forall>y. (y, x) \<in> R \<longrightarrow> (\<forall>x xa. X x xa y \<longrightarrow> xa = LNil \<or> (\<exists>obs' obs''. xa = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P x obs' \<and> (lfinite obs' \<longrightarrow> Ex (X (mrw_values P x (list_of obs')) obs'') \<or> ta_seq_consist P (mrw_values P x (list_of obs')) obs''))); X vs obs x\<rbrakk> \<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> Ex (X (mrw_values P vs (list_of obs')) obs'') \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
from step[OF \<open>X vs obs a\<close>]
[PROOF STATE]
proof (chain)
picking this:
obs = LNil \<or> (\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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''))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
obs = LNil \<or> (\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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''))

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. obs = LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. \<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'') \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
assume "obs = LNil"
[PROOF STATE]
proof (state)
this:
obs = LNil

goal (2 subgoals):
 1. obs = LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. \<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'') \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
obs = LNil

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<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'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'') \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'') \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
assume "?step vs obs a"
[PROOF STATE]
proof (state)
this:
\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'')

goal (1 subgoal):
 1. \<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'') \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'')
[PROOF STEP]
obtain obs' obs'' a'
          where obs: "obs = lappend obs' obs''"
          and sc_obs': "ta_seq_consist P vs obs'"
          and decr: "obs' = LNil \<Longrightarrow> (a', a) \<in> R"
          and fin: "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''"
[PROOF STATE]
proof (prove)
using this:
\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'')

goal (1 subgoal):
 1. (\<And>obs' obs'' a'. \<lbrakk>obs = lappend obs' obs''; ta_seq_consist P vs obs'; obs' = LNil \<Longrightarrow> (a', a) \<in> R; 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''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
obs = lappend obs' obs''
ta_seq_consist P vs obs'
obs' = LNil \<Longrightarrow> (a', a) \<in> R
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''

goal (1 subgoal):
 1. \<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> R) \<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'') \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
proof(cases "obs' = LNil")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. obs' = LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. obs' \<noteq> LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
obs' = LNil

goal (2 subgoals):
 1. obs' = LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. obs' \<noteq> LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
hence "lfinite obs'"
[PROOF STATE]
proof (prove)
using this:
obs' = LNil

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

goal (2 subgoals):
 1. obs' = LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. obs' \<noteq> LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
from fin[OF this]
[PROOF STATE]
proof (chain)
picking this:
X (mrw_values P vs (list_of obs')) obs'' a' \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X (mrw_values P vs (list_of obs')) obs'' a' \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs')) obs'' a' \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. ta_seq_consist P (mrw_values P vs (list_of obs')) 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
assume X: "X (mrw_values P vs (list_of obs')) obs'' a'"
[PROOF STATE]
proof (state)
this:
X (mrw_values P vs (list_of obs')) obs'' a'

goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs')) obs'' a' \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. ta_seq_consist P (mrw_values P vs (list_of obs')) 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
obs' = LNil
[PROOF STEP]
have "(a', a) \<in> R"
[PROOF STATE]
proof (prove)
using this:
obs' = LNil

goal (1 subgoal):
 1. (a', a) \<in> R
[PROOF STEP]
by(rule decr)
[PROOF STATE]
proof (state)
this:
(a', a) \<in> R

goal (2 subgoals):
 1. X (mrw_values P vs (list_of obs')) obs'' a' \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. ta_seq_consist P (mrw_values P vs (list_of obs')) 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
from IH[OF this X]
[PROOF STATE]
proof (chain)
picking this:
obs'' = LNil \<or> (\<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
obs'' = LNil \<or> (\<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a))

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. obs'' = LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. \<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
assume "obs'' = LNil"
[PROOF STATE]
proof (state)
this:
obs'' = LNil

goal (2 subgoals):
 1. obs'' = LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. \<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
with True obs
[PROOF STATE]
proof (chain)
picking this:
obs' = LNil
obs = lappend obs' obs''
obs'' = LNil
[PROOF STEP]
have "obs = LNil"
[PROOF STATE]
proof (prove)
using this:
obs' = LNil
obs = lappend obs' obs''
obs'' = LNil

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

goal (2 subgoals):
 1. obs'' = LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
 2. \<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
obs = LNil

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

goal (1 subgoal):
 1. \<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
assume "?step_concl (mrw_values P vs (list_of obs')) obs''"
[PROOF STATE]
proof (state)
this:
\<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> (\<exists>a. X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a)

goal (1 subgoal):
 1. \<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
hence "?step_concl vs obs"
[PROOF STATE]
proof (prove)
using this:
\<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> (\<exists>a. X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a)

goal (1 subgoal):
 1. \<exists>obs' obs''. obs = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'')
[PROOF STEP]
using True obs
[PROOF STATE]
proof (prove)
using this:
\<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> (\<exists>a. X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a)
obs' = LNil
obs = lappend obs' obs''

goal (1 subgoal):
 1. \<exists>obs' obs''. obs = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>obs' obs''. obs = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'')

goal (1 subgoal):
 1. \<exists>obs'a obs''a. obs'' = lappend obs'a obs''a \<and> obs'a \<noteq> LNil \<and> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'a \<and> (lfinite obs'a \<longrightarrow> Ex (X (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<or> ta_seq_consist P (mrw_values P (mrw_values P vs (list_of obs')) (list_of obs'a)) obs''a) \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>obs' obs''. obs = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vs obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs'')

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> 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> 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) 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> 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) 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> 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P (mrw_values P vs (list_of obs')) obs''

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
using obs True
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P (mrw_values P vs (list_of obs')) obs''
obs = lappend obs' obs''
obs' = LNil

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
by cases(auto cong: action.case_cong obs_event.case_cong intro: exI[where x="LCons x LNil" for x])
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

goal (1 subgoal):
 1. obs' \<noteq> LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. obs' \<noteq> LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
obs' \<noteq> LNil

goal (1 subgoal):
 1. obs' \<noteq> LNil \<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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
with obs sc_obs' fin
[PROOF STATE]
proof (chain)
picking this:
obs = lappend obs' obs''
ta_seq_consist P vs obs'
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''
obs' \<noteq> LNil
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
obs = lappend obs' obs''
ta_seq_consist P vs obs'
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''
obs' \<noteq> LNil

goal (1 subgoal):
 1. 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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
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> (\<exists>a. X (mrw_values P vs (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
X ?vsa2 ?obsa2 ?aa2 \<Longrightarrow> ?obsa2 = LNil \<or> (\<exists>obs' obs''. ?obsa2 = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P ?vsa2 obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>a. X (mrw_values P ?vsa2 (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P ?vsa2 (list_of obs')) obs''))

goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
note step' = this
[PROOF STATE]
proof (state)
this:
X ?vsa2 ?obsa2 ?aa2 \<Longrightarrow> ?obsa2 = LNil \<or> (\<exists>obs' obs''. ?obsa2 = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P ?vsa2 obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>a. X (mrw_values P ?vsa2 (list_of obs')) obs'' a) \<or> ta_seq_consist P (mrw_values P ?vsa2 (list_of obs')) obs''))

goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
from major
[PROOF STATE]
proof (chain)
picking this:
X vs obs a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X vs obs a

goal (1 subgoal):
 1. ta_seq_consist P vs obs
[PROOF STEP]
proof(coinduction arbitrary: vs obs a rule: ta_seq_consist_coinduct_append)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>vsa obsa a. X vsa obsa a \<Longrightarrow> obsa = LNil \<or> (\<exists>obs' obs''. obsa = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vsa obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>vs obs a. mrw_values P vsa (list_of obs') = vs \<and> obs'' = obs \<and> X vs obs a) \<or> ta_seq_consist P (mrw_values P vsa (list_of obs')) obs''))
[PROOF STEP]
case (ta_seq_consist vs obs a)
[PROOF STATE]
proof (state)
this:
X vs obs a

goal (1 subgoal):
 1. \<And>vsa obsa a. X vsa obsa a \<Longrightarrow> obsa = LNil \<or> (\<exists>obs' obs''. obsa = lappend obs' obs'' \<and> obs' \<noteq> LNil \<and> ta_seq_consist P vsa obs' \<and> (lfinite obs' \<longrightarrow> (\<exists>vs obs a. mrw_values P vsa (list_of obs') = vs \<and> obs'' = obs \<and> X vs obs a) \<or> ta_seq_consist P (mrw_values P vsa (list_of obs')) obs''))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
X vs obs a

goal (1 subgoal):
 1. 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> (\<exists>vs obs a. mrw_values P vs (list_of obs') = vs \<and> obs'' = obs \<and> X vs obs a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))
[PROOF STEP]
by simp(rule step')
[PROOF STATE]
proof (state)
this:
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> (\<exists>vs obs a. mrw_values P vs (list_of obs') = vs \<and> obs'' = obs \<and> X vs obs a) \<or> ta_seq_consist P (mrw_values P vs (list_of obs')) obs''))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_seq_consist_nthI:
  "(\<And>i ad al v. \<lbrakk> enat i < llength obs; lnth obs i = NormalAction (ReadMem ad al v);
      ta_seq_consist P vs (ltake (enat i) obs) \<rbrakk>
    \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>)
  \<Longrightarrow> ta_seq_consist P vs obs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i ad al v. \<lbrakk>enat i < llength obs; lnth obs i = NormalAction (ReadMem ad al v); ta_seq_consist P vs (ltake (enat i) obs)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>) \<Longrightarrow> ta_seq_consist P vs obs
[PROOF STEP]
proof(coinduction arbitrary: vs obs)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>vs obs. \<forall>i ad al v. enat i < llength obs \<longrightarrow> lnth obs i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vs (ltake (enat i) obs) \<longrightarrow> (\<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>) \<Longrightarrow> (\<exists>vsa. vs = vsa \<and> obs = LNil) \<or> (\<exists>ob vsa obsa. vs = vsa \<and> obs = LCons ob obsa \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vsa (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs obs. mrw_value P vsa ob = vs \<and> obsa = obs \<and> (\<forall>i ad al v. enat i < llength obs \<longrightarrow> lnth obs i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vs (ltake (enat i) obs) \<longrightarrow> (\<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vsa ob) obsa))
[PROOF STEP]
case (ta_seq_consist vs obs)
[PROOF STATE]
proof (state)
this:
\<forall>i ad al v. enat i < llength obs \<longrightarrow> lnth obs i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vs (ltake (enat i) obs) \<longrightarrow> (\<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>)

goal (1 subgoal):
 1. \<And>vs obs. \<forall>i ad al v. enat i < llength obs \<longrightarrow> lnth obs i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vs (ltake (enat i) obs) \<longrightarrow> (\<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>) \<Longrightarrow> (\<exists>vsa. vs = vsa \<and> obs = LNil) \<or> (\<exists>ob vsa obsa. vs = vsa \<and> obs = LCons ob obsa \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vsa (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs obs. mrw_value P vsa ob = vs \<and> obsa = obs \<and> (\<forall>i ad al v. enat i < llength obs \<longrightarrow> lnth obs i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vs (ltake (enat i) obs) \<longrightarrow> (\<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vsa ob) obsa))
[PROOF STEP]
hence nth:
    "\<And>i ad al v. \<lbrakk> enat i < llength obs; lnth obs i = NormalAction (ReadMem ad al v);
                   ta_seq_consist P vs (ltake (enat i) obs) \<rbrakk>
    \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<forall>i ad al v. enat i < llength obs \<longrightarrow> lnth obs i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vs (ltake (enat i) obs) \<longrightarrow> (\<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength obs; lnth obs i = NormalAction (ReadMem ad al v); ta_seq_consist P vs (ltake (enat i) obs)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>enat ?i < llength obs; lnth obs ?i = NormalAction (ReadMem ?ad ?al ?v); ta_seq_consist P vs (ltake (enat ?i) obs)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat ?i) obs)) (?ad, ?al) = \<lfloor>(?v, b)\<rfloor>

goal (1 subgoal):
 1. \<And>vs obs. \<forall>i ad al v. enat i < llength obs \<longrightarrow> lnth obs i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vs (ltake (enat i) obs) \<longrightarrow> (\<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>) \<Longrightarrow> (\<exists>vsa. vs = vsa \<and> obs = LNil) \<or> (\<exists>ob vsa obsa. vs = vsa \<and> obs = LCons ob obsa \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vsa (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs obs. mrw_value P vsa ob = vs \<and> obsa = obs \<and> (\<forall>i ad al v. enat i < llength obs \<longrightarrow> lnth obs i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vs (ltake (enat i) obs) \<longrightarrow> (\<exists>b. mrw_values P vs (list_of (ltake (enat i) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vsa ob) obsa))
[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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<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 = 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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
case 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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
 2. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
case (LCons ob obs')
[PROOF STATE]
proof (state)
this:
obs = LCons ob obs'

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
obs = LCons ob obs'

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
fix ad al v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
assume "ob = NormalAction (ReadMem ad al v)"
[PROOF STATE]
proof (state)
this:
ob = NormalAction (ReadMem ad al v)

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
with nth[of 0 ad al v] LCons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>enat 0 < llength obs; lnth obs 0 = NormalAction (ReadMem ad al v); ta_seq_consist P vs (ltake (enat 0) obs)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat 0) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>
obs = LCons ob obs'
ob = NormalAction (ReadMem ad al v)
[PROOF STEP]
have "\<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>enat 0 < llength obs; lnth obs 0 = NormalAction (ReadMem ad al v); ta_seq_consist P vs (ltake (enat 0) obs)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat 0) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>
obs = LCons ob obs'
ob = NormalAction (ReadMem ad al v)

goal (1 subgoal):
 1. \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
by(simp add: zero_enat_def[symmetric])
[PROOF STATE]
proof (state)
this:
\<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
note base = this
[PROOF STATE]
proof (state)
this:
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
fix i ad al v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
assume "enat i < llength obs'" "lnth obs' i = NormalAction (ReadMem ad al v)"
        and "ta_seq_consist P (mrw_value P vs ob) (ltake (enat i) obs')"
[PROOF STATE]
proof (state)
this:
enat i < llength obs'
lnth obs' i = NormalAction (ReadMem ad al v)
ta_seq_consist P (mrw_value P vs ob) (ltake (enat i) obs')

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
with LCons nth[of "Suc i" ad al v] base
[PROOF STATE]
proof (chain)
picking this:
obs = LCons ob obs'
\<lbrakk>enat (Suc i) < llength obs; lnth obs (Suc i) = NormalAction (ReadMem ad al v); ta_seq_consist P vs (ltake (enat (Suc i)) obs)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat (Suc i)) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>
enat i < llength obs'
lnth obs' i = NormalAction (ReadMem ad al v)
ta_seq_consist P (mrw_value P vs ob) (ltake (enat i) obs')
[PROOF STEP]
have "\<exists>b. mrw_values P (mrw_value P vs ob) (list_of (ltake (enat i) obs')) (ad, al) = \<lfloor>(v, b)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
obs = LCons ob obs'
\<lbrakk>enat (Suc i) < llength obs; lnth obs (Suc i) = NormalAction (ReadMem ad al v); ta_seq_consist P vs (ltake (enat (Suc i)) obs)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P vs (list_of (ltake (enat (Suc i)) obs)) (ad, al) = \<lfloor>(v, b)\<rfloor>
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>
enat i < llength obs'
lnth obs' i = NormalAction (ReadMem ad al v)
ta_seq_consist P (mrw_value P vs ob) (ltake (enat i) obs')

goal (1 subgoal):
 1. \<exists>b. mrw_values P (mrw_value P vs ob) (list_of (ltake (enat i) obs')) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
by(clarsimp simp add: eSuc_enat[symmetric] split: obs_event.split action.split)
[PROOF STATE]
proof (state)
this:
\<exists>b. mrw_values P (mrw_value P vs ob) (list_of (ltake (enat i) obs')) (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>enat ?i2 < llength obs'; lnth obs' ?i2 = NormalAction (ReadMem ?ad2 ?al2 ?v2); ta_seq_consist P (mrw_value P vs ob) (ltake (enat ?i2) obs')\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P (mrw_value P vs ob) (list_of (ltake (enat ?i2) obs')) (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>
\<lbrakk>enat ?i2 < llength obs'; lnth obs' ?i2 = NormalAction (ReadMem ?ad2 ?al2 ?v2); ta_seq_consist P (mrw_value P vs ob) (ltake (enat ?i2) obs')\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P (mrw_value P vs ob) (list_of (ltake (enat ?i2) obs')) (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>
[PROOF STEP]
have ?LCons
[PROOF STATE]
proof (prove)
using this:
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>
\<lbrakk>enat ?i2 < llength obs'; lnth obs' ?i2 = NormalAction (ReadMem ?ad2 ?al2 ?v2); ta_seq_consist P (mrw_value P vs ob) (ltake (enat ?i2) obs')\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P (mrw_value P vs ob) (list_of (ltake (enat ?i2) obs')) (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>

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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
using LCons
[PROOF STATE]
proof (prove)
using this:
ob = NormalAction (ReadMem ?ad2 ?al2 ?v2) \<Longrightarrow> \<exists>b. vs (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>
\<lbrakk>enat ?i2 < llength obs'; lnth obs' ?i2 = NormalAction (ReadMem ?ad2 ?al2 ?v2); ta_seq_consist P (mrw_value P vs ob) (ltake (enat ?i2) obs')\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P (mrw_value P vs ob) (list_of (ltake (enat ?i2) obs')) (?ad2, ?al2) = \<lfloor>(?v2, b)\<rfloor>
obs = LCons ob 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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs)
[PROOF STEP]
by(simp split: action.split obs_event.split)
[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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs)

goal (1 subgoal):
 1. \<And>x21 x22. obs = LCons x21 x22 \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))
[PROOF STEP]
..
[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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<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>vsa obsa. mrw_value P vs ob = vsa \<and> obs = obsa \<and> (\<forall>i ad al v. enat i < llength obsa \<longrightarrow> lnth obsa i = NormalAction (ReadMem ad al v) \<longrightarrow> ta_seq_consist P vsa (ltake (enat i) obsa) \<longrightarrow> (\<exists>b. mrw_values P vsa (list_of (ltake (enat i) obsa)) (ad, al) = \<lfloor>(v, b)\<rfloor>))) \<or> ta_seq_consist P (mrw_value P vs ob) obs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_seq_consist_into_non_speculative:
  "\<lbrakk> ta_seq_consist P vs obs; \<forall>adal. set_option (vs adal) \<subseteq> vs' adal \<times> UNIV \<rbrakk>
  \<Longrightarrow> non_speculative P vs' obs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ta_seq_consist P vs obs; \<forall>adal. set_option (vs adal) \<subseteq> vs' adal \<times> UNIV\<rbrakk> \<Longrightarrow> non_speculative P vs' obs
[PROOF STEP]
proof(coinduction arbitrary: vs' obs vs)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>vs' obs vs. \<lbrakk>ta_seq_consist P vs obs; \<forall>adal. set_option (vs adal) \<subseteq> vs' adal \<times> UNIV\<rbrakk> \<Longrightarrow> (\<exists>vs. vs' = vs \<and> obs = LNil) \<or> (\<exists>ob vs obsa. vs' = vs \<and> obs = LCons ob obsa \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> v \<in> vs (ad, al) | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs' obs vsa. w_value P vs ob = vs' \<and> obsa = obs \<and> ta_seq_consist P vsa obs \<and> (\<forall>adal. set_option (vsa adal) \<subseteq> vs' adal \<times> UNIV)) \<or> non_speculative P (w_value P vs ob) obsa))
[PROOF STEP]
case (non_speculative vs' obs vs)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs obs
\<forall>adal. set_option (vs adal) \<subseteq> vs' adal \<times> UNIV

goal (1 subgoal):
 1. \<And>vs' obs vs. \<lbrakk>ta_seq_consist P vs obs; \<forall>adal. set_option (vs adal) \<subseteq> vs' adal \<times> UNIV\<rbrakk> \<Longrightarrow> (\<exists>vs. vs' = vs \<and> obs = LNil) \<or> (\<exists>ob vs obsa. vs' = vs \<and> obs = LCons ob obsa \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> v \<in> vs (ad, al) | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs' obs vsa. w_value P vs ob = vs' \<and> obsa = obs \<and> ta_seq_consist P vsa obs \<and> (\<forall>adal. set_option (vsa adal) \<subseteq> vs' adal \<times> UNIV)) \<or> non_speculative P (w_value P vs ob) obsa))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs obs
\<forall>adal. set_option (vs adal) \<subseteq> vs' adal \<times> UNIV

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> v \<in> vs (ad, al) | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs' obsa vsa. w_value P vs ob = vs' \<and> obs = obsa \<and> ta_seq_consist P vsa obsa \<and> (\<forall>adal. set_option (vsa adal) \<subseteq> vs' adal \<times> UNIV)) \<or> non_speculative P (w_value P vs ob) obs))
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>adal. set_option (vs adal) \<subseteq> vs' adal \<times> UNIV; obs = LNil\<rbrakk> \<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> v \<in> vs (ad, al) | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs' obsa vsa. w_value P vs ob = vs' \<and> obs = obsa \<and> ta_seq_consist P vsa obsa \<and> (\<forall>adal. set_option (vsa adal) \<subseteq> vs' adal \<times> UNIV)) \<or> non_speculative P (w_value P vs ob) obs))
 2. \<And>ob obs. \<lbrakk>\<forall>adal. set_option (vs adal) \<subseteq> vs' adal \<times> UNIV; obs = LCons ob 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) obs\<rbrakk> \<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> v \<in> vs (ad, al) | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs' obsa vsa. w_value P vs ob = vs' \<and> obs = obsa \<and> ta_seq_consist P vsa obsa \<and> (\<forall>adal. set_option (vsa adal) \<subseteq> vs' adal \<times> UNIV)) \<or> non_speculative P (w_value P vs ob) obs))
[PROOF STEP]
apply(auto split: action.split_asm obs_event.split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>obs x31 x32 x33. \<lbrakk>ta_seq_consist P (vs((x31, x32) \<mapsto> (x33, True))) obs; \<forall>a b. set_option (vs (a, b)) \<subseteq> vs' (a, b) \<times> UNIV; obs = LCons (NormalAction (WriteMem x31 x32 x33)) obs; \<not> non_speculative P (vs'((x31, x32) := insert x33 (vs' (x31, x32)))) obs\<rbrakk> \<Longrightarrow> \<exists>vs. ta_seq_consist P vs obs \<and> (\<forall>a b. (a = x31 \<and> b = x32 \<longrightarrow> set_option (vs (x31, x32)) \<subseteq> insert x33 (vs' (x31, x32)) \<times> UNIV) \<and> ((a = x31 \<longrightarrow> b \<noteq> x32) \<longrightarrow> set_option (vs (a, b)) \<subseteq> vs' (a, b) \<times> UNIV))
 2. \<And>obs x41 x42. \<lbrakk>ta_seq_consist P (\<lambda>(ad', al). if x41 = ad' \<and> al \<in> addr_locs P x42 \<and> (case vs (x41, al) of None \<Rightarrow> True | \<lfloor>(v, xa)\<rfloor> \<Rightarrow> \<not> xa) then \<lfloor>(addr_loc_default P x42 al, False)\<rfloor> else vs (ad', al)) obs; \<forall>a b. set_option (vs (a, b)) \<subseteq> vs' (a, b) \<times> UNIV; obs = LCons (NormalAction (NewHeapElem x41 x42)) obs; \<not> non_speculative P (\<lambda>(ad', al). if x41 = ad' \<and> al \<in> addr_locs P x42 then insert (addr_loc_default P x42 al) (vs' (x41, al)) else vs' (ad', al)) obs\<rbrakk> \<Longrightarrow> \<exists>vs. ta_seq_consist P vs obs \<and> (\<forall>a b. (x41 = a \<and> b \<in> addr_locs P x42 \<longrightarrow> set_option (vs (a, b)) \<subseteq> insert (addr_loc_default P x42 b) (vs' (a, b)) \<times> UNIV) \<and> ((x41 = a \<longrightarrow> b \<notin> addr_locs P x42) \<longrightarrow> set_option (vs (a, b)) \<subseteq> vs' (a, b) \<times> UNIV))
[PROOF STEP]
apply(rule exI, erule conjI, auto)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[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> v \<in> vs (ad, al) | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ((\<exists>vs' obsa vsa. w_value P vs ob = vs' \<and> obs = obsa \<and> ta_seq_consist P vsa obsa \<and> (\<forall>adal. set_option (vsa adal) \<subseteq> vs' adal \<times> UNIV)) \<or> non_speculative P (w_value P vs ob) obs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma llist_of_list_of_append:
  "lfinite xs \<Longrightarrow> llist_of (list_of xs @ ys) = lappend xs (llist_of ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite xs \<Longrightarrow> llist_of (list_of xs @ ys) = lappend xs (llist_of ys)
[PROOF STEP]
unfolding lfinite_eq_range_llist_of
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> range llist_of \<Longrightarrow> llist_of (list_of xs @ ys) = lappend xs (llist_of ys)
[PROOF STEP]
by(clarsimp simp add: lappend_llist_of_llist_of)