proposition: Lemma low_OK : forall (cfg : BDDconfig) (node : ad), BDDconfig_OK cfg -> is_internal_node cfg node -> config_node_OK cfg (low cfg node).
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intros node H H0. inversion H0. inversion H1. inversion H2. unfold low in |- *. rewrite H3. cut (BDDbounded (fst (bs, (share, counter))) (low (bs, (share, counter)) node) (var (bs, (share, counter)) node)). unfold var, low in |- *. rewrite H3. intro H4. unfold config_node_OK in |- *. apply BDDbounded_node_OK with (n := x). assumption. apply low_bounded. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2