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

[PVS-Help] Re: Problems proving a lemma in PVS

>   theory_1[N: posint]: THEORY
>   %% All even integers >= 3N
>   S: TYPE = {t: posint | even?(t) AND t >= 3*N}
>   END theory_1

>   greater: LEMMA FORALL(s: S): EXISTS (i: int): 2*i=s AND i>=floor(N*(3/2))
>   This type checks correctly with no TCCs but I cannot prove it.

(typepred "s!1")
(inst 1 "floor(s!1/2)")

is a proof for your "greater"  lemma.