YES

Consider the TRS R consisting of the following rewrite rules:

	minus(minus(x)) -> x
	minux(+(x,y)) -> +(minus(y),minus(x))
	+(minus(x),+(x,y)) -> y
	+(+(x,y),minus(y)) -> x

The TRS R is transformed (by dropping rewrite rules whose left-hand
sides contain a function symbol which does not occur in any right-hand
side) into a TRS R' which is empty. Hence R is terminating.

__________________________________________________________________
TTTbox (0.003 seconds) - April 13, 2007
Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/SK90/4.01.trs