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

[PVS-Help] Prime factors



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