proposition: Lemma bool_fun_preservation_1 : forall cfg cfg' : BDDconfig, BDDconfig_OK cfg -> BDDconfig_OK cfg' -> (forall (x : BDDvar) (l r a : ad), MapGet _ (fst cfg) a = Some (x, (l, r)) -> MapGet _ (fst cfg') a = Some (x, (l, r))) -> forall (n : nat) (node : ad), n = nat_of_N (var cfg node) -> config_node_OK cfg node -> bool_fun_eq (bool_fun_of_BDD cfg' node) (bool_fun_of_BDD cfg node).
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intro cfg'. elim cfg'; clear cfg'; intros bs' y'. elim y'; clear y'; intros share' counter'. intros H H0 H1 n. apply lt_wf_ind with (P := fun n : nat => forall node : ad, n = nat_of_N (var (bs, (share, counter)) node) -> config_node_OK (bs, (share, counter)) node -> bool_fun_eq (bool_fun_of_BDD (bs', (share', counter')) node) (bool_fun_of_BDD (bs, (share, counter)) node)). intros n0 H2 node H3 H4. cut (config_node_OK (bs', (share', counter')) node). intro H5. elim H4; intro. rewrite H6. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)). rewrite (proj1 (bool_fun_of_BDD_semantics (bs', (share', counter')) H0)). unfold bool_fun_eq in |- *; reflexivity. elim H6; intro. rewrite H7. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs', (share', counter')) H0))) . rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) . unfold bool_fun_eq in |- *; reflexivity. cut (is_internal_node (bs, (share, counter)) node). cut (is_internal_node (bs', (share', counter')) node). intros H8 H9. cut (bool_fun_eq (bool_fun_of_BDD (bs', (share', counter')) (low (bs', (share', counter')) node)) (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node))). cut (bool_fun_eq (bool_fun_of_BDD (bs', (share', counter')) (high (bs', (share', counter')) node)) (bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node))). intros H10 H11. cut (var (bs, (share, counter)) node = var (bs', (share', counter')) node). intro H12. apply bool_fun_eq_lemma with (x := var (bs, (share, counter)) node). apply bool_fun_of_BDD_ext. apply bool_fun_of_BDD_ext. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD (bs', (share', counter')) (high (bs', (share', counter')) node)). apply bool_fun_eq_symm. rewrite H12. apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD (bs, (share, counter)) (high (bs, (share, counter)) node)). assumption. apply bool_fun_of_BDDhigh. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD (bs', (share', counter')) (low (bs', (share', counter')) node)). rewrite H12. apply bool_fun_eq_symm; apply bool_fun_of_BDDlow; assumption; assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node)). assumption. apply bool_fun_of_BDDlow; assumption; assumption. unfold var in |- *. inversion H9. inversion H12. inversion H13. rewrite H14. rewrite (H1 x x0 x1 node H14). reflexivity. cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node)). cut (config_node_OK (bs', (share', counter')) (high (bs', (share', counter')) node)). intros H10 H11. inversion H9. inversion H12. inversion H13. cut (high (bs', (share', counter')) node = high (bs, (share, counter)) node). cut (low (bs', (share', counter')) node = low (bs, (share, counter)) node). intros H15 H16. elim H11; intro. rewrite H16; rewrite H17. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)). rewrite (proj1 (bool_fun_of_BDD_semantics (bs', (share', counter')) H0)). unfold bool_fun_eq in |- *; reflexivity. elim H17; intro. rewrite H16; rewrite H18. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs', (share', counter')) H0))) . rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) . unfold bool_fun_eq in |- *; reflexivity. rewrite H16. apply H2 with (m := nat_of_N (var (bs, (share, counter)) (high (bs, (share, counter)) node))). rewrite H3. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. assumption. apply in_dom_is_internal. assumption. reflexivity. assumption. unfold low in |- *. rewrite H14. rewrite (H1 x x0 x1 node H14). reflexivity. unfold high in |- *. rewrite H14. rewrite (H1 x x0 x1 node H14). reflexivity. apply high_OK. assumption. assumption. apply high_OK. assumption. assumption. cut (low (bs', (share', counter')) node = low (bs, (share, counter)) node). intro H10. rewrite H10. cut (config_node_OK (bs, (share, counter)) (low (bs, (share, counter)) node)). intro H11. elim H11. intro H12. rewrite H12. rewrite (proj1 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)). rewrite (proj1 (bool_fun_of_BDD_semantics (bs', (share', counter')) H0)). unfold bool_fun_eq in |- *; reflexivity. intro H12. elim H12; intro. rewrite H13. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) . rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs', (share', counter')) H0))) . unfold bool_fun_eq in |- *; reflexivity. apply H2 with (m := nat_of_N (var (bs, (share, counter)) (low (bs, (share, counter)) node))). rewrite H3. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. apply in_dom_is_internal. assumption. reflexivity. apply low_OK. assumption. assumption. apply low_OK. assumption. assumption. unfold low in |- *. inversion H9. inversion H10. inversion H11. rewrite H12. rewrite (H1 x x0 x1 node H12). reflexivity. apply in_dom_is_internal. elim (option_sum _ (MapGet _ (fst (bs, (share, counter))) node)). intro y. elim y; intro x. elim x; intros x0 x1. elim x1; intros y0 y1 y2. unfold in_dom in |- *. rewrite (H1 x0 y0 y1 node y2). reflexivity. intro y. unfold in_dom in H7. rewrite y in H7; discriminate. apply in_dom_is_internal. assumption. elim H4; intro. rewrite H5. left; reflexivity. elim H5; intro. rewrite H6; right; left; reflexivity. right; right. elim (option_sum _ (MapGet _ (fst (bs, (share, counter))) node)). intro y. elim y; intro x. elim x; intro y0. intro y1. elim y1; intros y2 y3 y4. unfold in_dom in |- *; rewrite (H1 y0 y2 y3 node y4); reflexivity. intro y. unfold in_dom in H6; rewrite y in H6; discriminate. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2