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

[PVS-Help] prime(7) unprovable



Hi,

This says it all, I'm using PVS3.1:

prime(5) succeeds with a single (grind), but for prime(7) :

p7 :  

  |-------
{1}   prime(7)

Rule? (grind)
divides rewrites divides(m, 7)
  to EXISTS (k: int): k * m = 7
prime rewrites prime(7)
  to FORALL (m: posnat):
        (m > 1 AND m < 7) IMPLIES NOT (EXISTS (k: int): k * m = 7)
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to: 
p7 :  

{-1}  integer_pred(k!1)
{-2}  m!1 > 0
{-3}  m!1 > 1
{-4}  m!1 < 7
{-5}  k!1 * m!1 = 7
  |-------

Rule? 

%definitions divides and prime are from divisibiliy.pvs,primes.pvs (c) r.w.butler@larc.nasa.gov
divides(m:posnat,n:nat) : bool =
  (EXISTS (k:int): k*m = n)

prime(n:int) : bool =
  (FORALL (m:posnat): (m>1 AND m<n) IMPLIES NOT divides(m,n)) AND (n>1)

p7:CONJECTURE prime(7)

The '>' and '<' signs are also proven in prime.pvs in lemma 'prime_rew'

Regards,
Rene

r.c.ladan@student.tue.nl

PGP signature