YES

Consider the TRS R consisting of the following rewrite rules:

	+(x,+(y,z)) -> +(+(x,y),z)
	+(*(x,y),+(x,z)) -> *(x,+(y,z))
	+(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u)

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


__________________________________________________________________
TTTbox (0.010 seconds) - April 13, 2007
Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/SK90/2.06.trs