proposition: Lemma BDDvar_ordered_low : forall (cfg : BDDconfig) (node : ad), BDDconfig_OK cfg -> is_internal_node cfg node -> is_internal_node cfg (low cfg node) -> BDDcompare (var cfg (low cfg node)) (var cfg node) = Datatypes.Lt.
proof: Proof. intro cfg. elim cfg. clear cfg. intros bs y. elim y. clear y. intros share counter. intros node H H0 H1. elim H0. intros x H2. elim H2. intros l H3. elim H3. intros r H4. clear H2 H3. elim H1. intros x1 H2. elim H2. intros l1 H3. elim H3. intros r1 H5. clear H2 H3. unfold var, low in |- *. rewrite H4. unfold low in H5. rewrite H4 in H5. rewrite H5. elim H. intros H2 H3. clear H3. elim H2. intros H3 H6. elim H6. intros H7 H8. cut (BDD_OK bs node). intro H9. unfold BDD_OK in H9. unfold BDDordered in H9. simpl in H4. simpl in H5. rewrite H4 in H9. cut (node = BDDzero \/ node = BDDone \/ (exists x0 : BDDvar, (exists l0 : BDDvar, (exists r0 : BDDvar, MapGet _ bs node = Some (x0, (l0, r0)) /\ BDDcompare x0 (ad_S x) = Datatypes.Lt /\ N.eqb l0 r0 = false /\ BDDbounded bs l0 x0 /\ BDDbounded bs r0 x0)))). intros H10. elim H10. intro H11. rewrite H11 in H4. rewrite H4 in H3. discriminate H3. intro H11. elim H11. intro H12. rewrite H12 in H4. rewrite H4 in H6. elim H6. intros H13 H14. discriminate H13. intros H12. elim H12. clear H12. intros x0 H12. elim H12. clear H12. intros x2 H12. elim H12. intros x3 H13. clear H12. clear H10 H11. elim H13. intros H10 H11. rewrite H4 in H10. injection H10. intros H12 H14 H15. rewrite <- H12 in H11. rewrite <- H14 in H11. rewrite <- H15 in H11. clear H13 H10. cut (BDDbounded bs l x). intros H10. cut (l = BDDzero \/ l = BDDone \/ (exists xl : BDDvar, (exists ll : BDDvar, (exists rl : BDDvar, MapGet _ bs l = Some (xl, (ll, rl)) /\ BDDcompare xl x = Datatypes.Lt /\ N.eqb ll rl = false /\ BDDbounded bs ll xl /\ BDDbounded bs rl xl)))). intros H13. elim H13. intro H16. rewrite H16 in H5. rewrite H5 in H3. discriminate H3. intro H16. elim H16. intro H17. rewrite H17 in H5. rewrite H5 in H7. discriminate H7. intro H17. clear H13 H16. elim H17. clear H17. intros x4 H13. elim H13. clear H13. intros x5 H13. elim H13. clear H13. intros x6 H13. elim H13. clear H13. intros H13 H16. rewrite H5 in H13. injection H13. intros H17 H18 H19. rewrite <- H19 in H16. exact (proj1 H16). apply BDDbounded_lemma. assumption. exact (proj1 (proj2 (proj2 H11))). apply BDDbounded_lemma. assumption. apply H8. unfold in_dom in |- *. simpl in H4. rewrite H4. trivial. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1