# [PVS-Help] record types and boolean relations

```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

```