Re: [PVS-Help] TCC Question (Stack followup)

```On Mon, 3 Oct 2005, Jeff Maddalon wrote:

> Now back to the version with TCCs.  Since the TCCs arise in the definition of

First, thanks to jeff and Bruno for helping me to understand the issue.

One final question: What do I do in cases where the value of the return
type cannot be easily expressed in terms of the arguments?

e.g. This works:

multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | u=x } =
IF y=0 THEN
x
ELSE
ENDIF
MEASURE y

but this does not:

multiple_add_sub(x:nat, y:nat): RECURSIVE { u: nat | y>0 => u>0 } =
IF y=0 THEN
x
ELSE
ENDIF
MEASURE y

In the above I was trying to just provide the type information and not
x=u. If I have to provide x=u, I wonder what I would do for a nasty
function whose value isn't easily expressed in terms of the arguments:

complex(x:nat, y:nat): RECURSIVE { u: nat | u=??? } =
IF y=0 THEN
x
ELSE
complex( (x+1) * y * complex(x+2,y-1), y-1)-1
ENDIF
MEASURE y

Thanks,
David

_____________________________________________________________________
David Coppit                           david@coppit.org
The College of William and Mary        http://coppit.org/

"They have computers, and they may have other weapons of mass destruction."
Former Attorney General Janet Reno, speaking at LLNL of modern criminals

```