proposition: Lemma bisim_Str_pres_pair : forall (S0 S1: F_coalgebra) (xs0 ys0:S0.(states)) (xs1 ys1:S1.(states)), maximal_bisimulation _ _ xs0 ys0 -> maximal_bisimulation (Build_F_coalgebra (S0.(states)*S1.(states)) (fun x0x1 => (fst (S0.(transition) (fst x0x1)), (snd (S0.(transition) (fst x0x1)) , snd x0x1))) ) (Build_F_coalgebra (S0.(states)*S1.(states)) (fun x0x1 => (fst (S0.(transition) (fst x0x1)), (snd (S0.(transition) (fst x0x1)) , snd x0x1))) ) (xs0, xs1) (ys0, ys1).
proof: Proof. Proof. intros S0 S1 xs0 ys0 xs1 ys1 hyp. set (S0S1:=(S0.(states) * S1.(states))%type). destruct (maximal_bisimulation_is_bisimulation S0 S0) as [gamma _]. set (R_:=fun (x y:S0S1)=>{s0s1: S0.(states) * S0.(states) | fst s0s1 = fst x/\ snd s0s1 = fst y /\ maximal_bisimulation _ _ (fst x) (fst y)}). set (R'_:=fun (x y:S0S1)=>maximal_bisimulation _ _ (fst x) (fst y)). apply (bisimulation_maximal_bisimulation (Build_F_coalgebra S0S1 (fun x0x1 : S0S1 => (fst (transition S0 (fst x0x1)), (snd (transition S0 (fst x0x1)), snd x0x1)))) (Build_F_coalgebra S0S1 (fun x0x1 : S0S1 => (fst (transition S0 (fst x0x1)), (snd (transition S0 (fst x0x1)), snd x0x1)))) R'_). subst R'_; trivial. red; simpl. exists (gamma_bisim_Str_pres_pair S0 S1). clear. intros [[[xs0 xs1] [ys0 ys1]] hyp]. subst R'_. simpl in *; split; trivial. f_equal. destruct (bisim_Str_spelled S0 S0 (maximal_bisimulation S0 S0) xs0 ys0 hyp (maximal_bisimulation_is_bisimulation S0 S0)); trivial. Qed.
imports: WeaklyFinalCoalgebra