YES

Consider the TRS R consisting of the following rewrite rules:

	f(x,g(x)) -> x
	f(x,h(y)) -> f(h(x),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 rule:

	f(x,h(y)) -> f(h(x),y)

The TRS R is terminating because R' is match-bounded for
the set of all ground terms by 1.
A tree automaton compatible with match(R') and the set of all ground
terms has
	- 2 states (1,...,2)
	- 1 final state (1)
	- 5 transitions:
		f_1(2,1) -> 1
		f_0(1,1) -> 1
		h_1(2) -> 2
		h_1(1) -> 2
		h_0(1) -> 1
		


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