proposition: Lemma quadratic_absorbs :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) (quadratic (right_product (left_product xi (hd alpha)) (hd beta)) (tl alpha) (tl beta) p').
proof: Proof. intros xi alpha beta p t_l t_r t_m p'. rewrite quadratic_unfolded. rewrite (quadratic_unfolded (right_product (left_product xi (hd alpha)) (hd beta))). generalize (productive_q_emits_q _ _ _ p); intros t. generalize (modulus_q_productive_q xi alpha beta t p). rewrite (modulus_q_absorbs _ _ _ t t_l t_r t_m (emits_q_absorbs_inv _ _ _ t_l t_r t_m t)). rewrite (modulus_q_PI _ _ _ (emits_q_absorbs_inv xi alpha beta t_l t_r t_m t) (productive_q_emits_q (right_product (left_product xi (hd alpha)) (hd beta)) (tl alpha) (tl beta) p')). constructor; simpl; trivial; apply quadratic_EPI. Defined.
imports: digits