YES

Consider the TRS R consisting of the following rewrite rules:

	if(true,x,y) -> x
	if(false,x,y) -> y
	if(x,y,y) -> y
	if(if(x,y,z),u,v) -> if(x,if(y,u,v),if(z,u,v))

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:

	if(x,y,y) -> y
	if(if(x,y,z),u,v) -> if(x,if(y,u,v),if(z,u,v))

The TRS R is terminating because R' is match-raise-bounded for
RFC#'(R') by 0.
A raise-compatible and quasi-deterministic tree automaton compatible
with match(R') and RFC#'(R') has
	- 11 states (1,...,11)
	- 7 final states (1,2,7,8,9,10,11)
	- 52 transitions:
		8 -> 7
		9 -> 7
		10 -> 7
		11 -> 7
		u_0 -> 8
		u_0 -> 7
		u_0 -> 10
		v_0 -> 9
		v_0 -> 7
		v_0 -> 11
		#_0 -> 1
		if_0(1,9,10) -> 7
		if_0(1,11,9) -> 7
		if_0(1,11,6) -> 7
		if_0(1,5,11) -> 7
		if_0(1,9,8) -> 7
		if_0(1,10,11) -> 7
		if_0(1,7,7) -> 7
		if_0(1,8,10) -> 7
		if_0(1,5,9) -> 7
		if_0(1,5,6) -> 7
		if_0(1,10,9) -> 7
		if_0(1,10,6) -> 7
		if_0(1,8,8) -> 7
		if_0(1,9,11) -> 7
		if_0(1,10,4) -> 7
		if_0(1,7,10) -> 7
		if_0(1,11,7) -> 7
		if_0(1,9,9) -> 7
		if_0(1,9,6) -> 7
		if_0(1,3,11) -> 7
		if_0(1,7,8) -> 7
		if_0(1,8,11) -> 7
		if_0(1,5,7) -> 7
		if_0(1,3,9) -> 7
		if_0(1,10,7) -> 7
		if_0(1,11,10) -> 7
		if_0(1,8,9) -> 7
		if_0(1,8,6) -> 7
		if_0(1,3,4) -> 7
		if_0(1,7,11) -> 7
		if_0(1,11,8) -> 7
		if_0(1,8,4) -> 7
		if_0(1,5,10) -> 7
		if_0(1,9,7) -> 7
		if_0(1,10,10) -> 7
		if_0(1,7,9) -> 7
		if_0(1,7,6) -> 7
		if_0(1,5,8) -> 7
		if_0(1,10,8) -> 7
		if_0(1,11,11) -> 7
		if_0(1,8,7) -> 7
		


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