proposition: Lemma BDDneg_memo_OK_1_lemma_2_1' : forall (cfg : BDDconfig) (memo : BDDneg_memo), BDDconfig_OK cfg -> BDDneg_memo_OK_2 cfg memo -> BDDneg_memo_OK_2 cfg (BDDneg_memo_put memo BDDzero BDDone).
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y; elim y; clear y; intros share counter. intros memo H H0. unfold BDDneg_memo_OK_2 in |- *. intros node node' bound H1 H2. unfold BDDneg_memo_put, BDDneg_memo_lookup in H1. rewrite (MapPut_semantics ad memo BDDzero BDDone node) in H1. elim (sumbool_of_bool (N.eqb BDDzero node)). intro y. cut (BDDzero = node). intro H3. rewrite y in H1. injection H1. intros H4. rewrite <- H3. rewrite <- H4. split. left; reflexivity. elim bound. simpl in |- *. elim H. intros H5 H6. elim H5; intros. rewrite H7. reflexivity. intros n H5. simpl in |- *. elim H. intros H6 H7. elim H6; intros. simpl in H9. rewrite H8. reflexivity. apply Neqb_complete. assumption. intro y. rewrite y in H1. unfold BDDneg_memo_OK_2 in H0. apply H0. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1