[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] TCC question


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?

Thanks in advance


Francisco José Cháves (ENS-LIP) 
mailto: Francisco.Jose.Chaves.Alonso@ens-lyon.fr
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 84 36