Re: [PVS-Help] statements about skolemization constants

[Hendrik Tews <tews@tcs.inf.tu-dresden.de>]

Rene Ladan writes:
   From: Rene Ladan <r.c.ladan@student.tue.nl>
   Date: Tue, 20 Apr 2004 22:47:17 +0200
   Subject: [PVS-Help] statements about skolemization constants
   
   Infinite_Many_Primes: THEORY
   BEGIN
   
   non_prime_divides(m,n:nat) : bool =
     1<m AND m<n AND (EXISTS (k:nat): k*m = n)
   
   prime(n:nat) : bool =
     (FORALL (m:nat): NOT non_prime_divides(m,n))
   
   bigger_prime(n:nat) : bool = 
     (EXISTS (m:nat) : m>n AND prime(m))
   
   % this has no prove, gives rise to a counter-example
   main_statement : CONJECTURE
    NOT (FORALL (n:nat) : bigger_prime(n))
   

In Pvs you prove statements to be true, not false. So you should
write 

   main_statement : CONJECTURE
    (  NOT (FORALL (n:nat) : bigger_prime(n))  ) = false

or more succinct

   main_statement : CONJECTURE
    FORALL (n:nat) : bigger_prime(n)

In the prove of these conjectures you will need the counter
example in order to instanciate the exists in bigger_prime.


Bye,

Hendrik