YES

Consider the TRS R consisting of the following rewrite rule:

	f(f(y,z),f(x,f(a,x))) -> f(f(f(a,z),f(x,a)),f(a,y))

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
	- 8 states (1,...,8)
	- 1 final state (1)
	- 13 transitions:
		#_0 -> 3
		a_0 -> 2
		f_0(6,7) -> 1
		f_0(2,2) -> 5
		f_0(8,5) -> 6
		f_0(5,2) -> 5
		f_0(6,8) -> 1
		f_0(2,3) -> 8
		f_0(3,2) -> 5
		f_0(2,4) -> 7
		f_0(4,5) -> 6
		f_0(2,8) -> 7
		f_0(2,5) -> 4
		


__________________________________________________________________________
TTTbox (0.008 seconds) - April 13, 2007
Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/secret05/teparla1.trs