proposition: Lemma BDDmake_semantics : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), BDDconfig_OK cfg -> node_OK (fst cfg) l -> node_OK (fst cfg) r -> (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) -> 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)).
proof: Proof. intro cfg. elim cfg. clear cfg. intros bs y. elim y. clear y. intros share counter l r x. intros H H0 H1 H2 H3. cut (N.eqb l r = true \/ N.eqb l r = false). intro H4. elim H4. clear H4. intro H4. unfold BDDmake in |- *. rewrite H4. split. assumption. split. intro H5. discriminate H5. split. simpl in |- *. auto. split. simpl in |- *. auto. simpl in |- *. exact H0. intro H5. unfold BDDmake in |- *. rewrite H5. elim (option_sum _ (BDDshare_lookup share x l r)). clear H4. intro y. elim y. clear y. intro x0. intro y. rewrite y. split. simpl in |- *. exact H. split. intro H4. elim H. intros H6 H7. elim H7. intros H8 H9. unfold BDDsharing_OK in H8. simpl in |- *. apply (proj1 (H8 x l r x0)). assumption. split. intro H4. discriminate H4. simpl in |- *. split. intros a l' r' x'. tauto. unfold node_OK in |- *. right. right. unfold in_dom in |- *. cut (MapGet _ bs x0 = Some (x, (l, r))). intro H4. rewrite H4. trivial. elim H. intros H4 H6. exact (proj1 (proj1 H6 x l r x0) y). intro y. rewrite y. cut (BDDconfig_OK (fst (BDDalloc (bs, (share, counter)) x l r)) /\ MapGet _ (fst (fst (BDDalloc (bs, (share, counter)) x l r))) (snd (BDDalloc (bs, (share, counter)) x l r)) = Some (x, (l, r)) /\ (forall (a l' r' : ad) (x' : BDDvar), (MapGet _ (fst (fst (BDDalloc (bs, (share, counter)) x l r))) a = Some (x', (l', r')) -> MapGet _ (fst (bs, (share, counter))) a = Some (x', (l', r')) \/ snd (BDDalloc (bs, (share, counter)) x l r) = a) /\ (MapGet _ (fst (bs, (share, counter))) a = Some (x', (l', r')) -> MapGet _ (fst (fst (BDDalloc (bs, (share, counter)) x l r))) a = Some (x', (l', r')))) /\ node_OK (fst (fst (BDDalloc (bs, (share, counter)) x l r))) (snd (BDDalloc (bs, (share, counter)) x l r))). intro H6. split. exact (proj1 H6). split. intro H7. exact (proj1 (proj2 H6)). split. intro H7. discriminate H7. exact (proj2 (proj2 H6)). apply BDDalloc_semantics. assumption. assumption. assumption. unfold not in |- *. intro. rewrite H5 in H6. discriminate H6. assumption. assumption. intros. unfold not in |- *. intros. simpl in H6. rewrite <- H7 in H6. cut (BDDshare_lookup share x l r = Some a). rewrite y. discriminate. elim H. intros H8 H9. elim H9. intros H10 H11. unfold BDDsharing_OK in H10. exact (proj2 (H10 x l r a) H6). elim (N.eqb l r). auto. auto. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat