proposition: Lemma internal_node_not_constant_1 : forall cfg : BDDconfig, BDDconfig_OK cfg -> forall (n : nat) (node : ad), is_internal_node cfg node -> n = nat_of_N (var cfg node) -> ~ bool_fun_eq (bool_fun_of_BDD cfg node) bool_fun_zero /\ ~ bool_fun_eq (bool_fun_of_BDD cfg node) bool_fun_one.
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intro H. intro n. apply lt_wf_ind with (P := fun n : nat => forall node : ad, is_internal_node (bs, (share, counter)) node -> n = nat_of_N (var (bs, (share, counter)) node) -> ~ bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) node) bool_fun_zero /\ ~ bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) node) bool_fun_one). intros n0 H0 node H1 H2. inversion H1. inversion H3. inversion H4. cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node)). cut (config_node_OK (bs, (share, counter)) (low (bs, (share, counter)) node)). intros H6 H7. elim H6. intro H8. elim H7. intro H9. cut (N.eqb (low (bs, (share, counter)) node) (high (bs, (share, counter)) node) = true). rewrite (low_high_neq (bs, (share, counter)) node H H1). intro H10. discriminate H10. rewrite H8. rewrite H9. apply Neqb_correct. intro H9. elim H9; clear H9; intro. cut (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node) = bool_fun_one). cut (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node) = bool_fun_zero). cut (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node)) (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true)). intros H10 H11 H12. cut (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node)) (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) false)). intros H13. rewrite H12 in H10. rewrite H11 in H13. split; unfold not in |- *; intro. cut (bool_fun_eq (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true) (bool_fun_restrict bool_fun_zero (var (bs, (share, counter)) node) true)). intro H15. cut (bool_fun_eq bool_fun_one (bool_fun_restrict bool_fun_zero (var (bs, (share, counter)) node) true)). intro H16. cut (bool_fun_eq bool_fun_one bool_fun_zero). intro H17. absurd (bool_fun_eq bool_fun_one bool_fun_zero). exact bool_fun_one_zero_eq. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_zero (var (bs, (share, counter)) node) true). assumption. apply bool_fun_restrict_zero. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true). assumption. assumption. apply bool_fun_restrict_eq. assumption. cut (bool_fun_eq (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) false) (bool_fun_restrict bool_fun_one (var (bs, (share, counter)) node) false)). intro H15. cut (bool_fun_eq bool_fun_zero (bool_fun_restrict bool_fun_one (var (bs, (share, counter)) node) false)). intro H16. cut (bool_fun_eq bool_fun_zero bool_fun_one). intro H17. absurd (bool_fun_eq bool_fun_zero bool_fun_one). exact bool_fun_zero_one_eq. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_one (var (bs, (share, counter)) node) false). assumption. apply bool_fun_restrict_one. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) false). assumption. assumption. apply bool_fun_restrict_eq. assumption. apply bool_fun_of_BDDlow. assumption. assumption. apply bool_fun_of_BDDhigh. assumption. assumption. rewrite H8. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)). reflexivity. rewrite H9. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) . reflexivity. cut (~ bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node)) bool_fun_zero /\ ~ bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node)) bool_fun_one). intro H10. split; unfold not in |- *; intro. apply (proj1 H10). apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true). apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_zero (var (bs, (share, counter)) node) true). apply bool_fun_restrict_eq. assumption. apply bool_fun_restrict_zero. apply (proj2 H10). apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true). apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_one (var (bs, (share, counter)) node) true). apply bool_fun_restrict_eq. assumption. apply bool_fun_restrict_one. apply H0 with (m := nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node))). rewrite H2. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. assumption. apply in_dom_is_internal. assumption. apply in_dom_is_internal. assumption. reflexivity. intro H8. elim H8; intro. elim H7; intro. split; unfold not in |- *; intro. apply bool_fun_zero_one_eq. apply bool_fun_eq_trans with (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) false). apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_zero (var (bs, (share, counter)) node) false). apply bool_fun_eq_symm. apply bool_fun_restrict_zero. apply bool_fun_restrict_eq. apply bool_fun_eq_symm. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node)). apply bool_fun_eq_symm. apply bool_fun_of_BDDlow. assumption. assumption. rewrite H9. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) . unfold bool_fun_eq, bool_fun_one in |- *. reflexivity. apply bool_fun_zero_one_eq. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node)). rewrite H10. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)). unfold bool_fun_eq in |- *; reflexivity. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true). apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_one (var (bs, (share, counter)) node) true). apply bool_fun_restrict_eq. assumption. apply bool_fun_restrict_one. elim H10; intro. cut (N.eqb (low (bs, (share, counter)) node) (high (bs, (share, counter)) node) = false). rewrite H9. rewrite H11. rewrite (Neqb_correct BDDone). intro; discriminate. apply low_high_neq. assumption. assumption. cut (~ bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node)) bool_fun_zero /\ ~ bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node)) bool_fun_one). intro H12. split; unfold not in |- *; intro. apply (proj1 H12). apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true). apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_zero (var (bs, (share, counter)) node) true). apply bool_fun_restrict_eq. assumption. apply bool_fun_restrict_zero. apply (proj2 H12). apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true). apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_one (var (bs, (share, counter)) node) true). apply bool_fun_restrict_eq. assumption. apply bool_fun_restrict_one. apply H0 with (m := nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node))). rewrite H2. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. assumption. apply in_dom_is_internal. assumption. apply in_dom_is_internal. assumption. reflexivity. cut (~ bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node)) bool_fun_zero /\ ~ bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node)) bool_fun_one). intro H10. split; unfold not in |- *; intro. apply (proj1 H10). apply bool_fun_eq_trans with (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) false). apply bool_fun_of_BDDlow. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_zero (var (bs, (share, counter)) node) false). apply bool_fun_restrict_eq. assumption. apply bool_fun_restrict_zero. apply (proj2 H10). apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) false). apply bool_fun_of_BDDlow. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict bool_fun_one (var (bs, (share, counter)) node) false). apply bool_fun_restrict_eq. assumption. apply bool_fun_restrict_one. apply H0 with (m := nat_of_N (var (bs, (share, counter)) (low (bs, (share, counter)) node))). rewrite H2. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. apply in_dom_is_internal. assumption. apply in_dom_is_internal. assumption. reflexivity. apply low_OK. assumption. assumption. apply high_OK. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2