YES

Consider the TRS R consisting of the following rewrite rules:

	+(-(x,y),z) -> -(+(x,z),y)
	-(+(x,y),y) -> 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)
	- 27 transitions:
		2 -> 5
		4 -> 5
		6 -> 5
		#_0 -> 4
		#_0 -> 5
		#_0 -> 6
		+_0(4,6) -> 3
		+_0(2,2) -> 3
		+_0(6,4) -> 3
		+_0(2,6) -> 3
		+_0(4,4) -> 3
		+_0(2,4) -> 3
		+_0(6,2) -> 3
		+_0(6,6) -> 3
		+_0(4,2) -> 3
		-_0(3,4) -> 5
		-_0(4,6) -> 5
		-_0(6,4) -> 5
		-_0(5,2) -> 5
		-_0(4,4) -> 5
		-_0(5,6) -> 5
		-_0(3,2) -> 5
		-_0(3,6) -> 5
		-_0(6,2) -> 5
		-_0(5,4) -> 5
		-_0(6,6) -> 5
		-_0(4,2) -> 5
		


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