proposition: Lemma BDDalloc_no_new_node : forall (cfg : BDDconfig) (l l1 r r1 a : ad) (x x1 : BDDvar), MapGet _ (fst (fst (BDDalloc cfg x l r))) a = Some (x1, (l1, r1)) -> a = snd (snd cfg) \/ MapGet _ (fst cfg) a = Some (x1, (l1, r1)).
proof: Proof. intro cfg. elim cfg. clear cfg. intros bs y. elim y. clear y. intros share counter l l' r r' a x x'. simpl in |- *. rewrite (MapPut_semantics (BDDvar * (ad * ad)) bs counter (x, (l, r)) a). cut (N.eqb counter a = true \/ N.eqb counter a = false). intro H. elim H. clear H. intro H. left. rewrite (Neqb_complete counter a). trivial. assumption. intro H0. rewrite H0. auto. elim (N.eqb counter a). auto. auto. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat