proposition: Lemma shuffle_product_comm: forall xs ys, shuffle_product xs ys (=) shuffle_product ys xs.
proof: Proof. intros xs ys. set (R:=fun xs ys => { xs0: w.(states) & { ys0 : w.(states) | xs = shuffle_product xs0 ys0 /\ ys = shuffle_product ys0 xs0}}). apply (lambda_coinduction_strong Lambda_convolution R). subst R; simpl. exists xs; exists ys; split; auto. clear; exists gamma_shuffle_product_comm. intros [[s1 s2] [alpha [beta [hyp_l hyp_r]]]]. simpl in hyp_l, hyp_r, s1, s2. split. stepl (hd s1, (pointwise_plus (shuffle_product (tl alpha) beta) (shuffle_product alpha (tl beta)))); trivial; simpl; f_equal; subst s1. apply bisimilar_is_equal_Streams. rewrite (shuffle_product_cofixed alpha beta); apply refl_bisimilar. stepl (hd s1, (pointwise_plus (shuffle_product beta (tl alpha))) (shuffle_product (tl beta) alpha)). simpl; f_equal; subst s2. subst s1; rewrite shuffle_product_cofixed; rewrite (shuffle_product_cofixed beta alpha); simpl; auto with zarith. apply bisimilar_is_equal_Streams. rewrite (shuffle_product_cofixed beta alpha); apply pointwise_plus_comm. simpl; f_equal. Qed.
imports: LambdaCoiterationExamples IntensionalLambdaBisimulation ZStreamCoalgebra