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

["Cesar A. Munoz" <munoz@nianet.org>]

On Tue, 2006-04-11 at 13:05, TommyC wrote:
> 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? 

I don't know if there is a reason as I'am not sure what is the problem
you are having with the proof. Maybe you are missing the  subtype
predicate of "s" when skolemizing. The rest of the proof seems
straightforward to me. 

Cesar

-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4