fact: Fixpoint computeEmptySpace(A : Set)(t : DistApproxTree A)(P : A -> bool) := match t with | dat_leaf o => match o with | Some a => indicator (fun a' => (negb (P a'))) a | None => 0 end | dat_internal t1 t2 => (1 / 2) * (computeEmptySpace t1 P) + (1 / 2) * (computeEmptySpace t2 P) end.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat