[STATEMENT]
lemma complete_sc_in_Runs:
  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 "mthr.Runs s (complete_sc s vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mthr.Runs s (complete_sc s vs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mthr.Runs s (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. mthr.Runs s (complete_sc s vs)
[PROOF STEP]
let "?vs ttas'" = "mrw_values P vs (?ttas' ttas')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mthr.Runs s (complete_sc s vs)
[PROOF STEP]
define s' vs'
    and ttas :: "('thread_id \<times> ('l,'thread_id,'x,'m,'w, ('addr, 'thread_id) obs_event action) thread_action) list"
    where "s' = s" and "vs' = vs" and "ttas = []"
[PROOF STATE]
proof (state)
this:
s' = s
vs' = vs
ttas = []

goal (1 subgoal):
 1. mthr.Runs s (complete_sc s vs)
[PROOF STEP]
hence "s -\<triangleright>ttas\<rightarrow>* s'" "ta_seq_consist P vs (llist_of (?ttas' ttas))"
[PROOF STATE]
proof (prove)
using this:
s' = s
vs' = vs
ttas = []

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

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

goal (1 subgoal):
 1. mthr.Runs s' (complete_sc s' (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))))
[PROOF STEP]
proof(coinduction arbitrary: s' ttas rule: mthr.Runs.coinduct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s' ttas. \<lbrakk>s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s'a tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) = LCons tl tls \<and> redT sa tl s'a \<and> ((\<exists>s' ttas. s'a = s' \<and> tls = complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s'a tls))
[PROOF STEP]
case (Runs s' ttas')
[PROOF STATE]
proof (state)
this:
s -\<triangleright>ttas'\<rightarrow>* s'
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas')))

goal (1 subgoal):
 1. \<And>s' ttas. \<lbrakk>s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s'a tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) = LCons tl tls \<and> redT sa tl s'a \<and> ((\<exists>s' ttas. s'a = s' \<and> tls = complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s'a tls))
[PROOF STEP]
note Red = \<open>s -\<triangleright>ttas'\<rightarrow>* s'\<close>
      and sc = \<open>ta_seq_consist P vs (llist_of (?ttas' ttas'))\<close>
[PROOF STATE]
proof (state)
this:
s -\<triangleright>ttas'\<rightarrow>* s'
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))

goal (1 subgoal):
 1. \<And>s' ttas. \<lbrakk>s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s'a tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) = LCons tl tls \<and> redT sa tl s'a \<and> ((\<exists>s' ttas. s'a = s' \<and> tls = complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s' \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s'a tls))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
 2. \<nexists>t' ta'. Ex (redT_syntax1 s' t' ta') \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
 2. \<nexists>t' ta'. Ex (redT_syntax1 s' t' ta') \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
hence ?Stuck
[PROOF STATE]
proof (prove)
using this:
\<nexists>t' ta'. Ex (redT_syntax1 s' t' ta')

goal (1 subgoal):
 1. \<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)
[PROOF STEP]
by(simp add: complete_sc_def)
[PROOF STATE]
proof (state)
this:
\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)

goal (2 subgoals):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
 2. \<nexists>t' ta'. Ex (redT_syntax1 s' t' ta') \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)

goal (1 subgoal):
 1. (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))

goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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(auto)
[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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
[PROOF STEP]
using Red
[PROOF STATE]
proof (prove)
using this:
s' -t'\<triangleright>ta''\<rightarrow> s'''
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta''\<rbrace>\<^bsub>o\<^esub>)
s -\<triangleright>ttas'\<rightarrow>* s'

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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
moreover
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
from Red *
[PROOF STATE]
proof (chain)
picking this:
s -\<triangleright>ttas'\<rightarrow>* s'
case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
[PROOF STEP]
have "s -\<triangleright>ttas' @ [fst (Eps ?proceed)]\<rightarrow>* snd (Eps ?proceed)"
[PROOF STATE]
proof (prove)
using this:
s -\<triangleright>ttas'\<rightarrow>* s'
case SOME ((t', ta'), s''). s' -t'\<triangleright>ta'\<rightarrow> s'' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa

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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))
[PROOF STEP]
by(auto simp add: split_beta RedT_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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
\<exists>t' ta'. Ex (redT_syntax1 s' t' ta')
[PROOF STEP]
have "complete_sc s' (?vs ttas') = LCons (fst (Eps ?proceed)) (complete_sc (snd (Eps ?proceed)) (?vs (ttas' @ [fst (Eps ?proceed)])))"
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
complete_sc s' (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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' @ [fst (Eps ?proceed)])))"
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]))))
[PROOF STEP]
unfolding map_append concat_append lappend_llist_of_llist_of[symmetric]
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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 (lappend (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) [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(subst ta_seq_consist_lappend)(auto simp add: split_def)
[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>a. case a of (t, ta) \<Rightarrow> \<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> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
ultimately
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))
complete_sc s' (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]))))
[PROOF STEP]
have ?Step
[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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) xa
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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))
complete_sc s' (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))) (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<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>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))]))))

goal (1 subgoal):
 1. \<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls)
[PROOF STEP]
by(fastforce intro: exI[where x="ttas' @ [fst (Eps ?proceed)]"] simp del: split_paired_Ex)
[PROOF STATE]
proof (state)
this:
\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls)

goal (1 subgoal):
 1. \<exists>t' ta'. Ex (redT_syntax1 s' t' ta') \<Longrightarrow> (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls)

goal (1 subgoal):
 1. (\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s. s' = s \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LNil \<and> (\<forall>x xa. \<not> redT s x xa)) \<or> (\<exists>sa s' tls tl. s' = sa \<and> complete_sc s' (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas'))) = LCons tl tls \<and> redT sa tl s' \<and> ((\<exists>s'a ttas. s' = s'a \<and> tls = complete_sc s'a (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<and> s -\<triangleright>ttas\<rightarrow>* s'a \<and> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<or> mthr.Runs s' tls))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mthr.Runs s' (complete_sc s' (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))))

goal (1 subgoal):
 1. mthr.Runs s (complete_sc s vs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mthr.Runs s' (complete_sc s' (mrw_values P vs (concat (map (\<lambda>a. case a of (t, ta) \<Rightarrow> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))))

goal (1 subgoal):
 1. mthr.Runs s (complete_sc s vs)
[PROOF STEP]
by(simp add: s'_def ttas_def)
[PROOF STATE]
proof (state)
this:
mthr.Runs s (complete_sc s vs)

goal:
No subgoals!
[PROOF STEP]
qed