YES(?,O(n^1)) TRS: {f c(X, s Y) -> f c(s X, Y), g c(s X, Y) -> f c(X, s Y)} DUP: We consider a non-duplicating system. Trs: {f c(X, s Y) -> f c(s X, Y), g c(s X, Y) -> f c(X, s Y)} BOUND: Bound: match(-raise)-bounded by 2 Automaton: { s_2(8) -> 8* s_2(4) -> 8* s_2(3) -> 8* s_2(2) -> 8* s_2(1) -> 8* s_1(10) -> 10* s_1(8) -> 10* s_1(5) -> 5* s_1(4) -> 5* s_1(3) -> 5* s_1(2) -> 5* s_1(1) -> 5* s_0(4) -> 4* s_0(3) -> 4* s_0(2) -> 4* s_0(1) -> 4* c_2(8, 5) -> 9* c_2(8, 4) -> 9* c_2(8, 3) -> 9* c_2(8, 2) -> 9* c_2(8, 1) -> 9* c_1(10, 4) -> 6* c_1(10, 3) -> 6* c_1(10, 2) -> 6* c_1(10, 1) -> 6* c_1(5, 4) -> 7* c_1(5, 3) -> 7* c_1(5, 2) -> 7* c_1(5, 1) -> 7* c_1(4, 5) -> 6* c_1(3, 5) -> 6* c_1(2, 5) -> 6* c_1(1, 5) -> 6* c_0(4, 4) -> 3* c_0(4, 3) -> 3* c_0(4, 2) -> 3* c_0(4, 1) -> 3* c_0(3, 4) -> 3* c_0(3, 3) -> 3* c_0(3, 2) -> 3* c_0(3, 1) -> 3* c_0(2, 4) -> 3* c_0(2, 3) -> 3* c_0(2, 2) -> 3* c_0(2, 1) -> 3* c_0(1, 4) -> 3* c_0(1, 3) -> 3* c_0(1, 2) -> 3* c_0(1, 1) -> 3* g_0(4) -> 2* g_0(3) -> 2* g_0(2) -> 2* g_0(1) -> 2* f_2(9) -> 2* f_1(7) -> 1* f_1(6) -> 2* f_0(4) -> 1* f_0(3) -> 1* f_0(2) -> 1* f_0(1) -> 1* } Strict: {} Qed