fact: Fixpoint bool_fun_of_BDD_1 (cfg : BDDconfig) (node : ad) (bound : nat) {struct bound} : bool_fun := match MapGet _ (fst cfg) node with | None => if N.eqb node BDDzero then bool_fun_zero else bool_fun_one | Some (x, (l, r)) => match bound with | O => bool_fun_zero | S bound' => let bfl := bool_fun_of_BDD_1 cfg l bound' in let bfr := bool_fun_of_BDD_1 cfg r bound' in fun vb : var_binding => if vb x then bfr vb else bfl vb end end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1