YES

Consider the TRS R consisting of the following rewrite rules:

	f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v))
	f(x,y,y) -> y
	f(x,y,g(y)) -> x
	f(x,x,y) -> x
	f(g(x),x,y) -> y

The TRS R is transformed (by dropping rewrite rules whose left-hand
sides contain a function symbol which does not occur in any right-hand
side) into a TRS R' consisting of the following rewrite rules:

	f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v))
	f(x,y,y) -> y
	f(x,x,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)
	- 51 transitions:
		2 -> 5
		4 -> 5
		6 -> 5
		#_0 -> 4
		#_0 -> 5
		#_0 -> 6
		f_0(2,6,6) -> 5
		f_0(4,6,6) -> 5
		f_0(6,6,6) -> 5
		f_0(2,6,4) -> 5
		f_0(4,6,4) -> 5
		f_0(6,6,4) -> 5
		f_0(2,4,3) -> 5
		f_0(4,4,3) -> 5
		f_0(6,4,3) -> 5
		f_0(2,2,5) -> 5
		f_0(2,2,2) -> 5
		f_0(4,2,5) -> 5
		f_0(4,2,2) -> 5
		f_0(6,2,5) -> 5
		f_0(6,2,2) -> 5
		f_0(2,4,6) -> 5
		f_0(4,4,6) -> 5
		f_0(6,4,6) -> 5
		f_0(2,6,5) -> 5
		f_0(2,6,2) -> 5
		f_0(4,6,5) -> 5
		f_0(4,6,2) -> 5
		f_0(6,6,5) -> 5
		f_0(6,6,2) -> 5
		f_0(2,4,4) -> 5
		f_0(4,4,4) -> 5
		f_0(6,4,4) -> 5
		f_0(2,2,3) -> 5
		f_0(4,2,3) -> 5
		f_0(6,2,3) -> 5
		f_0(2,2,6) -> 5
		f_0(2,6,3) -> 5
		f_0(4,2,6) -> 5
		f_0(4,6,3) -> 5
		f_0(6,2,6) -> 5
		f_0(6,6,3) -> 5
		f_0(2,4,5) -> 5
		f_0(2,4,2) -> 5
		f_0(4,4,5) -> 5
		f_0(4,4,2) -> 5
		f_0(6,4,5) -> 5
		f_0(6,4,2) -> 5
		f_0(2,2,4) -> 5
		f_0(4,2,4) -> 5
		f_0(6,2,4) -> 5
		


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