[STATEMENT]
lemma red0_Red1'_FWweak_bisim:
  assumes wf: "wf_J_prog P"
  shows "FWdelay_bisimulation_diverge final_expr0 (mred0 P) final_expr1 (mred1' (compP1 P))
           (\<lambda>t. bisim_red0_Red1) bisim_wait01 (\<tau>MOVE0 P) (\<tau>MOVE1 (compP1 P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge final_expr0 (mred0 P) final_expr1 (mred1' (compP1 P)) (\<lambda>t. bisim_red0_Red1) bisim_wait01 (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge final_expr0 (mred0 P) final_expr1 (mred1' (compP1 P)) (\<lambda>t. bisim_red0_Red1) bisim_wait01 (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
interpret delay_bisimulation_diverge
    "mred0 P t"
    "mred1' (compP1 P) t"
    bisim_red0_Red1
    "ta_bisim (\<lambda>t. bisim_red0_Red1)" "\<tau>MOVE0 P" "\<tau>MOVE1 (compP1 P)"
    for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P

goal (1 subgoal):
 1. delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
by(rule delay_bisimulation_diverge_red0_Red1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge final_expr0 (mred0 P) final_expr1 (mred1' (compP1 P)) (\<lambda>t. bisim_red0_Red1) bisim_wait01 (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge final_expr0 (mred0 P) final_expr1 (mred1' (compP1 P)) (\<lambda>t. bisim_red0_Red1) bisim_wait01 (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s1 of (x1, m) \<Rightarrow> final_expr0 x1\<rbrakk> \<Longrightarrow> \<exists>s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1 s2' \<and> (case s2' of (x2, m) \<Rightarrow> final_expr1 x2)
 2. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 3. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 4. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 5. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 7. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
fix t and s1 and s2 :: "(('addr expr1 \<times> 'addr locals1) \<times> ('addr expr1 \<times> 'addr locals1) list) \<times> 'heap"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s1 of (x1, m) \<Rightarrow> final_expr0 x1\<rbrakk> \<Longrightarrow> \<exists>s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1 s2' \<and> (case s2' of (x2, m) \<Rightarrow> final_expr1 x2)
 2. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 3. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 4. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 5. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 7. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
assume "bisim_red0_Red1 s1 s2" "(\<lambda>(x1, m). final_expr0 x1) s1"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
case s1 of (x1, m) \<Rightarrow> final_expr0 x1

goal (7 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s1 of (x1, m) \<Rightarrow> final_expr0 x1\<rbrakk> \<Longrightarrow> \<exists>s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1 s2' \<and> (case s2' of (x2, m) \<Rightarrow> final_expr1 x2)
 2. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 3. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 4. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 5. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 7. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
case s1 of (x1, m) \<Rightarrow> final_expr0 x1

goal (7 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s1 of (x1, m) \<Rightarrow> final_expr0 x1\<rbrakk> \<Longrightarrow> \<exists>s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1 s2' \<and> (case s2' of (x2, m) \<Rightarrow> final_expr1 x2)
 2. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 3. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 4. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 5. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 7. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
hence "(\<lambda>(x2, m). final_expr1 x2) s2"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2
case s1 of (x1, m) \<Rightarrow> final_expr0 x1

goal (1 subgoal):
 1. case s2 of (x2, m) \<Rightarrow> final_expr1 x2
[PROOF STEP]
by(cases s1)(cases s2,auto simp add: bisim_red0_Red1_def final_iff elim!: bisim_list1_elim elim: bisim_list.cases)
[PROOF STATE]
proof (state)
this:
case s2 of (x2, m) \<Rightarrow> final_expr1 x2

goal (7 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s1 of (x1, m) \<Rightarrow> final_expr0 x1\<rbrakk> \<Longrightarrow> \<exists>s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1 s2' \<and> (case s2' of (x2, m) \<Rightarrow> final_expr1 x2)
 2. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 3. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 4. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 5. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 7. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 s1 s2
case s1 of (x1, m) \<Rightarrow> final_expr0 x1
case s2 of (x2, m) \<Rightarrow> final_expr1 x2
[PROOF STEP]
show "\<exists>s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(x2, m). final_expr1 x2) s2'"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2
case s1 of (x1, m) \<Rightarrow> final_expr0 x1
case s2 of (x2, m) \<Rightarrow> final_expr1 x2

goal (1 subgoal):
 1. \<exists>s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1 s2' \<and> (case s2' of (x2, m) \<Rightarrow> final_expr1 x2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1 s2' \<and> (case s2' of (x2, m) \<Rightarrow> final_expr1 x2)

goal (6 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 2. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 3. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 4. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 2. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 3. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 4. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
fix t s1 and s2 :: "(('addr expr1 \<times> 'addr locals1) \<times> ('addr expr1 \<times> 'addr locals1) list) \<times> 'heap"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 2. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 3. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 4. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
assume "bisim_red0_Red1 s1 s2" "(\<lambda>(x2, m). final_expr1 x2) s2"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
case s2 of (x2, m) \<Rightarrow> final_expr1 x2

goal (6 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 2. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 3. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 4. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
case s2 of (x2, m) \<Rightarrow> final_expr1 x2

goal (6 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 2. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 3. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 4. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
hence "(\<lambda>(x1, m). final_expr0 x1) s1"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2
case s2 of (x2, m) \<Rightarrow> final_expr1 x2

goal (1 subgoal):
 1. case s1 of (x1, m) \<Rightarrow> final_expr0 x1
[PROOF STEP]
by(cases s1)(cases s2,auto simp add: bisim_red0_Red1_def final_iff elim!: bisim_list1_elim elim: bisim_list.cases)
[PROOF STATE]
proof (state)
this:
case s1 of (x1, m) \<Rightarrow> final_expr0 x1

goal (6 subgoals):
 1. \<And>t s1 s2. \<lbrakk>bisim_red0_Red1 s1 s2; case s2 of (x2, m) \<Rightarrow> final_expr1 x2\<rbrakk> \<Longrightarrow> \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
 2. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 3. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 4. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 6. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 s1 s2
case s2 of (x2, m) \<Rightarrow> final_expr1 x2
case s1 of (x1, m) \<Rightarrow> final_expr0 x1
[PROOF STEP]
show "\<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (\<lambda>(x1, m). final_expr0 x1) s1'"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2
case s2 of (x2, m) \<Rightarrow> final_expr1 x2
case s1 of (x1, m) \<Rightarrow> final_expr0 x1

goal (1 subgoal):
 1. \<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s1'. red0_mthr.silent_moves P t s1 s1' \<and> bisim_red0_Red1 s1' s2 \<and> (case s1' of (x1, m) \<Rightarrow> final_expr0 x1)

goal (5 subgoals):
 1. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 2. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 3. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 2. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 3. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
fix t' x m1 x' m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 2. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 3. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
assume b: "bisim_red0_Red1 (x, m1) (x', m2)"
      and bo: "bisim_red0_Red1 (x1, m1) (x2, m2)"
      and \<tau>red1: "red0_mthr.silent_moves P t (x1, m1) (x1', m1)"
      and red1: "mred0 P t (x1', m1) ta1 (x1'', m1')"
      and \<tau>1: "\<not> \<tau>MOVE0 P (x1', m1) ta1 (x1'', m1')"
      and \<tau>red2: "Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2)"
      and red2: "mred1' (compP1 P) t (x2', m2) ta2 (x2'', m2')"
      and bo': "bisim_red0_Red1 (x1'', m1') (x2'', m2')"
      and tb: "ta_bisim (\<lambda>t. bisim_red0_Red1) ta1 ta2"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 (x, m1) (x', m2)
bisim_red0_Red1 (x1, m1) (x2, m2)
red0_mthr.silent_moves P t (x1, m1) (x1', m1)
red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'
\<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1')
Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2)
Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'
bisim_red0_Red1 (x1'', m1') (x2'', m2')
red0_Red1'.ta_bisim_bisim_syntax ta1 ta2

goal (5 subgoals):
 1. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 2. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 3. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
from b
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 (x, m1) (x', m2)
[PROOF STEP]
have "m1 = m2"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 (x, m1) (x', m2)

goal (1 subgoal):
 1. m1 = m2
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def split_beta)
[PROOF STATE]
proof (state)
this:
m1 = m2

goal (5 subgoals):
 1. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 2. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 3. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m1 = m2

goal (5 subgoals):
 1. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 2. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 3. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
from bo'
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 (x1'', m1') (x2'', m2')
[PROOF STEP]
have "m1' = m2'"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 (x1'', m1') (x2'', m2')

goal (1 subgoal):
 1. m1' = m2'
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def split_beta)
[PROOF STATE]
proof (state)
this:
m1' = m2'

goal (5 subgoals):
 1. \<And>t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'. \<lbrakk>bisim_red0_Red1 (x, m1) (xx, m2); bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2\<rbrakk> \<Longrightarrow> bisim_red0_Red1 (x, m1') (xx, m2')
 2. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 3. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 5. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m1 = m2
m1' = m2'
[PROOF STEP]
show "bisim_red0_Red1 (x, m1') (x', m2')"
[PROOF STATE]
proof (prove)
using this:
m1 = m2
m1' = m2'

goal (1 subgoal):
 1. bisim_red0_Red1 (x, m1') (x', m2')
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
m1 = m2
m1' = m2'
bisim_red0_Red1 (x, m1) (x', m2)

goal (1 subgoal):
 1. bisim_red0_Red1 (x, m1') (x', m2')
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def split_beta)
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 (x, m1') (x', m2')

goal (4 subgoals):
 1. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 2. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 2. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
fix t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 2. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
assume "bisim_red0_Red1 (x1, m1) (x2, m2)"
      and "red0_mthr.silent_moves P t (x1, m1) (x1', m1)"
      and red0: "mred0 P t (x1', m1) ta1 (x1'', m1')"
      and "\<not> \<tau>MOVE0 P (x1', m1) ta1 (x1'', m1')"
      and "Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2)"
      and red1: "mred1' (compP1 P) t (x2', m2) ta2 (x2'', m2')"
      and "\<not> \<tau>MOVE1 (compP1 P) (x2', m2) ta2 (x2'', m2')"
      and "bisim_red0_Red1 (x1'', m1') (x2'', m2')"
      and "ta_bisim01 ta1 ta2"
      and Suspend: "Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>" "Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 (x1, m1) (x2, m2)
red0_mthr.silent_moves P t (x1, m1) (x1', m1)
red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'
\<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1')
Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2)
Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'
\<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2')
bisim_red0_Red1 (x1'', m1') (x2'', m2')
red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>
Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>

goal (4 subgoals):
 1. \<And>t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); red0_mthr.silent_moves P t (x1, m1) (x1', m1); red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'; \<not> (case (x1', m1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 (x1'', m1'); Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2); Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'; \<not> (case (x2', m2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 (x2'', m2'); bisim_red0_Red1 (x1'', m1') (x2'', m2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta2; Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>; Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> bisim_wait01 x1'' x2''
 2. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 4. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
from red0 red1 Suspend
[PROOF STATE]
proof (chain)
picking this:
red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'
Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'
Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>
Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>
[PROOF STEP]
show "bisim_wait01 x1'' x2''"
[PROOF STATE]
proof (prove)
using this:
red0_mthr.r_syntax P t x1' m1 ta1 x1'' m1'
Red1_mthr.r_syntax False (compP1 P) t x2' m2 ta2 x2'' m2'
Suspend w \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>
Suspend w \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>

goal (1 subgoal):
 1. bisim_wait01 x1'' x2''
[PROOF STEP]
by(cases x2')(cases x2'', auto dest: Red_Suspend_is_call Red1_Suspend_is_call simp add: split_beta bisim_wait01_def is_call_def)
[PROOF STATE]
proof (state)
this:
bisim_wait01 x1'' x2''

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
fix t x1 m1 x2 m2 ta1 x1' m1'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
assume "bisim_red0_Red1 (x1, m1) (x2, m2)"
      and "bisim_wait01 x1 x2"
      and "mred0 P t (x1, m1) ta1 (x1', m1')"
      and wakeup: "Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 (x1, m1) (x2, m2)
bisim_wait01 x1 x2
red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'
Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 (x1, m1) (x2, m2)
bisim_wait01 x1 x2
red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'
Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
obtain e0 es0 where [simp]: "x1 = (e0, es0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e0 es0. x1 = (e0, es0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x1)
[PROOF STATE]
proof (state)
this:
x1 = (e0, es0)

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 = (e0, es0)

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
obtain e0' es0' where [simp]: "x1' = (e0', es0')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e0' es0'. x1' = (e0', es0') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x1')
[PROOF STATE]
proof (state)
this:
x1' = (e0', es0')

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1' = (e0', es0')

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
obtain e1 xs1 exs1 where [simp]: "x2 = ((e1, xs1), exs1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e1 xs1 exs1. x2 = ((e1, xs1), exs1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x2) auto
[PROOF STATE]
proof (state)
this:
x2 = ((e1, xs1), exs1)

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 (x1, m1) (x2, m2)
bisim_wait01 x1 x2
red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'
Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>
x1 = (e0, es0)
x1' = (e0', es0')
x2 = ((e1, xs1), exs1)
[PROOF STEP]
have bisim: "bisim_list1 (e0, es0) ((e1, xs1), exs1)"
      and m1: "m2 = m1"
      and call: "call e0 \<noteq> None" "call1 e1 \<noteq> None"
      and red: "P,t \<turnstile>0 \<langle>e0/es0, m1\<rangle> -ta1\<rightarrow> \<langle>e0'/es0', m1'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 (x1, m1) (x2, m2)
bisim_wait01 x1 x2
red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'
Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>
x1 = (e0, es0)
x1' = (e0', es0')
x2 = ((e1, xs1), exs1)

goal (1 subgoal):
 1. (bisim_list1 (e0, es0) ((e1, xs1), exs1) &&& m2 = m1) &&& (call e0 \<noteq> None &&& call1 e1 \<noteq> None) &&& P,t \<turnstile>0 \<langle>e0/es0,m1\<rangle> -ta1\<rightarrow> \<langle>e0'/es0',m1'\<rangle>
[PROOF STEP]
by(auto simp add: bisim_wait01_def bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
bisim_list1 (e0, es0) ((e1, xs1), exs1)
m2 = m1
call e0 \<noteq> None
call1 e1 \<noteq> None
P,t \<turnstile>0 \<langle>e0/es0,m1\<rangle> -ta1\<rightarrow> \<langle>e0'/es0',m1'\<rangle>

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
from red wakeup
[PROOF STATE]
proof (chain)
picking this:
P,t \<turnstile>0 \<langle>e0/es0,m1\<rangle> -ta1\<rightarrow> \<langle>e0'/es0',m1'\<rangle>
Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>
[PROOF STEP]
have "\<not> \<tau>Move0 P m1 (e0, es0)"
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile>0 \<langle>e0/es0,m1\<rangle> -ta1\<rightarrow> \<langle>e0'/es0',m1'\<rangle>
Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>

goal (1 subgoal):
 1. \<not> \<tau>Move0 P m1 (e0, es0)
[PROOF STEP]
by(auto elim!: red0.cases dest: red_\<tau>_taD[where extTA="extTA2J0 P", simplified])
[PROOF STATE]
proof (state)
this:
\<not> \<tau>Move0 P m1 (e0, es0)

goal (3 subgoals):
 1. \<And>t x1 m1 x2 m2 ta1 x1' m1'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; red0_mthr.r_syntax P t x1 m1 ta1 x1' m1'; Notified \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta1\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 3. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
with Red1_simulates_red0[OF wf red bisim] call m1
[PROOF STATE]
proof (chain)
picking this:
\<exists>ex2'' exs2''. bisim_list1 (e0', es0') (ex2'', exs2'') \<and> (if \<tau>Move0 P m1 (e0, es0) then \<tau>Red1't (compP1 P) t m1 ((e1, xs1), exs1) (ex2'', exs2'') \<and> ta1 = \<lbrace>\<rbrace> \<and> m1 = m1' else \<exists>ex2' exs2' ta'. \<tau>Red1'r (compP1 P) t m1 ((e1, xs1), exs1) (ex2', exs2') \<and> (call e0 = None \<or> call1 (fst (e1, xs1)) = None \<or> ex2' = (e1, xs1) \<and> exs2' = exs1) \<and> False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',m1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',m1'\<rangle> \<and> \<not> \<tau>Move1 P m1 (ex2', exs2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta')
call e0 \<noteq> None
call1 e1 \<noteq> None
m2 = m1
\<not> \<tau>Move0 P m1 (e0, es0)
[PROOF STEP]
show "\<exists>ta2 x2' m2'. mred1' (compP1 P) t (x2, m2) ta2 (x2', m2') \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> ta_bisim01 ta1 ta2"
[PROOF STATE]
proof (prove)
using this:
\<exists>ex2'' exs2''. bisim_list1 (e0', es0') (ex2'', exs2'') \<and> (if \<tau>Move0 P m1 (e0, es0) then \<tau>Red1't (compP1 P) t m1 ((e1, xs1), exs1) (ex2'', exs2'') \<and> ta1 = \<lbrace>\<rbrace> \<and> m1 = m1' else \<exists>ex2' exs2' ta'. \<tau>Red1'r (compP1 P) t m1 ((e1, xs1), exs1) (ex2', exs2') \<and> (call e0 = None \<or> call1 (fst (e1, xs1)) = None \<or> ex2' = (e1, xs1) \<and> exs2' = exs1) \<and> False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',m1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',m1'\<rangle> \<and> \<not> \<tau>Move1 P m1 (ex2', exs2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta')
call e0 \<noteq> None
call1 e1 \<noteq> None
m2 = m1
\<not> \<tau>Move0 P m1 (e0, es0)

goal (1 subgoal):
 1. \<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
\<exists>ta2 x2' m2'. Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
fix t x1 m1 x2 m2 ta2 x2' m2'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
assume "bisim_red0_Red1 (x1, m1) (x2, m2)"
      and "bisim_wait01 x1 x2"
      and "mred1' (compP1 P) t (x2, m2) ta2 (x2', m2')"
      and wakeup: "Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 (x1, m1) (x2, m2)
bisim_wait01 x1 x2
Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'
Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 (x1, m1) (x2, m2)
bisim_wait01 x1 x2
Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'
Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
obtain e0 es0 where [simp]: "x1 = (e0, es0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e0 es0. x1 = (e0, es0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x1)
[PROOF STATE]
proof (state)
this:
x1 = (e0, es0)

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 = (e0, es0)

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
obtain e1 xs1 exs1 where [simp]: "x2 = ((e1, xs1), exs1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e1 xs1 exs1. x2 = ((e1, xs1), exs1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x2) auto
[PROOF STATE]
proof (state)
this:
x2 = ((e1, xs1), exs1)

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x2 = ((e1, xs1), exs1)

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
obtain e1' xs1' exs1' where [simp]: "x2' = ((e1', xs1'), exs1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e1' xs1' exs1'. x2' = ((e1', xs1'), exs1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x2') auto
[PROOF STATE]
proof (state)
this:
x2' = ((e1', xs1'), exs1')

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 (x1, m1) (x2, m2)
bisim_wait01 x1 x2
Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'
Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>
x1 = (e0, es0)
x2 = ((e1, xs1), exs1)
x2' = ((e1', xs1'), exs1')
[PROOF STEP]
have bisim: "bisim_list1 (e0, es0) ((e1, xs1), exs1)"
      and m1: "m2 = m1"
      and call: "call e0 \<noteq> None" "call1 e1 \<noteq> None"
      and red: "False,compP1 P,t \<turnstile>1 \<langle>(e1, xs1)/exs1, m1\<rangle> -ta2\<rightarrow> \<langle>(e1', xs1')/exs1', m2'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 (x1, m1) (x2, m2)
bisim_wait01 x1 x2
Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'
Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>
x1 = (e0, es0)
x2 = ((e1, xs1), exs1)
x2' = ((e1', xs1'), exs1')

goal (1 subgoal):
 1. (bisim_list1 (e0, es0) ((e1, xs1), exs1) &&& m2 = m1) &&& (call e0 \<noteq> None &&& call1 e1 \<noteq> None) &&& False,compP1 P,t \<turnstile>1 \<langle>(e1, xs1)/exs1,m1\<rangle> -ta2\<rightarrow> \<langle>(e1', xs1')/exs1',m2'\<rangle>
[PROOF STEP]
by(auto simp add: bisim_wait01_def bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
bisim_list1 (e0, es0) ((e1, xs1), exs1)
m2 = m1
call e0 \<noteq> None
call1 e1 \<noteq> None
False,compP1 P,t \<turnstile>1 \<langle>(e1, xs1)/exs1,m1\<rangle> -ta2\<rightarrow> \<langle>(e1', xs1')/exs1',m2'\<rangle>

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
from red wakeup
[PROOF STATE]
proof (chain)
picking this:
False,compP1 P,t \<turnstile>1 \<langle>(e1, xs1)/exs1,m1\<rangle> -ta2\<rightarrow> \<langle>(e1', xs1')/exs1',m2'\<rangle>
Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>
[PROOF STEP]
have "\<not> \<tau>Move1 P m1 ((e1, xs1), exs1)"
[PROOF STATE]
proof (prove)
using this:
False,compP1 P,t \<turnstile>1 \<langle>(e1, xs1)/exs1,m1\<rangle> -ta2\<rightarrow> \<langle>(e1', xs1')/exs1',m2'\<rangle>
Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>

goal (1 subgoal):
 1. \<not> \<tau>Move1 P m1 ((e1, xs1), exs1)
[PROOF STEP]
by(auto elim!: Red1.cases dest: red1_\<tau>_taD)
[PROOF STATE]
proof (state)
this:
\<not> \<tau>Move1 P m1 ((e1, xs1), exs1)

goal (2 subgoals):
 1. \<And>t x1 m1 x2 m2 ta2 x2' m2'. \<lbrakk>bisim_red0_Red1 (x1, m1) (x2, m2); bisim_wait01 x1 x2; Red1_mthr.r_syntax False (compP1 P) t x2 m2 ta2 x2' m2'; Notified \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub> \<or> WokenUp \<in> set \<lbrace>ta2\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
 2. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
with red0_simulates_Red1[OF wf red bisim] m1 call
[PROOF STATE]
proof (chain)
picking this:
\<exists>e' es'. bisim_list1 (e', es') ((e1', xs1'), exs1') \<and> (if \<tau>Move1 P m1 ((e1, xs1), exs1) then (\<tau>Red0t P t m1 (e0, es0) (e', es') \<or> countInitBlock (fst (e1', xs1')) < countInitBlock (fst (e1, xs1)) \<and> exs1' = exs1 \<and> e' = e0 \<and> es' = es0) \<and> ta2 = \<lbrace>\<rbrace> \<and> m1 = m2' else \<exists>e'' es'' ta'. \<tau>Red0r P t m1 (e0, es0) (e'', es'') \<and> (call1 (fst (e1, xs1)) = None \<or> call e0 = None \<or> e'' = e0 \<and> es'' = es0) \<and> P,t \<turnstile>0 \<langle>e''/es'',m1\<rangle> -ta'\<rightarrow> \<langle>e'/es',m2'\<rangle> \<and> \<not> \<tau>Move0 P m1 (e'', es'') \<and> red0_Red1'.ta_bisim_bisim_syntax ta' ta2)
m2 = m1
call e0 \<noteq> None
call1 e1 \<noteq> None
\<not> \<tau>Move1 P m1 ((e1, xs1), exs1)
[PROOF STEP]
show "\<exists>ta1 x1' m1'. mred0 P t (x1, m1) ta1 (x1', m1') \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> ta_bisim01 ta1 ta2"
[PROOF STATE]
proof (prove)
using this:
\<exists>e' es'. bisim_list1 (e', es') ((e1', xs1'), exs1') \<and> (if \<tau>Move1 P m1 ((e1, xs1), exs1) then (\<tau>Red0t P t m1 (e0, es0) (e', es') \<or> countInitBlock (fst (e1', xs1')) < countInitBlock (fst (e1, xs1)) \<and> exs1' = exs1 \<and> e' = e0 \<and> es' = es0) \<and> ta2 = \<lbrace>\<rbrace> \<and> m1 = m2' else \<exists>e'' es'' ta'. \<tau>Red0r P t m1 (e0, es0) (e'', es'') \<and> (call1 (fst (e1, xs1)) = None \<or> call e0 = None \<or> e'' = e0 \<and> es'' = es0) \<and> P,t \<turnstile>0 \<langle>e''/es'',m1\<rangle> -ta'\<rightarrow> \<langle>e'/es',m2'\<rangle> \<and> \<not> \<tau>Move0 P m1 (e'', es'') \<and> red0_Red1'.ta_bisim_bisim_syntax ta' ta2)
m2 = m1
call e0 \<noteq> None
call1 e1 \<noteq> None
\<not> \<tau>Move1 P m1 ((e1, xs1), exs1)

goal (1 subgoal):
 1. \<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
\<exists>ta1 x1' m1'. red0_mthr.r_syntax P t x1 m1 ta1 x1' m1' \<and> bisim_red0_Red1 (x1', m1') (x2', m2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2

goal (1 subgoal):
 1. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
show "(\<exists>x. final_expr0 x) \<longleftrightarrow> (\<exists>x. final_expr1 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ex final_expr0 = Ex final_expr1
[PROOF STEP]
by(auto simp add: split_paired_Ex final_iff)
[PROOF STATE]
proof (state)
this:
Ex final_expr0 = Ex final_expr1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
FWdelay_bisimulation_diverge final_expr0 (mred0 P) final_expr1 (mred1' (compP1 P)) (\<lambda>t. bisim_red0_Red1) bisim_wait01 (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)

goal:
No subgoals!
[PROOF STEP]
qed