forall n: Name, p: PhoneNumber . forall b: PhoneBook . [true* . addPhone(n,p) . !(delPhone(n) || exists q: PhoneNumber . changePhone(n, q))* . findPhone(n) . !(delPhone(n) || exists q: PhoneNumber . changePhone(n, q))*] [getPhoneBook(b)] val(b(n) == p)