[STATEMENT]
lemma tbisim_flip [flip_simps]:
  "FWbisimulation_base.tbisim (\<lambda>t. flip (bisim t)) (flip bisim_wait) w t ts2 m2 ts1 m1 =
   FWbisimulation_base.tbisim bisim bisim_wait w t ts1 m1 ts2 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWbisimulation_base.tbisim (\<lambda>t. flip (bisim t)) (flip bisim_wait) w t ts2 m2 ts1 m1 = FWbisimulation_base.tbisim bisim bisim_wait w t ts1 m1 ts2 m2
[PROOF STEP]
unfolding FWbisimulation_base.tbisim_def flip_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case ts2 of None \<Rightarrow> ts1 = None | \<lfloor>(x1, ln)\<rfloor> \<Rightarrow> \<exists>x2. ts1 = \<lfloor>(x2, ln)\<rfloor> \<and> bisim t (x2, m1) (x1, m2) \<and> (w \<or> bisim_wait x2 x1)) = (case ts1 of None \<Rightarrow> ts2 = None | \<lfloor>(x1, ln)\<rfloor> \<Rightarrow> \<exists>x2. ts2 = \<lfloor>(x2, ln)\<rfloor> \<and> bisim t (x1, m1) (x2, m2) \<and> (w \<or> bisim_wait x1 x2))
[PROOF STEP]
by auto