proposition: Lemma BDDmake_var_order : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), BDDconfig_OK cfg -> config_node_OK cfg l -> config_node_OK cfg r -> (is_internal_node cfg l -> BDDcompare (var cfg l) x = Datatypes.Lt) -> (is_internal_node cfg r -> BDDcompare (var cfg r) x = Datatypes.Lt) -> BDDvar_le (var (fst (BDDmake cfg x l r)) (snd (BDDmake cfg x l r))) x = true.
proof: Proof. intros cfg l r x H H0 H1 H2 H3. cut (forall (xl : BDDvar) (ll rl : ad), MapGet _ (fst cfg) l = Some (xl, (ll, rl)) -> BDDcompare xl x = Datatypes.Lt). cut (forall (xr : BDDvar) (lr rr : ad), MapGet _ (fst cfg) r = Some (xr, (lr, rr)) -> BDDcompare xr x = Datatypes.Lt). intros H4 H5. cut (node_OK (fst cfg) l). cut (node_OK (fst cfg) r). intros H6 H7. cut (BDDconfig_OK (fst (BDDmake cfg x l r)) /\ (N.eqb l r = false -> MapGet _ (fst (fst (BDDmake cfg x l r))) (snd (BDDmake cfg x l r)) = Some (x, (l, r))) /\ (N.eqb l r = true -> snd (BDDmake cfg x l r) = l) /\ (forall (a l' r' : ad) (x' : BDDvar), (MapGet _ (fst (fst (BDDmake cfg x l r))) a = Some (x', (l', r')) -> MapGet _ (fst cfg) a = Some (x', (l', r')) \/ snd (BDDmake cfg x l r) = a) /\ (MapGet _ (fst cfg) a = Some (x', (l', r')) -> MapGet _ (fst (fst (BDDmake cfg x l r))) a = Some (x', (l', r')))) /\ node_OK (fst (fst (BDDmake cfg x l r))) (snd (BDDmake cfg x l r))). intros H8. elim H8; clear H8; intros. elim H9; clear H9; intros. elim H10; clear H10; intros. elim H11; clear H11; intros. elim (sumbool_of_bool (N.eqb l r)). intro y. rewrite (H10 y). unfold var in |- *. elim (option_sum _ (MapGet _ (fst cfg) l)); intro y0. elim y0. intro x0. elim x0. intro y1; intro y2. elim y2. intros y3 y4 y5. rewrite (proj2 (H11 l y3 y4 y1) y5). rewrite y5 in H5. cut (BDDcompare y1 x = Datatypes.Lt). intro H13. apply BDDvar_le_compare. assumption. apply H5 with (ll := y3) (rl := y4). reflexivity. elim H7; intro. rewrite H13. rewrite H13 in H8. rewrite (config_OK_zero (fst (BDDmake cfg x BDDzero r)) H8). unfold BDDzero in |- *. apply BDDvar_le_z. elim H13. intro H14. rewrite H14. rewrite H14 in H8. rewrite (config_OK_one (fst (BDDmake cfg x BDDone r)) H8). unfold BDDzero in |- *. apply BDDvar_le_z. intro H14. unfold in_dom in H14. rewrite y0 in H14. discriminate. intro y. unfold var in |- *. rewrite (H9 y). unfold BDDvar_le in |- *. unfold Nleb in |- *. apply leb_correct. apply le_n. apply BDDmake_semantics. assumption. assumption. assumption. assumption. assumption. assumption. assumption. intros xr lr rr H4. unfold is_internal_node in H3. unfold var in H3. rewrite H4 in H3. apply H3. split with xr. split with lr. split with rr. reflexivity. intros xl ll rl H4. unfold is_internal_node in H2. unfold var in H2. rewrite H4 in H2. apply H2. split with xl. split with ll. split with rl. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2