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

Re: your mail



Paul,

> I think the difficulty is because type nmod1 is disjunctive.  Proving
> this TCC may require a split. The decision procedures are not able to
> use its clauses effectively.  You might try breaking nmod1 into two
> types.  One for x < -1, the other for x > 1.  Then you could introduce
> two judgements for sums_cosnsin.

Thanks for your suggestion!

I just tried this (having nmod1_pos and nmod1_neg) and two of each of the
judgements I use. However, it still doesn't work. 

Any other ideas???


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
---------------------------------------------------------