Re: [PVS-Help] Getting the prover to use axioms

```You have to use the axiom as a lemma, e.g.,

(lemma "AxMaxId)

and then

(assert).

Cesar

Nikhil Dinesh wrote:
> Hi,
>
> I've been unable get the prover to use axioms in the theory. For example:
>
> state : THEORY
>
>   BEGIN
>
>   State : TYPE =
>    [#
>      fDomain : [nat -> bool],
>      fGetAtt : [nat, string -> string],
>      fMaxId : nat
>    #]
>
>
>   s : VAR State
>   i : VAR nat
>
>   AxMaxId : AXIOM
>     FORALL s:
>      LET maxId = fMaxId(s) IN
>      LET d = fDomain(s) IN
>       FORALL i: d(i) => i < maxId
>
>    ThCheck2 : CONJECTURE
>     FORALL s:
>      LET d = fDomain(s) in
>      LET maxId = fMaxId(s) IN
>       FORALL i: d(i) => i < maxId
>
>
>   END state
>
> The conjecture is identical to the axiom...so it should be provable,
> right? Here is the output of M-x  pr:
>
> ThCheck2 :
>
>   |-------
> {1}   FORALL s:
>         LET d = fDomain(s) IN
>           LET maxId = fMaxId(s) IN FORALL i: d(i) => i < maxId
>
> Rule? (grind)
> Trying repeated skolemization, instantiation, and if-lifting,
> this simplifies to:
> ThCheck2 :
>
> {-1}  i!1 >= 0
> {-2}  fDomain(s!1)(i!1)
>   |-------
> {1}   i!1 < fMaxId(s!1)
>
> How do I get the prover to use AxMaxId?
>
> Thanks,
> -Nikhil
>
>
>

--
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace         mailto:Cesar.A.Munoz@nasa.gov
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4

```