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

[PVS-Help] [PVS HELP] problem with lemma



Hi,

proof of lemma reduced to

<...>
-----
{1} fp(t!1, 0, n!1)

it can be prooved with fp1 axiom.


Rule? (lemma "fp1" (alloc "alloc!1" i "0" m"n!1" p "t!1"))

PVS returns:

Found 0 resolutions etc.

when i wrote:

Rule? (lemma "fp1[global]" (alloc "alloc!1" i "0" m"n!1" p "t!1"))

there is another error:

Couldn't find a definition or lemma named fp1[global]
Expecting a formula or constant
No resolution for fp1[global]

  Check the actual parameters; the following instances are visible,
  but don't match the given actuals:
    y_spec_why.fp1

No change on: (lemma "fp1[global]"
                (alloc "alloc!1" i "0" m "n!1" p "t!1"))

How can I use fp1 axiom?

example in attachment.

I use Caduceus  1.20, Why 2.20 and PVS 4.2

problem.tar.gz