We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { active(__(X1, X2)) -> __(X1, active(X2)) , active(__(X1, X2)) -> __(active(X1), X2) , active(__(X, nil())) -> mark(X) , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(nil(), X)) -> mark(X) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isList(V)) -> mark(isNeList(V)) , active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2))) , active(isList(nil())) -> mark(tt()) , active(isNeList(V)) -> mark(isQid(V)) , active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2))) , active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2))) , active(isQid(a())) -> mark(tt()) , active(isQid(e())) -> mark(tt()) , active(isQid(i())) -> mark(tt()) , active(isQid(o())) -> mark(tt()) , active(isQid(u())) -> mark(tt()) , active(isNePal(V)) -> mark(isQid(V)) , active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P))) , active(isPal(V)) -> mark(isNePal(V)) , active(isPal(nil())) -> mark(tt()) , __(X1, mark(X2)) -> mark(__(X1, X2)) , __(mark(X1), X2) -> mark(__(X1, X2)) , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , isNeList(ok(X)) -> ok(isNeList(X)) , isQid(ok(X)) -> ok(isQid(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , isPal(ok(X)) -> ok(isPal(X)) , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(tt()) -> ok(tt()) , proper(isList(X)) -> isList(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(isPal(X)) -> isPal(proper(X)) , proper(a()) -> ok(a()) , proper(e()) -> ok(e()) , proper(i()) -> ok(i()) , proper(o()) -> ok(o()) , proper(u()) -> ok(u()) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: YES(?,O(n^1)) The problem is match-bounded by 2. The enriched problem is compatible with the following automaton. { active_0(3) -> 1 , active_0(4) -> 1 , active_0(6) -> 1 , active_0(12) -> 1 , active_0(13) -> 1 , active_0(14) -> 1 , active_0(15) -> 1 , active_0(16) -> 1 , active_0(18) -> 1 , active_1(3) -> 28 , active_1(4) -> 28 , active_1(6) -> 28 , active_1(12) -> 28 , active_1(13) -> 28 , active_1(14) -> 28 , active_1(15) -> 28 , active_1(16) -> 28 , active_1(18) -> 28 , active_2(27) -> 29 , ___0(3, 3) -> 2 , ___0(3, 4) -> 2 , ___0(3, 6) -> 2 , ___0(3, 12) -> 2 , ___0(3, 13) -> 2 , ___0(3, 14) -> 2 , ___0(3, 15) -> 2 , ___0(3, 16) -> 2 , ___0(3, 18) -> 2 , ___0(4, 3) -> 2 , ___0(4, 4) -> 2 , ___0(4, 6) -> 2 , ___0(4, 12) -> 2 , ___0(4, 13) -> 2 , ___0(4, 14) -> 2 , ___0(4, 15) -> 2 , ___0(4, 16) -> 2 , ___0(4, 18) -> 2 , ___0(6, 3) -> 2 , ___0(6, 4) -> 2 , ___0(6, 6) -> 2 , ___0(6, 12) -> 2 , ___0(6, 13) -> 2 , ___0(6, 14) -> 2 , ___0(6, 15) -> 2 , ___0(6, 16) -> 2 , ___0(6, 18) -> 2 , ___0(12, 3) -> 2 , ___0(12, 4) -> 2 , ___0(12, 6) -> 2 , ___0(12, 12) -> 2 , ___0(12, 13) -> 2 , ___0(12, 14) -> 2 , ___0(12, 15) -> 2 , ___0(12, 16) -> 2 , ___0(12, 18) -> 2 , ___0(13, 3) -> 2 , ___0(13, 4) -> 2 , ___0(13, 6) -> 2 , ___0(13, 12) -> 2 , ___0(13, 13) -> 2 , ___0(13, 14) -> 2 , ___0(13, 15) -> 2 , ___0(13, 16) -> 2 , ___0(13, 18) -> 2 , ___0(14, 3) -> 2 , ___0(14, 4) -> 2 , ___0(14, 6) -> 2 , ___0(14, 12) -> 2 , ___0(14, 13) -> 2 , ___0(14, 14) -> 2 , ___0(14, 15) -> 2 , ___0(14, 16) -> 2 , ___0(14, 18) -> 2 , ___0(15, 3) -> 2 , ___0(15, 4) -> 2 , ___0(15, 6) -> 2 , ___0(15, 12) -> 2 , ___0(15, 13) -> 2 , ___0(15, 14) -> 2 , ___0(15, 15) -> 2 , ___0(15, 16) -> 2 , ___0(15, 18) -> 2 , ___0(16, 3) -> 2 , ___0(16, 4) -> 2 , ___0(16, 6) -> 2 , ___0(16, 12) -> 2 , ___0(16, 13) -> 2 , ___0(16, 14) -> 2 , ___0(16, 15) -> 2 , ___0(16, 16) -> 2 , ___0(16, 18) -> 2 , ___0(18, 3) -> 2 , ___0(18, 4) -> 2 , ___0(18, 6) -> 2 , ___0(18, 12) -> 2 , ___0(18, 13) -> 2 , ___0(18, 14) -> 2 , ___0(18, 15) -> 2 , ___0(18, 16) -> 2 , ___0(18, 18) -> 2 , ___1(3, 3) -> 20 , ___1(3, 4) -> 20 , ___1(3, 6) -> 20 , ___1(3, 12) -> 20 , ___1(3, 13) -> 20 , ___1(3, 14) -> 20 , ___1(3, 15) -> 20 , ___1(3, 16) -> 20 , ___1(3, 18) -> 20 , ___1(4, 3) -> 20 , ___1(4, 4) -> 20 , ___1(4, 6) -> 20 , ___1(4, 12) -> 20 , ___1(4, 13) -> 20 , ___1(4, 14) -> 20 , ___1(4, 15) -> 20 , ___1(4, 16) -> 20 , ___1(4, 18) -> 20 , ___1(6, 3) -> 20 , ___1(6, 4) -> 20 , ___1(6, 6) -> 20 , ___1(6, 12) -> 20 , ___1(6, 13) -> 20 , ___1(6, 14) -> 20 , ___1(6, 15) -> 20 , ___1(6, 16) -> 20 , ___1(6, 18) -> 20 , ___1(12, 3) -> 20 , ___1(12, 4) -> 20 , ___1(12, 6) -> 20 , ___1(12, 12) -> 20 , ___1(12, 13) -> 20 , ___1(12, 14) -> 20 , ___1(12, 15) -> 20 , ___1(12, 16) -> 20 , ___1(12, 18) -> 20 , ___1(13, 3) -> 20 , ___1(13, 4) -> 20 , ___1(13, 6) -> 20 , ___1(13, 12) -> 20 , ___1(13, 13) -> 20 , ___1(13, 14) -> 20 , ___1(13, 15) -> 20 , ___1(13, 16) -> 20 , ___1(13, 18) -> 20 , ___1(14, 3) -> 20 , ___1(14, 4) -> 20 , ___1(14, 6) -> 20 , ___1(14, 12) -> 20 , ___1(14, 13) -> 20 , ___1(14, 14) -> 20 , ___1(14, 15) -> 20 , ___1(14, 16) -> 20 , ___1(14, 18) -> 20 , ___1(15, 3) -> 20 , ___1(15, 4) -> 20 , ___1(15, 6) -> 20 , ___1(15, 12) -> 20 , ___1(15, 13) -> 20 , ___1(15, 14) -> 20 , ___1(15, 15) -> 20 , ___1(15, 16) -> 20 , ___1(15, 18) -> 20 , ___1(16, 3) -> 20 , ___1(16, 4) -> 20 , ___1(16, 6) -> 20 , ___1(16, 12) -> 20 , ___1(16, 13) -> 20 , ___1(16, 14) -> 20 , ___1(16, 15) -> 20 , ___1(16, 16) -> 20 , ___1(16, 18) -> 20 , ___1(18, 3) -> 20 , ___1(18, 4) -> 20 , ___1(18, 6) -> 20 , ___1(18, 12) -> 20 , ___1(18, 13) -> 20 , ___1(18, 14) -> 20 , ___1(18, 15) -> 20 , ___1(18, 16) -> 20 , ___1(18, 18) -> 20 , mark_0(3) -> 3 , mark_0(4) -> 3 , mark_0(6) -> 3 , mark_0(12) -> 3 , mark_0(13) -> 3 , mark_0(14) -> 3 , mark_0(15) -> 3 , mark_0(16) -> 3 , mark_0(18) -> 3 , mark_1(20) -> 2 , mark_1(20) -> 20 , mark_1(21) -> 5 , mark_1(21) -> 21 , nil_0() -> 4 , nil_1() -> 27 , and_0(3, 3) -> 5 , and_0(3, 4) -> 5 , and_0(3, 6) -> 5 , and_0(3, 12) -> 5 , and_0(3, 13) -> 5 , and_0(3, 14) -> 5 , and_0(3, 15) -> 5 , and_0(3, 16) -> 5 , and_0(3, 18) -> 5 , and_0(4, 3) -> 5 , and_0(4, 4) -> 5 , and_0(4, 6) -> 5 , and_0(4, 12) -> 5 , and_0(4, 13) -> 5 , and_0(4, 14) -> 5 , and_0(4, 15) -> 5 , and_0(4, 16) -> 5 , and_0(4, 18) -> 5 , and_0(6, 3) -> 5 , and_0(6, 4) -> 5 , and_0(6, 6) -> 5 , and_0(6, 12) -> 5 , and_0(6, 13) -> 5 , and_0(6, 14) -> 5 , and_0(6, 15) -> 5 , and_0(6, 16) -> 5 , and_0(6, 18) -> 5 , and_0(12, 3) -> 5 , and_0(12, 4) -> 5 , and_0(12, 6) -> 5 , and_0(12, 12) -> 5 , and_0(12, 13) -> 5 , and_0(12, 14) -> 5 , and_0(12, 15) -> 5 , and_0(12, 16) -> 5 , and_0(12, 18) -> 5 , and_0(13, 3) -> 5 , and_0(13, 4) -> 5 , and_0(13, 6) -> 5 , and_0(13, 12) -> 5 , and_0(13, 13) -> 5 , and_0(13, 14) -> 5 , and_0(13, 15) -> 5 , and_0(13, 16) -> 5 , and_0(13, 18) -> 5 , and_0(14, 3) -> 5 , and_0(14, 4) -> 5 , and_0(14, 6) -> 5 , and_0(14, 12) -> 5 , and_0(14, 13) -> 5 , and_0(14, 14) -> 5 , and_0(14, 15) -> 5 , and_0(14, 16) -> 5 , and_0(14, 18) -> 5 , and_0(15, 3) -> 5 , and_0(15, 4) -> 5 , and_0(15, 6) -> 5 , and_0(15, 12) -> 5 , and_0(15, 13) -> 5 , and_0(15, 14) -> 5 , and_0(15, 15) -> 5 , and_0(15, 16) -> 5 , and_0(15, 18) -> 5 , and_0(16, 3) -> 5 , and_0(16, 4) -> 5 , and_0(16, 6) -> 5 , and_0(16, 12) -> 5 , and_0(16, 13) -> 5 , and_0(16, 14) -> 5 , and_0(16, 15) -> 5 , and_0(16, 16) -> 5 , and_0(16, 18) -> 5 , and_0(18, 3) -> 5 , and_0(18, 4) -> 5 , and_0(18, 6) -> 5 , and_0(18, 12) -> 5 , and_0(18, 13) -> 5 , and_0(18, 14) -> 5 , and_0(18, 15) -> 5 , and_0(18, 16) -> 5 , and_0(18, 18) -> 5 , and_1(3, 3) -> 21 , and_1(3, 4) -> 21 , and_1(3, 6) -> 21 , and_1(3, 12) -> 21 , and_1(3, 13) -> 21 , and_1(3, 14) -> 21 , and_1(3, 15) -> 21 , and_1(3, 16) -> 21 , and_1(3, 18) -> 21 , and_1(4, 3) -> 21 , and_1(4, 4) -> 21 , and_1(4, 6) -> 21 , and_1(4, 12) -> 21 , and_1(4, 13) -> 21 , and_1(4, 14) -> 21 , and_1(4, 15) -> 21 , and_1(4, 16) -> 21 , and_1(4, 18) -> 21 , and_1(6, 3) -> 21 , and_1(6, 4) -> 21 , and_1(6, 6) -> 21 , and_1(6, 12) -> 21 , and_1(6, 13) -> 21 , and_1(6, 14) -> 21 , and_1(6, 15) -> 21 , and_1(6, 16) -> 21 , and_1(6, 18) -> 21 , and_1(12, 3) -> 21 , and_1(12, 4) -> 21 , and_1(12, 6) -> 21 , and_1(12, 12) -> 21 , and_1(12, 13) -> 21 , and_1(12, 14) -> 21 , and_1(12, 15) -> 21 , and_1(12, 16) -> 21 , and_1(12, 18) -> 21 , and_1(13, 3) -> 21 , and_1(13, 4) -> 21 , and_1(13, 6) -> 21 , and_1(13, 12) -> 21 , and_1(13, 13) -> 21 , and_1(13, 14) -> 21 , and_1(13, 15) -> 21 , and_1(13, 16) -> 21 , and_1(13, 18) -> 21 , and_1(14, 3) -> 21 , and_1(14, 4) -> 21 , and_1(14, 6) -> 21 , and_1(14, 12) -> 21 , and_1(14, 13) -> 21 , and_1(14, 14) -> 21 , and_1(14, 15) -> 21 , and_1(14, 16) -> 21 , and_1(14, 18) -> 21 , and_1(15, 3) -> 21 , and_1(15, 4) -> 21 , and_1(15, 6) -> 21 , and_1(15, 12) -> 21 , and_1(15, 13) -> 21 , and_1(15, 14) -> 21 , and_1(15, 15) -> 21 , and_1(15, 16) -> 21 , and_1(15, 18) -> 21 , and_1(16, 3) -> 21 , and_1(16, 4) -> 21 , and_1(16, 6) -> 21 , and_1(16, 12) -> 21 , and_1(16, 13) -> 21 , and_1(16, 14) -> 21 , and_1(16, 15) -> 21 , and_1(16, 16) -> 21 , and_1(16, 18) -> 21 , and_1(18, 3) -> 21 , and_1(18, 4) -> 21 , and_1(18, 6) -> 21 , and_1(18, 12) -> 21 , and_1(18, 13) -> 21 , and_1(18, 14) -> 21 , and_1(18, 15) -> 21 , and_1(18, 16) -> 21 , and_1(18, 18) -> 21 , tt_0() -> 6 , tt_1() -> 27 , isList_0(3) -> 7 , isList_0(4) -> 7 , isList_0(6) -> 7 , isList_0(12) -> 7 , isList_0(13) -> 7 , isList_0(14) -> 7 , isList_0(15) -> 7 , isList_0(16) -> 7 , isList_0(18) -> 7 , isList_1(3) -> 22 , isList_1(4) -> 22 , isList_1(6) -> 22 , isList_1(12) -> 22 , isList_1(13) -> 22 , isList_1(14) -> 22 , isList_1(15) -> 22 , isList_1(16) -> 22 , isList_1(18) -> 22 , isNeList_0(3) -> 8 , isNeList_0(4) -> 8 , isNeList_0(6) -> 8 , isNeList_0(12) -> 8 , isNeList_0(13) -> 8 , isNeList_0(14) -> 8 , isNeList_0(15) -> 8 , isNeList_0(16) -> 8 , isNeList_0(18) -> 8 , isNeList_1(3) -> 23 , isNeList_1(4) -> 23 , isNeList_1(6) -> 23 , isNeList_1(12) -> 23 , isNeList_1(13) -> 23 , isNeList_1(14) -> 23 , isNeList_1(15) -> 23 , isNeList_1(16) -> 23 , isNeList_1(18) -> 23 , isQid_0(3) -> 9 , isQid_0(4) -> 9 , isQid_0(6) -> 9 , isQid_0(12) -> 9 , isQid_0(13) -> 9 , isQid_0(14) -> 9 , isQid_0(15) -> 9 , isQid_0(16) -> 9 , isQid_0(18) -> 9 , isQid_1(3) -> 24 , isQid_1(4) -> 24 , isQid_1(6) -> 24 , isQid_1(12) -> 24 , isQid_1(13) -> 24 , isQid_1(14) -> 24 , isQid_1(15) -> 24 , isQid_1(16) -> 24 , isQid_1(18) -> 24 , isNePal_0(3) -> 10 , isNePal_0(4) -> 10 , isNePal_0(6) -> 10 , isNePal_0(12) -> 10 , isNePal_0(13) -> 10 , isNePal_0(14) -> 10 , isNePal_0(15) -> 10 , isNePal_0(16) -> 10 , isNePal_0(18) -> 10 , isNePal_1(3) -> 25 , isNePal_1(4) -> 25 , isNePal_1(6) -> 25 , isNePal_1(12) -> 25 , isNePal_1(13) -> 25 , isNePal_1(14) -> 25 , isNePal_1(15) -> 25 , isNePal_1(16) -> 25 , isNePal_1(18) -> 25 , isPal_0(3) -> 11 , isPal_0(4) -> 11 , isPal_0(6) -> 11 , isPal_0(12) -> 11 , isPal_0(13) -> 11 , isPal_0(14) -> 11 , isPal_0(15) -> 11 , isPal_0(16) -> 11 , isPal_0(18) -> 11 , isPal_1(3) -> 26 , isPal_1(4) -> 26 , isPal_1(6) -> 26 , isPal_1(12) -> 26 , isPal_1(13) -> 26 , isPal_1(14) -> 26 , isPal_1(15) -> 26 , isPal_1(16) -> 26 , isPal_1(18) -> 26 , a_0() -> 12 , a_1() -> 27 , e_0() -> 13 , e_1() -> 27 , i_0() -> 14 , i_1() -> 27 , o_0() -> 15 , o_1() -> 27 , u_0() -> 16 , u_1() -> 27 , proper_0(3) -> 17 , proper_0(4) -> 17 , proper_0(6) -> 17 , proper_0(12) -> 17 , proper_0(13) -> 17 , proper_0(14) -> 17 , proper_0(15) -> 17 , proper_0(16) -> 17 , proper_0(18) -> 17 , proper_1(3) -> 28 , proper_1(4) -> 28 , proper_1(6) -> 28 , proper_1(12) -> 28 , proper_1(13) -> 28 , proper_1(14) -> 28 , proper_1(15) -> 28 , proper_1(16) -> 28 , proper_1(18) -> 28 , ok_0(3) -> 18 , ok_0(4) -> 18 , ok_0(6) -> 18 , ok_0(12) -> 18 , ok_0(13) -> 18 , ok_0(14) -> 18 , ok_0(15) -> 18 , ok_0(16) -> 18 , ok_0(18) -> 18 , ok_1(20) -> 2 , ok_1(20) -> 20 , ok_1(21) -> 5 , ok_1(21) -> 21 , ok_1(22) -> 7 , ok_1(22) -> 22 , ok_1(23) -> 8 , ok_1(23) -> 23 , ok_1(24) -> 9 , ok_1(24) -> 24 , ok_1(25) -> 10 , ok_1(25) -> 25 , ok_1(26) -> 11 , ok_1(26) -> 26 , ok_1(27) -> 17 , ok_1(27) -> 28 , top_0(3) -> 19 , top_0(4) -> 19 , top_0(6) -> 19 , top_0(12) -> 19 , top_0(13) -> 19 , top_0(14) -> 19 , top_0(15) -> 19 , top_0(16) -> 19 , top_0(18) -> 19 , top_1(28) -> 19 , top_2(29) -> 19 } Hurray, we answered YES(?,O(n^1))