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

Re: [PVS-Help] using "exists_not"



Rene,
Try 

(use "exists_not[nat]")

In general, when using a definition from a parameterized theory, provide
the actual parameters.

Cesar

On Thu, 2004-04-08 at 08:00, Rene Ladan wrote:
> 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
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855