6 A Note on Mechanizing Higher Order Logic J. A. Robinson

Of course, it is not at all obvious that (5) and (1) describe the same function. In order to prove that they do, however, it is necessary only to check that the result of applying (5) to an arbitrary object z is the same as the result of applying (1) to z. In fact, we have (xx(sQRT((rimEs x)((pLus x)oNE)))z) (sQRT((TimEs z)((pLus z)oNE))) when (1) is applied to z.