[STATEMENT]
lemma delay_bisimulation_red0_Red1:
  assumes wf: "wf_J_prog P"
  shows "delay_bisimulation_measure (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 (ta_bisim (\<lambda>t. bisim_red0_Red1)) (\<tau>MOVE0 P) (\<tau>MOVE1 (compP1 P)) (\<lambda>es es'. False) (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e'< countInitBlock e)"
  (is "delay_bisimulation_measure _ _ _ _ _ _ ?\<mu>1 ?\<mu>2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_measure (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>) (\<lambda>es es'. False) (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
proof(unfold_locales)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
fix s1 s2 s1'
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
assume "bisim_red0_Red1 s1 s2" "red0_mthr.silent_move P t s1 s1'"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
red0_mthr.silent_move P t s1 s1'

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
red0_mthr.silent_move P t s1 s1'

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex1 exs1 h1 where s1: "s1 = ((ex1, exs1), h1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex1 exs1 h1. s1 = ((ex1, exs1), h1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1, auto)
[PROOF STATE]
proof (state)
this:
s1 = ((ex1, exs1), h1)

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = ((ex1, exs1), h1)

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex1' exs1' h1' where s1': "s1' = ((ex1', exs1'), h1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex1' exs1' h1'. s1' = ((ex1', exs1'), h1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1', auto)
[PROOF STATE]
proof (state)
this:
s1' = ((ex1', exs1'), h1')

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1' = ((ex1', exs1'), h1')

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex2 exs2 h2 where s2: "s2 = ((ex2, exs2), h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex2 exs2 h2. s2 = ((ex2, exs2), h2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2, auto)
[PROOF STATE]
proof (state)
this:
s2 = ((ex2, exs2), h2)

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 s1 s2
red0_mthr.silent_move P t s1 s1'
s1 = ((ex1, exs1), h1)
s1' = ((ex1', exs1'), h1')
s2 = ((ex2, exs2), h2)
[PROOF STEP]
have bisim: "bisim_list1 (ex1, exs1) (ex2, exs2)"
    and heap: "h1 = h2"
    and red: "P,t \<turnstile>0 \<langle>ex1/exs1,h1\<rangle> -\<epsilon>\<rightarrow> \<langle>ex1'/exs1',h1'\<rangle>"
    and \<tau>: "\<tau>Move0 P h1 (ex1, exs1)"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2
red0_mthr.silent_move P t s1 s1'
s1 = ((ex1, exs1), h1)
s1' = ((ex1', exs1'), h1')
s2 = ((ex2, exs2), h2)

goal (1 subgoal):
 1. (bisim_list1 (ex1, exs1) (ex2, exs2) &&& h1 = h2) &&& P,t \<turnstile>0 \<langle>ex1/exs1,h1\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>ex1'/exs1',h1'\<rangle> &&& \<tau>Move0 P h1 (ex1, exs1)
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def red0_mthr.silent_move_iff)
[PROOF STATE]
proof (state)
this:
bisim_list1 (ex1, exs1) (ex2, exs2)
h1 = h2
P,t \<turnstile>0 \<langle>ex1/exs1,h1\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>ex1'/exs1',h1'\<rangle>
\<tau>Move0 P h1 (ex1, exs1)

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from Red1_simulates_red0[OF wf red bisim] \<tau>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ex2'' exs2''. bisim_list1 (ex1', exs1') (ex2'', exs2'') \<and> (if \<tau>Move0 P h1 (ex1, exs1) then \<tau>Red1't (compP1 P) t h1 (ex2, exs2) (ex2'', exs2'') \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> h1 = h1' else \<exists>ex2' exs2' ta'. \<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2') \<and> (call ex1 = None \<or> call1 (fst ex2) = None \<or> ex2' = ex2 \<and> exs2' = exs2) \<and> False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle> \<and> \<not> \<tau>Move1 P h1 (ex2', exs2') \<and> red0_Red1'.ta_bisim_bisim_syntax \<lbrace>\<rbrace> ta')
\<tau>Move0 P h1 (ex1, exs1)
[PROOF STEP]
obtain ex2'' exs2'' where bisim': "bisim_list1 (ex1', exs1') (ex2'', exs2'')"
    and red': "\<tau>Red1't (compP1 P) t h1 (ex2, exs2) (ex2'', exs2'')"
    and [simp]: "h1' = h1"
[PROOF STATE]
proof (prove)
using this:
\<exists>ex2'' exs2''. bisim_list1 (ex1', exs1') (ex2'', exs2'') \<and> (if \<tau>Move0 P h1 (ex1, exs1) then \<tau>Red1't (compP1 P) t h1 (ex2, exs2) (ex2'', exs2'') \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> h1 = h1' else \<exists>ex2' exs2' ta'. \<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2') \<and> (call ex1 = None \<or> call1 (fst ex2) = None \<or> ex2' = ex2 \<and> exs2' = exs2) \<and> False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle> \<and> \<not> \<tau>Move1 P h1 (ex2', exs2') \<and> red0_Red1'.ta_bisim_bisim_syntax \<lbrace>\<rbrace> ta')
\<tau>Move0 P h1 (ex1, exs1)

goal (1 subgoal):
 1. (\<And>ex2'' exs2''. \<lbrakk>bisim_list1 (ex1', exs1') (ex2'', exs2''); \<tau>Red1't (compP1 P) t h1 (ex2, exs2) (ex2'', exs2''); h1' = h1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bisim_list1 (ex1', exs1') (ex2'', exs2'')
\<tau>Red1't (compP1 P) t h1 (ex2, exs2) (ex2'', exs2'')
h1' = h1

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from \<tau>Red1't_into_Red1'_\<tau>mthr_silent_movet[OF red'] bisim' heap
[PROOF STATE]
proof (chain)
picking this:
Red1_mthr.silent_movet False (compP1 P) t ((ex2, exs2), h1) ((ex2'', exs2''), h1)
bisim_list1 (ex1', exs1') (ex2'', exs2'')
h1 = h2
[PROOF STEP]
have "\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2'"
[PROOF STATE]
proof (prove)
using this:
Red1_mthr.silent_movet False (compP1 P) t ((ex2, exs2), h1) ((ex2'', exs2''), h1)
bisim_list1 (ex1', exs1') (ex2'', exs2'')
h1 = h2

goal (1 subgoal):
 1. \<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2'
[PROOF STEP]
unfolding s2 s1'
[PROOF STATE]
proof (prove)
using this:
Red1_mthr.silent_movet False (compP1 P) t ((ex2, exs2), h1) ((ex2'', exs2''), h1)
bisim_list1 (ex1', exs1') (ex2'', exs2'')
h1 = h2

goal (1 subgoal):
 1. \<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t ((ex2, exs2), h2) s2' \<and> bisim_red0_Red1 ((ex1', exs1'), h1') s2'
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2'

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; red0_mthr.silent_move P t s1 s1'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 5. wfP (\<lambda>es es'. False)
 6. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
thus "bisim_red0_Red1 s1' s2 \<and> ?\<mu>1^++ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2'

goal (1 subgoal):
 1. bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1' s2 \<and> (\<lambda>es es'. False)\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' \<and> bisim_red0_Red1 s1' s2')

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
fix s1 s2 s2'
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
assume "bisim_red0_Red1 s1 s2" "Red1_mthr.silent_move False (compP1 P) t s2 s2'"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
Red1_mthr.silent_move False (compP1 P) t s2 s2'

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
Red1_mthr.silent_move False (compP1 P) t s2 s2'

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex1 exs1 h1 where s1: "s1 = ((ex1, exs1), h1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex1 exs1 h1. s1 = ((ex1, exs1), h1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1, auto)
[PROOF STATE]
proof (state)
this:
s1 = ((ex1, exs1), h1)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = ((ex1, exs1), h1)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex2 exs2 h2 where s2: "s2 = ((ex2, exs2), h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex2 exs2 h2. s2 = ((ex2, exs2), h2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2, auto)
[PROOF STATE]
proof (state)
this:
s2 = ((ex2, exs2), h2)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s2 = ((ex2, exs2), h2)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex2' exs2' h2' where s2': "s2' = ((ex2', exs2'), h2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex2' exs2' h2'. s2' = ((ex2', exs2'), h2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2', auto)
[PROOF STATE]
proof (state)
this:
s2' = ((ex2', exs2'), h2')

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 s1 s2
Red1_mthr.silent_move False (compP1 P) t s2 s2'
s1 = ((ex1, exs1), h1)
s2 = ((ex2, exs2), h2)
s2' = ((ex2', exs2'), h2')
[PROOF STEP]
have bisim: "bisim_list1 (ex1, exs1) (ex2, exs2)"
    and heap: "h1 = h2"
    and red: "False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2,h2\<rangle> -\<epsilon>\<rightarrow> \<langle>ex2'/exs2',h2'\<rangle>"
    and \<tau>: "\<tau>Move1 P h2 (ex2, exs2)"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2
Red1_mthr.silent_move False (compP1 P) t s2 s2'
s1 = ((ex1, exs1), h1)
s2 = ((ex2, exs2), h2)
s2' = ((ex2', exs2'), h2')

goal (1 subgoal):
 1. (bisim_list1 (ex1, exs1) (ex2, exs2) &&& h1 = h2) &&& False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2,h2\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>ex2'/exs2',h2'\<rangle> &&& \<tau>Move1 P h2 (ex2, exs2)
[PROOF STEP]
by(fastforce simp add: bisim_red0_Red1_def Red1_mthr.silent_move_iff)+
[PROOF STATE]
proof (state)
this:
bisim_list1 (ex1, exs1) (ex2, exs2)
h1 = h2
False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2,h2\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>ex2'/exs2',h2'\<rangle>
\<tau>Move1 P h2 (ex2, exs2)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from red0_simulates_Red1[OF wf red bisim] \<tau>
[PROOF STATE]
proof (chain)
picking this:
\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h2 (ex2, exs2) then (\<tau>Red0t P t h2 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1) \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> h2 = h2' else \<exists>e'' es'' ta'. \<tau>Red0r P t h2 (ex1, exs1) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call ex1 = None \<or> e'' = ex1 \<and> es'' = exs1) \<and> P,t \<turnstile>0 \<langle>e''/es'',h2\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle> \<and> \<not> \<tau>Move0 P h2 (e'', es'') \<and> red0_Red1'.ta_bisim_bisim_syntax ta' \<lbrace>\<rbrace>)
\<tau>Move1 P h2 (ex2, exs2)
[PROOF STEP]
obtain e' es' where bisim': "bisim_list1 (e', es') (ex2', exs2')"
    and red': "\<tau>Red0t P t h2 (ex1, exs1) (e', es') \<or>
               countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1"
    and [simp]: "h2' = h2"
[PROOF STATE]
proof (prove)
using this:
\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h2 (ex2, exs2) then (\<tau>Red0t P t h2 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1) \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> h2 = h2' else \<exists>e'' es'' ta'. \<tau>Red0r P t h2 (ex1, exs1) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call ex1 = None \<or> e'' = ex1 \<and> es'' = exs1) \<and> P,t \<turnstile>0 \<langle>e''/es'',h2\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle> \<and> \<not> \<tau>Move0 P h2 (e'', es'') \<and> red0_Red1'.ta_bisim_bisim_syntax ta' \<lbrace>\<rbrace>)
\<tau>Move1 P h2 (ex2, exs2)

goal (1 subgoal):
 1. (\<And>e' es'. \<lbrakk>bisim_list1 (e', es') (ex2', exs2'); \<tau>Red0t P t h2 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1; h2' = h2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bisim_list1 (e', es') (ex2', exs2')
\<tau>Red0t P t h2 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1
h2' = h2

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; Red1_mthr.silent_move False (compP1 P) t s2 s2'\<rbrakk> \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 4. wfP (\<lambda>es es'. False)
 5. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from red'
[PROOF STATE]
proof (chain)
picking this:
\<tau>Red0t P t h2 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1
[PROOF STEP]
show "bisim_red0_Red1 s1 s2' \<and> ?\<mu>2^++ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')"
    (is "?refl \<or> ?step")
[PROOF STATE]
proof (prove)
using this:
\<tau>Red0t P t h2 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1

goal (1 subgoal):
 1. bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<tau>Red0t P t h2 (ex1, exs1) (e', es') \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 2. countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1 \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
assume "\<tau>Red0t P t h2 (ex1, exs1) (e', es')"
[PROOF STATE]
proof (state)
this:
\<tau>Red0t P t h2 (ex1, exs1) (e', es')

goal (2 subgoals):
 1. \<tau>Red0t P t h2 (ex1, exs1) (e', es') \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 2. countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1 \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
from \<tau>Red0t_into_red0_\<tau>mthr_silent_movet[OF this] bisim' heap
[PROOF STATE]
proof (chain)
picking this:
red0_mthr.silent_movet P t ((ex1, exs1), h2) ((e', es'), h2)
bisim_list1 (e', es') (ex2', exs2')
h1 = h2
[PROOF STEP]
have ?step
[PROOF STATE]
proof (prove)
using this:
red0_mthr.silent_movet P t ((ex1, exs1), h2) ((e', es'), h2)
bisim_list1 (e', es') (ex2', exs2')
h1 = h2

goal (1 subgoal):
 1. \<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2'
[PROOF STEP]
unfolding s1 s2'
[PROOF STATE]
proof (prove)
using this:
red0_mthr.silent_movet P t ((ex1, exs1), h2) ((e', es'), h2)
bisim_list1 (e', es') (ex2', exs2')
h1 = h2

goal (1 subgoal):
 1. \<exists>s1'. red0_mthr.silent_movet P t ((ex1, exs1), h1) s1' \<and> bisim_red0_Red1 s1' ((ex2', exs2'), h2')
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2'

goal (2 subgoals):
 1. \<tau>Red0t P t h2 (ex1, exs1) (e', es') \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
 2. countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1 \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2'

goal (1 subgoal):
 1. bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')

goal (1 subgoal):
 1. countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1 \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1 \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
assume "countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1"
[PROOF STATE]
proof (state)
this:
countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1

goal (1 subgoal):
 1. countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1 \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
hence ?refl
[PROOF STATE]
proof (prove)
using this:
countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1

goal (1 subgoal):
 1. bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2
[PROOF STEP]
using bisim' heap
[PROOF STATE]
proof (prove)
using this:
countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1
bisim_list1 (e', es') (ex2', exs2')
h1 = h2

goal (1 subgoal):
 1. bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2
[PROOF STEP]
unfolding s1 s2' s2
[PROOF STATE]
proof (prove)
using this:
countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1
bisim_list1 (e', es') (ex2', exs2')
h1 = h2

goal (1 subgoal):
 1. bisim_red0_Red1 ((ex1, exs1), h1) ((ex2', exs2'), h2') \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ ((ex2', exs2'), h2') ((ex2, exs2), h2)
[PROOF STEP]
by (auto simp add: bisim_red0_Red1_def split_beta)
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2

goal (1 subgoal):
 1. countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1 \<Longrightarrow> bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2

goal (1 subgoal):
 1. bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2' \<and> (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. red0_mthr.silent_movet P t s1 s1' \<and> bisim_red0_Red1 s1' s2')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
fix s1 s2 ta1 s1'
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
assume "bisim_red0_Red1 s1 s2"  and "mred0 P t s1 ta1 s1'" and \<tau>: "\<not> \<tau>MOVE0 P s1 ta1 s1'"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
mred0 P t s1 ta1 s1'
\<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
mred0 P t s1 ta1 s1'
\<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex1 exs1 h1 where s1: "s1 = ((ex1, exs1), h1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex1 exs1 h1. s1 = ((ex1, exs1), h1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1, auto)
[PROOF STATE]
proof (state)
this:
s1 = ((ex1, exs1), h1)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = ((ex1, exs1), h1)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex1' exs1' h1' where s1': "s1' = ((ex1', exs1'), h1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex1' exs1' h1'. s1' = ((ex1', exs1'), h1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1', auto)
[PROOF STATE]
proof (state)
this:
s1' = ((ex1', exs1'), h1')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1' = ((ex1', exs1'), h1')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex2 exs2 h2 where s2: "s2 = ((ex2, exs2), h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex2 exs2 h2. s2 = ((ex2, exs2), h2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2, auto)
[PROOF STATE]
proof (state)
this:
s2 = ((ex2, exs2), h2)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 s1 s2
mred0 P t s1 ta1 s1'
\<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'
s1 = ((ex1, exs1), h1)
s1' = ((ex1', exs1'), h1')
s2 = ((ex2, exs2), h2)
[PROOF STEP]
have heap: "h2 = h1"
    and bisim: "bisim_list1 (ex1, exs1) (ex2, exs2)"
    and red: "P,t \<turnstile>0 \<langle>ex1/exs1,h1\<rangle> -ta1\<rightarrow> \<langle>ex1'/exs1',h1'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2
mred0 P t s1 ta1 s1'
\<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'
s1 = ((ex1, exs1), h1)
s1' = ((ex1', exs1'), h1')
s2 = ((ex2, exs2), h2)

goal (1 subgoal):
 1. h2 = h1 &&& bisim_list1 (ex1, exs1) (ex2, exs2) &&& P,t \<turnstile>0 \<langle>ex1/exs1,h1\<rangle> -ta1\<rightarrow> \<langle>ex1'/exs1',h1'\<rangle>
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
h2 = h1
bisim_list1 (ex1, exs1) (ex2, exs2)
P,t \<turnstile>0 \<langle>ex1/exs1,h1\<rangle> -ta1\<rightarrow> \<langle>ex1'/exs1',h1'\<rangle>

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from \<tau>
[PROOF STATE]
proof (chain)
picking this:
\<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'
[PROOF STEP]
have "\<not> \<tau>Move0 P h1 (ex1, exs1)"
[PROOF STATE]
proof (prove)
using this:
\<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'

goal (1 subgoal):
 1. \<not> \<tau>Move0 P h1 (ex1, exs1)
[PROOF STEP]
unfolding s1
[PROOF STATE]
proof (prove)
using this:
\<not> (case ((ex1, exs1), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'

goal (1 subgoal):
 1. \<not> \<tau>Move0 P h1 (ex1, exs1)
[PROOF STEP]
using red
[PROOF STATE]
proof (prove)
using this:
\<not> (case ((ex1, exs1), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'
P,t \<turnstile>0 \<langle>ex1/exs1,h1\<rangle> -ta1\<rightarrow> \<langle>ex1'/exs1',h1'\<rangle>

goal (1 subgoal):
 1. \<not> \<tau>Move0 P h1 (ex1, exs1)
[PROOF STEP]
by(auto elim!: red0.cases dest: red_\<tau>_taD[where extTA="extTA2J0 P", OF extTA2J0_\<epsilon>])
[PROOF STATE]
proof (state)
this:
\<not> \<tau>Move0 P h1 (ex1, exs1)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
with Red1_simulates_red0[OF wf red bisim]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ex2'' exs2''. bisim_list1 (ex1', exs1') (ex2'', exs2'') \<and> (if \<tau>Move0 P h1 (ex1, exs1) then \<tau>Red1't (compP1 P) t h1 (ex2, exs2) (ex2'', exs2'') \<and> ta1 = \<lbrace>\<rbrace> \<and> h1 = h1' else \<exists>ex2' exs2' ta'. \<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2') \<and> (call ex1 = None \<or> call1 (fst ex2) = None \<or> ex2' = ex2 \<and> exs2' = exs2) \<and> False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle> \<and> \<not> \<tau>Move1 P h1 (ex2', exs2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta')
\<not> \<tau>Move0 P h1 (ex1, exs1)
[PROOF STEP]
obtain ex2'' exs2'' ex2' exs2' ta'
    where bisim': "bisim_list1 (ex1', exs1') (ex2'', exs2'')"
    and red': "\<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2')"
    and red'': "False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle>"
    and \<tau>': "\<not> \<tau>Move1 P h1 (ex2', exs2')"
    and ta: "ta_bisim01 ta1 ta'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ex2'' exs2''. bisim_list1 (ex1', exs1') (ex2'', exs2'') \<and> (if \<tau>Move0 P h1 (ex1, exs1) then \<tau>Red1't (compP1 P) t h1 (ex2, exs2) (ex2'', exs2'') \<and> ta1 = \<lbrace>\<rbrace> \<and> h1 = h1' else \<exists>ex2' exs2' ta'. \<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2') \<and> (call ex1 = None \<or> call1 (fst ex2) = None \<or> ex2' = ex2 \<and> exs2' = exs2) \<and> False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle> \<and> \<not> \<tau>Move1 P h1 (ex2', exs2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta')
\<not> \<tau>Move0 P h1 (ex1, exs1)

goal (1 subgoal):
 1. (\<And>ex2'' exs2'' ex2' exs2' ta'. \<lbrakk>bisim_list1 (ex1', exs1') (ex2'', exs2''); \<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2'); False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle>; \<not> \<tau>Move1 P h1 (ex2', exs2'); red0_Red1'.ta_bisim_bisim_syntax ta1 ta'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bisim_list1 (ex1', exs1') (ex2'', exs2'')
\<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2')
False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle>
\<not> \<tau>Move1 P h1 (ex2', exs2')
red0_Red1'.ta_bisim_bisim_syntax ta1 ta'

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from red''
[PROOF STATE]
proof (chain)
picking this:
False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle>
[PROOF STEP]
have "mred1' (compP1 P) t ((ex2', exs2'), h1) ta' ((ex2'', exs2''), h1')"
[PROOF STATE]
proof (prove)
using this:
False,compP1 P,t \<turnstile>1 \<langle>ex2'/exs2',h1\<rangle> -ta'\<rightarrow> \<langle>ex2''/exs2'',h1'\<rangle>

goal (1 subgoal):
 1. Red1_mthr.r_syntax False (compP1 P) t (ex2', exs2') h1 ta' (ex2'', exs2'') h1'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Red1_mthr.r_syntax False (compP1 P) t (ex2', exs2') h1 ta' (ex2'', exs2'') h1'

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Red1_mthr.r_syntax False (compP1 P) t (ex2', exs2') h1 ta' (ex2'', exs2'') h1'

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from \<tau>'
[PROOF STATE]
proof (chain)
picking this:
\<not> \<tau>Move1 P h1 (ex2', exs2')
[PROOF STEP]
have "\<not> \<tau>MOVE1 (compP1 P) ((ex2', exs2'), h1) ta' ((ex2'', exs2''), h1')"
[PROOF STATE]
proof (prove)
using this:
\<not> \<tau>Move1 P h1 (ex2', exs2')

goal (1 subgoal):
 1. \<not> (case ((ex2', exs2'), h1) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta' ((ex2'', exs2''), h1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (case ((ex2', exs2'), h1) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta' ((ex2'', exs2''), h1')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> (case ((ex2', exs2'), h1) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta' ((ex2'', exs2''), h1')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from red'
[PROOF STATE]
proof (chain)
picking this:
\<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2')
[PROOF STEP]
have "Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)"
[PROOF STATE]
proof (prove)
using this:
\<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2')

goal (1 subgoal):
 1. Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)
[PROOF STEP]
unfolding s2 heap
[PROOF STATE]
proof (prove)
using this:
\<tau>Red1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2')

goal (1 subgoal):
 1. Red1_mthr.silent_moves False (compP1 P) t ((ex2, exs2), h1) ((ex2', exs2'), h1)
[PROOF STEP]
by(rule \<tau>Red1'r_into_Red1'_\<tau>mthr_silent_moves)
[PROOF STATE]
proof (state)
this:
Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from bisim'
[PROOF STATE]
proof (chain)
picking this:
bisim_list1 (ex1', exs1') (ex2'', exs2'')
[PROOF STEP]
have "bisim_red0_Red1 ((ex1', exs1'), h1') ((ex2'', exs2''), h1')"
[PROOF STATE]
proof (prove)
using this:
bisim_list1 (ex1', exs1') (ex2'', exs2'')

goal (1 subgoal):
 1. bisim_red0_Red1 ((ex1', exs1'), h1') ((ex2'', exs2''), h1')
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 ((ex1', exs1'), h1') ((ex2'', exs2''), h1')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>bisim_red0_Red1 s1 s2; mred0 P t s1 tl1 s1'; \<not> (case s1 of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 3. wfP (\<lambda>es es'. False)
 4. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Red1_mthr.r_syntax False (compP1 P) t (ex2', exs2') h1 ta' (ex2'', exs2'') h1'
\<not> (case ((ex2', exs2'), h1) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta' ((ex2'', exs2''), h1')
Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)
bisim_red0_Red1 ((ex1', exs1'), h1') ((ex2'', exs2''), h1')
[PROOF STEP]
show "\<exists>s2' s2'' ta2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' ta2 s2'' \<and>
             \<not> \<tau>MOVE1 (compP1 P) s2' ta2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> ta_bisim01 ta1 ta2"
[PROOF STATE]
proof (prove)
using this:
Red1_mthr.r_syntax False (compP1 P) t (ex2', exs2') h1 ta' (ex2'', exs2'') h1'
\<not> (case ((ex2', exs2'), h1) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta' ((ex2'', exs2''), h1')
Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)
bisim_red0_Red1 ((ex1', exs1'), h1') ((ex2'', exs2''), h1')

goal (1 subgoal):
 1. \<exists>s2' s2'' ta2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' ta2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
[PROOF STEP]
using ta
[PROOF STATE]
proof (prove)
using this:
Red1_mthr.r_syntax False (compP1 P) t (ex2', exs2') h1 ta' (ex2'', exs2'') h1'
\<not> (case ((ex2', exs2'), h1) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta' ((ex2'', exs2''), h1')
Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)
bisim_red0_Red1 ((ex1', exs1'), h1') ((ex2'', exs2''), h1')
red0_Red1'.ta_bisim_bisim_syntax ta1 ta'

goal (1 subgoal):
 1. \<exists>s2' s2'' ta2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' ta2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
[PROOF STEP]
unfolding s1'
[PROOF STATE]
proof (prove)
using this:
Red1_mthr.r_syntax False (compP1 P) t (ex2', exs2') h1 ta' (ex2'', exs2'') h1'
\<not> (case ((ex2', exs2'), h1) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta' ((ex2'', exs2''), h1')
Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)
bisim_red0_Red1 ((ex1', exs1'), h1') ((ex2'', exs2''), h1')
red0_Red1'.ta_bisim_bisim_syntax ta1 ta'

goal (1 subgoal):
 1. \<exists>s2' s2'' ta2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' ta2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'' \<and> bisim_red0_Red1 ((ex1', exs1'), h1') s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s2' s2'' ta2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' \<and> mred1' (compP1 P) t s2' ta2 s2'' \<and> \<not> (case s2' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'' \<and> bisim_red0_Red1 s1' s2'' \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
fix s1 s2 ta2 s2'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
assume "bisim_red0_Red1 s1 s2"  and "mred1' (compP1 P) t s2 ta2 s2'" and \<tau>: "\<not> \<tau>MOVE1 (compP1 P) s2 ta2 s2'"
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
mred1' (compP1 P) t s2 ta2 s2'
\<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 s1 s2
mred1' (compP1 P) t s2 ta2 s2'
\<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex1 exs1 h1 where s1: "s1 = ((ex1, exs1), h1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex1 exs1 h1. s1 = ((ex1, exs1), h1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1, auto)
[PROOF STATE]
proof (state)
this:
s1 = ((ex1, exs1), h1)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = ((ex1, exs1), h1)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex2 exs2 h2 where s2: "s2 = ((ex2, exs2), h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex2 exs2 h2. s2 = ((ex2, exs2), h2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2, auto)
[PROOF STATE]
proof (state)
this:
s2 = ((ex2, exs2), h2)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s2 = ((ex2, exs2), h2)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
obtain ex2' exs2' h2' where s2': "s2' = ((ex2', exs2'), h2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex2' exs2' h2'. s2' = ((ex2', exs2'), h2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2', auto)
[PROOF STATE]
proof (state)
this:
s2' = ((ex2', exs2'), h2')

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_red0_Red1 s1 s2
mred1' (compP1 P) t s2 ta2 s2'
\<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'
s1 = ((ex1, exs1), h1)
s2 = ((ex2, exs2), h2)
s2' = ((ex2', exs2'), h2')
[PROOF STEP]
have heap: "h2 = h1"
    and bisim: "bisim_list1 (ex1, exs1) (ex2, exs2)"
    and red: "False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2,h1\<rangle> -ta2\<rightarrow> \<langle>ex2'/exs2',h2'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
bisim_red0_Red1 s1 s2
mred1' (compP1 P) t s2 ta2 s2'
\<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'
s1 = ((ex1, exs1), h1)
s2 = ((ex2, exs2), h2)
s2' = ((ex2', exs2'), h2')

goal (1 subgoal):
 1. h2 = h1 &&& bisim_list1 (ex1, exs1) (ex2, exs2) &&& False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2,h1\<rangle> -ta2\<rightarrow> \<langle>ex2'/exs2',h2'\<rangle>
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
h2 = h1
bisim_list1 (ex1, exs1) (ex2, exs2)
False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2,h1\<rangle> -ta2\<rightarrow> \<langle>ex2'/exs2',h2'\<rangle>

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from \<tau> heap
[PROOF STATE]
proof (chain)
picking this:
\<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'
h2 = h1
[PROOF STEP]
have "\<not> \<tau>Move1 P h2 (ex2, exs2)"
[PROOF STATE]
proof (prove)
using this:
\<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'
h2 = h1

goal (1 subgoal):
 1. \<not> \<tau>Move1 P h2 (ex2, exs2)
[PROOF STEP]
unfolding s2
[PROOF STATE]
proof (prove)
using this:
\<not> (case ((ex2, exs2), h2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'
h2 = h1

goal (1 subgoal):
 1. \<not> \<tau>Move1 P h2 (ex2, exs2)
[PROOF STEP]
using red
[PROOF STATE]
proof (prove)
using this:
\<not> (case ((ex2, exs2), h2) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) ta2 s2'
h2 = h1
False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2,h1\<rangle> -ta2\<rightarrow> \<langle>ex2'/exs2',h2'\<rangle>

goal (1 subgoal):
 1. \<not> \<tau>Move1 P h2 (ex2, exs2)
[PROOF STEP]
by(fastforce elim!: Red1.cases dest: red1_\<tau>_taD)
[PROOF STATE]
proof (state)
this:
\<not> \<tau>Move1 P h2 (ex2, exs2)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
with red0_simulates_Red1[OF wf red bisim]
[PROOF STATE]
proof (chain)
picking this:
\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h1 (ex2, exs2) then (\<tau>Red0t P t h1 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1) \<and> ta2 = \<lbrace>\<rbrace> \<and> h1 = h2' else \<exists>e'' es'' ta'. \<tau>Red0r P t h1 (ex1, exs1) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call ex1 = None \<or> e'' = ex1 \<and> es'' = exs1) \<and> P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle> \<and> \<not> \<tau>Move0 P h1 (e'', es'') \<and> red0_Red1'.ta_bisim_bisim_syntax ta' ta2)
\<not> \<tau>Move1 P h2 (ex2, exs2)
[PROOF STEP]
obtain e' es' e'' es'' ta'
    where bisim': "bisim_list1 (e', es') (ex2', exs2')"
    and red': "\<tau>Red0r P t h1 (ex1, exs1) (e'', es'')"
    and red'': "P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle>"
    and \<tau>': "\<not> \<tau>Move0 P h1 (e'', es'')"
    and ta: "ta_bisim01 ta' ta2"
[PROOF STATE]
proof (prove)
using this:
\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h1 (ex2, exs2) then (\<tau>Red0t P t h1 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1) \<and> ta2 = \<lbrace>\<rbrace> \<and> h1 = h2' else \<exists>e'' es'' ta'. \<tau>Red0r P t h1 (ex1, exs1) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call ex1 = None \<or> e'' = ex1 \<and> es'' = exs1) \<and> P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle> \<and> \<not> \<tau>Move0 P h1 (e'', es'') \<and> red0_Red1'.ta_bisim_bisim_syntax ta' ta2)
\<not> \<tau>Move1 P h2 (ex2, exs2)

goal (1 subgoal):
 1. (\<And>e' es' e'' es'' ta'. \<lbrakk>bisim_list1 (e', es') (ex2', exs2'); \<tau>Red0r P t h1 (ex1, exs1) (e'', es''); P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle>; \<not> \<tau>Move0 P h1 (e'', es''); red0_Red1'.ta_bisim_bisim_syntax ta' ta2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using heap
[PROOF STATE]
proof (prove)
using this:
\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h1 (ex2, exs2) then (\<tau>Red0t P t h1 (ex1, exs1) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = ex1 \<and> es' = exs1) \<and> ta2 = \<lbrace>\<rbrace> \<and> h1 = h2' else \<exists>e'' es'' ta'. \<tau>Red0r P t h1 (ex1, exs1) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call ex1 = None \<or> e'' = ex1 \<and> es'' = exs1) \<and> P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle> \<and> \<not> \<tau>Move0 P h1 (e'', es'') \<and> red0_Red1'.ta_bisim_bisim_syntax ta' ta2)
\<not> \<tau>Move1 P h2 (ex2, exs2)
h2 = h1

goal (1 subgoal):
 1. (\<And>e' es' e'' es'' ta'. \<lbrakk>bisim_list1 (e', es') (ex2', exs2'); \<tau>Red0r P t h1 (ex1, exs1) (e'', es''); P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle>; \<not> \<tau>Move0 P h1 (e'', es''); red0_Red1'.ta_bisim_bisim_syntax ta' ta2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bisim_list1 (e', es') (ex2', exs2')
\<tau>Red0r P t h1 (ex1, exs1) (e'', es'')
P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle>
\<not> \<tau>Move0 P h1 (e'', es'')
red0_Red1'.ta_bisim_bisim_syntax ta' ta2

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from red''
[PROOF STATE]
proof (chain)
picking this:
P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle>
[PROOF STEP]
have "mred0 P t ((e'', es''), h1) ta' ((e', es'), h2')"
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile>0 \<langle>e''/es'',h1\<rangle> -ta'\<rightarrow> \<langle>e'/es',h2'\<rangle>

goal (1 subgoal):
 1. red0_mthr.r_syntax P t (e'', es'') h1 ta' (e', es') h2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
red0_mthr.r_syntax P t (e'', es'') h1 ta' (e', es') h2'

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
red0_mthr.r_syntax P t (e'', es'') h1 ta' (e', es') h2'

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from red'
[PROOF STATE]
proof (chain)
picking this:
\<tau>Red0r P t h1 (ex1, exs1) (e'', es'')
[PROOF STEP]
have "red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)"
[PROOF STATE]
proof (prove)
using this:
\<tau>Red0r P t h1 (ex1, exs1) (e'', es'')

goal (1 subgoal):
 1. red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)
[PROOF STEP]
by(rule \<tau>Red0r_into_red0_\<tau>mthr_silent_moves)
[PROOF STATE]
proof (state)
this:
red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from \<tau>'
[PROOF STATE]
proof (chain)
picking this:
\<not> \<tau>Move0 P h1 (e'', es'')
[PROOF STEP]
have "\<not> \<tau>MOVE0 P ((e'', es''), h1) ta' ((e', es'), h2')"
[PROOF STATE]
proof (prove)
using this:
\<not> \<tau>Move0 P h1 (e'', es'')

goal (1 subgoal):
 1. \<not> (case ((e'', es''), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta' ((e', es'), h2')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> (case ((e'', es''), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta' ((e', es'), h2')

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> (case ((e'', es''), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta' ((e', es'), h2')

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
from bisim'
[PROOF STATE]
proof (chain)
picking this:
bisim_list1 (e', es') (ex2', exs2')
[PROOF STEP]
have "bisim_red0_Red1 ((e', es'), h2') ((ex2', exs2'), h2')"
[PROOF STATE]
proof (prove)
using this:
bisim_list1 (e', es') (ex2', exs2')

goal (1 subgoal):
 1. bisim_red0_Red1 ((e', es'), h2') ((ex2', exs2'), h2')
[PROOF STEP]
by(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (state)
this:
bisim_red0_Red1 ((e', es'), h2') ((ex2', exs2'), h2')

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>bisim_red0_Red1 s1 s2; mred1' (compP1 P) t s2 tl2 s2'; \<not> (case s2 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' tl1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax tl1 tl2
 2. wfP (\<lambda>es es'. False)
 3. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
red0_mthr.r_syntax P t (e'', es'') h1 ta' (e', es') h2'
red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)
\<not> (case ((e'', es''), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta' ((e', es'), h2')
bisim_red0_Red1 ((e', es'), h2') ((ex2', exs2'), h2')
[PROOF STEP]
show "\<exists>s1' s1'' ta1. red0_mthr.silent_moves P t s1 s1' \<and>
             mred0 P t s1' ta1 s1'' \<and> \<not> \<tau>MOVE0 P s1' ta1 s1'' \<and>
             bisim_red0_Red1 s1'' s2' \<and> ta_bisim01 ta1 ta2"
[PROOF STATE]
proof (prove)
using this:
red0_mthr.r_syntax P t (e'', es'') h1 ta' (e', es') h2'
red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)
\<not> (case ((e'', es''), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta' ((e', es'), h2')
bisim_red0_Red1 ((e', es'), h2') ((ex2', exs2'), h2')

goal (1 subgoal):
 1. \<exists>s1' s1'' ta1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' ta1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
[PROOF STEP]
using ta
[PROOF STATE]
proof (prove)
using this:
red0_mthr.r_syntax P t (e'', es'') h1 ta' (e', es') h2'
red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)
\<not> (case ((e'', es''), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta' ((e', es'), h2')
bisim_red0_Red1 ((e', es'), h2') ((ex2', exs2'), h2')
red0_Red1'.ta_bisim_bisim_syntax ta' ta2

goal (1 subgoal):
 1. \<exists>s1' s1'' ta1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' ta1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
[PROOF STEP]
unfolding s1 s2'
[PROOF STATE]
proof (prove)
using this:
red0_mthr.r_syntax P t (e'', es'') h1 ta' (e', es') h2'
red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)
\<not> (case ((e'', es''), h1) of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta' ((e', es'), h2')
bisim_red0_Red1 ((e', es'), h2') ((ex2', exs2'), h2')
red0_Red1'.ta_bisim_bisim_syntax ta' ta2

goal (1 subgoal):
 1. \<exists>s1' s1'' ta1. red0_mthr.silent_moves P t ((ex1, exs1), h1) s1' \<and> mred0 P t s1' ta1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'' \<and> bisim_red0_Red1 s1'' ((ex2', exs2'), h2') \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s1' s1'' ta1. red0_mthr.silent_moves P t s1 s1' \<and> mred0 P t s1' ta1 s1'' \<and> \<not> (case s1' of (es, h) \<Rightarrow> \<lambda>ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ta1 s1'' \<and> bisim_red0_Red1 s1'' s2' \<and> red0_Red1'.ta_bisim_bisim_syntax ta1 ta2

goal (2 subgoals):
 1. wfP (\<lambda>es es'. False)
 2. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wfP (\<lambda>es es'. False)
 2. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
show "wfP ?\<mu>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wfP (\<lambda>es es'. False)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wfP (\<lambda>es es'. False)

goal (1 subgoal):
 1. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
have "wf (measure countInitBlock)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (measure countInitBlock)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
wf (measure countInitBlock)

goal (1 subgoal):
 1. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
hence "wf (inv_image (measure countInitBlock) (\<lambda>(((e', xs'), exs'), h'). e'))"
[PROOF STATE]
proof (prove)
using this:
wf (measure countInitBlock)

goal (1 subgoal):
 1. wf (inv_image (measure countInitBlock) (\<lambda>(((e', xs'), exs'), h'). e'))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
wf (inv_image (measure countInitBlock) (\<lambda>(((e', xs'), exs'), h'). e'))

goal (1 subgoal):
 1. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wf (inv_image (measure countInitBlock) (\<lambda>(((e', xs'), exs'), h'). e'))

goal (1 subgoal):
 1. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
have "inv_image (measure countInitBlock) (\<lambda>(((e', xs'), exs'), h'). e') = {(s2', s2). ?\<mu>2 s2' s2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_image (measure countInitBlock) (\<lambda>(((e', xs'), exs'), h'). e') = {(s2', s2). (case s2' of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e', xs') \<Rightarrow> \<lambda>exs' h' (((e, xs), exs), h). countInitBlock e' < countInitBlock e) xa) xa) s2}
[PROOF STEP]
by(simp add: inv_image_def split_beta)
[PROOF STATE]
proof (state)
this:
inv_image (measure countInitBlock) (\<lambda>(((e', xs'), exs'), h'). e') = {(s2', s2). (case s2' of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e', xs') \<Rightarrow> \<lambda>exs' h' (((e, xs), exs), h). countInitBlock e' < countInitBlock e) xa) xa) s2}

goal (1 subgoal):
 1. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wf {(s2', s2). (case s2' of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e', xs') \<Rightarrow> \<lambda>exs' h' (((e, xs), exs), h). countInitBlock e' < countInitBlock e) xa) xa) s2}
[PROOF STEP]
show "wfP ?\<mu>2"
[PROOF STATE]
proof (prove)
using this:
wf {(s2', s2). (case s2' of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e', xs') \<Rightarrow> \<lambda>exs' h' (((e, xs), exs), h). countInitBlock e' < countInitBlock e) xa) xa) s2}

goal (1 subgoal):
 1. wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
by(simp add: wfP_def)
[PROOF STATE]
proof (state)
this:
wfP (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)

goal:
No subgoals!
[PROOF STEP]
qed