# [PVS-Help] Proof: limit of strictly monotonic function over naturals

```Yoshimi Takano <yoshimi.takano@gmail.com> writes:
> I'm still unexperienced in using PVS, so could anyone please tell me
> how to prove the following theorem?
>
>   f: VAR [nat -> int]
>
>   strictly_monotonic(f): bool =
>     FORALL (n: nat): f(n) < f(n + 1)
>
>   unbounded(f): bool =
>     FORALL (x: int): EXISTS (n: nat): f(n) >= x
>
>   strictly_monotonic_unbounded: THEOREM
>     FORALL f: strictly_monotonic(f) IMPLIES unbounded(f)

You want to do some kind of induction over 'x' in the expansion of
'unbounded'.  However, induction is over the nats, not the ints.
Observe, though, that for any given 'x', the distance between 'x' and
'f(n)' is decreasing for increasing values of 'n'.  This suggests using
measure induction.  One measure you could try is 'x - f(0)', but this
doesn't quite work, because that measure might be negative.  Then
observe that if it is negative, you are done, because then 'f(0)' is the
element you need to show that you have reached or exceeded 'x'.  This

(expand* "unbounded" "strictly_monotonic")
(skosimp)
(measure-induct+ "IF x >= f!1(0) THEN x - f!1(0) ELSE 0 ENDIF" ("x"))
(("1"
(inst - "x!1 - 1")
(smash)
(("1" (skolem!) (inst - "n!1") (inst + "1 + n!1") (assert))
("2" (inst - "0") (inst + "1") (assert))
("3" (inst + "0") (assert))))
("2" (assert))))

Regards,
--
Jerry James
Email: james@ittc.ku.edu -or- jamesj@acm.org
WWW:   http://www.ittc.ku.edu/~james/

```