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