proposition: Lemma BDDneg_memo_OK_1_lemma_1_1_1 : forall (bound : nat) (cfg : BDDconfig) (node node' : ad), BDDconfig_OK cfg -> config_node_OK cfg node -> config_node_OK cfg node' -> (is_internal_node cfg node -> nat_of_N (var cfg node) < bound) -> bool_fun_eq (bool_fun_of_BDD cfg node') (bool_fun_neg (bool_fun_of_BDD cfg node)) -> BDDneg_2 cfg node bound = (cfg, node').
proof: Proof. intro bound. apply lt_wf_ind with (P := fun bound : nat => forall (cfg : BDDconfig) (node node' : ad), BDDconfig_OK cfg -> config_node_OK cfg node -> config_node_OK cfg node' -> (is_internal_node cfg node -> nat_of_N (var cfg node) < bound) -> bool_fun_eq (bool_fun_of_BDD cfg node') (bool_fun_neg (bool_fun_of_BDD cfg node)) -> BDDneg_2 cfg node bound = (cfg, node')). intros n H. intro cfg. elim cfg; clear cfg; intros bs y; elim y; clear y; intros share counter. intros node node' H0 H1 H2 H3 H4. elim H1; intro. cut (node' = BDDone). intro H6. rewrite H5. rewrite H6. elim n. unfold BDDneg_2 in |- *. rewrite (config_OK_zero (bs, (share, counter)) H0). cut (N.eqb BDDzero BDDzero = true). intro H7. rewrite H7. reflexivity. apply Neqb_correct. intros n0 H7. unfold BDDneg_2 in |- *. fold BDDneg_2 in |- *. rewrite (config_OK_zero (bs, (share, counter)) H0). cut (N.eqb BDDzero BDDzero = true). intro H8. rewrite H8. reflexivity. apply Neqb_correct. rewrite H5 in H4. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H0)) in H4. rewrite bool_fun_neg_zero in H4. rewrite <- (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H0))) in H4. apply BDDunique with (cfg := (bs, (share, counter))). assumption. assumption. right; left; reflexivity. assumption. elim H5; clear H5; intro. cut (node' = BDDzero). intro H6. rewrite H5. rewrite H6. elim n. unfold BDDneg_2 in |- *. rewrite (config_OK_one (bs, (share, counter)) H0). cut (N.eqb BDDone BDDzero = false). intro H7. rewrite H7. reflexivity. simpl in |- *. reflexivity. intros n0 H7. unfold BDDneg_2 in |- *. fold BDDneg_2 in |- *. rewrite (config_OK_one (bs, (share, counter)) H0). cut (N.eqb BDDone BDDzero = false). intro H8. rewrite H8. reflexivity. reflexivity. rewrite H5 in H4. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H0))) in H4. rewrite bool_fun_neg_one in H4. rewrite <- (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H0)) in H4. apply BDDunique with (cfg := (bs, (share, counter))). assumption. assumption. left; reflexivity. assumption. elim (nat_sum n); intro y. elim y; clear y. intros m H6. rewrite H6. simpl in |- *. cut (is_internal_node (bs, (share, counter)) node). intro H7. inversion H7. inversion H8. inversion H9. simpl in H10. rewrite H10. cut (is_internal_node (bs, (share, counter)) node'). intro H11. inversion H11. inversion H12. inversion H13. clear H8 H9 H12 H13. cut (BDDneg_2 (bs, (share, counter)) x0 m = (bs, (share, counter), x3)). intro H8. rewrite H8. simpl in |- *. cut (BDDneg_2 (bs, (share, counter)) x1 m = (bs, (share, counter), x4)). intro H9. rewrite H9. simpl in |- *. unfold BDDmake in |- *. simpl in |- *. cut (N.eqb x3 x4 = false). intro H12. rewrite H12. elim H0. intros H13 H15. unfold BDDsharing_OK in H15. cut (x = x2). intro H16. rewrite H16. rewrite (proj2 (proj1 H15 x2 x3 x4 node') H14). reflexivity. cut (x = var (bs, (share, counter)) node). cut (x2 = var (bs, (share, counter)) node'). intros H16 H17. rewrite H16. rewrite H17. apply bool_fun_neg_eq_var_2 with (cfg := (bs, (share, counter))). assumption. assumption. assumption. assumption. unfold var in |- *. rewrite H14. reflexivity. unfold var in |- *. simpl in |- *; rewrite H10; reflexivity. cut (x3 = low (bs, (share, counter)) node'). cut (x4 = high (bs, (share, counter)) node'). intros H12 H13. rewrite H13. rewrite H12. apply low_high_neq. assumption. assumption. unfold high in |- *; rewrite H14; reflexivity. unfold low in |- *; rewrite H14; reflexivity. cut (x1 = high (bs, (share, counter)) node). cut (x4 = high (bs, (share, counter)) node'). intros H9 H12. rewrite H9; rewrite H12. apply H. rewrite H6. unfold lt in |- *. apply le_n. assumption. apply high_OK. assumption. assumption. apply high_OK. assumption. assumption. intro H13. apply lt_trans_1 with (y := nat_of_N (var (bs, (share, counter)) node)). apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. assumption. assumption. rewrite <- H6; apply H3. assumption. 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 (bool_fun_restrict (bool_fun_neg (bool_fun_of_BDD (bs, (share, counter)) node)) (var (bs, (share, counter)) node') true). apply bool_fun_restrict_eq. assumption. cut (var (bs, (share, counter)) node = var (bs, (share, counter)) node'). intro H13. rewrite <- H13. apply bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) true)). apply bool_fun_restrict_neg_1. apply bool_fun_of_BDD_ext. apply bool_fun_eq_neg_1. apply bool_fun_eq_symm. apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_neg_eq_var_2. assumption. assumption. assumption. assumption. unfold high in |- *; rewrite H14; reflexivity. unfold high in |- *; simpl in |- *; rewrite H10; reflexivity. cut (x0 = low (bs, (share, counter)) node). cut (x3 = low (bs, (share, counter)) node'). intros H8 H9. rewrite H8; rewrite H9. apply H. rewrite H6. unfold lt in |- *. apply le_n. assumption. apply low_OK. assumption. assumption. apply low_OK. assumption. assumption. intros H12. apply lt_trans_1 with (y := nat_of_N (var (bs, (share, counter)) node)). apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. assumption. rewrite <- H6; apply H3. assumption. 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 (bool_fun_restrict (bool_fun_neg (bool_fun_of_BDD (bs, (share, counter)) node)) (var (bs, (share, counter)) node') false). apply bool_fun_restrict_eq. assumption. cut (var (bs, (share, counter)) node = var (bs, (share, counter)) node'). intro H12. rewrite <- H12. apply bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node) (var (bs, (share, counter)) node) false)). apply bool_fun_restrict_neg_1. apply bool_fun_of_BDD_ext. apply bool_fun_eq_neg_1. apply bool_fun_eq_symm. apply bool_fun_of_BDDlow. assumption. assumption. apply bool_fun_neg_eq_var_2. assumption. assumption. assumption. assumption. unfold low in |- *; rewrite H14; reflexivity. unfold low in |- *; simpl in |- *; rewrite H10; reflexivity. elim H2; intro. rewrite H11 in H4. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H0)) in H4. rewrite <- bool_fun_neg_one in H4. absurd (bool_fun_eq bool_fun_one (bool_fun_of_BDD (bs, (share, counter)) node)). apply bool_fun_neq_lemma. exact (proj2 (internal_node_not_constant (bs, (share, counter)) node H0 H7)). apply bool_fun_eq_neg. assumption. elim H11; clear H11; intro. rewrite H11 in H4. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H0))) in H4. rewrite <- bool_fun_neg_zero in H4. absurd (bool_fun_eq bool_fun_zero (bool_fun_of_BDD (bs, (share, counter)) node)). apply bool_fun_neq_lemma. exact (proj1 (internal_node_not_constant (bs, (share, counter)) node H0 H7)). apply bool_fun_eq_neg. assumption. apply in_dom_is_internal. assumption. apply in_dom_is_internal. assumption. absurd (nat_of_N (var (bs, (share, counter)) node) < n). rewrite y. apply lt_n_O. apply H3. apply in_dom_is_internal. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4