proposition: Lemma bool_fun_of_BDDlow : forall (cfg : BDDconfig) (node : ad), BDDconfig_OK cfg -> is_internal_node cfg node -> bool_fun_eq (bool_fun_of_BDD cfg (low cfg node)) (bool_fun_restrict (bool_fun_of_BDD cfg node) (var cfg node) false).
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intros node H H0. rewrite (proj2 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H)) node H0). unfold bool_fun_restrict in |- *. unfold bool_fun_eval in |- *. unfold bool_fun_eq in |- *. unfold bool_fun_eval in |- *. unfold augment at 1 in |- *. unfold BDDvar_eq in |- *. cut (N.eqb (var (bs, (share, counter)) node) (var (bs, (share, counter)) node) = true). intro H1. rewrite H1. intro vb. cut (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node) (augment vb (var (bs, (share, counter)) node) false) = bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node) vb). intro H2. rewrite H2. reflexivity. change (bool_fun_eval (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node)) (augment vb (var (bs, (share, counter)) node) false) = bool_fun_eval (bool_fun_of_BDD (bs, (share, counter)) (low (bs, (share, counter)) node)) vb) in |- *. apply bool_fun_independent_lemma. apply bool_fun_of_BDD_ext. apply BDDvar_independent_low. assumption. assumption. apply Neqb_correct. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2