[PVS-Help] recursive functions calling each other

["Lucian M. Patcas" <lucian.patcas@xxxxxxxxx>]

Hi there,

I have two recursive functions that call each other:

a(x: nat): RECURSIVE bool =
...
b(x)
...
MEASURE x

b(y: nat): RECURSIVE bool =
...
a(y)
...
MEASURE y

I don't know how to do this without getting resolution errors.

Thanks for your help,
Lucian