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

No Subject




Hanne,

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.

Please let me know if this works.

Regards,

-- 
-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/