fact: Fixpoint BDDneg_2 (cfg : BDDconfig) (node : ad) (bound : nat) {struct bound} : BDDconfig * ad := match MapGet _ (fst cfg) node with | None => if N.eqb node BDDzero then (cfg, BDDone) else (cfg, BDDzero) | Some (x, (l, r)) => match bound with | O => (initBDDconfig, BDDzero) | S bound' => BDDmake (fst (BDDneg_2 (fst (BDDneg_2 cfg l bound')) r bound')) x (snd (BDDneg_2 cfg l bound')) (snd (BDDneg_2 (fst (BDDneg_2 cfg l bound')) r bound')) end end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1