Re: [PVS-Help] Prime factors

["Ricky W. Butler" <R.W.Butler@larc.nasa.gov>]

Since the lemmas involve set equalities, you will have
to use (APPLY-EXTENSIONALITY 1) before (GRIND).  Sets
are functions.  TAB E will save you some typing.

Rick Butler

At 06:57 AM 11/4/2004, Ingo Feinerer wrote:
>Hi!
>
>I am wondering why I can't prove following specification:
>
>prime: THEORY
>   BEGIN
>     n: VAR nat
>
>     factors(n): set[nat] =
>       { x: nat | x >= 2 AND x <= (n - 1) AND rem(x)(n) = 0 }
>
>     factors_test: LEMMA factors(8) = add(2, add(4, emptyset[nat]))
>     factors_test2: LEMMA factors(17) = emptyset[nat]
>   END prime
>
>I have tried "(grind)" to prove "factors_test", but no simplification
>happens. The result set is well defined (input are natural numbers, and the
>values are bounded), so it should be possible to prove this.
>
>Thanks for any advice,
>
>Ingo