[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Dear PVS users

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)

Thanks in advance.