[STATEMENT]
lemma FWdelay_bisimulation_diverge_flip:
  "FWdelay_bisimulation_diverge final2 r2 final1 r1 (\<lambda>t. flip (bisim t)) (flip bisim_wait) \<tau>move2 \<tau>move1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge final2 r2 final1 r1 (\<lambda>t. flip (bisim t)) (flip bisim_wait) \<tau>move2 \<tau>move1
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. FWdelay_bisimulation_obs final2 r2 final1 r1 (\<lambda>t. flip (bisim t)) (flip bisim_wait) \<tau>move2 \<tau>move1
 2. FWdelay_bisimulation_diverge_axioms r2 r1 (\<lambda>t. flip (bisim t)) \<tau>move2 \<tau>move1
[PROOF STEP]
apply(rule FWdelay_bisimulation_obs_flip)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge_axioms r2 r1 (\<lambda>t. flip (bisim t)) \<tau>move2 \<tau>move1
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge_axioms.intro)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. delay_bisimulation_diverge (r2 t) (r1 t) (flip (bisim t)) (ta_bisim (\<lambda>t. flip (bisim t))) \<tau>move2 \<tau>move1
[PROOF STEP]
apply(unfold flip_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. delay_bisimulation_diverge (r1 t) (r2 t) (bisim t) ta_bisim_bisim_syntax \<tau>move1 \<tau>move2
[PROOF STEP]
apply(rule delay_bisimulation_diverge_axioms)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done