YES

Consider the TRS R consisting of the following rewrite rule:

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

The TRS R is terminating because R is match-raise-bounded for
the set of all ground terms by 2.
A raise-consistent and quasi-deterministic tree automaton compatible
with match(R) and the set of all ground terms has
	- 5 states (1,...,5)
	- 3 final states (1,3,5)
	- 88 transitions:
		f_2(4,5) -> 1
		f_2(5,5) -> 1
		f_2(4,3) -> 1
		f_2(5,3) -> 1
		f_1(2,5) -> 1
		f_1(5,1) -> 1
		f_1(2,1) -> 1
		f_1(5,5) -> 1
		f_1(3,5) -> 1
		f_1(3,1) -> 1
		f_1(2,3) -> 1
		f_1(5,3) -> 1
		f_1(3,3) -> 1
		f_0(1,3) -> 1
		f_0(5,5) -> 1
		f_0(3,5) -> 1
		f_0(3,1) -> 1
		f_0(1,5) -> 1
		f_0(1,1) -> 1
		f_0(5,3) -> 1
		f_0(3,3) -> 1
		f_0(5,1) -> 1
		g_2(3,3) -> 4
		g_2(3,3) -> 2
		g_2(3,3) -> 1
		g_2(3,3) -> 3
		g_2(3,3) -> 5
		g_2(5,1) -> 5
		g_2(5,1) -> 3
		g_2(5,1) -> 1
		g_2(5,1) -> 2
		g_2(5,1) -> 4
		g_2(5,5) -> 5
		g_2(5,5) -> 3
		g_2(5,5) -> 1
		g_2(5,5) -> 2
		g_2(5,5) -> 4
		g_2(3,5) -> 5
		g_2(3,5) -> 3
		g_2(3,5) -> 1
		g_2(3,5) -> 2
		g_2(3,5) -> 4
		g_2(3,1) -> 4
		g_2(3,1) -> 2
		g_2(3,1) -> 1
		g_2(3,1) -> 3
		g_2(3,1) -> 5
		g_2(5,3) -> 5
		g_2(5,3) -> 3
		g_2(5,3) -> 1
		g_2(5,3) -> 2
		g_2(5,3) -> 4
		g_1(5,1) -> 3
		g_1(5,1) -> 2
		g_1(5,1) -> 1
		g_1(1,3) -> 3
		g_1(1,3) -> 1
		g_1(1,3) -> 2
		g_1(5,5) -> 3
		g_1(5,5) -> 2
		g_1(5,5) -> 1
		g_1(3,5) -> 3
		g_1(3,5) -> 2
		g_1(3,5) -> 1
		g_1(3,1) -> 3
		g_1(3,1) -> 1
		g_1(3,1) -> 2
		g_1(1,5) -> 3
		g_1(1,5) -> 2
		g_1(1,5) -> 1
		g_1(1,1) -> 2
		g_1(1,1) -> 1
		g_1(1,1) -> 3
		g_1(5,3) -> 3
		g_1(5,3) -> 2
		g_1(5,3) -> 1
		g_1(3,3) -> 3
		g_1(3,3) -> 1
		g_1(3,3) -> 2
		g_0(1,3) -> 1
		g_0(5,5) -> 1
		g_0(3,5) -> 1
		g_0(3,1) -> 1
		g_0(1,5) -> 1
		g_0(1,1) -> 1
		g_0(5,3) -> 1
		g_0(3,3) -> 1
		g_0(5,1) -> 1
		


________________________________________________________________
TTTbox (0.010 seconds) - April 13, 2007
Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/HM/t006.trs