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

Re: [PVS-Help] using "exists_not"



Rene,

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

PVS normalizes sequents (by moving formulas to the other side of the
line) so that top level negations are removed.   It normally does this
automatically and this is the first time I've seen it not happen.
However, just doing an (assert) or (prop) will fix it and give you

  |------------
  {1} (FORALL(n:nat): boolean_function(n))

from which you should be able to proceed.

Regards,
John Rushby