[STATEMENT]
lemma delay_bisimulation_diverge_red0_Red1:
  assumes "wf_J_prog P"
  shows "delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 (ta_bisim (\<lambda>t. bisim_red0_Red1)) (\<tau>MOVE0 P) (\<tau>MOVE1 (compP1 P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
interpret delay_bisimulation_measure
    "mred0 P t" "mred1' (compP1 P) t" "bisim_red0_Red1" "ta_bisim (\<lambda>t. bisim_red0_Red1)" "\<tau>MOVE0 P" "\<tau>MOVE1 (compP1 P)"
    "\<lambda>es es'. False" "\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e'< countInitBlock e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_measure (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) (\<lambda>es es'. False) (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P

goal (1 subgoal):
 1. delay_bisimulation_measure (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) (\<lambda>es es'. False) (\<lambda>(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e' < countInitBlock e)
[PROOF STEP]
by(rule delay_bisimulation_red0_Red1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 red0_Red1'.ta_bisim_bisim_syntax (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>)

goal:
No subgoals!
[PROOF STEP]
qed