proposition: Lemma BDDalloc_preserves_one : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), BDDconfig_OK cfg -> MapGet _ (fst (fst (BDDalloc cfg x l r))) BDDone = None.
proof: Proof. intro cfg. elim cfg. clear cfg. intro y. intro y0. elim y0. clear y0. intros y0 y1 l r x H. simpl in |- *. elim H. clear H. intros H H0. elim H0. clear H0. intros H0 H1. elim H1. clear H1. intros H1 H2. clear H1 H0. elim H. clear H. intros H H0. clear H. elim H0. clear H0. intros H H0. clear H0. rewrite (MapPut_semantics (BDDvar * (ad * ad)) y y1 (x, (l, r)) BDDone). cut (N.eqb y1 BDDone = false). intro H0. rewrite H0. assumption. cut (N.eqb y1 BDDone = true -> False). intro H0. apply not_true_is_false. exact H0. intro H0. rewrite (Neqb_complete y1 BDDone) in H2. compute in H2. discriminate H2. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat