proposition: Lemma BDDneg_preserves_bool_fun : forall (cfg : BDDconfig) (negm : BDDneg_memo) (node : ad), BDDconfig_OK cfg -> BDDneg_memo_OK_2 cfg negm -> config_node_OK cfg node -> forall node' : ad, config_node_OK cfg node' -> bool_fun_eq (bool_fun_of_BDD (fst (BDDneg cfg negm node)) node') (bool_fun_of_BDD cfg node').
proof: Proof. intros. apply nodes_preserved_3. assumption. apply BDDneg_keeps_config_OK. assumption. assumption. assumption. apply BDDneg_preserves_nodes. assumption. assumption. assumption. assumption. Qed.
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 bdd9