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

[PVS-Help] Problems proving a lemma in PVS

Dear helpers,
I have the following theory written and type-checked in PVS
theory_1[N: posint]: THEORY
%% All even integers >= 3N
S: TYPE = {t: posint | even?(t) AND t >= 3*N}
END theory_1
and have been asked to develop and prove a lemma that means "if s is of type S then there is an integer i with 2*i=s and i is greater than or equal to floor(N*3/2)".
What I have developed is
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. Is there a reason why I cannot prove this? If you need more information just reply to this e-mail.
Thanks very much for your help,
Tom Clark