YES

Consider the TRS R consisting of the following rewrite rules:

	*(i(x),x) -> 1
	*(1,y) -> y
	*(x,0) -> 0
	*(*(x,y),z) -> *(x,*(y,z))

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:

	*(x,0) -> 0
	*(*(x,y),z) -> *(x,*(y,z))

The TRS R is terminating because R' is match-bounded for
RFC#(R') by 1.
A tree automaton compatible with match(R') and RFC#(R') has
	- 4 states (1,...,4)
	- 2 final states (1,2)
	- 8 transitions:
		1 -> 4
		2 -> 4
		#_0 -> 3
		*_0(3,4) -> 2
		*_0(3,3) -> 4
		0_1 -> 2
		0_0 -> 1
		0_0 -> 2
		


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