proposition: Lemma BDDneg_1_lemma_4 : forall (arg : BDDconfig * ad * BDDneg_memo) (x : BDDvar) (l r : ad) (bound bound' : nat), bound = S bound' -> BDDneg_memo_lookup (snd arg) (snd (fst arg)) = None -> MapGet _ (fst (fst (fst arg))) (snd (fst arg)) = Some (x, (l, r)) -> BDDneg_1 arg bound = (BDDmake (fst (fst (BDDneg_1 (fst (fst (BDDneg_1 (fst (fst arg), l, snd arg) bound')), r, snd (BDDneg_1 (fst (fst arg), l, snd arg) bound')) bound'))) x (snd (fst (BDDneg_1 (fst (fst arg), l, snd arg) bound'))) (snd (fst (BDDneg_1 (fst (fst (BDDneg_1 (fst (fst arg), l, snd arg) bound')), r, snd (BDDneg_1 (fst (fst arg), l, snd arg) bound')) bound'))), BDDneg_memo_put (snd (BDDneg_1 (fst (fst (BDDneg_1 (fst (fst arg), l, snd arg) bound')), r, snd (BDDneg_1 (fst (fst arg), l, snd arg) bound')) bound')) (snd (fst arg)) (snd (BDDmake (fst (fst (BDDneg_1 (fst (fst (BDDneg_1 (fst (fst arg), l, snd arg) bound')), r, snd (BDDneg_1 (fst (fst arg), l, snd arg) bound')) bound'))) x (snd (fst (BDDneg_1 (fst (fst arg), l, snd arg) bound'))) (snd (fst (BDDneg_1 (fst (fst (BDDneg_1 (fst (fst arg), l, snd arg) bound')), r, snd (BDDneg_1 (fst (fst arg), l, snd arg) bound')) bound')))))).
proof: Proof. intro arg. elim arg. clear arg; intro y. elim y; clear y. intros cfg node memo x l r. intros bound bound' H H0 H1. elim (nat_sum bound). intro y. elim y; clear y; intros x0 y. rewrite H in y. injection y; intro. rewrite H. simpl in |- *. simpl in H0, H1. rewrite H0; rewrite H1. reflexivity. intro y. rewrite H in y; discriminate. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4