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