proposition: Lemma BDDunique_1 : forall cfg : BDDconfig, BDDconfig_OK cfg -> forall (n : nat) (node1 node2 : ad), n = max (nat_of_N (var cfg node1)) (nat_of_N (var cfg node2)) -> config_node_OK cfg node1 -> config_node_OK cfg node2 -> bool_fun_eq (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2) -> node1 = node2.
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intros H n. apply lt_wf_ind with (P := fun n : nat => forall node1 node2 : ad, n = max (nat_of_N (var (bs, (share, counter)) node1)) (nat_of_N (var (bs, (share, counter)) node2)) -> config_node_OK (bs, (share, counter)) node1 -> config_node_OK (bs, (share, counter)) node2 -> bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) node1) (bool_fun_of_BDD (bs, (share, counter)) node2) -> node1 = node2). intros n0 H00. intros node1 node2 H0 H1 H2 H3. elim H1; intro. elim H2; intro. rewrite H4; rewrite H5; reflexivity. elim H5; intro. rewrite H4 in H3. rewrite H6 in H3. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)) in H3. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) in H3. absurd (bool_fun_eq bool_fun_zero bool_fun_one). exact bool_fun_zero_one_eq. assumption. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) node2) bool_fun_zero). cut (is_internal_node (bs, (share, counter)) node2). intro H7. exact (proj1 (internal_node_not_constant (bs, (share, counter)) node2 H H7)). apply in_dom_is_internal. assumption. apply bool_fun_eq_trans with (bool_fun_of_BDD (bs, (share, counter)) node1). apply bool_fun_eq_symm; assumption. rewrite H4. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)). unfold bool_fun_eq in |- *; reflexivity. elim H4; intro. elim H2; intro. rewrite H5 in H3; rewrite H6 in H3. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)) in H3. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) in H3. absurd (bool_fun_eq bool_fun_one bool_fun_zero). exact bool_fun_one_zero_eq. assumption. elim H6; intro. rewrite H5; rewrite H7; reflexivity. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) node2) bool_fun_one). cut (is_internal_node (bs, (share, counter)) node2). intro H8. exact (proj2 (internal_node_not_constant (bs, (share, counter)) node2 H H8)). apply in_dom_is_internal. assumption. rewrite H5 in H3. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) in H3. apply bool_fun_eq_symm. assumption. elim H2; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) node1) bool_fun_zero). cut (is_internal_node (bs, (share, counter)) node1). intro H7. exact (proj1 (internal_node_not_constant (bs, (share, counter)) node1 H H7)). apply in_dom_is_internal; assumption. rewrite H6 in H3. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)) in H3. assumption. elim H6; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) node1) bool_fun_one). cut (is_internal_node (bs, (share, counter)) node1). intro H8. exact (proj2 (internal_node_not_constant (bs, (share, counter)) node1 H H8)). apply in_dom_is_internal; assumption. rewrite H7 in H3. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) in H3. assumption. cut (is_internal_node (bs, (share, counter)) node1). cut (is_internal_node (bs, (share, counter)) node2). intros H8 H9. elim (relation_sum (BDDcompare (var (bs, (share, counter)) node1) (var (bs, (share, counter)) node2))); intro y. elim y; clear y; intro y0. cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node1)). cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node2)). cut (config_node_OK (bs, (share, counter)) (low (bs, (share, counter)) node1)). cut (config_node_OK (bs, (share, counter)) (low (bs, (share, counter)) node2)). intros H10 H11 H12 H13. cut (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). cut (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2))). intros H14 H15. cut (high (bs, (share, counter)) node1 = high (bs, (share, counter)) node2). cut (low (bs, (share, counter)) node1 = low (bs, (share, counter)) node2). intros H16 H17. apply no_duplicate_node with (cfg := (bs, (share, counter))). assumption. assumption. assumption. apply BDDcompare_eq; assumption. assumption. assumption. elim H11; intro. elim H10; intro. rewrite H16; rewrite H17; reflexivity. elim H17; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2))). rewrite H16; rewrite H18. apply bool_fun_neq_zero_one. assumption. assumption. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2))). apply bool_fun_neq_lemma. rewrite H16. apply bool_fun_neq_internal_zero. assumption. apply in_dom_is_internal. assumption. assumption. elim H16; intro. elim H10; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2))). rewrite H17; rewrite H18. apply bool_fun_neq_one_zero. assumption. assumption. elim H18; intro. rewrite H17; rewrite H19; reflexivity. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2))). rewrite H17. apply bool_fun_neq_lemma. apply bool_fun_neq_internal_one. assumption. apply in_dom_is_internal. assumption. assumption. elim H10; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2))). rewrite H18. apply bool_fun_neq_internal_zero. assumption. apply in_dom_is_internal. assumption. assumption. elim H18; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2))). rewrite H19. apply bool_fun_neq_internal_one. assumption. apply in_dom_is_internal. assumption. assumption. apply H00 with (m := max (nat_of_N (var (bs, (share, counter)) (low (bs, (share, counter)) node1))) (nat_of_N (var (bs, (share, counter)) (low (bs, (share, counter)) node2)))). rewrite H0. apply lt_max_1_2. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. apply in_dom_is_internal; assumption. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. apply in_dom_is_internal; assumption. apply in_dom_is_internal; assumption. reflexivity. assumption. assumption. assumption. elim H13; intro. elim H12; intro. rewrite H16; rewrite H17; reflexivity. elim H17; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H16; rewrite H18; apply bool_fun_neq_zero_one. assumption. assumption. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H16. apply bool_fun_neq_lemma. apply bool_fun_neq_internal_zero. assumption. apply in_dom_is_internal. assumption. assumption. elim H16; intro. rewrite H17 in H15. elim H12; intro. rewrite H18 in H15. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) BDDone) (bool_fun_of_BDD (bs, (share, counter)) BDDzero)). apply bool_fun_neq_one_zero. assumption. assumption. elim H18; intro. rewrite H17; rewrite H19; reflexivity. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) BDDone) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). apply bool_fun_neq_lemma. apply bool_fun_neq_internal_one. assumption. apply in_dom_is_internal. assumption. assumption. elim H12; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H18. apply bool_fun_neq_internal_zero. assumption. apply in_dom_is_internal. assumption. assumption. elim H18; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H19. apply bool_fun_neq_internal_one. assumption. apply in_dom_is_internal. assumption. assumption. apply H00 with (m := max (nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node1))) (nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node2)))). rewrite H0. apply lt_max_1_2. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. assumption. apply in_dom_is_internal. assumption. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. apply in_dom_is_internal. assumption. apply in_dom_is_internal. assumption. reflexivity. assumption. assumption. assumption. apply bool_fun_eq_trans with (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node1) false). apply bool_fun_of_BDDlow. assumption. assumption. apply bool_fun_eq_trans with (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node2) false). cut (var (bs, (share, counter)) node1 = var (bs, (share, counter)) node2). intro H14. rewrite H14. apply bool_fun_restrict_eq. assumption. apply BDDcompare_eq. assumption. apply bool_fun_eq_symm. apply bool_fun_of_BDDlow. assumption. assumption. apply bool_fun_eq_trans with (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node1) true). apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_eq_trans with (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node2) true). cut (var (bs, (share, counter)) node1 = var (bs, (share, counter)) node2). intro H14. rewrite H14. apply bool_fun_restrict_eq. assumption. apply BDDcompare_eq. assumption. apply bool_fun_eq_symm. apply bool_fun_of_BDDhigh. assumption. assumption. apply low_OK. assumption. assumption. apply low_OK. assumption. assumption. apply high_OK. assumption. assumption. apply high_OK. assumption. assumption. cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node1)). cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node2)). cut (config_node_OK (bs, (share, counter)) (low (bs, (share, counter)) node1)). cut (config_node_OK (bs, (share, counter)) (low (bs, (share, counter)) node2)). intros H10 H11 H12 H13. cut (low (bs, (share, counter)) node2 = high (bs, (share, counter)) node2). intros H14. cut (N.eqb (low (bs, (share, counter)) node2) (high (bs, (share, counter)) node2) = false). rewrite H14. rewrite (Neqb_correct (high (bs, (share, counter)) node2)). intro H15. discriminate H15. apply low_high_neq. assumption. assumption. cut (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). intro H14. elim H10; intro. elim H12; intro. rewrite H15; rewrite H16; reflexivity. elim H16; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H15; rewrite H17. apply bool_fun_neq_zero_one. assumption. assumption. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H15. apply bool_fun_neq_lemma. apply bool_fun_neq_internal_zero. assumption. apply in_dom_is_internal; assumption. assumption. elim H15; intro. elim H12; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H16; rewrite H17. apply bool_fun_neq_one_zero. assumption. assumption. elim H17; intro. rewrite H16; rewrite H18; reflexivity. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H16. apply bool_fun_neq_lemma. apply bool_fun_neq_internal_one. assumption. apply in_dom_is_internal. assumption. assumption. elim H12; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H17. apply bool_fun_neq_internal_zero. assumption. apply in_dom_is_internal. assumption. assumption. elim H17; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node2)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node2))). rewrite H18. apply bool_fun_neq_internal_one. assumption. apply in_dom_is_internal. assumption. assumption. apply H00 with (m := max (nat_of_N (var (bs, (share, counter)) (low (bs, (share, counter)) node2))) (nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node2)))). rewrite H0. apply lt_max_2. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. apply in_dom_is_internal; assumption. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. apply in_dom_is_internal; assumption. apply in_dom_is_internal; assumption. reflexivity. assumption. assumption. assumption. cut (bool_fun_eq (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node2) false) (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node2) true)). intro H14. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node2) false). apply bool_fun_of_BDDlow. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node2) true). assumption. apply bool_fun_eq_symm. apply bool_fun_of_BDDhigh. assumption. assumption. cut (bool_fun_eq (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node2) false) (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node2) true)). intro H14. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node2) false). apply bool_fun_restrict_eq. apply bool_fun_eq_symm. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node2) true). assumption. apply bool_fun_restrict_eq. assumption. cut (bool_fun_independent (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node2)). intro H14. unfold bool_fun_independent in H14. unfold bool_fun_eq in |- *. unfold bool_fun_restrict in |- *. unfold bool_fun_eval at 1 3 in |- *. intro vb. rewrite (H14 vb); reflexivity. apply BDDvar_independent_1 with (n := nat_of_N (var (bs, (share, counter)) node1)). assumption. assumption. reflexivity. assumption. apply low_OK. assumption. assumption. apply low_OK. assumption. assumption. apply high_OK. assumption. assumption. apply high_OK. assumption. assumption. cut (BDDcompare (var (bs, (share, counter)) node2) (var (bs, (share, counter)) node1) = Datatypes.Lt). clear y; intro y. cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node1)). cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node2)). cut (config_node_OK (bs, (share, counter)) (low (bs, (share, counter)) node1)). cut (config_node_OK (bs, (share, counter)) (low (bs, (share, counter)) node2)). intros H10 H11 H12 H13. cut (low (bs, (share, counter)) node1 = high (bs, (share, counter)) node1). intros H14. cut (N.eqb (low (bs, (share, counter)) node1) (high (bs, (share, counter)) node1) = false). rewrite H14. rewrite (Neqb_correct (high (bs, (share, counter)) node1)). intro H15. discriminate H15. apply low_high_neq. assumption. assumption. cut (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1))). intro H14. elim H11; intro. elim H13; intro. rewrite H15; rewrite H16; reflexivity. elim H16; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1))). rewrite H15; rewrite H17. apply bool_fun_neq_zero_one. assumption. assumption. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1))). rewrite H15. apply bool_fun_neq_lemma. apply bool_fun_neq_internal_zero. assumption. apply in_dom_is_internal; assumption. assumption. elim H15; intro. elim H13; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1))). rewrite H16; rewrite H17. apply bool_fun_neq_one_zero. assumption. assumption. elim H17; intro. rewrite H16; rewrite H18; reflexivity. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1))). rewrite H16. apply bool_fun_neq_lemma. apply bool_fun_neq_internal_one. assumption. apply in_dom_is_internal. assumption. assumption. elim H13; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1))). rewrite H17. apply bool_fun_neq_internal_zero. assumption. apply in_dom_is_internal. assumption. assumption. elim H17; intro. absurd (bool_fun_eq (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node1)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node1))). rewrite H18. apply bool_fun_neq_internal_one. assumption. apply in_dom_is_internal. assumption. assumption. apply H00 with (m := max (nat_of_N (var (bs, (share, counter)) (low (bs, (share, counter)) node1))) (nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node1)))). rewrite H0. apply lt_max_12. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. apply in_dom_is_internal; assumption. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. apply in_dom_is_internal; assumption. apply in_dom_is_internal; assumption. reflexivity. assumption. assumption. assumption. cut (bool_fun_eq (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node1) false) (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node1) true)). intro H14. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node1) false). apply bool_fun_of_BDDlow. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node1) (var (bs, (share, counter)) node1) true). assumption. apply bool_fun_eq_symm. apply bool_fun_of_BDDhigh. assumption. assumption. cut (bool_fun_eq (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node1) false) (bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node1) true)). intro H14. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node1) false). apply bool_fun_restrict_eq. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_restrict (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node1) true). assumption. apply bool_fun_restrict_eq. apply bool_fun_eq_symm. assumption. cut (bool_fun_independent (bool_fun_of_BDD (bs, (share, counter)) node2) (var (bs, (share, counter)) node1)). intro H14. unfold bool_fun_independent in H14. unfold bool_fun_eq in |- *. unfold bool_fun_restrict in |- *. unfold bool_fun_eval at 1 3 in |- *. intro vb. rewrite (H14 vb); reflexivity. apply BDDvar_independent_1 with (n := nat_of_N (var (bs, (share, counter)) node2)). assumption. assumption. reflexivity. assumption. apply low_OK. assumption. assumption. apply low_OK. assumption. assumption. apply high_OK. assumption. assumption. apply high_OK. assumption. assumption. apply BDDcompare_sup_inf. assumption. apply in_dom_is_internal. assumption. 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