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

[PVS-Help] Prime factors


I am wondering why I can't prove following specification:

prime: THEORY
    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,