proposition: Lemma BDDneg_1_1_eq_1 : forall (bound : nat) (cfg : BDDconfig) (memo : BDDneg_memo) (node : ad), BDDneg_1_1 cfg memo node bound = BDDneg_1 (cfg, node, memo) bound.
proof: Proof. simple induction bound. intros cfg memo node. simpl in |- *. reflexivity. simpl in |- *. intros n H cfg memo node. elim (MapGet (BDDvar * (ad * ad)) (fst cfg) node). 2:{ reflexivity. } intro a. elim a. intros y y0. elim y0. intros y1 y2. cut (BDDneg_1_1 cfg memo y1 n = BDDneg_1 (cfg, y1, memo) n). intro H0. rewrite H0. elim (BDDneg_1 (cfg, y1, memo) n). intros y3 y4. elim y3. intros y5 y6. simpl in |- *. cut (BDDneg_1_1 y5 y4 y2 n = BDDneg_1 (y5, y2, y4) n). intro H1. rewrite H1. elim (BDDneg_1 (y5, y2, y4) n). intros y7 y8. simpl in |- *. elim y7. intros y9 y10. simpl in |- *. elim (BDDmake y9 y y6 y10). intros y11 y12. simpl in |- *. reflexivity. apply H. apply H. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2 bdd6 bdd7 BDDdummy_lemma_2 BDDdummy_lemma_3 BDDdummy_lemma_4 bdd8