YES

Consider the TRS R consisting of the following rewrite rules:

	\(x,x) -> e
	/(x,x) -> e
	.(e,x) -> x
	.(x,e) -> x
	\(e,x) -> x
	/(x,e) -> x
	.(x,\(x,y)) -> y
	.(/(y,x),x) -> y
	\(x,.(x,y)) -> y
	/(.(y,x),x) -> y
	/(x,\(y,x)) -> y
	\(/(x,y),x) -> y

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/D33/01.trs