proposition: Lemma homographic_emits_strong: forall mu alpha (p:productive_h mu alpha), exists n, (exists d:Digit, productive_h (product (inv_digit d) (product_init mu alpha n)) (drop n alpha) /\ Incl_M (product_init mu alpha n) d/\ forall p', bisim (homographic mu alpha p) (Cons d (homographic (product (inv_digit d) (product_init mu alpha n)) (drop n alpha) p'))).
proof: Proof. intros mu alpha H_productive. generalize (productive_h_emits_h mu alpha H_productive); intro H_emits. exists (depth_h mu alpha H_emits). destruct (depth_h_modulus_h mu alpha H_emits (depth_h mu alpha H_emits) (refl_equal _)) as [d H_modulus]. exists d; split. generalize (modulus_h_productive_h mu alpha H_emits H_productive); rewrite H_modulus; trivial. split. destruct (depth_h_Incl_M_inf_strong _ _ H_emits (depth_h mu alpha 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 (homographic_unfolded mu alpha H_productive); constructor; simpl; [ idtac | apply homographic_EPI_strong ]; rewrite <- (modulus_h_PI _ _ H_emits (productive_h_emits_h mu alpha H_productive)); rewrite H_modulus; trivial. Defined.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep