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

Re: infix-problem

PVS is not an automatic theorem prover--you have to give it some help.
In this case, getting rid of all the irrelevant clutter does the job:

(SKOSIMP*) (HIDE -1 -2 -3 -4) (GRIND)

You might want to download the tutorial examples and work through them
before trying your own.