YES

Consider the TRS R consisting of the following rewrite rules:

	g(0,f(x,x)) -> x
	g(x,s(y)) -> g(f(x,y),0)
	g(s(x),y) -> g(f(x,y),0)
	g(f(x,y),0) -> f(g(x,0),g(y,0))

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' consisting of the following rewrite rules:

	g(0,f(x,x)) -> x
	g(f(x,y),0) -> f(g(x,0),g(y,0))

The TRS R is terminating because R' is match-raise-bounded for
RFC#'(R') by 0.
A raise-compatible and quasi-deterministic tree automaton compatible
with match(R') and RFC#'(R') has
	- 7 states (1,...,7)
	- 3 final states (1,2,7)
	- 12 transitions:
		#_0 -> 1
		0_0 -> 3
		f_0(4,6) -> 7
		f_0(6,7) -> 7
		f_0(7,6) -> 7
		f_0(4,7) -> 7
		f_0(6,5) -> 7
		f_0(7,7) -> 7
		f_0(4,5) -> 7
		f_0(7,5) -> 7
		f_0(6,6) -> 7
		g_0(1,3) -> 6
		


___________________________________________________________________
TTTbox (0.005 seconds) - April 13, 2007
Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/various/23.trs