proposition: Lemma BDDalloc_adjusts_counter : forall (cfg : BDDconfig) (x : BDDvar) (l r a : ad), BDDconfig_OK cfg -> (forall a : ad, Nleb (snd (snd (fst (BDDalloc cfg x l r)))) a = true -> MapGet _ (fst (fst (BDDalloc cfg x l r))) a = None) /\ Nleb (ad_S (ad_S N0)) (snd (snd (fst (BDDalloc cfg x l r)))) = true.
proof: Proof. intro cfg. elim cfg. clear cfg. intro y. intro y0. elim y0. clear y0. intros y0 y1 x l r a H. split. simpl in |- *. intros a0 H0. rewrite (MapPut_semantics (BDDvar * (ad * ad)) y y1 (x, (l, r)) a0). cut (N.eqb y1 a0 = false). intro H1. rewrite H1. elim H. intros. elim H3. intros. elim H5. intros. apply H6. apply ad_S_le_then_le. assumption. apply ad_S_le_then_neq. assumption. simpl in |- *. elim H. intros. elim H1. intros. elim H3. intros. apply le_then_le_S. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat