proposition: Lemma BDDunique : forall cfg : BDDconfig, BDDconfig_OK cfg -> forall node1 node2 : ad, config_node_OK cfg node1 -> config_node_OK cfg node2 -> bool_fun_eq (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2) -> node1 = node2.
proof: Proof. intros cfg H node1 node2 H0 H1 H2. apply BDDunique_1 with (cfg := cfg) (n := max (nat_of_N (var cfg node1)) (nat_of_N (var cfg node2))). assumption. reflexivity. assumption. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2