[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