[PVS-Help] Getting the prover to use axioms

[Nikhil Dinesh <nikhild@xxxxxxxxxxxxxx>]

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