proposition: Lemma lowDistApprox_repeat_left_total : forall (A : Set)(c : Comp A)(P : A -> bool) a, well_formed_comp c -> left_total (lowDistApprox_repeat c P a).
proof: Proof. unfold left_total; intuition. edestruct (sumList_rel_left_total (fun (i : nat) (r : Rat) => forall r1'1 : Rat, sumList_rel (fun a0 : A => lowDistApprox c a0 n) (filter (fun a0 : A => negb (P a0)) (getSupport c)) r1'1 -> r == expRat r1'1 i) (getNats O (S n))). intuition. edestruct (sumList_rel_left_total (fun a1 : A => lowDistApprox c a1 n) (filter (fun a1 : A => negb (P a1)) (getSupport c)) ). intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. econstructor. intuition. eapply expRat_eqRat_compat. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. edestruct (@lowDistApprox_left_total). eapply comp_eq_dec; eauto. eauto. unfold lowDistApprox_repeat, ratMult_rel, expRat_rel, indicator_rel. econstructor. intuition. eapply ratMult_eqRat_compat. symmetry. eapply H2; eauto. case_eq (P a); intuition. left. intuition. assert (indicator P a == 1). unfold indicator. rewrite H4. intuition. eapply H5. right. intuition. unfold indicator. rewrite H4. intuition. eapply lowDistApprox_func; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat