YES

Consider the TRS R consisting of the following rewrite rules:

	or(x,x) -> x
	and(x,x) -> x
	not(not(x)) -> x
	not(and(x,y)) -> or(not(x),not(y))
	not(or(x,y)) -> and(not(x),not(y))

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
	- 8 states (1,...,8)
	- 6 final states (1,2,5,6,7,8)
	- 41 transitions:
		4 -> 6
		7 -> 6
		8 -> 6
		not_0(7) -> 6
		not_0(1) -> 6
		not_0(8) -> 6
		or_0(3,4) -> 6
		or_0(6,7) -> 6
		or_0(8,8) -> 6
		or_0(3,8) -> 6
		or_0(6,4) -> 6
		or_0(7,6) -> 6
		or_0(6,8) -> 6
		or_0(7,7) -> 6
		or_0(7,4) -> 6
		or_0(8,6) -> 6
		or_0(3,6) -> 6
		or_0(7,8) -> 6
		or_0(6,6) -> 6
		or_0(8,7) -> 6
		or_0(3,7) -> 6
		or_0(8,4) -> 6
		#_0 -> 7
		#_0 -> 6
		#_0 -> 8
		and_0(4,6) -> 6
		and_0(6,7) -> 6
		and_0(8,8) -> 6
		and_0(6,4) -> 6
		and_0(7,6) -> 6
		and_0(4,7) -> 6
		and_0(6,8) -> 6
		and_0(4,4) -> 6
		and_0(7,7) -> 6
		and_0(4,8) -> 6
		and_0(7,4) -> 6
		and_0(8,6) -> 6
		and_0(7,8) -> 6
		and_0(6,6) -> 6
		and_0(8,7) -> 6
		and_0(8,4) -> 6
		


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