YES

Consider the TRS R consisting of the following rewrite rules:

	+(*(x,y),*(x,z)) -> *(x,+(y,z))
	+(+(x,y),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-consistent and quasi-deterministic tree automaton compatible
with match(R) and RFC#'(R) has
	- 9 states (1,...,9)
	- 6 final states (1,4,5,7,8,9)
	- 14 transitions:
		u_0 -> 6
		#_0 -> 2
		*_0(2,9) -> 7
		*_0(2,3) -> 7
		*_0(2,7) -> 7
		*_0(2,8) -> 7
		+_0(2,9) -> 8
		+_0(2,2) -> 3
		+_0(7,6) -> 9
		+_0(2,3) -> 8
		+_0(2,7) -> 8
		+_0(2,4) -> 8
		+_0(2,8) -> 8
		+_0(1,6) -> 9
		


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