proposition: Lemma BDDbounded_node_OK : forall (bs : BDDstate) (node : ad) (n : BDDvar), BDDbounded bs node n -> node_OK bs node.
proof: Proof. intros bs node n H. cut (node = BDDzero \/ node = BDDone \/ (exists x : BDDvar, (exists l : BDDvar, (exists r : BDDvar, MapGet _ bs node = Some (x, (l, r)) /\ BDDcompare x n = Datatypes.Lt /\ N.eqb l r = false /\ BDDbounded bs l x /\ BDDbounded bs r x)))). intros H0. elim H0; intro. left. assumption. elim H1; intro. right; left; assumption. inversion H2. inversion H3. inversion H4. right; right. unfold in_dom in |- *. rewrite (proj1 H5); reflexivity. apply BDDbounded_lemma. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat