No Subject

[Hanne Gottliebsen <hago@dcs.st-and.ac.uk>]

I am trying to write judgements wrt cos(x)+y being non-zero for y < -1 or
y > 1.

The following gives us most of that:

a : VAR nnreal
x : VAR real
mod_le(a) : NONEMPTY_TYPE = { x : real | -a <= x AND x <= a } CONTAINING 0
nmod1 : NONEMPTY_TYPE = { x | -1 > x OR x > 1}

cos_is_in_mod1 : JUDGEMENT cos(x) HAS_TYPE mod_le(1)

sums_cosnsin : JUDGEMENT +(x:mod_le(1),y:nmod1) HAS_TYPE nzreal

2nmod1 : JUDGEMENT 2 HAS_TYPE nmod1


With this,   

test1 : LEMMA
   continuous(lambda (x:real) : 1/(cos(x)+2), y)

generates no TCCs whereas this one does:

test2 : LEMMA
   continuous(lambda (x:real) : 1/(cos(x)+3), y)
                                         ^^^


So I need to make 2nmod1 general - but is that possible at all?


Thanks,
Hanne
---------------------------------------------------------
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
---------------------------------------------------------