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

No Subject





a : VAR nnreal

mod_le(a) : NONEMPTY_TYPE 
   = { x : real | -a <= x AND x <= a } 

nmod1 : NONEMPTY_TYPE = { x : real | -1 > x OR x > 1}

mod_le1_fun : TYPE = 
   [real -> mod_le(1)] %functions with range in -1 to 1

nmod1_fun : TYPE = 
   [real -> nmod1] %functions with range _only_ outside -1 to 1

g : VAR mod_le1_fun
g1 : VAR nmod1_fun 

sums_nzfun : JUDGEMENT +(g,g1) HAS_TYPE nzfun

I want to use this with cos and sine which I have proven to be in
mod_le1_fun, however to use it with constants I found I had to add
something like this:

2nmod1 : JUDGEMENT 2 HAS_TYPE nmod1 

Then the constant function 2 can be used for g1 in sums_nzfun.


But this is obviously not a solution, as I don't want to restrict myself
to 2! Is there anyway for me to tell PVS that the reals <-1 or >1 are in
nmod1??? 



---------------------------------------------------------
Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
  - I want a single-skin cotton tent like Mr Weasley's
---------------------------------------------------------