proposition: Lemma bool_fun_preservation : forall (cfg cfg' : BDDconfig) (node : ad), BDDconfig_OK cfg -> BDDconfig_OK cfg' -> (forall (x : BDDvar) (l r a : ad), MapGet _ (fst cfg) a = Some (x, (l, r)) -> MapGet _ (fst cfg') a = Some (x, (l, r))) -> config_node_OK cfg node -> bool_fun_eq (bool_fun_of_BDD cfg' node) (bool_fun_of_BDD cfg node).
proof: Proof. intros cfg cfg' node H H0 H1 H2. apply bool_fun_preservation_1 with (n := nat_of_N (var cfg node)). assumption. assumption. assumption. reflexivity. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2