proposition: Lemma BDDalloc_preserves_nodes : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), BDDconfig_OK cfg -> forall (a l1 r1 : ad) (x1 : BDDvar), MapGet _ (fst cfg) a = Some (x1, (l1, r1)) -> MapGet _ (fst (fst (BDDalloc cfg x l r))) a = Some (x1, (l1, r1)).
proof: Proof. intro cfg. elim cfg. clear cfg. intro y. intro y0. elim y0. clear y0. simpl in |- *. intros y0 y1 l r x H a l1 r1 x1 H0. elim H. clear H. intros H H1. rewrite (MapPut_semantics (BDDvar * (ad * ad)) y y1 (x, (l, r)) a). cut (N.eqb y1 a = false). intro H2. rewrite H2. assumption. cut (N.eqb y1 a <> true). intros H2. apply not_true_is_false. assumption. unfold not in |- *. intros H2. elim H1. intros H3 H4. elim H4. intros H5 H6. lapply (H5 a). intros H7. rewrite H7 in H0. discriminate H0. lapply (Neqb_complete y1 a). intros H7. rewrite H7. apply Nleb_refl. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat