# Phonebook example from WIFT'95 paper not working?

```Hi, I'm just starting " A Tutorial Intro. to PVS" from WIFT;95, and PVS's
response to the second example is not what the paper promises.  On page
11, relating to CONJECTURE DelAdd2, the paper says that "(grind :theories
("phone_1")) strategy proves this".  however,  PVS Version 2.1 (patch
level 2.417) says:

|-------
{1}    FORALL (bk: B), (nm: N), (pn: P):
FindPhone(bk, nm) = n0 => DelPhone(AddPhone(bk, nm, pn), nm) =bk

Rule? (grind :theories ("phone_1"))
FindAx rewrites FindPhone(bk, nm)
to  bk(nm)
to  bk WITH [(nm) := pn]
Delax rewrites DelPhone(bk WITH [(nm) := pn], nm)
to  bk WITH [(nm) := n0]
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to:

{-1}    bk!1(nm!1) = n0
|-------
{1}    bk!1 WITH [(nm!1) := n0] = bk!1

Rule?

Help, What do I do now?

thanks....

-------------------------------------
btw, here is my phone_1.pvs file:
phone_1 : THEORY

BEGIN

N : TYPE
P : TYPE
B : TYPE = [N -> P]

n0: P
emptybook : B
emptyax: AXIOM FORALL (nm: N) : emptybook(nm) = n0

FindPhone : [B, N -> P]
FindAx : AXIOM FORALL (bk:B) (nm: N): FindPhone(bk,nm) = bk(nm)

Addax : AXIOM FORALL (bk:B),(nm:N),(pn:P):
AddPhone(bk,nm,pn) = bk WITH [(nm) := pn]

FindAdd: CONJECTURE FORALL (bk:B), (nm:N), (pn:P):

DelPhone : [B, N -> B]
Delax : AXIOM FORALL (bk:B),(nm:N): DelPhone (bk,nm) = bk WITH [(nm) := n0]

DelAdd2: CONJECTURE FORALL (bk:B),(nm:N),(pn:P) :
FindPhone(bk,nm) = n0 =>  DelPhone(AddPhone(bk,nm,pn),nm) = bk

END phone_1

- Byron

```