YES

Consider the TRS R consisting of the following rewrite rules:

	f(j(x,y),y) -> g(f(x,k(y)))
	f(x,h1(y,z)) -> h2(0,x,h1(y,z))
	g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
	h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
	i(f(x,h(y))) -> y
	i(h2(s(x),y,h1(x,z))) -> z
	k(h(x)) -> h1(0,x)
	k(h1(x,y)) -> h1(s(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.005 seconds) - April 13, 2007
Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/SK90/2.61.trs