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

[PVS-Help] Using a finite subtype of nat and auto proving



——
logic : THEORY
BEGIN
D: TYPE = {i: nat | 1 <= i AND i <= 5}

D2: TYPE = {i: nat | i = 1 OR i= 2 OR i=3 OR i=4 OR i=5}

conj1: CONJECTURE (FORALL (x:D2) : x*x >= x)

END logic
————

(grind) works on conj1 with type D2.

But if we replace D2 with D, then (grind) will not work. In fact, I did not see how to prove it.

Is there a simple way to use D rather than D2 and to prove the conjecture?

Thanks

Jonathan