[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
>   BEGIN
>
>   %% 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.

(skosimp*)
(typepred "s!1")
(inst 1 "floor(s!1/2)")
(grind)

is a proof for your "greater"  lemma.

-Johan