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