proposition: Lemma BDDvar_independent_1 : forall (cfg : BDDconfig) (n : nat) (node : ad) (x : BDDvar), BDDconfig_OK cfg -> is_internal_node cfg node -> n = nat_of_N (var cfg node) -> BDDcompare (var cfg node) x = Datatypes.Lt -> bool_fun_independent (bool_fun_of_BDD cfg node) x.
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intro n. apply lt_wf_ind with (P := fun n : nat => forall (node : ad) (x : BDDvar), BDDconfig_OK (bs, (share, counter)) -> is_internal_node (bs, (share, counter)) node -> n = nat_of_N (var (bs, (share, counter)) node) -> BDDcompare (var (bs, (share, counter)) node) x = Datatypes.Lt -> bool_fun_independent (bool_fun_of_BDD (bs, (share, counter)) node) x). intros n0 H node x H0 H1 H2 H3. cut (bool_fun_independent (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node)) x). cut (bool_fun_independent (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node)) x). intros H4 H5. rewrite (proj2 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H0)) node H1). unfold bool_fun_independent in |- *. unfold bool_fun_eval in |- *. intro vb. unfold bool_fun_independent in H4, H5. unfold bool_fun_eval in H4, H5. inversion H1. inversion H6. inversion H7. unfold var, high, low in |- *. rewrite H8. unfold augment at 1 4 in |- *. cut (BDDvar_eq x x0 = false). intro H9. rewrite H9. unfold var, high, low in H5, H4. rewrite H8 in H4. rewrite H8 in H5. rewrite (H4 vb). rewrite (H5 vb). reflexivity. unfold BDDvar_eq in |- *. cut (N.eqb x x0 <> true). elim (N.eqb x x0). intro H9. absurd (true = true). assumption. reflexivity. reflexivity. unfold not in |- *. intro H9. unfold var in H3. rewrite H8 in H3. cut (nat_of_N x0 < nat_of_N x). cut (x = x0). intro H10. rewrite H10. exact (lt_irrefl (nat_of_N x0)). apply Neqb_complete. assumption. apply BDDcompare_lt. assumption. cut (node_OK bs (high (bs, (share, counter)) node)). intro H4. elim H4. intro H5. rewrite H5. apply bool_fun_independent_zero. assumption. intro H5. elim H5; intro H6. rewrite H6. apply bool_fun_independent_one. assumption. apply H 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. unfold is_internal_node in |- *. elim (option_sum _ (MapGet (BDDvar * (ad * ad)) (fst (bs, (share, counter))) (high (bs, (share, counter)) node))). intro y. elim y. intro x0. elim x0. intro y0. intro y1. elim y1. intro y2. intro y3. split with y0. split with y2. split with y3. assumption. intro y. unfold in_dom in H6. simpl in y. rewrite y in H6. discriminate H6. assumption. apply in_dom_is_internal. assumption. reflexivity. apply BDDcompare_trans with (y := var (bs, (share, counter)) node). apply BDDvar_ordered_high. assumption. assumption. apply in_dom_is_internal. assumption. assumption. exact (high_OK (bs, (share, counter)) node H0 H1). cut (node_OK bs (low (bs, (share, counter)) node)). intro H4. elim H4. intro H5. rewrite H5. apply bool_fun_independent_zero. assumption. intro H5. elim H5; intro H6. rewrite H6. apply bool_fun_independent_one. assumption. apply H 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. assumption. apply in_dom_is_internal. assumption. reflexivity. apply BDDcompare_trans with (y := var (bs, (share, counter)) node). apply BDDvar_ordered_low. assumption. assumption. apply in_dom_is_internal. assumption. assumption. exact (low_OK (bs, (share, counter)) node H0 H1). Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2