YES

Consider the TRS R consisting of the following rewrite rules:

	f(a) -> g(h(a))
	h(g(x)) -> g(h(f(x)))
	k(x,h(x),a) -> h(x)
	k(f(x),y,x) -> f(x)

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(a) -> g(h(a))
	h(g(x)) -> g(h(f(x)))

The TRS R is terminating because R' is match-bounded for
the set of all ground terms by 2.
A tree automaton compatible with match(R') and the set of all ground
terms has
	- 9 states (1,...,9)
	- 1 final state (1)
	- 17 transitions:
		4 -> 1
		4 -> 5
		5 -> 2
		6 -> 2
		9 -> 3
		a_1 -> 2
		a_0 -> 1
		f_2(3) -> 7
		f_1(3) -> 6
		f_1(1) -> 5
		f_0(1) -> 1
		g_2(8) -> 9
		g_1(3) -> 4
		g_0(1) -> 1
		h_2(7) -> 8
		h_1(2) -> 3
		h_0(1) -> 1
		


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