# problem

```
Dear experts:

I met the following problem while trying to prove a theorem involving
the recursive function c_sealed_in () using type t as one of its
arguments.

(1) I define t as a non-negative real number as follows

*** type declaration ********************

K: posreal

non_neg: TYPE = { x: real | x>=0 } CONTAINING 0

time: TYPE = non_neg

t: VAR time

clock: TYPE = { t: time | EXISTS(n: nat): t=n*K } CONTAINING 0

x: VAR clock

init(x): bool = (x=0)

noninit_elem: TYPE ={ x | not init(x) }

y: VAR noninit_elem

pre(y): clock = y - K

(2) I defined a recursive function using t as its arguments.

****** function definition

c_sealed_in(param_trip,manual_reset)(t): RECURSIVE bool =
IF  init(t) THEN  TRUE ELSE
COND
Held_For(param_trip,seal_in_delay)(t) -> TRUE,
NOT Held_For(param_trip,seal_in_delay)(t)
AND manual_reset(t) -> FALSE,
NOT Held_For(param_trip,seal_in_delay)(t) AND
NOT manual_reset(t) ->
c_sealed_in(param_trip,manual_reset)(pre(t)),
ENDCOND
ENDIF
MEASURE rank(t)

(3) In the actual proof, we get the sequent Seal.1 as follows

****** problematic sequent *****************
Seal.1:

{-1}    (x!1 = 0)
{-2}    c_sealed_in(param_trip!1, manual_reset!1)(0)
|-------
{1}

(4) After expanding the function definition, pre(0) appears as an argument
to function c_sealed_in(). So we encounter infinite loop after using
grind.

Rule? (EXPAND "c_sealed_in")
Expanding the definition of c_sealed_in,
this simplifies to:
Seal.1:

[-1]    (x!1 = 0)
{-2}    IF 0=0 THEN TRUE
ELSE COND
Held_For(param_trip!1, seal_in_delay)(0) -> TRUE,
manual_reset!1(0) -> FALSE,
ELSE -> c_sealed_in(param_trip!1, manual_reset!1)(pre(0))
ENDCOND
ENDIF
|-------
[1]

(5) My question: Since we define the argument t as a non-negative real
number, why the PVS allows the negative number appear as the function
argument after rewriting the recursive function? Is this a problem in my
function definition or a PVS bug.