proposition: Lemma quadratic_emits_R :forall xi alpha beta (p:productive_q xi alpha beta), ~(Incl_T xi LL) -> (Incl_T xi RR) -> forall p', bisim (quadratic xi alpha beta p) (Cons RR (quadratic (m_product inv_RR xi) alpha beta p')).
proof: Proof. intros xi alpha beta p t_l t_r p'. rewrite quadratic_unfolded. rewrite (quadratic_unfolded (m_product inv_RR xi)). generalize (productive_q_emits_q _ _ _ p); intros t. generalize (modulus_q_productive_q xi alpha beta t p). rewrite (modulus_q_R _ _ _ t t_l t_r). intros. constructor; simpl; trivial. rewrite <- quadratic_unfolded; apply quadratic_EPI. Defined.
imports: digits