We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { active(nats()) -> mark(cons(0(), incr(nats()))) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(incr(X)) -> incr(active(X)) , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))) , active(pairs()) -> mark(cons(0(), incr(odds()))) , active(odds()) -> mark(incr(pairs())) , active(s(X)) -> s(active(X)) , active(head(X)) -> head(active(X)) , active(head(cons(X, XS))) -> mark(X) , active(tail(X)) -> tail(active(X)) , active(tail(cons(X, XS))) -> mark(XS) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , incr(mark(X)) -> mark(incr(X)) , incr(ok(X)) -> ok(incr(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , proper(nats()) -> ok(nats()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(incr(X)) -> incr(proper(X)) , proper(pairs()) -> ok(pairs()) , proper(odds()) -> ok(odds()) , proper(s(X)) -> s(proper(X)) , proper(head(X)) -> head(proper(X)) , proper(tail(X)) -> tail(proper(X)) , 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 9. The enriched problem is compatible with the following automaton. { active_0(2) -> 1 , active_0(3) -> 1 , active_0(5) -> 1 , active_0(7) -> 1 , active_0(8) -> 1 , active_0(13) -> 1 , active_1(2) -> 25 , active_1(3) -> 25 , active_1(5) -> 25 , active_1(7) -> 25 , active_1(8) -> 25 , active_1(13) -> 25 , active_2(16) -> 26 , active_2(18) -> 26 , active_2(19) -> 26 , active_3(38) -> 36 , active_4(28) -> 53 , active_4(31) -> 46 , active_4(50) -> 52 , active_5(41) -> 61 , active_5(44) -> 54 , active_5(74) -> 60 , active_6(56) -> 81 , active_6(72) -> 65 , active_6(79) -> 80 , active_7(69) -> 91 , active_7(78) -> 82 , active_7(103) -> 90 , active_8(97) -> 105 , active_8(98) -> 109 , active_8(106) -> 107 , active_9(102) -> 108 , nats_0() -> 2 , nats_1() -> 18 , nats_2() -> 30 , nats_3() -> 45 , nats_4() -> 58 , nats_5() -> 71 , nats_6() -> 100 , mark_0(2) -> 3 , mark_0(3) -> 3 , mark_0(5) -> 3 , mark_0(7) -> 3 , mark_0(8) -> 3 , mark_0(13) -> 3 , mark_1(15) -> 1 , mark_1(15) -> 25 , mark_1(20) -> 4 , mark_1(20) -> 20 , mark_1(21) -> 6 , mark_1(21) -> 21 , mark_1(22) -> 9 , mark_1(22) -> 22 , mark_1(23) -> 10 , mark_1(23) -> 23 , mark_1(24) -> 11 , mark_1(24) -> 24 , mark_2(27) -> 26 , mark_3(47) -> 46 , mark_4(49) -> 36 , mark_4(55) -> 54 , mark_5(59) -> 52 , mark_6(75) -> 60 , mark_7(83) -> 80 , cons_0(2, 2) -> 4 , cons_0(2, 3) -> 4 , cons_0(2, 5) -> 4 , cons_0(2, 7) -> 4 , cons_0(2, 8) -> 4 , cons_0(2, 13) -> 4 , cons_0(3, 2) -> 4 , cons_0(3, 3) -> 4 , cons_0(3, 5) -> 4 , cons_0(3, 7) -> 4 , cons_0(3, 8) -> 4 , cons_0(3, 13) -> 4 , cons_0(5, 2) -> 4 , cons_0(5, 3) -> 4 , cons_0(5, 5) -> 4 , cons_0(5, 7) -> 4 , cons_0(5, 8) -> 4 , cons_0(5, 13) -> 4 , cons_0(7, 2) -> 4 , cons_0(7, 3) -> 4 , cons_0(7, 5) -> 4 , cons_0(7, 7) -> 4 , cons_0(7, 8) -> 4 , cons_0(7, 13) -> 4 , cons_0(8, 2) -> 4 , cons_0(8, 3) -> 4 , cons_0(8, 5) -> 4 , cons_0(8, 7) -> 4 , cons_0(8, 8) -> 4 , cons_0(8, 13) -> 4 , cons_0(13, 2) -> 4 , cons_0(13, 3) -> 4 , cons_0(13, 5) -> 4 , cons_0(13, 7) -> 4 , cons_0(13, 8) -> 4 , cons_0(13, 13) -> 4 , cons_1(2, 2) -> 20 , cons_1(2, 3) -> 20 , cons_1(2, 5) -> 20 , cons_1(2, 7) -> 20 , cons_1(2, 8) -> 20 , cons_1(2, 13) -> 20 , cons_1(3, 2) -> 20 , cons_1(3, 3) -> 20 , cons_1(3, 5) -> 20 , cons_1(3, 7) -> 20 , cons_1(3, 8) -> 20 , cons_1(3, 13) -> 20 , cons_1(5, 2) -> 20 , cons_1(5, 3) -> 20 , cons_1(5, 5) -> 20 , cons_1(5, 7) -> 20 , cons_1(5, 8) -> 20 , cons_1(5, 13) -> 20 , cons_1(7, 2) -> 20 , cons_1(7, 3) -> 20 , cons_1(7, 5) -> 20 , cons_1(7, 7) -> 20 , cons_1(7, 8) -> 20 , cons_1(7, 13) -> 20 , cons_1(8, 2) -> 20 , cons_1(8, 3) -> 20 , cons_1(8, 5) -> 20 , cons_1(8, 7) -> 20 , cons_1(8, 8) -> 20 , cons_1(8, 13) -> 20 , cons_1(13, 2) -> 20 , cons_1(13, 3) -> 20 , cons_1(13, 5) -> 20 , cons_1(13, 7) -> 20 , cons_1(13, 8) -> 20 , cons_1(13, 13) -> 20 , cons_1(16, 17) -> 15 , cons_2(28, 29) -> 27 , cons_2(32, 33) -> 26 , cons_3(28, 37) -> 38 , cons_3(39, 40) -> 36 , cons_3(41, 48) -> 47 , cons_4(41, 51) -> 50 , cons_4(53, 37) -> 36 , cons_4(56, 57) -> 55 , cons_4(62, 63) -> 54 , cons_5(56, 66) -> 72 , cons_5(61, 51) -> 52 , cons_5(67, 68) -> 65 , cons_6(69, 73) -> 78 , cons_6(76, 77) -> 75 , cons_6(81, 66) -> 65 , cons_7(84, 85) -> 83 , cons_7(86, 87) -> 80 , cons_7(91, 73) -> 82 , cons_7(97, 85) -> 103 , cons_8(92, 93) -> 90 , cons_8(102, 104) -> 106 , cons_8(105, 85) -> 90 , cons_9(108, 104) -> 107 , 0_0() -> 5 , 0_1() -> 16 , 0_2() -> 28 , 0_3() -> 41 , 0_4() -> 56 , 0_5() -> 69 , 0_6() -> 98 , incr_0(2) -> 6 , incr_0(3) -> 6 , incr_0(5) -> 6 , incr_0(7) -> 6 , incr_0(8) -> 6 , incr_0(13) -> 6 , incr_1(2) -> 21 , incr_1(3) -> 21 , incr_1(5) -> 21 , incr_1(7) -> 21 , incr_1(8) -> 21 , incr_1(13) -> 21 , incr_1(18) -> 17 , incr_1(19) -> 15 , incr_2(30) -> 29 , incr_2(31) -> 27 , incr_2(34) -> 33 , incr_2(35) -> 26 , incr_3(30) -> 37 , incr_3(31) -> 38 , incr_3(42) -> 40 , incr_3(43) -> 36 , incr_3(45) -> 48 , incr_4(44) -> 50 , incr_4(45) -> 51 , incr_4(46) -> 36 , incr_4(47) -> 49 , incr_4(58) -> 57 , incr_4(64) -> 63 , incr_5(54) -> 52 , incr_5(55) -> 59 , incr_5(58) -> 66 , incr_5(70) -> 68 , incr_6(65) -> 60 , incr_6(66) -> 77 , incr_6(71) -> 73 , incr_6(72) -> 74 , incr_6(94) -> 88 , incr_7(73) -> 85 , incr_7(78) -> 79 , incr_7(82) -> 80 , incr_7(88) -> 87 , incr_7(99) -> 95 , incr_7(100) -> 101 , incr_8(95) -> 93 , incr_8(101) -> 104 , pairs_0() -> 7 , pairs_1() -> 19 , pairs_2() -> 31 , pairs_3() -> 44 , odds_0() -> 8 , odds_1() -> 18 , odds_2() -> 30 , odds_3() -> 45 , odds_4() -> 58 , odds_5() -> 71 , odds_6() -> 100 , s_0(2) -> 9 , s_0(3) -> 9 , s_0(5) -> 9 , s_0(7) -> 9 , s_0(8) -> 9 , s_0(13) -> 9 , s_1(2) -> 22 , s_1(3) -> 22 , s_1(5) -> 22 , s_1(7) -> 22 , s_1(8) -> 22 , s_1(13) -> 22 , s_6(56) -> 76 , s_6(69) -> 97 , s_7(69) -> 84 , s_7(89) -> 86 , s_7(91) -> 105 , s_7(98) -> 102 , s_8(96) -> 92 , s_8(109) -> 108 , head_0(2) -> 10 , head_0(3) -> 10 , head_0(5) -> 10 , head_0(7) -> 10 , head_0(8) -> 10 , head_0(13) -> 10 , head_1(2) -> 23 , head_1(3) -> 23 , head_1(5) -> 23 , head_1(7) -> 23 , head_1(8) -> 23 , head_1(13) -> 23 , tail_0(2) -> 11 , tail_0(3) -> 11 , tail_0(5) -> 11 , tail_0(7) -> 11 , tail_0(8) -> 11 , tail_0(13) -> 11 , tail_1(2) -> 24 , tail_1(3) -> 24 , tail_1(5) -> 24 , tail_1(7) -> 24 , tail_1(8) -> 24 , tail_1(13) -> 24 , proper_0(2) -> 12 , proper_0(3) -> 12 , proper_0(5) -> 12 , proper_0(7) -> 12 , proper_0(8) -> 12 , proper_0(13) -> 12 , proper_1(2) -> 25 , proper_1(3) -> 25 , proper_1(5) -> 25 , proper_1(7) -> 25 , proper_1(8) -> 25 , proper_1(13) -> 25 , proper_2(15) -> 26 , proper_2(16) -> 32 , proper_2(17) -> 33 , proper_2(18) -> 34 , proper_2(19) -> 35 , proper_3(27) -> 36 , proper_3(28) -> 39 , proper_3(29) -> 40 , proper_3(30) -> 42 , proper_3(31) -> 43 , proper_4(41) -> 62 , proper_4(45) -> 64 , proper_4(48) -> 63 , proper_4(49) -> 52 , proper_5(47) -> 54 , proper_5(56) -> 67 , proper_5(57) -> 68 , proper_5(58) -> 70 , proper_5(59) -> 60 , proper_6(55) -> 65 , proper_6(58) -> 94 , proper_6(75) -> 80 , proper_7(56) -> 89 , proper_7(66) -> 88 , proper_7(71) -> 99 , proper_7(76) -> 86 , proper_7(77) -> 87 , proper_7(83) -> 90 , proper_8(69) -> 96 , proper_8(73) -> 95 , proper_8(84) -> 92 , proper_8(85) -> 93 , ok_0(2) -> 13 , ok_0(3) -> 13 , ok_0(5) -> 13 , ok_0(7) -> 13 , ok_0(8) -> 13 , ok_0(13) -> 13 , ok_1(16) -> 12 , ok_1(16) -> 25 , ok_1(18) -> 12 , ok_1(18) -> 25 , ok_1(19) -> 12 , ok_1(19) -> 25 , ok_1(20) -> 4 , ok_1(20) -> 20 , ok_1(21) -> 6 , ok_1(21) -> 21 , ok_1(22) -> 9 , ok_1(22) -> 22 , ok_1(23) -> 10 , ok_1(23) -> 23 , ok_1(24) -> 11 , ok_1(24) -> 24 , ok_2(28) -> 32 , ok_2(30) -> 34 , ok_2(31) -> 35 , ok_3(37) -> 33 , ok_3(38) -> 26 , ok_3(41) -> 39 , ok_3(44) -> 43 , ok_3(45) -> 42 , ok_4(50) -> 36 , ok_4(51) -> 40 , ok_4(56) -> 62 , ok_4(58) -> 64 , ok_5(66) -> 63 , ok_5(69) -> 67 , ok_5(69) -> 89 , ok_5(71) -> 70 , ok_5(71) -> 94 , ok_5(72) -> 54 , ok_6(73) -> 68 , ok_6(73) -> 88 , ok_6(74) -> 52 , ok_6(78) -> 65 , ok_6(97) -> 86 , ok_6(98) -> 96 , ok_6(100) -> 99 , ok_7(79) -> 60 , ok_7(85) -> 87 , ok_7(101) -> 95 , ok_7(102) -> 92 , ok_7(103) -> 80 , ok_8(104) -> 93 , ok_8(106) -> 90 , top_0(2) -> 14 , top_0(3) -> 14 , top_0(5) -> 14 , top_0(7) -> 14 , top_0(8) -> 14 , top_0(13) -> 14 , top_1(25) -> 14 , top_2(26) -> 14 , top_3(36) -> 14 , top_4(52) -> 14 , top_5(60) -> 14 , top_6(80) -> 14 , top_7(90) -> 14 , top_8(107) -> 14 } Hurray, we answered YES(?,O(n^1))