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