YES

Consider the TRS R consisting of the following rewrite rules:

	rev(a) -> a
	rev(b) -> b
	rev(++(x,y)) -> ++(rev(y),rev(x))
	rev(++(x,x)) -> rev(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
	- 10 states (1,...,10)
	- 8 final states (1,2,3,5,7,8,9,10)
	- 29 transitions:
		#_0 -> 4
		++_0(9,6) -> 8
		++_0(8,8) -> 8
		++_0(10,9) -> 8
		++_0(5,9) -> 8
		++_0(7,10) -> 8
		++_0(7,6) -> 8
		++_0(9,7) -> 8
		++_0(8,9) -> 8
		++_0(10,10) -> 8
		++_0(10,6) -> 8
		++_0(5,6) -> 8
		++_0(7,7) -> 8
		++_0(9,8) -> 8
		++_0(8,10) -> 8
		++_0(5,10) -> 8
		++_0(8,6) -> 8
		++_0(10,7) -> 8
		++_0(5,7) -> 8
		++_0(7,8) -> 8
		++_0(9,9) -> 8
		++_0(8,7) -> 8
		++_0(10,8) -> 8
		++_0(5,8) -> 8
		++_0(7,9) -> 8
		++_0(9,10) -> 8
		rev_0(4) -> 7
		a_0 -> 9
		b_0 -> 10
		


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