proposition: Lemma BDDneg_1_lemma_2 : forall (arg : BDDconfig * ad * BDDneg_memo) (bound : nat), BDDneg_memo_lookup (snd arg) (snd (fst arg)) = None -> MapGet _ (fst (fst (fst arg))) (snd (fst arg)) = None -> BDDneg_1 arg bound = (if N.eqb (snd (fst arg)) BDDzero then (fst (fst arg), BDDone, BDDneg_memo_put (snd arg) BDDzero BDDone) else (fst (fst arg), BDDzero, BDDneg_memo_put (snd arg) BDDone BDDzero)).
proof: Proof. intro arg. elim arg. clear arg; intro y. elim y; clear y. intros cfg node memo bound. intros H H0. unfold BDDneg_1 in |- *. simpl in |- *. elim bound; rewrite H; simpl in |- *. simpl in H0. rewrite H0; reflexivity. fold BDDneg_1 in |- *. simpl in H0. rewrite H0. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4