[PVS-Help] record types and boolean relations

["Vera Pantelic" <pantelv@univmail.cis.mcmaster.ca>]

Hi,

When I want to prove the theorem proba as in:

proba1  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declaratio%ns
  % ENDASSUMING
  state: TYPE+ = [#a: int, b: int#]
  x: state
  P(x: state): bool = (a(x) = 2)
  f(x :{x: state | a(x) /= 1}, y: state): bool =
  table
  |a(x) = 1| ||
  |P(x)| a(y) = a(x) + 3||
  |a(x) = 5| a(y) = a(x) + 5||
  endtable
  proba: THEOREM forall (x: state): P(x) => exists (y: state): f(x, y)
 

  END proba1

I can do it only by exlicitly using the record type while instantiating
as in:

(proba1
 (proba 0
  (proba-1 nil 3325859506 3325901665
   ("" (skolem!)
    (("" (expand "f")
      (("" (ground)
        ((""
          (inst +
           "LET a = 3 + a(x!1), b = b(x!1) IN (#a := a, b := b#)")
          (("" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
However, since the function f given here is rather simplified version
of my function, I find it tedious and sometimes even impossible to do a
translation of the boolean relations by which the f is given to the
assignment (or LET) statements of record types. Is there any way of
instatiating in the previous proof without using the assignment
statements, but rather just boolean relation ?

Thanks.

Vera