fact: Fixpoint BDDor_1_1 (cfg : BDDconfig) (memo : BDDor_memo) (node1 node2 : ad) (bound : nat) {struct bound} : BDDconfig * (ad * BDDor_memo) := match BDDor_memo_lookup memo node1 node2 with | Some node => (cfg, (node, memo)) | None => if N.eqb node1 BDDzero then (cfg, (node2, BDDor_memo_put memo BDDzero node2 node2)) else if N.eqb node1 BDDone then (cfg, (BDDone, BDDor_memo_put memo BDDone node2 BDDone)) else if N.eqb node2 BDDzero then (cfg, (node1, BDDor_memo_put memo node1 BDDzero node1)) else if N.eqb node2 BDDone then (cfg, (BDDone, BDDor_memo_put memo node1 BDDone BDDone)) else match bound with | O => (initBDDconfig, (BDDzero, initBDDor_memo)) | S bound' => match BDDcompare (var cfg node1) (var cfg node2) with | Datatypes.Eq => match BDDdummy3 (BDDor_1_1 cfg memo (low cfg node1) (low cfg node2) bound') with | BDDdummy3 (cfgl, (nodel, memol)) => match BDDdummy3 (BDDor_1_1 cfgl memol (high cfg node1) (high cfg node2) bound') with | BDDdummy3 (cfgr, (noder, memor)) => match BDDdummy2 (BDDmake cfgr (var cfg node1) nodel noder) with | BDDdummy2 (cfg', node') => (cfg', (node', BDDor_memo_put memor node1 node2 node')) end end end | Datatypes.Lt => match BDDdummy3 (BDDor_1_1 cfg memo node1 (low cfg node2) bound') with | BDDdummy3 (cfgl, (nodel, memol)) => match BDDdummy3 (BDDor_1_1 cfgl memol node1 (high cfg node2) bound') with | BDDdummy3 (cfgr, (noder, memor)) => match BDDdummy2 (BDDmake cfgr (var cfg node2) nodel noder) with | BDDdummy2 (cfg', node') => (cfg', (node', BDDor_memo_put memor node1 node2 node')) end end end | Datatypes.Gt => match BDDdummy3 (BDDor_1_1 cfg memo (low cfg node1) node2 bound') with | BDDdummy3 (cfgl, (nodel, memol)) => match BDDdummy3 (BDDor_1_1 cfgl memol (high cfg node1) node2 bound') with | BDDdummy3 (cfgr, (noder, memor)) => match BDDdummy2 (BDDmake cfgr (var cfg node1) nodel noder) with | BDDdummy2 (cfg', node') => (cfg', (node', BDDor_memo_put memor node1 node2 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