proposition: Lemma BDDmake_preserves_nodes : forall (cfg : BDDconfig) (x : BDDvar) (l r : ad), BDDconfig_OK cfg -> nodes_preserved cfg (fst (BDDmake cfg x l r)).
proof: Proof. intro cfg. elim cfg; clear cfg. intros bs y. elim y; clear y; intros share counter. intros x l r H00. unfold nodes_preserved in |- *. unfold BDDmake in |- *. elim (sumbool_of_bool (N.eqb l r)). intro y. rewrite y. simpl in |- *. intros; assumption. intro y. rewrite y. simpl in |- *. elim (option_sum _ (BDDshare_lookup share x l r)). intro y0. inversion y0. rewrite H. simpl in |- *. intros x1 l0 r0 node H0. assumption. intro y0. rewrite y0. simpl in |- *. elim H00. intros H H0 x0 l0 r0 node H1. rewrite (MapPut_semantics (BDDvar * (ad * ad)) bs counter (x, (l, r)) node). elim (sumbool_of_bool (N.eqb counter node)). intro y1. absurd (counter = node). unfold not in |- *; intro. cut (MapGet (BDDvar * (ad * ad)) bs node = None). intro H3. rewrite H1 in H3; discriminate. apply (proj1 (proj2 H0)). rewrite H2. unfold Nleb in |- *. apply leb_correct. apply le_n. apply Neqb_complete. assumption. intro y1. rewrite y1. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4