YES

Consider the TRS R consisting of the following rewrite rules:

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

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


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