proposition: Lemma quadratic_emits_strong: forall xi alpha beta (p:productive_q xi alpha beta), exists n, (exists d:Digit, productive_q (m_product (inv_digit d) (product_init_zip xi alpha beta n)) (drop n alpha) (drop n beta) /\ Incl_T (product_init_zip xi alpha beta n) d/\ forall p', bisim (quadratic xi alpha beta p) (Cons d (quadratic (m_product (inv_digit d) (product_init_zip xi alpha beta n)) (drop n alpha) (drop n beta) p'))).
proof: Proof. intros xi alpha beta H_productive. generalize (productive_q_emits_q xi alpha beta H_productive); intro H_emits. exists (depth_q xi alpha beta H_emits). destruct (depth_q_modulus_q xi alpha beta H_emits (depth_q xi alpha beta H_emits) (refl_equal _)) as [d H_modulus]. exists d; split. generalize (modulus_q_productive_q xi alpha beta H_emits H_productive); rewrite H_modulus; trivial. split. destruct (depth_q_Incl_T_inf_strong _ _ _ H_emits (depth_q xi alpha beta H_emits) (refl_equal _)) as [[[H_Incl H_modulus']|[H_Incl H_modulus']]|[H_Incl H_modulus']]; rewrite H_modulus in H_modulus'; simpl in H_modulus'; rewrite H_modulus'; assumption... intros H_productive'. rewrite (quadratic_unfolded xi alpha beta H_productive); constructor; simpl; [ idtac | apply quadratic_EPI_strong ]; rewrite <- (modulus_q_PI _ _ _ H_emits (productive_q_emits_q xi alpha beta H_productive)); rewrite H_modulus; trivial. Defined.
imports: digits Refining_T quadratic Streams_addenda rep RIneq QArithSternBrocot(R_addenda)