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

[PVS-Help] using "exists_not"


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)))

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

PGP signature