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

[PVS-Help] using "exists_not"



Hi,

I'm using PVS 3.1 and want to apply the rule exists_not on the statement
NOT(NOT(FORALL (n:nat): boolean_function(n)))

PVS starts with
 {-1} NOT(FORALL(n:nat): boolean_function(n)))
 |------------
 (false)

when I give the command (use "exists_not") it answers with:
"
Found 0 resolutions for exists_not relative to the substitution.
Please check substitution, provide actual parameters for lemma name,
or supply more substitutions.
"

Using (prop) and then (use "not_forall") gives the same message.

In both cases there are no changes.

Rene Ladan
r.c.ladan@student.tue.nl

PGP signature