YES Consider the TRS R consisting of the following rewrite rules: f(s(X),X) -> f(X,a(X)) f(X,c(X)) -> f(s(X),X) f(X,X) -> c(X) The TRS R is terminating because R is match-raise-bounded for the set of all ground terms by 3. A raise-consistent and quasi-deterministic tree automaton compatible with match(R) and the set of all ground terms has - 15 states (1,...,15) - 10 final states (1,4,5,8,9,10,11,13,14,15) - 489 transitions: s_2(10) -> 10 s_2(10) -> 5 s_2(10) -> 1 s_2(10) -> 3 s_2(10) -> 7 s_2(5) -> 7 s_2(5) -> 3 s_2(5) -> 1 s_2(5) -> 5 s_2(5) -> 10 s_1(10) -> 5 s_1(10) -> 3 s_1(10) -> 1 s_1(4) -> 5 s_1(4) -> 1 s_1(4) -> 3 s_1(13) -> 5 s_1(13) -> 3 s_1(13) -> 1 s_1(8) -> 5 s_1(8) -> 3 s_1(8) -> 1 s_1(11) -> 5 s_1(11) -> 3 s_1(11) -> 1 s_1(5) -> 5 s_1(5) -> 1 s_1(5) -> 3 s_1(14) -> 5 s_1(14) -> 3 s_1(14) -> 1 s_1(15) -> 5 s_1(15) -> 3 s_1(15) -> 1 s_1(9) -> 5 s_1(9) -> 3 s_1(9) -> 1 s_1(1) -> 3 s_1(1) -> 1 s_1(1) -> 5 s_0(5) -> 1 s_0(15) -> 1 s_0(9) -> 1 s_0(13) -> 1 s_0(1) -> 1 s_0(10) -> 1 s_0(4) -> 1 s_0(14) -> 1 s_0(8) -> 1 s_0(11) -> 1 a_3(5) -> 9 a_3(5) -> 1 a_3(5) -> 2 a_3(5) -> 4 a_3(5) -> 14 a_3(10) -> 12 a_3(10) -> 4 a_3(10) -> 1 a_3(10) -> 2 a_3(10) -> 9 a_3(10) -> 13 a_3(10) -> 14 a_3(10) -> 15 a_2(9) -> 9 a_2(9) -> 2 a_2(9) -> 1 a_2(9) -> 4 a_2(9) -> 8 a_2(9) -> 6 a_2(9) -> 11 a_2(15) -> 11 a_2(15) -> 6 a_2(15) -> 8 a_2(15) -> 4 a_2(15) -> 1 a_2(15) -> 2 a_2(15) -> 9 a_2(1) -> 4 a_2(1) -> 1 a_2(1) -> 2 a_2(1) -> 9 a_2(10) -> 9 a_2(10) -> 2 a_2(10) -> 1 a_2(10) -> 4 a_2(4) -> 6 a_2(4) -> 2 a_2(4) -> 1 a_2(4) -> 4 a_2(4) -> 8 a_2(4) -> 9 a_2(4) -> 11 a_2(13) -> 11 a_2(13) -> 6 a_2(13) -> 8 a_2(13) -> 4 a_2(13) -> 1 a_2(13) -> 2 a_2(13) -> 9 a_2(8) -> 9 a_2(8) -> 2 a_2(8) -> 1 a_2(8) -> 4 a_2(8) -> 8 a_2(8) -> 6 a_2(8) -> 11 a_2(11) -> 11 a_2(11) -> 6 a_2(11) -> 8 a_2(11) -> 4 a_2(11) -> 1 a_2(11) -> 2 a_2(11) -> 9 a_2(5) -> 4 a_2(5) -> 2 a_2(5) -> 1 a_2(5) -> 9 a_2(14) -> 11 a_2(14) -> 6 a_2(14) -> 8 a_2(14) -> 4 a_2(14) -> 1 a_2(14) -> 2 a_2(14) -> 9 a_1(10) -> 4 a_1(10) -> 2 a_1(10) -> 1 a_1(4) -> 4 a_1(4) -> 1 a_1(4) -> 2 a_1(13) -> 4 a_1(13) -> 2 a_1(13) -> 1 a_1(8) -> 4 a_1(8) -> 2 a_1(8) -> 1 a_1(11) -> 4 a_1(11) -> 2 a_1(11) -> 1 a_1(5) -> 4 a_1(5) -> 1 a_1(5) -> 2 a_1(14) -> 4 a_1(14) -> 2 a_1(14) -> 1 a_1(15) -> 4 a_1(15) -> 2 a_1(15) -> 1 a_1(9) -> 4 a_1(9) -> 2 a_1(9) -> 1 a_1(1) -> 2 a_1(1) -> 1 a_1(1) -> 4 a_0(5) -> 1 a_0(15) -> 1 a_0(9) -> 1 a_0(13) -> 1 a_0(1) -> 1 a_0(10) -> 1 a_0(4) -> 1 a_0(14) -> 1 a_0(8) -> 1 a_0(11) -> 1 c_3(13) -> 1 c_3(11) -> 1 c_3(14) -> 1 c_3(8) -> 1 c_3(15) -> 1 c_3(9) -> 1 c_3(10) -> 1 c_3(4) -> 1 c_2(9) -> 1 c_2(15) -> 1 c_2(10) -> 1 c_2(4) -> 1 c_2(13) -> 1 c_2(8) -> 1 c_2(11) -> 1 c_2(5) -> 1 c_2(14) -> 1 c_1(10) -> 1 c_1(4) -> 1 c_1(13) -> 1 c_1(8) -> 1 c_1(11) -> 1 c_1(5) -> 1 c_1(14) -> 1 c_1(15) -> 1 c_1(9) -> 1 c_1(1) -> 1 c_0(5) -> 1 c_0(15) -> 1 c_0(9) -> 1 c_0(13) -> 1 c_0(1) -> 1 c_0(10) -> 1 c_0(4) -> 1 c_0(14) -> 1 c_0(8) -> 1 c_0(11) -> 1 f_3(10,14) -> 1 f_3(5,14) -> 1 f_3(10,11) -> 1 f_3(5,11) -> 1 f_3(10,15) -> 1 f_3(5,15) -> 1 f_3(10,12) -> 1 f_3(10,9) -> 1 f_3(5,9) -> 1 f_3(10,13) -> 1 f_3(5,13) -> 1 f_2(1,9) -> 1 f_2(4,15) -> 1 f_2(8,6) -> 1 f_2(11,13) -> 1 f_2(15,4) -> 1 f_2(13,14) -> 1 f_2(14,9) -> 1 f_2(15,15) -> 1 f_2(8,14) -> 1 f_2(9,9) -> 1 f_2(10,4) -> 1 f_2(14,6) -> 1 f_2(15,11) -> 1 f_2(1,13) -> 1 f_2(4,9) -> 1 f_2(5,4) -> 1 f_2(7,5) -> 1 f_2(10,11) -> 1 f_2(15,8) -> 1 f_2(14,13) -> 1 f_2(5,11) -> 1 f_2(9,13) -> 1 f_2(10,8) -> 1 f_2(13,4) -> 1 f_2(11,14) -> 1 f_2(13,15) -> 1 f_2(4,13) -> 1 f_2(5,8) -> 1 f_2(8,4) -> 1 f_2(10,5) -> 1 f_2(10,15) -> 1 f_2(13,11) -> 1 f_2(5,15) -> 1 f_2(8,11) -> 1 f_2(9,6) -> 1 f_2(13,8) -> 1 f_2(15,9) -> 1 f_2(14,14) -> 1 f_2(4,6) -> 1 f_2(8,8) -> 1 f_2(9,14) -> 1 f_2(11,4) -> 1 f_2(10,9) -> 1 f_2(15,6) -> 1 f_2(4,14) -> 1 f_2(5,9) -> 1 f_2(7,10) -> 1 f_2(8,15) -> 1 f_2(11,11) -> 1 f_2(1,4) -> 1 f_2(15,13) -> 1 f_2(1,14) -> 1 f_2(10,13) -> 1 f_2(11,8) -> 1 f_2(14,4) -> 1 f_2(13,9) -> 1 f_2(14,15) -> 1 f_2(1,11) -> 1 f_2(5,13) -> 1 f_2(8,9) -> 1 f_2(9,4) -> 1 f_2(10,10) -> 1 f_2(13,6) -> 1 f_2(11,15) -> 1 f_2(14,11) -> 1 f_2(1,8) -> 1 f_2(4,4) -> 1 f_2(9,11) -> 1 f_2(14,8) -> 1 f_2(13,13) -> 1 f_2(15,14) -> 1 f_2(1,15) -> 1 f_2(4,11) -> 1 f_2(8,13) -> 1 f_2(9,8) -> 1 f_2(10,14) -> 1 f_2(11,9) -> 1 f_2(4,8) -> 1 f_2(5,14) -> 1 f_2(11,6) -> 1 f_2(9,15) -> 1 f_1(10,1) -> 1 f_1(10,11) -> 1 f_1(14,2) -> 1 f_1(15,8) -> 1 f_1(14,13) -> 1 f_1(5,1) -> 1 f_1(3,10) -> 1 f_1(5,11) -> 1 f_1(9,2) -> 1 f_1(9,13) -> 1 f_1(10,8) -> 1 f_1(11,14) -> 1 f_1(13,4) -> 1 f_1(13,15) -> 1 f_1(4,2) -> 1 f_1(4,13) -> 1 f_1(5,8) -> 1 f_1(8,4) -> 1 f_1(10,5) -> 1 f_1(15,2) -> 1 f_1(10,15) -> 1 f_1(13,11) -> 1 f_1(3,4) -> 1 f_1(5,5) -> 1 f_1(5,15) -> 1 f_1(8,11) -> 1 f_1(13,8) -> 1 f_1(15,9) -> 1 f_1(14,14) -> 1 f_1(3,11) -> 1 f_1(8,8) -> 1 f_1(9,14) -> 1 f_1(11,4) -> 1 f_1(10,9) -> 1 f_1(3,8) -> 1 f_1(4,14) -> 1 f_1(5,9) -> 1 f_1(8,15) -> 1 f_1(11,11) -> 1 f_1(1,4) -> 1 f_1(15,13) -> 1 f_1(3,5) -> 1 f_1(1,14) -> 1 f_1(3,15) -> 1 f_1(10,2) -> 1 f_1(10,13) -> 1 f_1(11,8) -> 1 f_1(13,9) -> 1 f_1(14,4) -> 1 f_1(14,15) -> 1 f_1(1,11) -> 1 f_1(3,1) -> 1 f_1(5,2) -> 1 f_1(5,13) -> 1 f_1(8,9) -> 1 f_1(9,4) -> 1 f_1(10,10) -> 1 f_1(11,15) -> 1 f_1(14,11) -> 1 f_1(1,8) -> 1 f_1(3,9) -> 1 f_1(4,4) -> 1 f_1(9,11) -> 1 f_1(13,2) -> 1 f_1(14,8) -> 1 f_1(13,13) -> 1 f_1(15,14) -> 1 f_1(1,15) -> 1 f_1(4,11) -> 1 f_1(8,2) -> 1 f_1(8,13) -> 1 f_1(9,8) -> 1 f_1(10,14) -> 1 f_1(11,9) -> 1 f_1(3,13) -> 1 f_1(4,8) -> 1 f_1(5,14) -> 1 f_1(9,15) -> 1 f_1(1,9) -> 1 f_1(4,15) -> 1 f_1(5,10) -> 1 f_1(11,2) -> 1 f_1(11,13) -> 1 f_1(15,4) -> 1 f_1(13,14) -> 1 f_1(14,9) -> 1 f_1(15,15) -> 1 f_1(8,14) -> 1 f_1(9,9) -> 1 f_1(10,4) -> 1 f_1(1,2) -> 1 f_1(15,11) -> 1 f_1(1,13) -> 1 f_1(3,14) -> 1 f_1(4,9) -> 1 f_1(5,4) -> 1 f_0(10,15) -> 1 f_0(13,11) -> 1 f_0(5,5) -> 1 f_0(8,1) -> 1 f_0(5,15) -> 1 f_0(8,11) -> 1 f_0(13,8) -> 1 f_0(15,9) -> 1 f_0(14,14) -> 1 f_0(1,10) -> 1 f_0(8,8) -> 1 f_0(9,14) -> 1 f_0(11,4) -> 1 f_0(10,9) -> 1 f_0(13,5) -> 1 f_0(4,14) -> 1 f_0(5,9) -> 1 f_0(8,5) -> 1 f_0(11,1) -> 1 f_0(8,15) -> 1 f_0(11,11) -> 1 f_0(1,4) -> 1 f_0(15,13) -> 1 f_0(1,14) -> 1 f_0(4,10) -> 1 f_0(10,13) -> 1 f_0(11,8) -> 1 f_0(13,9) -> 1 f_0(14,4) -> 1 f_0(15,10) -> 1 f_0(14,15) -> 1 f_0(1,11) -> 1 f_0(5,13) -> 1 f_0(8,9) -> 1 f_0(9,4) -> 1 f_0(11,5) -> 1 f_0(10,10) -> 1 f_0(14,1) -> 1 f_0(11,15) -> 1 f_0(14,11) -> 1 f_0(1,8) -> 1 f_0(4,4) -> 1 f_0(9,1) -> 1 f_0(9,11) -> 1 f_0(14,8) -> 1 f_0(13,13) -> 1 f_0(1,5) -> 1 f_0(15,14) -> 1 f_0(1,15) -> 1 f_0(4,11) -> 1 f_0(8,13) -> 1 f_0(9,8) -> 1 f_0(10,14) -> 1 f_0(11,9) -> 1 f_0(14,5) -> 1 f_0(13,10) -> 1 f_0(1,1) -> 1 f_0(4,8) -> 1 f_0(5,14) -> 1 f_0(8,10) -> 1 f_0(9,5) -> 1 f_0(9,15) -> 1 f_0(1,9) -> 1 f_0(4,5) -> 1 f_0(4,15) -> 1 f_0(5,10) -> 1 f_0(11,13) -> 1 f_0(15,4) -> 1 f_0(13,14) -> 1 f_0(14,9) -> 1 f_0(15,15) -> 1 f_0(4,1) -> 1 f_0(8,14) -> 1 f_0(9,9) -> 1 f_0(10,4) -> 1 f_0(11,10) -> 1 f_0(15,1) -> 1 f_0(15,11) -> 1 f_0(1,13) -> 1 f_0(4,9) -> 1 f_0(5,4) -> 1 f_0(10,1) -> 1 f_0(10,11) -> 1 f_0(15,8) -> 1 f_0(14,13) -> 1 f_0(5,1) -> 1 f_0(5,11) -> 1 f_0(9,13) -> 1 f_0(10,8) -> 1 f_0(13,4) -> 1 f_0(11,14) -> 1 f_0(13,15) -> 1 f_0(15,5) -> 1 f_0(14,10) -> 1 f_0(4,13) -> 1 f_0(5,8) -> 1 f_0(8,4) -> 1 f_0(9,10) -> 1 f_0(10,5) -> 1 f_0(13,1) -> 1 ___________________________________________________________________ TTTbox (0.234 seconds) - April 13, 2007 Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/Rubio/koen.trs