proposition: Lemma bool_fun_of_BDD_1_change_bound : forall cfg : BDDconfig, BDDconfig_OK cfg -> forall (bound : nat) (node : ad), nat_of_N (var cfg node) < bound -> bool_fun_of_BDD_1 cfg node bound = bool_fun_of_BDD_1 cfg node (S (nat_of_N (var cfg node))).
proof: Proof. intro cfg. elim cfg. clear cfg. intros bs y. elim y. clear y. intros share counter. intro H. intro bound. apply lt_wf_ind with (P := fun bound : nat => forall node : ad, nat_of_N (var (bs, (share, counter)) node) < bound -> bool_fun_of_BDD_1 (bs, (share, counter)) node bound = bool_fun_of_BDD_1 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node)))). intros n H0 node H1. elim (option_sum _ (MapGet _ (fst (bs, (share, counter))) node)). intros y. elim y. clear y. intro x. elim x. clear x. intros x y. elim y. clear y. intros l r. intros y. cut (is_internal_node (bs, (share, counter)) node). intro H2. cut (bool_fun_of_BDD_1 (bs, (share, counter)) node n = (fun vb : var_binding => match vb (var (bs, (share, counter)) node) with | true => bool_fun_of_BDD_1 (bs, (share, counter)) (high (bs, (share, counter)) node) (pred n) vb | false => bool_fun_of_BDD_1 (bs, (share, counter)) (low (bs, (share, counter)) node) (pred n) vb end)). intro H3. rewrite H3. cut (bool_fun_of_BDD_1 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node))) = (fun vb : var_binding => match vb (var (bs, (share, counter)) node) with | true => bool_fun_of_BDD_1 (bs, (share, counter)) (high (bs, (share, counter)) node) (pred (S (nat_of_N (var (bs, (share, counter)) node)))) vb | false => bool_fun_of_BDD_1 (bs, (share, counter)) (low (bs, (share, counter)) node) (pred (S (nat_of_N (var (bs, (share, counter)) node)))) vb end)). intro H4. rewrite H4. unfold pred at 3 4 in |- *. cut (bool_fun_of_BDD_1 (bs, (share, counter)) (high (bs, (share, counter)) node) (pred n) = bool_fun_of_BDD_1 (bs, (share, counter)) (high (bs, (share, counter)) node) (nat_of_N (var (bs, (share, counter)) node))). intro H5. rewrite H5. cut (bool_fun_of_BDD_1 (bs, (share, counter)) (low (bs, (share, counter)) node) (pred n) = bool_fun_of_BDD_1 (bs, (share, counter)) (low (bs, (share, counter)) node) (nat_of_N (var (bs, (share, counter)) node))). intro H6. rewrite H6. trivial. elim (option_sum _ (MapGet _ (fst (bs, (share, counter))) (low (bs, (share, counter)) node))). intros y0. elim y0. clear y0. intro x0. elim x0. clear x0. intros xl y0. elim y0. clear y0. intros ll rl. intros y0. cut (nat_of_N (var (bs, (share, counter)) (low (bs, (share, counter)) node)) < pred n). intro H6. cut (nat_of_N (var (bs, (share, counter)) (low (bs, (share, counter)) node)) < nat_of_N (var (bs, (share, counter)) node)). intro H7. clear H3 H4 H5. cut (pred n < n). intro H3. rewrite (H0 (pred n) H3 (low (bs, (share, counter)) node) H6). rewrite (H0 (nat_of_N (var (bs, (share, counter)) node)) H1 (low (bs, (share, counter)) node) H7). trivial. apply lt_pred_n_n. apply neq_O_lt. unfold not in |- *. intro H3. rewrite <- H3 in H1. cut (~ nat_of_N (var (bs, (share, counter)) node) < 0). unfold not in |- *. tauto. apply lt_n_O. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. unfold is_internal_node in |- *. split with xl. split with ll. split with rl. assumption. apply le_lt_trans with (m := pred (nat_of_N (var (bs, (share, counter)) node))). cut (forall x y : nat, x < y -> x <= pred y). intro H6. apply H6. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. unfold is_internal_node in |- *. split with xl. split with ll. split with rl. assumption. unfold lt in |- *. double induction x0 y1. auto. intro n0. intros H6 H7. auto with arith. auto with arith. intros n0 H6 n1 H7 H8. unfold pred in |- *. auto with arith. apply lt_pred. assumption. unfold not in |- *. intro H6. cut (var (bs, (share, counter)) node = N0). cut (var (bs, (share, counter)) node <> N0). auto. apply INFERIEUR_neq_O with (x := var (bs, (share, counter)) (low (bs, (share, counter)) node)). apply BDDvar_ordered_low. assumption. assumption. split with xl. split with ll. split with rl. assumption. apply O_N0. assumption. intros y0. apply bool_fun_of_BDD_1_semantics_2. assumption. elim (option_sum _ (MapGet _ (fst (bs, (share, counter))) (high (bs, (share, counter)) node))). intros y0. elim y0. clear y0. intro x0. elim x0. clear x0. intros xr y0. elim y0. clear y0. intros lr rr. intros y0. cut (nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node)) < pred n). intro H5. cut (nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node)) < nat_of_N (var (bs, (share, counter)) node)). intro H6. clear H3 H4. cut (pred n < n). intro H3. rewrite (H0 (nat_of_N (var (bs, (share, counter)) node)) H1 (high (bs, (share, counter)) node) H6). rewrite (H0 (pred n) H3 (high (bs, (share, counter)) node) H5). trivial. apply lt_pred_n_n. apply neq_O_lt. unfold not in |- *. intro H3. rewrite <- H3 in H1. cut (~ nat_of_N (var (bs, (share, counter)) node) < 0). unfold not in |- *. tauto. apply lt_n_O. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. assumption. unfold is_internal_node in |- *. split with xr. split with lr. split with rr. assumption. apply le_lt_trans with (m := pred (nat_of_N (var (bs, (share, counter)) node))). cut (forall x y : nat, x < y -> x <= pred y). intro H5. apply H5. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. assumption. unfold is_internal_node in |- *. split with xr. split with lr. split with rr. assumption. unfold lt in |- *. double induction x0 y1. auto. intro n0. intros H5 H6. auto with arith. auto with arith. intros n0 H5 n1 H6 H7. unfold pred in |- *. auto with arith. apply lt_pred. assumption. unfold not in |- *. intro H5. cut (var (bs, (share, counter)) node = N0). cut (var (bs, (share, counter)) node <> N0). auto. apply INFERIEUR_neq_O with (x := var (bs, (share, counter)) (high (bs, (share, counter)) node)). apply BDDvar_ordered_high. assumption. assumption. split with xr. split with lr. split with rr. assumption. apply O_N0. assumption. intro y0. apply bool_fun_of_BDD_1_semantics_2. assumption. apply (proj2 (proj2 (bool_fun_of_BDD_1_semantics_1 (bs, (share, counter)) H (S (nat_of_N (var (bs, (share, counter)) node)))))). unfold is_internal_node in |- *. split with x. split with l. split with r. assumption. auto with arith. apply (proj2 (proj2 (bool_fun_of_BDD_1_semantics_1 (bs, (share, counter)) H n))). unfold is_internal_node in |- *. split with x. split with l. split with r. assumption. auto with arith. unfold is_internal_node in |- *. split with x. split with l. split with r. assumption. intros y. apply bool_fun_of_BDD_1_semantics_2. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1