proposition: Lemma bool_fun_neg_eq_var_2 : forall (cfg : BDDconfig) (node node' : ad), BDDconfig_OK cfg -> is_internal_node cfg node -> is_internal_node cfg node' -> bool_fun_eq (bool_fun_of_BDD cfg node') (bool_fun_neg (bool_fun_of_BDD cfg node)) -> var cfg node = var cfg node'.
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y; elim y; clear y; intros share counter. intros node node' H H0 H1 H2. cut (BDDconfig_OK (fst (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node))))) /\ (forall (x : BDDvar) (l r a : ad), MapGet _ (fst (bs, (share, counter))) a = Some (x, (l, r)) -> MapGet _ (fst (fst (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node)))))) a = Some (x, (l, r))) /\ (is_internal_node (bs, (share, counter)) node -> is_internal_node (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))))) /\ var (bs, (share, counter)) node = var (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)))))) /\ config_node_OK (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))))) /\ bool_fun_eq (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)))))) (bool_fun_neg (bool_fun_of_BDD (bs, (share, counter)) node))). intro H3. cut (var (bs, (share, counter)) node' = var (fst (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node))))) node'). intro H4. cut (var (bs, (share, counter)) node = var (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. rewrite H4. cut (snd (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node)))) = node'). intro H6. rewrite H6. reflexivity. apply BDDunique with (cfg := fst (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node))))). exact (proj1 H3). exact (proj1 (proj2 (proj2 (proj2 H3)))). inversion H1. inversion H6. inversion H7. right. right. unfold in_dom in |- *. rewrite (proj1 (proj2 H3) x x0 x1 node' H8). reflexivity. apply bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_of_BDD (bs, (share, counter)) node)). exact (proj2 (proj2 (proj2 (proj2 H3)))). apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD (bs, (share, counter)) node'). apply bool_fun_eq_symm; assumption. apply bool_fun_eq_symm. apply bool_fun_preservation. assumption. exact (proj1 H3). exact (proj1 (proj2 H3)). right. right. unfold in_dom in |- *. inversion H1. inversion H6. inversion H7. rewrite H8; reflexivity. exact (proj2 (proj1 (proj2 (proj2 H3)) H0)). inversion H1. inversion H4. inversion H5. unfold var at 1 2 in |- *. rewrite (proj1 (proj2 H3) x x0 x1 node' H6). rewrite H6. reflexivity. apply BDDneg_2_lemma. assumption. right. right. inversion H0. inversion H3. inversion H4. unfold in_dom in |- *; rewrite H5; reflexivity. 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