YES

Consider the TRS R consisting of the following rewrite rules:

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

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


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