# Re: [PVS-Help] [PVS HELP] problem with lemma

```Hi Михаил,

The problem is that you're trying to instantiate a nested forall in one
shot

fp1: AXIOM
(FORALL (alloc: alloc_table):
(FORALL (i: int):
(i >= 0 IMPLIES
(FORALL (m: int):
(0 < m AND m < 32 IMPLIES
(FORALL (p: pointer[global]):
(valid[global](alloc, p) AND valid_range[global](alloc, p, i, m) IMPLIES
fp(p, i, m) >= 0)))))))

You can bring in fp1 with alloc instantiated:

Rule? (lemma "fp1" (alloc "alloc!1"))
Applying fp1 where
alloc gets alloc!1,
this simplifies to:
min_impl_po_1.1 :

{-1}  FORALL (i: int):
(i >= 0 IMPLIES
(FORALL (m: int):
(0 < m AND m < 32 IMPLIES
(FORALL (p: pointer[global]):
(valid[global](alloc!1, p) AND
valid_range[global](alloc!1, p, i, m)
IMPLIES fp(p, i, m) >= 0)))))
...

But after that you need to use inst to instantiate the rest (plus some
simplification, i.e., assert to get the quantifier to the top).

Hope this helps,
Sam

Гильмендинов Михаил <mix_-@mail.ru> wrote:

> 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

```