fact: Fixpoint BDDneg_1_1 (cfg : BDDconfig) (memo : BDDneg_memo) (node : ad) (bound : nat) {struct bound} : BDDconfig * ad * BDDneg_memo := match BDDneg_memo_lookup memo node with | Some node' => (cfg, node', memo) | None => match MapGet _ (fst cfg) node with | None => if N.eqb node BDDzero then (cfg, BDDone, BDDneg_memo_put memo BDDzero BDDone) else (cfg, BDDzero, BDDneg_memo_put memo BDDone BDDzero) | Some (x, (l, r)) => match bound with | O => (initBDDconfig, BDDzero, initBDDneg_memo) | S bound' => match BDDdummy1 (BDDneg_1_1 cfg memo l bound') with | BDDdummy1 ((cfgl, nodel), memol) => match BDDdummy1 (BDDneg_1_1 cfgl memol r bound') with | BDDdummy1 ((cfgr, noder), memor) => match BDDdummy2 (BDDmake cfgr x nodel noder) with | BDDdummy2 (cfg', node') => (cfg', node', BDDneg_memo_put memor node node') end end end end end end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2 bdd6 bdd7 BDDdummy_lemma_2 BDDdummy_lemma_3 BDDdummy_lemma_4 bdd8