proposition: Lemma BDDalloc_keeps_state_OK : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), BDDconfig_OK cfg -> node_OK (fst cfg) l -> node_OK (fst cfg) r -> N.eqb l r <> true -> (forall (xl : BDDvar) (ll rl : ad), MapGet _ (fst cfg) l = Some (xl, (ll, rl)) -> BDDcompare xl x = Datatypes.Lt) -> (forall (xr : BDDvar) (lr rr : ad), MapGet _ (fst cfg) r = Some (xr, (lr, rr)) -> BDDcompare xr x = Datatypes.Lt) -> BDDstate_OK (fst (fst (BDDalloc cfg x l r))).
proof: Proof. intro cfg. elim cfg. clear cfg. intro y. intro y0. elim y0. clear y0. intros y0 y1 l r x H H0 H1 H2 H3 H4. split. apply BDDalloc_preserves_zero. assumption. split. apply BDDalloc_preserves_one. simpl in H0, H1, H3, H4. assumption. simpl in |- *. simpl in H0, H1, H3, H4. intros a H5. unfold BDD_OK in |- *. unfold BDDordered in |- *. unfold in_dom in H5. elim (option_sum _ (MapGet (BDDvar * (ad * ad)) (MapPut (BDDvar * (ad * ad)) y y1 (x, (l, r))) a)). intros y2. elim y2. clear y2. intro x0. elim x0. intro y2. intro y3. elim y3. intro y4. intro y5. intro y6. rewrite y6. clear H5 x0 y3. elim (BDDalloc_no_new_node_1 (y, (y0, y1)) l y4 r y5 a x y2 y6). intros H5. injection H5. clear H5. intros H5 H6 H7. rewrite H7. rewrite H5 in y6. rewrite H6 in y6. rewrite H7 in y6. clear H5 H6 H7. clear y2 y4 y5. apply BDDbounded_2 with (x := x) (l := l) (r := r). assumption. apply BDDcompare_succ. apply not_true_is_false. assumption. elim H. intros H5 H6. elim H5. intros H7 H8. elim H8. intros H9 H10. unfold node_OK in H0. elim H0. intro H11. rewrite H11. apply BDDbounded_0. intros H11. elim H11. intros H12. rewrite H12. apply BDDbounded_1. intros H12. lapply (H10 l). intros H13. unfold BDD_OK in H10. unfold BDDordered in H10. unfold in_dom in H12. clear H11. elim (option_sum _ (MapGet (BDDvar * (ad * ad)) y l)). intros y2. elim y2. clear y2. intro x0. elim x0. clear x0. intro y2. intro y3. elim y3. clear y3. intros y3 y4 y5. clear H8. clear H12. unfold BDD_OK in H13. unfold BDDordered in H13. rewrite y5 in H13. lapply (BDDcompare_1 y2 x). intros H8. elim H8. intros H11. lapply (increase_bound y (ad_S y2) x l). intros H12. cut (BDDbounded y l x). intros H14. lapply (boundedness_preservation y (MapPut _ y y1 (x, (l, r)))). intros. apply H15. assumption. intros. cut (MapGet _ (fst (fst (BDDalloc (y, (y0, y1)) x l r))) a0 = Some (x0, (l0, r0))). simpl in |- *. trivial. apply BDDalloc_preserves_nodes. assumption. simpl in |- *. assumption. exact (H12 H11). assumption. intros. rewrite H11 in H13. lapply (boundedness_preservation y (MapPut _ y y1 (x, (l, r)))). intros. apply H12. assumption. intros. cut (MapGet _ (fst (fst (BDDalloc (y, (y0, y1)) x l r))) a0 = Some (x0, (l0, r0))). simpl in |- *. trivial. apply BDDalloc_preserves_nodes. assumption. assumption. apply H3 with (xl := y2) (ll := y3) (rl := y4). assumption. intro y2. rewrite y2 in H12. discriminate H12. assumption. unfold node_OK in H1. elim H1. intro H5. rewrite H5. apply BDDbounded_0. intros H5. elim H5. clear H5. intros H5. rewrite H5. apply BDDbounded_1. intros H6. unfold in_dom in H6. clear H5. elim (option_sum _ (MapGet (BDDvar * (ad * ad)) y r)). intros y2. elim y2. clear y2. intro x0. elim x0. clear x0. intro y2. intro y3. elim y3. clear y3. intros y3 y4 y5. clear H6. elim H. intros H5 H6. elim H5. intros H7 H8. elim H8. clear H8. intros H8 H9. unfold in_dom in H9. lapply (H9 r). intros H10. unfold BDD_OK in H10. unfold BDDordered in H10. rewrite y5 in H10. lapply (BDDcompare_1 y2 x). intros H11. elim H11. intros H12. lapply (increase_bound y (ad_S y2) x r). intros H13. cut (BDDbounded y r x). intros H14. lapply (boundedness_preservation y (MapPut _ y y1 (x, (l, r)))). intros H15. apply H15. assumption. intros a0 l0 r0 x0 H15. cut (MapGet _ (fst (fst (BDDalloc (y, (y0, y1)) x l r))) a0 = Some (x0, (l0, r0))). simpl in |- *. trivial. apply BDDalloc_preserves_nodes. assumption. simpl in |- *. assumption. exact (H13 H12). assumption. intros H12. rewrite H12 in H10. lapply (boundedness_preservation y (MapPut _ y y1 (x, (l, r)))). intros H13. apply H13. assumption. intros a0 l0 r0 x0 H13. cut (MapGet _ (fst (fst (BDDalloc (y, (y0, y1)) x l r))) a0 = Some (x0, (l0, r0))). simpl in |- *. trivial. apply BDDalloc_preserves_nodes. assumption. simpl in |- *. assumption. apply H4 with (xr := y2) (lr := y3) (rr := y4). assumption. rewrite y5. trivial. intro y2. rewrite y2 in H6. discriminate H6. intros H5. simpl in H5. lapply (boundedness_preservation y (MapPut _ y y1 (x, (l, r)))). intros H6. apply H6. elim H. intros H7 H8. elim H7. intros H9 H10. elim H10. intros H11 H12. lapply (H12 a). intros H13. unfold BDD_OK in H13. unfold BDDordered in H13. rewrite H5 in H13. assumption. unfold in_dom in |- *. rewrite H5. trivial. intros a0 l0 r0 x0 H6. cut (MapGet _ (fst (fst (BDDalloc (y, (y0, y1)) x l r))) a0 = Some (x0, (l0, r0))). simpl in |- *. trivial. apply BDDalloc_preserves_nodes. assumption. simpl in |- *. assumption. intros y2. rewrite y2. trivial. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat