proposition: Lemma evalDet_lowDistApprox_ls_not_done: forall (A : Set) (c : Comp A) (s : Blist) (a2 : A) (n : nat), well_formed_comp c -> (forall s' (a : A), In s' (getAllBlists n) -> evalDet c (s ++ s') (ca_done a) -> False) -> lowDistApprox_ls c a2 n s 0.
proof: Proof. intuition. unfold lowDistApprox_ls. exists (listRepeat (@ca_eof A) (length (getAllBlists n))). exists O. intuition. eapply rel_map_listRepeat; intuition. destruct (@evalDet_dec _ c (s ++ a)). trivial. destruct H2. exfalso. eapply H0. eauto. eauto. trivial. eapply pred_count_eq_none; intuition. assert (a = (ca_eof A)). eapply in_listRepeat_inv. eauto. subst. discriminate. eapply rat_num_0. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat