[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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.
-- Paul S. Miner | phone: (757) 864-6201
-- 1 South Wright St. / MS 130 | fax: (757) 864-4234
-- NASA Langley Research Center | mailto:firstname.lastname@example.org
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/