YES

Consider the TRS R consisting of the following rewrite rules:

	f(x,x) -> f(a,b)
	b -> c

The TRS R is terminating because R is match-raise-bounded for
RFC#'(R) by 1.
A raise-compatible and quasi-deterministic tree automaton compatible
with match(R) and RFC#'(R) has
	- 6 states (1,...,6)
	- 4 final states (1,4,5,6)
	- 9 transitions:
		a_0 -> 2
		b_0 -> 3
		c_1 -> 3
		c_1 -> 5
		c_1 -> 6
		c_0 -> 5
		f_0(2,6) -> 1
		f_0(2,3) -> 1
		f_0(2,5) -> 1
		


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