[STATEMENT]
lemma Red1_execd_delay_bisim:
  assumes wf: "wf_J1_prog P"
  shows "delay_bisimulation_diverge (mred1 P t) (mexecd (compP2 P) t) (wbisim1 t) (ta_bisim wbisim1) (\<tau>MOVE1 P) (\<tau>MOVE2 (compP2 P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge (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>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. delay_bisimulation_diverge (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>)
[PROOF STEP]
interpret 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]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_J1_prog P

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]
by(rule Red1_execd_weak_bisim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. delay_bisimulation_diverge (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>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge (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>)
[PROOF STEP]
by(unfold_locales)
[PROOF STATE]
proof (state)
this:
delay_bisimulation_diverge (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>)

goal:
No subgoals!
[PROOF STEP]
qed