[STATEMENT]
lemma Red1_execd_weak_bisim:
  assumes wf: "wf_J1_prog P"
  shows "delay_bisimulation_measure (mred1 P t) (mexecd (compP2 P) t) (wbisim1 t) (ta_bisim wbisim1) (\<tau>MOVE1 P) (\<tau>MOVE2 (compP2 P)) (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e') (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_measure (mred1 P t) (mexecd (compP2 P) t) (wbisim1 t) (ta_bisim wbisim1) (\<lambda>(exexs, h) ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) (\<lambda>((xcp, frs), h) ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e') (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
fix s1 s2 s1'
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
assume "wbisim1 t s1 s2" and "\<tau>trsys.silent_move (mred1 P t) (\<tau>MOVE1 P) s1 s1'"
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2
Red1_mthr.silent_move True P t s1 s1'

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2
Red1_mthr.silent_move True P t s1 s1'

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain e xs exs h where s1: "s1 = (((e, xs), exs), h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e xs exs h. s1 = (((e, xs), exs), h) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1) auto
[PROOF STATE]
proof (state)
this:
s1 = (((e, xs), exs), h)

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (((e, xs), exs), h)

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain e' xs' exs' h1' where s1': "s1' = (((e', xs'), exs'), h1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e' xs' exs' h1'. s1' = (((e', xs'), exs'), h1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1') auto
[PROOF STATE]
proof (state)
this:
s1' = (((e', xs'), exs'), h1')

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1' = (((e', xs'), exs'), h1')

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain xcp frs h2 where s2: "s2 = ((xcp, frs), h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp frs h2. s2 = ((xcp, frs), h2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2) auto
[PROOF STATE]
proof (state)
this:
s2 = ((xcp, frs), h2)

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wbisim1 t s1 s2
Red1_mthr.silent_move True P t s1 s1'
s1 = (((e, xs), exs), h)
s1' = (((e', xs'), exs'), h1')
s2 = ((xcp, frs), h2)
[PROOF STEP]
have [simp]: "h2 = h" and red: "True,P,t \<turnstile>1 \<langle>(e, xs)/exs,h\<rangle> -\<epsilon>\<rightarrow> \<langle>(e', xs')/exs',h1'\<rangle>"
    and \<tau>: "\<tau>Move1 P h ((e, xs), exs)" and bisim: "bisim1_list1 t h (e, xs) exs xcp frs"
[PROOF STATE]
proof (prove)
using this:
wbisim1 t s1 s2
Red1_mthr.silent_move True P t s1 s1'
s1 = (((e, xs), exs), h)
s1' = (((e', xs'), exs'), h1')
s2 = ((xcp, frs), h2)

goal (1 subgoal):
 1. (h2 = h &&& True,P,t \<turnstile>1 \<langle>(e, xs)/exs,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>(e', xs')/exs',h1'\<rangle>) &&& \<tau>Move1 P h ((e, xs), exs) &&& bisim1_list1 t h (e, xs) exs xcp frs
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
h2 = h
True,P,t \<turnstile>1 \<langle>(e, xs)/exs,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>(e', xs')/exs',h1'\<rangle>
\<tau>Move1 P h ((e, xs), exs)
bisim1_list1 t h (e, xs) exs xcp frs

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from red \<tau> bisim
[PROOF STATE]
proof (chain)
picking this:
True,P,t \<turnstile>1 \<langle>(e, xs)/exs,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>(e', xs')/exs',h1'\<rangle>
\<tau>Move1 P h ((e, xs), exs)
bisim1_list1 t h (e, xs) exs xcp frs
[PROOF STEP]
have h1' [simp]: "h1' = h"
[PROOF STATE]
proof (prove)
using this:
True,P,t \<turnstile>1 \<langle>(e, xs)/exs,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>(e', xs')/exs',h1'\<rangle>
\<tau>Move1 P h ((e, xs), exs)
bisim1_list1 t h (e, xs) exs xcp frs

goal (1 subgoal):
 1. h1' = h
[PROOF STEP]
by(auto dest: \<tau>move1_heap_unchanged elim!: Red1.cases bisim1_list1.cases)
[PROOF STATE]
proof (state)
this:
h1' = h

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from exec_1_simulates_Red1_\<tau>[OF wf red[unfolded h1'] bisim \<tau>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xcp' frs'. (if sim12_size e' < sim12_size e then \<tau>Exec_1_dr else \<tau>Exec_1_dt) (compP2 P) t (xcp, h, frs) (xcp', h, frs') \<and> bisim1_list1 t h (e', xs') exs' xcp' frs'
[PROOF STEP]
obtain xcp' frs'
    where exec: "(if sim12_size e' < sim12_size e then \<tau>Exec_1_dr else \<tau>Exec_1_dt) (compP2 P) t (xcp, h, frs) (xcp', h, frs')"
    and bisim': "bisim1_list1 t h (e', xs') exs' xcp' frs'"
[PROOF STATE]
proof (prove)
using this:
\<exists>xcp' frs'. (if sim12_size e' < sim12_size e then \<tau>Exec_1_dr else \<tau>Exec_1_dt) (compP2 P) t (xcp, h, frs) (xcp', h, frs') \<and> bisim1_list1 t h (e', xs') exs' xcp' frs'

goal (1 subgoal):
 1. (\<And>xcp' frs'. \<lbrakk>(if sim12_size e' < sim12_size e then \<tau>Exec_1_dr else \<tau>Exec_1_dt) (compP2 P) t (xcp, h, frs) (xcp', h, frs'); bisim1_list1 t h (e', xs') exs' xcp' frs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(if sim12_size e' < sim12_size e then \<tau>Exec_1_dr else \<tau>Exec_1_dt) (compP2 P) t (xcp, h, frs) (xcp', h, frs')
bisim1_list1 t h (e', xs') exs' xcp' frs'

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
(if sim12_size e' < sim12_size e then \<tau>Exec_1_dr else \<tau>Exec_1_dt) (compP2 P) t (xcp, h, frs) (xcp', h, frs')
[PROOF STEP]
have "(if (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e') (((e', xs'), exs'), h) (((e, xs), exs), h) then \<tau>trsys.silent_moves (mexecd (compP2 P) t) (\<tau>MOVE2 (compP2 P)) else \<tau>trsys.silent_movet (mexecd (compP2 P) t) (\<tau>MOVE2 (compP2 P))) ((xcp, frs), h) ((xcp', frs'), h)"
[PROOF STATE]
proof (prove)
using this:
(if sim12_size e' < sim12_size e then \<tau>Exec_1_dr else \<tau>Exec_1_dt) (compP2 P) t (xcp, h, frs) (xcp', h, frs')

goal (1 subgoal):
 1. (if (case (((e', xs'), exs'), h) of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) (((e, xs), exs), h) then execd_mthr.silent_moves (compP2 P) t else execd_mthr.silent_movet (compP2 P) t) ((xcp, frs), h) ((xcp', frs'), h)
[PROOF STEP]
by(auto simp add: \<tau>Exec_1_dr_conv_rtranclp \<tau>Exec_1_dt_conv_tranclp)
[PROOF STATE]
proof (state)
this:
(if (case (((e', xs'), exs'), h) of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) (((e, xs), exs), h) then execd_mthr.silent_moves (compP2 P) t else execd_mthr.silent_movet (compP2 P) t) ((xcp, frs), h) ((xcp', frs'), h)

goal (6 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s1'. \<lbrakk>wbisim1 t s1 s2; Red1_mthr.silent_move True P t s1 s1'\<rbrakk> \<Longrightarrow> wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
 4. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 5. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 6. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
thus "wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or>
       (\<exists>s2'. (\<tau>trsys.silent_movet (mexecd (compP2 P) t) (\<tau>MOVE2 (compP2 P))) s2 s2' \<and> wbisim1 t s1' s2')"
[PROOF STATE]
proof (prove)
using this:
(if (case (((e', xs'), exs'), h) of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) (((e, xs), exs), h) then execd_mthr.silent_moves (compP2 P) t else execd_mthr.silent_movet (compP2 P) t) ((xcp, frs), h) ((xcp', frs'), h)

goal (1 subgoal):
 1. wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
[PROOF STEP]
using bisim' s1 s1' s2
[PROOF STATE]
proof (prove)
using this:
(if (case (((e', xs'), exs'), h) of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) (((e, xs), exs), h) then execd_mthr.silent_moves (compP2 P) t else execd_mthr.silent_movet (compP2 P) t) ((xcp, frs), h) ((xcp', frs'), h)
bisim1_list1 t h (e', xs') exs' xcp' frs'
s1 = (((e, xs), exs), h)
s1' = (((e', xs'), exs'), h1')
s2 = ((xcp, frs), h2)

goal (1 subgoal):
 1. wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')
[PROOF STEP]
by -(rule delay_bisimulation_base.simulation_silent1I', auto split del: if_split)
[PROOF STATE]
proof (state)
this:
wbisim1 t s1' s2 \<and> (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')\<^sup>+\<^sup>+ s1' s1 \<or> (\<exists>s2'. execd_mthr.silent_movet (compP2 P) t s2 s2' \<and> wbisim1 t s1' s2')

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
fix s1 s2 s2'
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
assume "wbisim1 t s1 s2" and "\<tau>trsys.silent_move (mexecd (compP2 P) t) (\<tau>MOVE2 (compP2 P)) s2 s2'"
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2
execd_mthr.silent_move (compP2 P) t s2 s2'

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2
execd_mthr.silent_move (compP2 P) t s2 s2'

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain e xs exs h1 where s1: "s1 = (((e, xs), exs), h1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e xs exs h1. s1 = (((e, xs), exs), h1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1) auto
[PROOF STATE]
proof (state)
this:
s1 = (((e, xs), exs), h1)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (((e, xs), exs), h1)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain xcp frs h where s2: "s2 = ((xcp, frs), h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp frs h. s2 = ((xcp, frs), h) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2) auto
[PROOF STATE]
proof (state)
this:
s2 = ((xcp, frs), h)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s2 = ((xcp, frs), h)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain xcp' frs' h2' where s2': "s2' = ((xcp', frs'), h2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp' frs' h2'. s2' = ((xcp', frs'), h2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2') auto
[PROOF STATE]
proof (state)
this:
s2' = ((xcp', frs'), h2')

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wbisim1 t s1 s2
execd_mthr.silent_move (compP2 P) t s2 s2'
s1 = (((e, xs), exs), h1)
s2 = ((xcp, frs), h)
s2' = ((xcp', frs'), h2')
[PROOF STEP]
have [simp]: "h1 = h" and exec: "exec_1_d (compP2 P) t (Normal (xcp, h, frs)) \<epsilon> (Normal (xcp', h2', frs'))"
    and \<tau>: "\<tau>Move2 (compP2 P) (xcp, h, frs)" and bisim: "bisim1_list1 t h (e, xs) exs xcp frs"
[PROOF STATE]
proof (prove)
using this:
wbisim1 t s1 s2
execd_mthr.silent_move (compP2 P) t s2 s2'
s1 = (((e, xs), exs), h1)
s2 = ((xcp, frs), h)
s2' = ((xcp', frs'), h2')

goal (1 subgoal):
 1. (h1 = h &&& compP2 P,t \<turnstile> Normal (xcp, h, frs) -\<lbrace>\<rbrace>-jvmd\<rightarrow> Normal (xcp', h2', frs')) &&& \<tau>Move2 (compP2 P) (xcp, h, frs) &&& bisim1_list1 t h (e, xs) exs xcp frs
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
h1 = h
compP2 P,t \<turnstile> Normal (xcp, h, frs) -\<lbrace>\<rbrace>-jvmd\<rightarrow> Normal (xcp', h2', frs')
\<tau>Move2 (compP2 P) (xcp, h, frs)
bisim1_list1 t h (e, xs) exs xcp frs

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from \<tau>Red1_simulates_exec_1_\<tau>[OF wf exec bisim \<tau>]
[PROOF STATE]
proof (chain)
picking this:
h = h2' \<and> (\<exists>e' xs' exs'. (if sim21_size (compP2 P) (xcp', frs') (xcp, frs) then \<tau>Red1r else \<tau>Red1t) P t h ((e, xs), exs) ((e', xs'), exs') \<and> bisim1_list1 t h (e', xs') exs' xcp' frs')
[PROOF STEP]
obtain e' xs' exs' where [simp]: "h2' = h"
    and red: "(if sim21_size (compP2 P) (xcp', frs') (xcp, frs) then \<tau>Red1r else \<tau>Red1t) P t h ((e, xs), exs) ((e', xs'), exs')"
    and bisim': "bisim1_list1 t h (e', xs') exs' xcp' frs'"
[PROOF STATE]
proof (prove)
using this:
h = h2' \<and> (\<exists>e' xs' exs'. (if sim21_size (compP2 P) (xcp', frs') (xcp, frs) then \<tau>Red1r else \<tau>Red1t) P t h ((e, xs), exs) ((e', xs'), exs') \<and> bisim1_list1 t h (e', xs') exs' xcp' frs')

goal (1 subgoal):
 1. (\<And>e' xs' exs'. \<lbrakk>h2' = h; (if sim21_size (compP2 P) (xcp', frs') (xcp, frs) then \<tau>Red1r else \<tau>Red1t) P t h ((e, xs), exs) ((e', xs'), exs'); bisim1_list1 t h (e', xs') exs' xcp' frs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h2' = h
(if sim21_size (compP2 P) (xcp', frs') (xcp, frs) then \<tau>Red1r else \<tau>Red1t) P t h ((e, xs), exs) ((e', xs'), exs')
bisim1_list1 t h (e', xs') exs' xcp' frs'

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from red
[PROOF STATE]
proof (chain)
picking this:
(if sim21_size (compP2 P) (xcp', frs') (xcp, frs) then \<tau>Red1r else \<tau>Red1t) P t h ((e, xs), exs) ((e', xs'), exs')
[PROOF STEP]
have "(if ((\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') ((xcp', frs'), h2') ((xcp, frs), h)) then \<tau>trsys.silent_moves (mred1 P t) (\<tau>MOVE1 P) else \<tau>trsys.silent_movet (mred1 P t) (\<tau>MOVE1 P)) (((e, xs), exs), h) (((e', xs'), exs'), h)"
[PROOF STATE]
proof (prove)
using this:
(if sim21_size (compP2 P) (xcp', frs') (xcp, frs) then \<tau>Red1r else \<tau>Red1t) P t h ((e, xs), exs) ((e', xs'), exs')

goal (1 subgoal):
 1. (if (case ((xcp', frs'), h2') of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') ((xcp, frs), h) then Red1_mthr.silent_moves True P t else Red1_mthr.silent_movet True P t) (((e, xs), exs), h) (((e', xs'), exs'), h)
[PROOF STEP]
by(auto dest: \<tau>Red1r_rtranclpD \<tau>Red1t_tranclpD)
[PROOF STATE]
proof (state)
this:
(if (case ((xcp', frs'), h2') of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') ((xcp, frs), h) then Red1_mthr.silent_moves True P t else Red1_mthr.silent_movet True P t) (((e, xs), exs), h) (((e', xs'), exs'), h)

goal (5 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. \<And>s1 s2 s2'. \<lbrakk>wbisim1 t s1 s2; execd_mthr.silent_move (compP2 P) t s2 s2'\<rbrakk> \<Longrightarrow> wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
 4. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 5. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
thus "wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or>
       (\<exists>s1'. \<tau>trsys.silent_movet (mred1 P t) (\<tau>MOVE1 P) s1 s1' \<and> wbisim1 t s1' s2')"
[PROOF STATE]
proof (prove)
using this:
(if (case ((xcp', frs'), h2') of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') ((xcp, frs), h) then Red1_mthr.silent_moves True P t else Red1_mthr.silent_movet True P t) (((e, xs), exs), h) (((e', xs'), exs'), h)

goal (1 subgoal):
 1. wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
[PROOF STEP]
using bisim' s1 s2 s2'
[PROOF STATE]
proof (prove)
using this:
(if (case ((xcp', frs'), h2') of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') ((xcp, frs), h) then Red1_mthr.silent_moves True P t else Red1_mthr.silent_movet True P t) (((e, xs), exs), h) (((e', xs'), exs'), h)
bisim1_list1 t h (e', xs') exs' xcp' frs'
s1 = (((e, xs), exs), h1)
s2 = ((xcp, frs), h)
s2' = ((xcp', frs'), h2')

goal (1 subgoal):
 1. wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')
[PROOF STEP]
by -(rule delay_bisimulation_base.simulation_silent2I', auto split del: if_split)
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2' \<and> (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')\<^sup>+\<^sup>+ s2' s2 \<or> (\<exists>s1'. Red1_mthr.silent_movet True P t s1 s1' \<and> wbisim1 t s1' s2')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
fix s1 s2 tl1 s1'
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
assume "wbisim1 t s1 s2" and "mred1 P t s1 tl1 s1'" and "\<not> \<tau>MOVE1 P s1 tl1 s1'"
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2
mred1 P t s1 tl1 s1'
\<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2
mred1 P t s1 tl1 s1'
\<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain e xs exs h where s1: "s1 = (((e, xs), exs), h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e xs exs h. s1 = (((e, xs), exs), h) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1) auto
[PROOF STATE]
proof (state)
this:
s1 = (((e, xs), exs), h)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (((e, xs), exs), h)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain e' xs' exs' h1' where s1': "s1' = (((e', xs'), exs'), h1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e' xs' exs' h1'. s1' = (((e', xs'), exs'), h1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1') auto
[PROOF STATE]
proof (state)
this:
s1' = (((e', xs'), exs'), h1')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1' = (((e', xs'), exs'), h1')

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain xcp frs h2 where s2: "s2 = ((xcp, frs), h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp frs h2. s2 = ((xcp, frs), h2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2) auto
[PROOF STATE]
proof (state)
this:
s2 = ((xcp, frs), h2)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wbisim1 t s1 s2
mred1 P t s1 tl1 s1'
\<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'
s1 = (((e, xs), exs), h)
s1' = (((e', xs'), exs'), h1')
s2 = ((xcp, frs), h2)
[PROOF STEP]
have [simp]: "h2 = h"  and red: "True,P,t \<turnstile>1 \<langle>(e, xs)/exs,h\<rangle> -tl1\<rightarrow> \<langle>(e', xs')/exs',h1'\<rangle>"
    and \<tau>: "\<not> \<tau>Move1 P h ((e, xs), exs)" and bisim: "bisim1_list1 t h (e, xs) exs xcp frs"
[PROOF STATE]
proof (prove)
using this:
wbisim1 t s1 s2
mred1 P t s1 tl1 s1'
\<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'
s1 = (((e, xs), exs), h)
s1' = (((e', xs'), exs'), h1')
s2 = ((xcp, frs), h2)

goal (1 subgoal):
 1. (h2 = h &&& True,P,t \<turnstile>1 \<langle>(e, xs)/exs,h\<rangle> -tl1\<rightarrow> \<langle>(e', xs')/exs',h1'\<rangle>) &&& \<not> \<tau>Move1 P h ((e, xs), exs) &&& bisim1_list1 t h (e, xs) exs xcp frs
[PROOF STEP]
by(fastforce elim!: Red1.cases dest: red1_\<tau>_taD)+
[PROOF STATE]
proof (state)
this:
h2 = h
True,P,t \<turnstile>1 \<langle>(e, xs)/exs,h\<rangle> -tl1\<rightarrow> \<langle>(e', xs')/exs',h1'\<rangle>
\<not> \<tau>Move1 P h ((e, xs), exs)
bisim1_list1 t h (e, xs) exs xcp frs

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from exec_1_simulates_Red1_not_\<tau>[OF wf red bisim \<tau>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xcp' frs'. \<tau>Exec_1_dr (compP2 P) t (xcp, h, frs) (xcp', h, frs') \<and> (\<exists>ta' xcp'' frs''. compP2 P,t \<turnstile> Normal (xcp', h, frs') -ta'-jvmd\<rightarrow> Normal (xcp'', h1', frs'') \<and> \<not> \<tau>Move2 (compP2 P) (xcp', h, frs') \<and> ta_bisim wbisim1 tl1 ta' \<and> bisim1_list1 t h1' (e', xs') exs' xcp'' frs'') \<and> (call1 e = None \<or> (case frs of [] \<Rightarrow> False | (stk, loc, C, M, pc) # FRS \<Rightarrow> \<forall>M' n. instrs_of (compP2 P) C M ! pc \<noteq> Invoke M' n) \<or> xcp' = xcp \<and> frs' = frs)
[PROOF STEP]
obtain ta' xcp' frs' xcp'' frs''
    where exec1: "\<tau>Exec_1_dr (compP2 P) t (xcp, h, frs) (xcp', h, frs')"
    and exec2: "exec_1_d (compP2 P) t (Normal (xcp', h, frs')) ta' (Normal (xcp'', h1', frs''))"
    and \<tau>': "\<not> \<tau>Move2 (compP2 P) (xcp', h, frs')"
    and bisim': "bisim1_list1 t h1' (e', xs') exs' xcp'' frs''"
    and ta': "ta_bisim wbisim1 tl1 ta'"
[PROOF STATE]
proof (prove)
using this:
\<exists>xcp' frs'. \<tau>Exec_1_dr (compP2 P) t (xcp, h, frs) (xcp', h, frs') \<and> (\<exists>ta' xcp'' frs''. compP2 P,t \<turnstile> Normal (xcp', h, frs') -ta'-jvmd\<rightarrow> Normal (xcp'', h1', frs'') \<and> \<not> \<tau>Move2 (compP2 P) (xcp', h, frs') \<and> ta_bisim wbisim1 tl1 ta' \<and> bisim1_list1 t h1' (e', xs') exs' xcp'' frs'') \<and> (call1 e = None \<or> (case frs of [] \<Rightarrow> False | (stk, loc, C, M, pc) # FRS \<Rightarrow> \<forall>M' n. instrs_of (compP2 P) C M ! pc \<noteq> Invoke M' n) \<or> xcp' = xcp \<and> frs' = frs)

goal (1 subgoal):
 1. (\<And>xcp' frs' ta' xcp'' frs''. \<lbrakk>\<tau>Exec_1_dr (compP2 P) t (xcp, h, frs) (xcp', h, frs'); compP2 P,t \<turnstile> Normal (xcp', h, frs') -ta'-jvmd\<rightarrow> Normal (xcp'', h1', frs''); \<not> \<tau>Move2 (compP2 P) (xcp', h, frs'); bisim1_list1 t h1' (e', xs') exs' xcp'' frs''; ta_bisim wbisim1 tl1 ta'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<tau>Exec_1_dr (compP2 P) t (xcp, h, frs) (xcp', h, frs')
compP2 P,t \<turnstile> Normal (xcp', h, frs') -ta'-jvmd\<rightarrow> Normal (xcp'', h1', frs'')
\<not> \<tau>Move2 (compP2 P) (xcp', h, frs')
bisim1_list1 t h1' (e', xs') exs' xcp'' frs''
ta_bisim wbisim1 tl1 ta'

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from exec1
[PROOF STATE]
proof (chain)
picking this:
\<tau>Exec_1_dr (compP2 P) t (xcp, h, frs) (xcp', h, frs')
[PROOF STEP]
have "\<tau>trsys.silent_moves (mexecd (compP2 P) t) (\<tau>MOVE2 (compP2 P)) ((xcp, frs), h) ((xcp', frs'), h)"
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_1_dr (compP2 P) t (xcp, h, frs) (xcp', h, frs')

goal (1 subgoal):
 1. execd_mthr.silent_moves (compP2 P) t ((xcp, frs), h) ((xcp', frs'), h)
[PROOF STEP]
by(rule \<tau>Exec_1_dr_rtranclpD)
[PROOF STATE]
proof (state)
this:
execd_mthr.silent_moves (compP2 P) t ((xcp, frs), h) ((xcp', frs'), h)

goal (4 subgoals):
 1. \<And>s1 s2 tl1 s1'. \<lbrakk>wbisim1 t s1 s2; mred1 P t s1 tl1 s1'; \<not> (case s1 of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'\<rbrakk> \<Longrightarrow> \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
 2. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 3. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 4. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
thus "\<exists>s2' s2'' tl2. \<tau>trsys.silent_moves (mexecd (compP2 P) t) (\<tau>MOVE2 (compP2 P)) s2 s2' \<and>
                       mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> \<tau>MOVE2 (compP2 P) s2' tl2 s2'' \<and>
                       wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2"
[PROOF STATE]
proof (prove)
using this:
execd_mthr.silent_moves (compP2 P) t ((xcp, frs), h) ((xcp', frs'), h)

goal (1 subgoal):
 1. \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
using bisim' exec2 \<tau>' s1 s1' s2 ta'
[PROOF STATE]
proof (prove)
using this:
execd_mthr.silent_moves (compP2 P) t ((xcp, frs), h) ((xcp', frs'), h)
bisim1_list1 t h1' (e', xs') exs' xcp'' frs''
compP2 P,t \<turnstile> Normal (xcp', h, frs') -ta'-jvmd\<rightarrow> Normal (xcp'', h1', frs'')
\<not> \<tau>Move2 (compP2 P) (xcp', h, frs')
s1 = (((e, xs), exs), h)
s1' = (((e', xs'), exs'), h1')
s2 = ((xcp, frs), h2)
ta_bisim wbisim1 tl1 ta'

goal (1 subgoal):
 1. \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
unfolding \<open>h2 = h\<close>
[PROOF STATE]
proof (prove)
using this:
execd_mthr.silent_moves (compP2 P) t ((xcp, frs), h) ((xcp', frs'), h)
bisim1_list1 t h1' (e', xs') exs' xcp'' frs''
compP2 P,t \<turnstile> Normal (xcp', h, frs') -ta'-jvmd\<rightarrow> Normal (xcp'', h1', frs'')
\<not> \<tau>Move2 (compP2 P) (xcp', h, frs')
s1 = (((e, xs), exs), h)
s1' = (((e', xs'), exs'), h1')
s2 = ((xcp, frs), h)
ta_bisim wbisim1 tl1 ta'

goal (1 subgoal):
 1. \<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
apply(subst (1 2) split_paired_Ex)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>execd_mthr.silent_moves (compP2 P) t ((xcp, frs), h) ((xcp', frs'), h); bisim1_list1 t h1' (e', xs') exs' xcp'' frs''; compP2 P,t \<turnstile> Normal (xcp', h, frs') -ta'-jvmd\<rightarrow> Normal (xcp'', h1', frs''); \<not> \<tau>Move2 (compP2 P) (xcp', h, frs'); s1 = (((e, xs), exs), h); s1' = (((e', xs'), exs'), h1'); s2 = ((xcp, frs), h); ta_bisim wbisim1 tl1 ta'\<rbrakk> \<Longrightarrow> \<exists>a b aa ba tl2. execd_mthr.silent_moves (compP2 P) t s2 (a, b) \<and> execd_mthr.r_syntax (compP2 P) t a b tl2 aa ba \<and> \<not> (case (a, b) of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 (aa, ba) \<and> wbisim1 t s1' (aa, ba) \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
apply(subst (1 2) split_paired_Ex)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>execd_mthr.silent_moves (compP2 P) t ((xcp, frs), h) ((xcp', frs'), h); bisim1_list1 t h1' (e', xs') exs' xcp'' frs''; compP2 P,t \<turnstile> Normal (xcp', h, frs') -ta'-jvmd\<rightarrow> Normal (xcp'', h1', frs''); \<not> \<tau>Move2 (compP2 P) (xcp', h, frs'); s1 = (((e, xs), exs), h); s1' = (((e', xs'), exs'), h1'); s2 = ((xcp, frs), h); ta_bisim wbisim1 tl1 ta'\<rbrakk> \<Longrightarrow> \<exists>a b ba aa bb bc tl2. execd_mthr.silent_moves (compP2 P) t s2 ((a, b), ba) \<and> execd_mthr.r_syntax (compP2 P) t (a, b) ba tl2 (aa, bb) bc \<and> \<not> (case ((a, b), ba) of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 ((aa, bb), bc) \<and> wbisim1 t s1' ((aa, bb), bc) \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
by clarify ((rule exI conjI|assumption)+, auto)
[PROOF STATE]
proof (state)
this:
\<exists>s2' s2'' tl2. execd_mthr.silent_moves (compP2 P) t s2 s2' \<and> mexecd (compP2 P) t s2' tl2 s2'' \<and> \<not> (case s2' of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'' \<and> wbisim1 t s1' s2'' \<and> ta_bisim wbisim1 tl1 tl2

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
fix s1 s2 tl2 s2'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
assume "wbisim1 t s1 s2" and "mexecd (compP2 P) t s2 tl2 s2'" and "\<not> \<tau>MOVE2 (compP2 P) s2 tl2 s2'"
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2
mexecd (compP2 P) t s2 tl2 s2'
\<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wbisim1 t s1 s2
mexecd (compP2 P) t s2 tl2 s2'
\<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain e xs exs h1 where s1: "s1 = (((e, xs), exs), h1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e xs exs h1. s1 = (((e, xs), exs), h1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s1) auto
[PROOF STATE]
proof (state)
this:
s1 = (((e, xs), exs), h1)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (((e, xs), exs), h1)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain xcp frs h where s2: "s2 = ((xcp, frs), h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp frs h. s2 = ((xcp, frs), h) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2) auto
[PROOF STATE]
proof (state)
this:
s2 = ((xcp, frs), h)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s2 = ((xcp, frs), h)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
obtain xcp' frs' h2' where s2': "s2' = ((xcp', frs'), h2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp' frs' h2'. s2' = ((xcp', frs'), h2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s2') auto
[PROOF STATE]
proof (state)
this:
s2' = ((xcp', frs'), h2')

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wbisim1 t s1 s2
mexecd (compP2 P) t s2 tl2 s2'
\<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'
s1 = (((e, xs), exs), h1)
s2 = ((xcp, frs), h)
s2' = ((xcp', frs'), h2')
[PROOF STEP]
have [simp]: "h1 = h"  and exec: "exec_1_d (compP2 P) t (Normal (xcp, h, frs)) tl2 (Normal (xcp', h2', frs'))"
    and \<tau>: "\<not> \<tau>Move2 (compP2 P) (xcp, h, frs)" and bisim: "bisim1_list1 t h (e, xs) exs xcp frs"
[PROOF STATE]
proof (prove)
using this:
wbisim1 t s1 s2
mexecd (compP2 P) t s2 tl2 s2'
\<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'
s1 = (((e, xs), exs), h1)
s2 = ((xcp, frs), h)
s2' = ((xcp', frs'), h2')

goal (1 subgoal):
 1. (h1 = h &&& compP2 P,t \<turnstile> Normal (xcp, h, frs) -tl2-jvmd\<rightarrow> Normal (xcp', h2', frs')) &&& \<not> \<tau>Move2 (compP2 P) (xcp, h, frs) &&& bisim1_list1 t h (e, xs) exs xcp frs
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>compP2 P,t \<turnstile> Normal (xcp, h, frs) -tl2-jvmd\<rightarrow> Normal (xcp', h2', frs'); s1 = (((e, xs), exs), h); s2 = ((xcp, frs), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs xcp frs; h1 = h; \<tau>Move2 (compP2 P) (xcp, h, frs); tl2 \<noteq> \<lbrace>\<rbrace>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule jvmd_NormalE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xcpa ha f frsa. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((xcp, frs), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs xcp frs; h1 = h; \<tau>Move2 (compP2 P) (xcp, h, frs); tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (xcp, h, frs); (tl2, xcp', h2', frs') \<in> exec (compP2 P) t (xcp, h, frs); (xcp, h, frs) = (xcpa, ha, f # frsa)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases xcp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xcpa ha f frsa. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((xcp, frs), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs xcp frs; h1 = h; \<tau>Move2 (compP2 P) (xcp, h, frs); tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (xcp, h, frs); (tl2, xcp', h2', frs') \<in> exec (compP2 P) t (xcp, h, frs); (xcp, h, frs) = (xcpa, ha, f # frsa); xcp = None\<rbrakk> \<Longrightarrow> False
 2. \<And>xcpa ha f frsa a. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((xcp, frs), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs xcp frs; h1 = h; \<tau>Move2 (compP2 P) (xcp, h, frs); tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (xcp, h, frs); (tl2, xcp', h2', frs') \<in> exec (compP2 P) t (xcp, h, frs); (xcp, h, frs) = (xcpa, ha, f # frsa); xcp = \<lfloor>a\<rfloor>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac b frsa. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (a, aa, ab, ac, b) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((a, aa, ab, ac, b) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (a, aa, ab, ac, b) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) ab ac ! b) (compP2 P) t h a aa ab ac b frsa; frs = (a, aa, ab, ac, b) # frsa; xcp = None; b < length (instrs_of (compP2 P) ab ac); \<tau>instr (compP2 P) h a (instrs_of (compP2 P) ab ac ! b)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac stk loc C M pc frs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>stk loc C M pc frsa. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac "instrs_of (compP2 P) C M ! pc")
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>stk loc C M pc frsa x1. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = Load x1\<rbrakk> \<Longrightarrow> False
 2. \<And>stk loc C M pc frsa x2. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = Store x2\<rbrakk> \<Longrightarrow> False
 3. \<And>stk loc C M pc frsa x3. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = Push x3\<rbrakk> \<Longrightarrow> False
 4. \<And>stk loc C M pc frsa x4. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = New x4\<rbrakk> \<Longrightarrow> False
 5. \<And>stk loc C M pc frsa x5. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = NewArray x5\<rbrakk> \<Longrightarrow> False
 6. \<And>stk loc C M pc frsa. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = ALoad\<rbrakk> \<Longrightarrow> False
 7. \<And>stk loc C M pc frsa. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = AStore\<rbrakk> \<Longrightarrow> False
 8. \<And>stk loc C M pc frsa. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = ALength\<rbrakk> \<Longrightarrow> False
 9. \<And>stk loc C M pc frsa x91 x92. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> False
 10. \<And>stk loc C M pc frsa x101 x102. \<lbrakk>s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); (tl2, xcp', h2', frs') \<in> exec_instr (instrs_of (compP2 P) C M ! pc) (compP2 P) t h stk loc C M pc frsa; frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); \<tau>instr (compP2 P) h stk (instrs_of (compP2 P) C M ! pc); instrs_of (compP2 P) C M ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> False
A total of 24 subgoals...
[PROOF STEP]
apply(simp_all split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>stk loc C M pc frsa x141 x142. \<lbrakk>frs = (stk, loc, C, M, pc) # frsa; xcp = None; pc < length (instrs_of (compP2 P) C M); instrs_of (compP2 P) C M ! pc = Invoke x141 x142; s1 = (((e, xs), exs), h); s2 = ((None, (stk, loc, C, M, pc) # frsa), h); s2' = ((xcp', frs'), h2'); bisim1_list1 t h (e, xs) exs None ((stk, loc, C, M, pc) # frsa); h1 = h; tl2 \<noteq> \<lbrace>\<rbrace>; check (compP2 P) (None, h, (stk, loc, C, M, pc) # frsa); stk ! x142 \<noteq> Null; x142 < length stk; \<forall>T. typeof_addr h (the_Addr (stk ! x142)) = \<lfloor>T\<rfloor> \<longrightarrow> (\<forall>Ts Tr D. compP2 P \<turnstile> class_type_of T sees x141: Ts\<rightarrow>Tr = Native in D \<longrightarrow> \<tau>external_defs D x141); snd (snd (snd (method (compP2 P) (class_type_of (the (typeof_addr h (the_Addr (stk ! x142))))) x141))) = None; \<exists>a aa ab ac ad b. tl2 = (a, map (convert_new_thread_action (extNTA2JVM (compP2 P))) aa, ab, ac, ad, b) \<and> (\<exists>va. (case va of RetVal v \<Rightarrow> xcp' = None \<and> frs' = (v # drop (Suc x142) stk, loc, C, M, pc + 1) # frsa | RetExc a \<Rightarrow> xcp' = \<lfloor>a\<rfloor> \<and> frs' = (stk, loc, C, M, pc) # frsa | RetStaySame \<Rightarrow> xcp' = None \<and> frs' = (stk, loc, C, M, pc) # frsa) \<and> ((a, aa, ab, ac, ad, b), va, h2') \<in> red_external_aggr (compP2 P) t (the_Addr (stk ! x142)) x141 (rev (take x142 stk)) h)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(auto dest!: \<tau>external_red_external_aggr_TA_empty simp add: check_def has_method_def \<tau>external_def \<tau>external'_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
h1 = h
compP2 P,t \<turnstile> Normal (xcp, h, frs) -tl2-jvmd\<rightarrow> Normal (xcp', h2', frs')
\<not> \<tau>Move2 (compP2 P) (xcp, h, frs)
bisim1_list1 t h (e, xs) exs xcp frs

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from \<tau>Red1_simulates_exec_1_not_\<tau>[OF wf exec bisim \<tau>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>e' xs' exs' ta' e'' xs'' exs''. \<tau>Red1r P t h ((e, xs), exs) ((e', xs'), exs') \<and> True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle> \<and> \<not> \<tau>Move1 P h ((e', xs'), exs') \<and> ta_bisim wbisim1 ta' tl2 \<and> bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs' \<and> (call1 e = None \<or> (case frs of [] \<Rightarrow> False | (stk, loc, C, M, pc) # FRS \<Rightarrow> \<forall>M' n. instrs_of (compP2 P) C M ! pc \<noteq> Invoke M' n) \<or> e' = e \<and> xs' = xs \<and> exs' = exs)
[PROOF STEP]
obtain e' xs' exs' ta' e'' xs'' exs''
    where red1: "\<tau>Red1r P t h ((e, xs), exs) ((e', xs'), exs')"
    and red2: "True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle>"
    and \<tau>': "\<not> \<tau>Move1 P h ((e', xs'), exs')" and ta': "ta_bisim wbisim1 ta' tl2"
    and bisim': "bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'"
[PROOF STATE]
proof (prove)
using this:
\<exists>e' xs' exs' ta' e'' xs'' exs''. \<tau>Red1r P t h ((e, xs), exs) ((e', xs'), exs') \<and> True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle> \<and> \<not> \<tau>Move1 P h ((e', xs'), exs') \<and> ta_bisim wbisim1 ta' tl2 \<and> bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs' \<and> (call1 e = None \<or> (case frs of [] \<Rightarrow> False | (stk, loc, C, M, pc) # FRS \<Rightarrow> \<forall>M' n. instrs_of (compP2 P) C M ! pc \<noteq> Invoke M' n) \<or> e' = e \<and> xs' = xs \<and> exs' = exs)

goal (1 subgoal):
 1. (\<And>e' xs' exs' ta' e'' xs'' exs''. \<lbrakk>\<tau>Red1r P t h ((e, xs), exs) ((e', xs'), exs'); True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle>; \<not> \<tau>Move1 P h ((e', xs'), exs'); ta_bisim wbisim1 ta' tl2; bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<tau>Red1r P t h ((e, xs), exs) ((e', xs'), exs')
True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle>
\<not> \<tau>Move1 P h ((e', xs'), exs')
ta_bisim wbisim1 ta' tl2
bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from red1
[PROOF STATE]
proof (chain)
picking this:
\<tau>Red1r P t h ((e, xs), exs) ((e', xs'), exs')
[PROOF STEP]
have "\<tau>trsys.silent_moves (mred1 P t) (\<tau>MOVE1 P) (((e, xs), exs), h) (((e', xs'), exs'), h)"
[PROOF STATE]
proof (prove)
using this:
\<tau>Red1r P t h ((e, xs), exs) ((e', xs'), exs')

goal (1 subgoal):
 1. Red1_mthr.silent_moves True P t (((e, xs), exs), h) (((e', xs'), exs'), h)
[PROOF STEP]
by(rule \<tau>Red1r_rtranclpD)
[PROOF STATE]
proof (state)
this:
Red1_mthr.silent_moves True P t (((e, xs), exs), h) (((e', xs'), exs'), h)

goal (3 subgoals):
 1. \<And>s1 s2 tl2 s2'. \<lbrakk>wbisim1 t s1 s2; mexecd (compP2 P) t s2 tl2 s2'; \<not> (case s2 of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 (compP2 P) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl2 s2'\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
 2. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 3. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
thus "\<exists>s1' s1'' tl1. \<tau>trsys.silent_moves (mred1 P t) (\<tau>MOVE1 P) s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and>
                      \<not> \<tau>MOVE1 P s1' tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2"
[PROOF STATE]
proof (prove)
using this:
Red1_mthr.silent_moves True P t (((e, xs), exs), h) (((e', xs'), exs'), h)

goal (1 subgoal):
 1. \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
using bisim' red2 \<tau>' s1 s2 s2' \<open>h1 = h\<close> ta'
[PROOF STATE]
proof (prove)
using this:
Red1_mthr.silent_moves True P t (((e, xs), exs), h) (((e', xs'), exs'), h)
bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'
True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle>
\<not> \<tau>Move1 P h ((e', xs'), exs')
s1 = (((e, xs), exs), h1)
s2 = ((xcp, frs), h)
s2' = ((xcp', frs'), h2')
h1 = h
ta_bisim wbisim1 ta' tl2

goal (1 subgoal):
 1. \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Red1_mthr.silent_moves True P t (((e, xs), exs), h) (((e', xs'), exs'), h); bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'; True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle>; \<not> \<tau>Move1 P h ((e', xs'), exs'); s1 = (((e, xs), exs), h1); s2 = ((xcp, frs), h); s2' = ((xcp', frs'), h2'); h1 = h; ta_bisim wbisim1 ta' tl2\<rbrakk> \<Longrightarrow> \<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
apply(rule exI[where x="(((e', xs'), exs'), h)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Red1_mthr.silent_moves True P t (((e, xs), exs), h) (((e', xs'), exs'), h); bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'; True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle>; \<not> \<tau>Move1 P h ((e', xs'), exs'); s1 = (((e, xs), exs), h1); s2 = ((xcp, frs), h); s2' = ((xcp', frs'), h2'); h1 = h; ta_bisim wbisim1 ta' tl2\<rbrakk> \<Longrightarrow> \<exists>s1'' tl1. Red1_mthr.silent_moves True P t s1 (((e', xs'), exs'), h) \<and> mred1 P t (((e', xs'), exs'), h) tl1 s1'' \<and> \<not> (case (((e', xs'), exs'), h) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
apply(rule exI[where x="(((e'', xs''), exs''), h2')"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Red1_mthr.silent_moves True P t (((e, xs), exs), h) (((e', xs'), exs'), h); bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'; True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle>; \<not> \<tau>Move1 P h ((e', xs'), exs'); s1 = (((e, xs), exs), h1); s2 = ((xcp, frs), h); s2' = ((xcp', frs'), h2'); h1 = h; ta_bisim wbisim1 ta' tl2\<rbrakk> \<Longrightarrow> \<exists>tl1. Red1_mthr.silent_moves True P t s1 (((e', xs'), exs'), h) \<and> Red1_mthr.r_syntax True P t ((e', xs'), exs') h tl1 ((e'', xs''), exs'') h2' \<and> \<not> (case (((e', xs'), exs'), h) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 (((e'', xs''), exs''), h2') \<and> wbisim1 t (((e'', xs''), exs''), h2') s2' \<and> ta_bisim wbisim1 tl1 tl2
[PROOF STEP]
apply(rule exI[where x="ta'"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Red1_mthr.silent_moves True P t (((e, xs), exs), h) (((e', xs'), exs'), h); bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'; True,P,t \<turnstile>1 \<langle>(e', xs')/exs',h\<rangle> -ta'\<rightarrow> \<langle>(e'', xs'')/exs'',h2'\<rangle>; \<not> \<tau>Move1 P h ((e', xs'), exs'); s1 = (((e, xs), exs), h1); s2 = ((xcp, frs), h); s2' = ((xcp', frs'), h2'); h1 = h; ta_bisim wbisim1 ta' tl2\<rbrakk> \<Longrightarrow> Red1_mthr.silent_moves True P t s1 (((e', xs'), exs'), h) \<and> Red1_mthr.r_syntax True P t ((e', xs'), exs') h ta' ((e'', xs''), exs'') h2' \<and> \<not> (case (((e', xs'), exs'), h) of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) ta' (((e'', xs''), exs''), h2') \<and> wbisim1 t (((e'', xs''), exs''), h2') s2' \<and> ta_bisim wbisim1 ta' tl2
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>s1' s1'' tl1. Red1_mthr.silent_moves True P t s1 s1' \<and> mred1 P t s1' tl1 s1'' \<and> \<not> (case s1' of (exexs, h) \<Rightarrow> \<lambda>ta s. \<tau>Move1 P h exexs \<and> ta = \<lbrace>\<rbrace>) tl1 s1'' \<and> wbisim1 t s1'' s2' \<and> ta_bisim wbisim1 tl1 tl2

goal (2 subgoals):
 1. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 2. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 2. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
have "wf (inv_image {(x, y). x < y} (\<lambda>(((e, xs), exs), h). sim12_size e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (inv_image {(x, y). x < y} (\<lambda>(((e, xs), exs), h). sim12_size e))
[PROOF STEP]
by(rule wf_inv_image)(rule wf_less)
[PROOF STATE]
proof (state)
this:
wf (inv_image {(x, y). x < y} (\<lambda>(((e, xs), exs), h). sim12_size e))

goal (2 subgoals):
 1. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 2. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wf (inv_image {(x, y). x < y} (\<lambda>(((e, xs), exs), h). sim12_size e))

goal (2 subgoals):
 1. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 2. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
have "inv_image {(x, y). x < y} (\<lambda>(((e, xs), exs), h). sim12_size e) =
    {(x, y). (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e') x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_image {(x, y). x < y} (\<lambda>(((e, xs), exs), h). sim12_size e) = {(x, y). (case x of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_image {(x, y). x < y} (\<lambda>(((e, xs), exs), h). sim12_size e) = {(x, y). (case x of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) y}

goal (2 subgoals):
 1. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
 2. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wf {(x, y). (case x of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) y}
[PROOF STEP]
show "wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')"
[PROOF STATE]
proof (prove)
using this:
wf {(x, y). (case x of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) y}

goal (1 subgoal):
 1. wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')
[PROOF STEP]
unfolding wfP_def
[PROOF STATE]
proof (prove)
using this:
wf {(x, y). (case x of (x, xa) \<Rightarrow> (case x of (x, xa) \<Rightarrow> (case x of (e, xs) \<Rightarrow> \<lambda>exs h (((e', xs'), exs'), h'). sim12_size e < sim12_size e') xa) xa) y}

goal (1 subgoal):
 1. wf {((((e, xs), exs), h), ((e', xs'), exs'), h'). sim12_size e < sim12_size e'}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wfP (\<lambda>(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')

goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
from wfP_sim21_size
[PROOF STATE]
proof (chain)
picking this:
wfP (sim21_size ?P)
[PROOF STEP]
have "wf {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'}"
[PROOF STATE]
proof (prove)
using this:
wfP (sim21_size ?P)

goal (1 subgoal):
 1. wf {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'}
[PROOF STEP]
by(unfold wfP_def)
[PROOF STATE]
proof (state)
this:
wf {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'}

goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
hence "wf (inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst)"
[PROOF STATE]
proof (prove)
using this:
wf {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'}

goal (1 subgoal):
 1. wf (inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst)
[PROOF STEP]
by(rule wf_inv_image)
[PROOF STATE]
proof (state)
this:
wf (inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst)

goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wf (inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst)

goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
have "inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst =
    {((xcpfrs, h), (xcpfrs', h)). sim21_size (compP2 P) xcpfrs xcpfrs'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst = {((xcpfrs, h), xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst = {((xcpfrs, h), xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs'}

goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst = {((xcpfrs, h), xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs'}

goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
have "\<dots> = {(x, y). (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {((xcpfrs, h), xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs'} = {(x, y). (case x of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') y}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
{((xcpfrs, h), xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs'} = {(x, y). (case x of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') y}

goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wf {(x, y). (case x of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') y}
[PROOF STEP]
show "wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')"
[PROOF STATE]
proof (prove)
using this:
wf {(x, y). (case x of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') y}

goal (1 subgoal):
 1. wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')
[PROOF STEP]
unfolding wfP_def
[PROOF STATE]
proof (prove)
using this:
wf {(x, y). (case x of (xcpfrs, h) \<Rightarrow> \<lambda>(xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') y}

goal (1 subgoal):
 1. wf {((xcpfrs, h), xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs'}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wfP (\<lambda>(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')

goal:
No subgoals!
[PROOF STEP]
qed