fact: Definition lowDistApprox (A : Set)(c : Comp A)(a : A)(n : nat)(v : Rat) := exists vals count, rel_map (evalDet c) (getAllBlists n) vals /\ pred_count (eq (ca_done a)) vals count /\ v == (count / expnat 2 n).
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat