[STATEMENT]
lemma complete_sc_ta_seq_consist:
  assumes cau: "sc_completion s vs"
  and ta_seq_consist_convert_RA: "\<And>vs ln. ta_seq_consist P vs (llist_of (convert_RA ln))"
  shows "ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
define vs' where "vs' = vs"
[PROOF STATE]
proof (state)
this:
vs' = vs

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
let ?obs = "\<lambda>ttas. lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
define obs where "obs = ?obs (complete_sc s vs)"
[PROOF STATE]
proof (state)
this:
obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs))

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
define a where "a = complete_sc s vs'"
[PROOF STATE]
proof (state)
this:
a = complete_sc s vs'

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
let ?ttas' = "\<lambda>ttas' :: ('thread_id \<times> ('l,'thread_id,'x,'m,'w,('addr, 'thread_id) obs_event action) thread_action) list.
               concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
let ?vs = "\<lambda>ttas'. mrw_values P vs (?ttas' ttas')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
from vs'_def obs_def
[PROOF STATE]
proof (chain)
picking this:
vs' = vs
obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs))
[PROOF STEP]
have "s -\<triangleright>[]\<rightarrow>* s" "ta_seq_consist P vs (llist_of (?ttas' []))" "vs' = ?vs []"
[PROOF STATE]
proof (prove)
using this:
vs' = vs
obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs))

goal (1 subgoal):
 1. s -\<triangleright>[]\<rightarrow>* s &&& ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) []))) &&& vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) []))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
s -\<triangleright>[]\<rightarrow>* s
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) [])))
vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) []))

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
hence "\<exists>s' ttas'. obs = ?obs (complete_sc s' vs') \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and>
                    ta_seq_consist P vs (llist_of (?ttas' ttas')) \<and> vs' = ?vs ttas' \<and>
                    a = complete_sc s' vs'"
[PROOF STATE]
proof (prove)
using this:
s -\<triangleright>[]\<rightarrow>* s
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) [])))
vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) []))

goal (1 subgoal):
 1. \<exists>s' ttas'. obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs')) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vs'
[PROOF STEP]
unfolding obs_def vs'_def a_def
[PROOF STATE]
proof (prove)
using this:
s -\<triangleright>[]\<rightarrow>* s
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) [])))
vs = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) []))

goal (1 subgoal):
 1. \<exists>s' ttas'. lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)) = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs)) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> complete_sc s vs = complete_sc s' vs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>s' ttas'. obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs')) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vs'

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>s' ttas'. obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs')) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vs'

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
have "wf (inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = [])))"
    (is "wf ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = [])))
[PROOF STEP]
by(rule wf_inv_image)(rule wellorder_class.wf)
[PROOF STATE]
proof (state)
this:
wf (inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = [])))

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' ttas'. obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs')) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vs'
wf (inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = [])))
[PROOF STEP]
show "ta_seq_consist P vs' obs"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' ttas'. obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs')) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vs'
wf (inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = [])))

goal (1 subgoal):
 1. ta_seq_consist P vs' obs
[PROOF STEP]
proof(coinduct vs' obs a rule: ta_seq_consist_coinduct_append_wf)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>vsa obs a. \<exists>s' ttas'. obs = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vsa)) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vsa = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vsa \<Longrightarrow> obs = LNil \<or> (\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vsa obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vsa (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vsa (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vsa (list_of obs'))) \<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:
\<exists>s' ttas'. obs = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs')) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs' = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vs'

goal (1 subgoal):
 1. \<And>vsa obs a. \<exists>s' ttas'. obs = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vsa)) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vsa = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vsa \<Longrightarrow> obs = LNil \<or> (\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vsa obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vsa (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vsa (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vsa (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vsa (list_of obs')) obs''))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' ttas'. obs = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs')) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs' = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vs'
[PROOF STEP]
obtain s' ttas' where obs_def: "obs = ?obs (complete_sc s' (?vs ttas'))"
      and Red: "s -\<triangleright>ttas'\<rightarrow>* s'"
      and sc: "ta_seq_consist P vs (llist_of (?ttas' ttas'))"
      and vs'_def: "vs' = ?vs ttas'"
      and a_def: "a = complete_sc s' vs'"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' ttas'. obs = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vs')) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vs' = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vs'

goal (1 subgoal):
 1. (\<And>s' ttas'. \<lbrakk>obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))))); s -\<triangleright>ttas'\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))); vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')); a = complete_sc s' vs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))
s -\<triangleright>ttas'\<rightarrow>* s'
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))
vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))
a = complete_sc s' vs'

goal (1 subgoal):
 1. \<And>vsa obs a. \<exists>s' ttas'. obs = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' vsa)) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> vsa = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a = complete_sc s' vsa \<Longrightarrow> obs = LNil \<or> (\<exists>obs' obs'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vsa obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vsa (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vsa (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vsa (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vsa (list_of obs')) obs''))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
proof(cases "\<exists>t' ta' s''. s' -t'\<triangleright>ta'\<rightarrow> s''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
 2. \<nexists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>t' ta'. Ex (redT_syntax1 s' t' ta')

goal (2 subgoals):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
 2. \<nexists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
hence "obs = LNil"
[PROOF STATE]
proof (prove)
using this:
\<nexists>t' ta'. Ex (redT_syntax1 s' t' ta')

goal (1 subgoal):
 1. obs = LNil
[PROOF STEP]
unfolding obs_def complete_sc_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>t' ta'. Ex (redT_syntax1 s' t' ta')

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (unfold_llist (\<lambda>(s, vs). \<forall>t ta s'. \<not> s -t\<triangleright>ta\<rightarrow> s') (\<lambda>(s, vs). fst (SOME ((t, ta), s'). s -t\<triangleright>ta\<rightarrow> s' \<and> ta_seq_consist P vs (llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>))) (\<lambda>(s, vs). let ((t, ta), s') = SOME ((t, ta), s'). s -t\<triangleright>ta\<rightarrow> s' \<and> ta_seq_consist P vs (llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) in (s', mrw_values P vs \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (s', mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))))) = LNil
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
obs = LNil

goal (2 subgoals):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
 2. \<nexists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
hence ?LNil
[PROOF STATE]
proof (prove)
using this:
obs = LNil

goal (1 subgoal):
 1. obs = LNil
[PROOF STEP]
unfolding obs_def
[PROOF STATE]
proof (prove)
using this:
lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))))) = LNil

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))))) = LNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
obs = LNil

goal (2 subgoals):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
 2. \<nexists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))

goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>t' ta'. Ex (redT_syntax1 s' t' ta')

goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
let ?proceed = "\<lambda>((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (?vs ttas') (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
let ?tta = "fst (Eps ?proceed)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
let ?s' = "snd (Eps ?proceed)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
\<exists>t' ta'. Ex (redT_syntax1 s' t' ta')
[PROOF STEP]
obtain t' ta' s'' where red: "s' -t'\<triangleright>ta'\<rightarrow> s''"
[PROOF STATE]
proof (prove)
using this:
\<exists>t' ta'. Ex (redT_syntax1 s' t' ta')

goal (1 subgoal):
 1. (\<And>t' ta' s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s' -t'\<triangleright>ta'\<rightarrow> s''

goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s' -t'\<triangleright>ta'\<rightarrow> s''
[PROOF STEP]
obtain ta'' s''' where "s' -t'\<triangleright>ta''\<rightarrow> s'''"
        and "ta_seq_consist P (?vs ttas') (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
s' -t'\<triangleright>ta'\<rightarrow> s''

goal (1 subgoal):
 1. (\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>; thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t' ta'; redT_upd s' t' ta' x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (redT_normal x x' m')
[PROOF STATE]
proof (state)
this:
t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>
thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>
actions_ok s' t' ta'
redT_upd s' t' ta' x' m' s''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>; thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t' ta'; redT_upd s' t' ta' x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note red = \<open>t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>\<close>
          and ts''t' = \<open>thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>\<close>
          and aok = \<open>actions_ok s' t' ta'\<close>
          and s''' = \<open>redT_upd s' t' ta' x' m' s''\<close>
[PROOF STATE]
proof (state)
this:
t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>
thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>
actions_ok s' t' ta'
redT_upd s' t' ta' x' m' s''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>; thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t' ta'; redT_upd s' t' ta' x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from sc_completionD[OF cau Red sc ts''t' red aok]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ta' x'' m''. t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t' ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
obtain ta'' x'' m'' where red': "t' \<turnstile> \<langle>x, shr s'\<rangle> -ta''\<rightarrow> \<langle>x'', m''\<rangle>"
          and aok': "actions_ok s' t' ta''"
          and sc': "ta_seq_consist P (?vs ttas') (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>ta' x'' m''. t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t' ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)

goal (1 subgoal):
 1. (\<And>ta'' x'' m''. \<lbrakk>t' \<turnstile> \<langle>x, shr s'\<rangle> -ta''\<rightarrow> \<langle>x'', m''\<rangle>; actions_ok s' t' ta''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t' \<turnstile> \<langle>x, shr s'\<rangle> -ta''\<rightarrow> \<langle>x'', m''\<rangle>
actions_ok s' t' ta''
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>; thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t' ta'; redT_upd s' t' ta' x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from redT_updWs_total
[PROOF STATE]
proof (chain)
picking this:
\<exists>ws'. redT_updWs ?t ?ws ?was ws'
[PROOF STEP]
obtain ws' where "redT_updWs t' (wset s') \<lbrace>ta''\<rbrace>\<^bsub>w\<^esub> ws'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ws'. redT_updWs ?t ?ws ?was ws'

goal (1 subgoal):
 1. (\<And>ws'. redT_updWs t' (wset s') \<lbrace>ta''\<rbrace>\<^bsub>w\<^esub> ws' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
redT_updWs t' (wset s') \<lbrace>ta''\<rbrace>\<^bsub>w\<^esub> ws'

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>; thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t' ta'; redT_upd s' t' ta' x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
redT_updWs t' (wset s') \<lbrace>ta''\<rbrace>\<^bsub>w\<^esub> ws'
[PROOF STEP]
obtain s''' where "redT_upd s' t' ta'' x'' m'' s'''"
[PROOF STATE]
proof (prove)
using this:
redT_updWs t' (wset s') \<lbrace>ta''\<rbrace>\<^bsub>w\<^esub> ws'

goal (1 subgoal):
 1. (\<And>s'''. redT_upd s' t' ta'' x'' m'' s''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
redT_upd s' t' ta'' x'' m'' s'''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>; thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t' ta'; redT_upd s' t' ta' x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with red' ts''t' aok'
[PROOF STATE]
proof (chain)
picking this:
t' \<turnstile> \<langle>x, shr s'\<rangle> -ta''\<rightarrow> \<langle>x'', m''\<rangle>
thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>
actions_ok s' t' ta''
redT_upd s' t' ta'' x'' m'' s'''
[PROOF STEP]
have "s' -t'\<triangleright>ta''\<rightarrow> s'''"
[PROOF STATE]
proof (prove)
using this:
t' \<turnstile> \<langle>x, shr s'\<rangle> -ta''\<rightarrow> \<langle>x'', m''\<rangle>
thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>
actions_ok s' t' ta''
redT_upd s' t' ta'' x'' m'' s'''

goal (1 subgoal):
 1. s' -t'\<triangleright>ta''\<rightarrow> s'''
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s' -t'\<triangleright>ta''\<rightarrow> s'''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; t' \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x', m'\<rangle>; thr s' t' = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t' ta'; redT_upd s' t' ta' x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
s' -t'\<triangleright>ta''\<rightarrow> s'''

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using sc'
[PROOF STATE]
proof (prove)
using this:
s' -t'\<triangleright>ta''\<rightarrow> s'''
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(rule that)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case redT_acquire
[PROOF STATE]
proof (state)
this:
ta' = (K$ [], [], [], [], [], convert_RA ln_)
thr s' t' = \<lfloor>(x_, ln_)\<rfloor>
\<not> waiting (wset s' t')
may_acquire_all (locks s') t' ln_
0 < ln_ $ n_
s'' = (acquire_all (locks s') t' ln_, (thr s'(t' \<mapsto> (x_, no_wait_locks)), shr s'), wset s', interrupts s')

goal (1 subgoal):
 1. \<And>x n ln. \<lbrakk>\<And>ta'' s'''. \<lbrakk>s' -t'\<triangleright>ta''\<rightarrow> s'''; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)\<rbrakk> \<Longrightarrow> thesis; ta' = (K$ [], [], [], [], [], convert_RA ln); thr s' t' = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t'); may_acquire_all (locks s') t' ln; 0 < ln $ n; s'' = (acquire_all (locks s') t' ln, (thr s'(t' \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
ta' = (K$ [], [], [], [], [], convert_RA ln_)
thr s' t' = \<lfloor>(x_, ln_)\<rfloor>
\<not> waiting (wset s' t')
may_acquire_all (locks s') t' ln_
0 < ln_ $ n_
s'' = (acquire_all (locks s') t' ln_, (thr s'(t' \<mapsto> (x_, no_wait_locks)), shr s'), wset s', interrupts s')

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(simp add: that[OF red] ta_seq_consist_convert_RA)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s' -t'\<triangleright>ta''\<rightarrow> s'''
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)

goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
hence "?proceed ((t', ta''), s''')"
[PROOF STATE]
proof (prove)
using this:
s' -t'\<triangleright>ta''\<rightarrow> s'''
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)

goal (1 subgoal):
 1. case ((t', ta''), s''') of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
case ((t', ta''), s''') of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa

goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
hence "?proceed (Eps ?proceed)"
[PROOF STATE]
proof (prove)
using this:
case ((t', ta''), s''') of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa

goal (1 subgoal):
 1. case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
[PROOF STEP]
by(rule someI)
[PROOF STATE]
proof (state)
this:
case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa

goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
 2. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
 2. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
\<exists>t' ta'. Ex (redT_syntax1 s' t' ta')
[PROOF STEP]
have csc_unfold: "complete_sc s' (?vs ttas') = LCons ?tta (complete_sc ?s' (?vs (ttas' @ [?tta])))"
[PROOF STATE]
proof (prove)
using this:
\<exists>t' ta'. Ex (redT_syntax1 s' t' ta')

goal (1 subgoal):
 1. complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))
[PROOF STEP]
unfolding complete_sc_def
[PROOF STATE]
proof (prove)
using this:
\<exists>t' ta'. Ex (redT_syntax1 s' t' ta')

goal (1 subgoal):
 1. unfold_llist (\<lambda>(s, vs). \<forall>t ta s'. \<not> s -t\<triangleright>ta\<rightarrow> s') (\<lambda>(s, vs). fst (SOME ((t, ta), s'). s -t\<triangleright>ta\<rightarrow> s' \<and> ta_seq_consist P vs (llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>))) (\<lambda>(s, vs). let ((t, ta), s') = SOME ((t, ta), s'). s -t\<triangleright>ta\<rightarrow> s' \<and> ta_seq_consist P vs (llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) in (s', mrw_values P vs \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (s', mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (unfold_llist (\<lambda>(s, vs). \<forall>t ta s'. \<not> s -t\<triangleright>ta\<rightarrow> s') (\<lambda>(s, vs). fst (SOME ((t, ta), s'). s -t\<triangleright>ta\<rightarrow> s' \<and> ta_seq_consist P vs (llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>))) (\<lambda>(s, vs). let ((t, ta), s') = SOME ((t, ta), s'). s -t\<triangleright>ta\<rightarrow> s' \<and> ta_seq_consist P vs (llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) in (s', mrw_values P vs \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)), mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
hence "obs = lappend (llist_of \<lbrace>snd ?tta\<rbrace>\<^bsub>o\<^esub>) (?obs (complete_sc ?s' (?vs (ttas' @ [?tta]))))"
[PROOF STATE]
proof (prove)
using this:
complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))

goal (1 subgoal):
 1. obs = lappend (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))))
[PROOF STEP]
using obs_def
[PROOF STATE]
proof (prove)
using this:
complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))
obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))

goal (1 subgoal):
 1. obs = lappend (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))))
[PROOF STEP]
by(simp add: split_beta)
[PROOF STATE]
proof (state)
this:
obs = lappend (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
obs = lappend (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
have "ta_seq_consist P vs' (llist_of \<lbrace>snd ?tta\<rbrace>\<^bsub>o\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P vs' (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
using \<open>?proceed (Eps ?proceed)\<close> vs'_def
[PROOF STATE]
proof (prove)
using this:
case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
vs' = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))

goal (1 subgoal):
 1. ta_seq_consist P vs' (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
by(clarsimp simp add: split_beta)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs' (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs' (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs' (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
assume "llist_of \<lbrace>snd ?tta\<rbrace>\<^bsub>o\<^esub> = LNil"
[PROOF STATE]
proof (state)
this:
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
from obs_def \<open>obs \<noteq> LNil\<close>
[PROOF STATE]
proof (chain)
picking this:
obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))
obs \<noteq> LNil
[PROOF STEP]
have "lfinite (ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []) (complete_sc s' (?vs ttas')))"
[PROOF STATE]
proof (prove)
using this:
obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))
obs \<noteq> LNil

goal (1 subgoal):
 1. lfinite (ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))
[PROOF STEP]
unfolding lfinite_ltakeWhile
[PROOF STATE]
proof (prove)
using this:
obs = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))
obs \<noteq> LNil

goal (1 subgoal):
 1. lfinite (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas')))) \<or> (\<exists>x\<in>lset (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas')))). \<not> (case x of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))
[PROOF STEP]
by(fastforce simp add: split_def lconcat_eq_LNil)
[PROOF STATE]
proof (state)
this:
lfinite (ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil
lfinite (ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))
[PROOF STEP]
have "(complete_sc ?s' (?vs (ttas' @ [?tta])), a) \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil
lfinite (ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []) (complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))))

goal (1 subgoal):
 1. (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))), a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))
[PROOF STEP]
unfolding a_def vs'_def csc_unfold
[PROOF STATE]
proof (prove)
using this:
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil
lfinite (ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []) (LCons (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))))

goal (1 subgoal):
 1. (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))), LCons (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))
[PROOF STEP]
by(clarsimp simp add: split_def llist_of_eq_LNil_conv)(auto simp add: lfinite_eq_range_llist_of)
[PROOF STATE]
proof (state)
this:
(complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))), a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil \<Longrightarrow> (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))), a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil \<Longrightarrow> (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))), a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
have "?obs (complete_sc ?s' (?vs (ttas' @ [?tta]))) = ?obs (complete_sc ?s' (mrw_values P vs' (list_of (llist_of \<lbrace>snd ?tta\<rbrace>\<^bsub>o\<^esub>))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))) = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))))
[PROOF STEP]
unfolding vs'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))) = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))))
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))) = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))) = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
from \<open>?proceed (Eps ?proceed)\<close> Red
[PROOF STATE]
proof (chain)
picking this:
case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
s -\<triangleright>ttas'\<rightarrow>* s'
[PROOF STEP]
have "s -\<triangleright>ttas' @ [?tta]\<rightarrow>* ?s'"
[PROOF STATE]
proof (prove)
using this:
case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
s -\<triangleright>ttas'\<rightarrow>* s'

goal (1 subgoal):
 1. s -\<triangleright>ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]\<rightarrow>* snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))
[PROOF STEP]
by(auto simp add: RedT_def split_def intro: rtrancl3p_step)
[PROOF STATE]
proof (state)
this:
s -\<triangleright>ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]\<rightarrow>* snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s -\<triangleright>ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]\<rightarrow>* snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
from sc \<open>?proceed (Eps ?proceed)\<close>
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))
case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
[PROOF STEP]
have "ta_seq_consist P vs (llist_of (?ttas' (ttas' @ [?tta])))"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))
case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) of (x, xa) \<Rightarrow> (case x of (t', ta') \<Rightarrow> \<lambda>s''. s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa

goal (1 subgoal):
 1. ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]))))
[PROOF STEP]
by(clarsimp simp add: split_def ta_seq_consist_lappend lappend_llist_of_llist_of[symmetric] simp del: lappend_llist_of_llist_of)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]))))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]))))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
have "mrw_values P vs' (list_of (llist_of \<lbrace>snd ?tta\<rbrace>\<^bsub>o\<^esub>)) = ?vs (ttas' @ [?tta])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)) = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))
[PROOF STEP]
unfolding vs'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)) = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)) = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)) = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
have "complete_sc ?s' (?vs (ttas' @ [?tta])) = complete_sc ?s' (mrw_values P vs' (list_of (llist_of \<lbrace>snd ?tta\<rbrace>\<^bsub>o\<^esub>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))) = complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))
[PROOF STEP]
unfolding vs'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))) = complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))
[PROOF STEP]
by(simp add: split_def)
[PROOF STATE]
proof (state)
this:
complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))) = complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))

goal (1 subgoal):
 1. obs \<noteq> LNil \<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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs''))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
obs = lappend (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))))
ta_seq_consist P vs' (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil \<Longrightarrow> (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))), a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))
lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))) = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))))
s -\<triangleright>ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]\<rightarrow>* snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]))))
mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)) = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))
complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))) = complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))
[PROOF STEP]
have "?lappend"
[PROOF STATE]
proof (prove)
using this:
obs = lappend (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))))
ta_seq_consist P vs' (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)
llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub> = LNil \<Longrightarrow> (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))), a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))
lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))))) = lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))))
s -\<triangleright>ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]\<rightarrow>* snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]))))
mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)) = mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))
complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas' @ [fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))])))) = complete_sc (snd (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs' (list_of (llist_of \<lbrace>snd (fst (SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)))\<rbrace>\<^bsub>o\<^esub>)))

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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs'')
[PROOF STEP]
by blast
[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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<or> ta_seq_consist P (mrw_values P vs' (list_of obs')) obs'')

goal (1 subgoal):
 1. 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> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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'' a'. obs = lappend obs' obs'' \<and> ta_seq_consist P vs' obs' \<and> (obs' = LNil \<longrightarrow> (a', a) \<in> inv_image {(m, n). m < n} (llength \<circ> ltakeWhile (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> = []))) \<and> (lfinite obs' \<longrightarrow> (\<exists>s' ttas'. obs'' = lconcat (lmap (\<lambda>a. case a of (t, ta) \<Rightarrow> llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s' (mrw_values P vs' (list_of obs')))) \<and> s -\<triangleright>ttas'\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) \<and> mrw_values P vs' (list_of obs') = mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')) \<and> a' = complete_sc s' (mrw_values P vs' (list_of obs'))) \<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