proposition: Lemma BDDneg_memo_OK_bool_fun_1 : forall (cfg : BDDconfig) (memo : BDDneg_memo) (node node' : ad), BDDconfig_OK cfg -> BDDneg_memo_OK_1 cfg memo -> config_node_OK cfg node -> BDDneg_memo_lookup memo node = Some node' -> bool_fun_eq (bool_fun_of_BDD cfg node') (bool_fun_neg (bool_fun_of_BDD cfg node)).
proof: Proof. intro cfg. elim cfg; clear cfg. intros bs y. elim y; clear y; intros share counter. intros memo node node' H H0 H1 H2. unfold BDDneg_memo_OK_1 in H0. cut (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node))) = (bs, (share, counter), node')). intro H3. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < S (nat_of_N (var (bs, (share, counter)) node))). intro H4. cut (bool_fun_of_BDD (bs, (share, counter)) node' = bool_fun_of_BDD (fst (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node))))) (snd (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node)))))). intro H5. rewrite H5. exact (proj2 (proj2 (proj2 (proj2 (BDDneg_2_lemma (S (nat_of_N (var (bs, (share, counter)) node))) (bs, (share, counter)) node H H1 H4))))). rewrite H3. simpl in |- *. reflexivity. intro H4. unfold lt in |- *; apply le_n. apply H0. assumption. assumption. intro H3. unfold lt in |- *; apply le_n. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4