proposition: Lemma BDDneg_memo_OK_bool_fun_1' : forall (cfg : BDDconfig) (memo : BDDneg_memo) (node node' : ad), BDDconfig_OK cfg -> BDDneg_memo_OK_2 cfg memo -> config_node_OK cfg node -> BDDneg_memo_lookup memo node = Some node' -> bool_fun_eq (bool_fun_of_BDD cfg node') (bool_fun_neg (bool_fun_of_BDD cfg node)).
proof: Proof. intros cfg memo node node' H H0 H1 H2. apply BDDneg_memo_OK_bool_fun_1 with (memo := memo). assumption. apply BDDneg_memo_OK_1_2. assumption. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4