YES

Consider the TRS R consisting of the following rewrite rules:

	.(1,x) -> x
	.(x,1) -> x
	.(i(x),x) -> 1
	.(x,i(x)) -> 1
	i(1) -> 1
	i(i(x)) -> x
	.(i(y),.(y,z)) -> z
	.(y,.(i(y),z)) -> z

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.004 seconds) - April 13, 2007
Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/D33/02.trs