# Re: [PVS-Help] TCC question

```Francisco,

Note that when you write derivable[T](f), you are not declaring the type
of f, as f was defined somewhere.

For instance, when you write

sqrt_derivable_fun : LEMMA derivable[posreal](sqrt)

the type of sqrt is [nnreal -> real]. The type-checker tries to check
this type against [posreal -> real],  which is the type derivable
expects.

In some instances, PVS magically restricts the type of a function to the
type it expects. In this case sqrt : [nnreal->real] is automatically
restricted to LAMBDA(x:posreal):sqrt(x). This is the function that you
are actually passing to derivable. Use the Emacs command:
prettyprint-expanded (C-c C-q e) to see all the "invisible" coercions.

inv_sqrt_derivable_fun: LEMMA derivable[posreal](1/sqrt)

the PVS type-checker fails to compute the coercion you expect. You can
solve the problem easily by explicitly writing the restriction:

inv_sqrt_derivable_fun: LEMMA
derivable[posreal](LAMBDA(x:posreal):1/sqrt(x))

No TCC is generated in this case.

Hope that it helps,
Cesar

On Tue, 2006-02-14 at 09:16, Francisco Jose CHAVES ALONSO wrote:
> Hello,
>
> I have the following LEMMA:
>
>   inv_sqrt_derivable_fun: LEMMA derivable[posreal](1/sqrt)
>
> By the definition of derivable, in the theory derivatives with the
> parameter posreal, I have that  1/sqrt is of type
>
>   posreal -> real
>
> then the parameter of sqrt must be of type posreal, but my lemma
> generate the TCC
>
>   inv_sqrt_derivable_fun_TCC1: OBLIGATION FORALL (x1: nonneg_real):
> sqrt(x1) /= 0;
>
> That I can't prove. Why x1 in the TCC is not of type posreal as I
> expected and how can I solve it?
>