We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { active(incr(X)) -> incr(active(X)) , active(incr(nil())) -> mark(nil()) , active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(s(X)) -> s(active(X)) , active(adx(X)) -> adx(active(X)) , active(adx(nil())) -> mark(nil()) , active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))) , active(nats()) -> mark(adx(zeros())) , active(zeros()) -> mark(cons(0(), zeros())) , active(head(X)) -> head(active(X)) , active(head(cons(X, L))) -> mark(X) , active(tail(X)) -> tail(active(X)) , active(tail(cons(X, L))) -> mark(L) , incr(mark(X)) -> mark(incr(X)) , incr(ok(X)) -> ok(incr(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , adx(mark(X)) -> mark(adx(X)) , adx(ok(X)) -> ok(adx(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(incr(X)) -> incr(proper(X)) , proper(nil()) -> ok(nil()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(adx(X)) -> adx(proper(X)) , proper(nats()) -> ok(nats()) , proper(zeros()) -> ok(zeros()) , proper(0()) -> ok(0()) , 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: innermost runtime complexity Answer: YES(?,O(n^1)) The problem is match-bounded by 10. The enriched problem is compatible with the following automaton. { active_0(3) -> 1 , active_0(4) -> 1 , active_0(8) -> 1 , active_0(9) -> 1 , active_0(10) -> 1 , active_0(14) -> 1 , active_1(3) -> 26 , active_1(4) -> 26 , active_1(8) -> 26 , active_1(9) -> 26 , active_1(10) -> 26 , active_1(14) -> 26 , active_2(17) -> 27 , active_2(18) -> 27 , active_2(25) -> 27 , active_3(34) -> 33 , active_4(29) -> 40 , active_4(30) -> 39 , active_4(42) -> 44 , active_5(37) -> 46 , active_5(38) -> 45 , active_5(56) -> 51 , active_6(48) -> 67 , active_6(55) -> 54 , active_6(65) -> 66 , active_7(60) -> 77 , active_7(64) -> 68 , active_7(87) -> 76 , active_8(84) -> 98 , active_8(85) -> 79 , active_8(92) -> 93 , active_9(88) -> 94 , active_9(102) -> 115 , active_9(108) -> 120 , active_9(113) -> 101 , active_10(109) -> 119 , active_10(117) -> 118 , incr_0(3) -> 2 , incr_0(4) -> 2 , incr_0(8) -> 2 , incr_0(9) -> 2 , incr_0(10) -> 2 , incr_0(14) -> 2 , incr_1(3) -> 19 , incr_1(4) -> 19 , incr_1(8) -> 19 , incr_1(9) -> 19 , incr_1(10) -> 19 , incr_1(14) -> 19 , incr_6(62) -> 61 , incr_7(70) -> 69 , incr_7(72) -> 66 , incr_7(78) -> 91 , incr_7(85) -> 87 , incr_8(79) -> 76 , incr_8(86) -> 97 , incr_8(88) -> 92 , incr_8(103) -> 100 , incr_9(94) -> 93 , incr_9(110) -> 105 , incr_9(114) -> 116 , nil_0() -> 3 , nil_1() -> 25 , mark_0(3) -> 4 , mark_0(4) -> 4 , mark_0(8) -> 4 , mark_0(9) -> 4 , mark_0(10) -> 4 , mark_0(14) -> 4 , mark_1(16) -> 1 , mark_1(16) -> 26 , mark_1(19) -> 2 , mark_1(19) -> 19 , mark_1(20) -> 5 , mark_1(20) -> 20 , mark_1(21) -> 6 , mark_1(21) -> 21 , mark_1(22) -> 7 , mark_1(22) -> 22 , mark_1(23) -> 11 , mark_1(23) -> 23 , mark_1(24) -> 12 , mark_1(24) -> 24 , mark_2(28) -> 27 , mark_3(41) -> 40 , mark_4(43) -> 33 , mark_4(47) -> 46 , mark_5(50) -> 44 , mark_6(61) -> 51 , mark_7(69) -> 66 , mark_7(89) -> 76 , mark_8(95) -> 93 , cons_0(3, 3) -> 5 , cons_0(3, 4) -> 5 , cons_0(3, 8) -> 5 , cons_0(3, 9) -> 5 , cons_0(3, 10) -> 5 , cons_0(3, 14) -> 5 , cons_0(4, 3) -> 5 , cons_0(4, 4) -> 5 , cons_0(4, 8) -> 5 , cons_0(4, 9) -> 5 , cons_0(4, 10) -> 5 , cons_0(4, 14) -> 5 , cons_0(8, 3) -> 5 , cons_0(8, 4) -> 5 , cons_0(8, 8) -> 5 , cons_0(8, 9) -> 5 , cons_0(8, 10) -> 5 , cons_0(8, 14) -> 5 , cons_0(9, 3) -> 5 , cons_0(9, 4) -> 5 , cons_0(9, 8) -> 5 , cons_0(9, 9) -> 5 , cons_0(9, 10) -> 5 , cons_0(9, 14) -> 5 , cons_0(10, 3) -> 5 , cons_0(10, 4) -> 5 , cons_0(10, 8) -> 5 , cons_0(10, 9) -> 5 , cons_0(10, 10) -> 5 , cons_0(10, 14) -> 5 , cons_0(14, 3) -> 5 , cons_0(14, 4) -> 5 , cons_0(14, 8) -> 5 , cons_0(14, 9) -> 5 , cons_0(14, 10) -> 5 , cons_0(14, 14) -> 5 , cons_1(3, 3) -> 20 , cons_1(3, 4) -> 20 , cons_1(3, 8) -> 20 , cons_1(3, 9) -> 20 , cons_1(3, 10) -> 20 , cons_1(3, 14) -> 20 , cons_1(4, 3) -> 20 , cons_1(4, 4) -> 20 , cons_1(4, 8) -> 20 , cons_1(4, 9) -> 20 , cons_1(4, 10) -> 20 , cons_1(4, 14) -> 20 , cons_1(8, 3) -> 20 , cons_1(8, 4) -> 20 , cons_1(8, 8) -> 20 , cons_1(8, 9) -> 20 , cons_1(8, 10) -> 20 , cons_1(8, 14) -> 20 , cons_1(9, 3) -> 20 , cons_1(9, 4) -> 20 , cons_1(9, 8) -> 20 , cons_1(9, 9) -> 20 , cons_1(9, 10) -> 20 , cons_1(9, 14) -> 20 , cons_1(10, 3) -> 20 , cons_1(10, 4) -> 20 , cons_1(10, 8) -> 20 , cons_1(10, 9) -> 20 , cons_1(10, 10) -> 20 , cons_1(10, 14) -> 20 , cons_1(14, 3) -> 20 , cons_1(14, 4) -> 20 , cons_1(14, 8) -> 20 , cons_1(14, 9) -> 20 , cons_1(14, 10) -> 20 , cons_1(14, 14) -> 20 , cons_1(18, 17) -> 16 , cons_2(30, 29) -> 28 , cons_2(31, 32) -> 27 , cons_3(30, 29) -> 34 , cons_3(35, 36) -> 33 , cons_3(38, 37) -> 41 , cons_4(38, 37) -> 42 , cons_4(39, 29) -> 33 , cons_4(48, 49) -> 47 , cons_4(52, 53) -> 46 , cons_5(45, 37) -> 44 , cons_5(48, 49) -> 55 , cons_5(57, 58) -> 54 , cons_6(48, 63) -> 62 , cons_6(60, 59) -> 64 , cons_6(60, 78) -> 85 , cons_6(67, 49) -> 54 , cons_7(60, 71) -> 70 , cons_7(73, 74) -> 72 , cons_7(77, 59) -> 68 , cons_7(77, 78) -> 79 , cons_7(84, 86) -> 88 , cons_7(90, 91) -> 89 , cons_8(80, 81) -> 79 , cons_8(96, 97) -> 95 , cons_8(98, 86) -> 94 , cons_8(99, 100) -> 93 , cons_8(102, 97) -> 113 , cons_9(104, 105) -> 101 , cons_9(109, 116) -> 117 , cons_9(115, 97) -> 101 , cons_10(119, 116) -> 118 , s_0(3) -> 6 , s_0(4) -> 6 , s_0(8) -> 6 , s_0(9) -> 6 , s_0(10) -> 6 , s_0(14) -> 6 , s_1(3) -> 21 , s_1(4) -> 21 , s_1(8) -> 21 , s_1(9) -> 21 , s_1(10) -> 21 , s_1(14) -> 21 , s_7(60) -> 90 , s_7(84) -> 102 , s_8(80) -> 99 , s_8(84) -> 96 , s_8(98) -> 115 , s_8(108) -> 109 , s_9(106) -> 104 , s_9(120) -> 119 , adx_0(3) -> 7 , adx_0(4) -> 7 , adx_0(8) -> 7 , adx_0(9) -> 7 , adx_0(10) -> 7 , adx_0(14) -> 7 , adx_1(3) -> 22 , adx_1(4) -> 22 , adx_1(8) -> 22 , adx_1(9) -> 22 , adx_1(10) -> 22 , adx_1(14) -> 22 , adx_1(17) -> 16 , adx_2(29) -> 28 , adx_2(32) -> 27 , adx_3(29) -> 34 , adx_3(36) -> 33 , adx_4(37) -> 42 , adx_4(40) -> 33 , adx_4(41) -> 43 , adx_5(46) -> 44 , adx_5(47) -> 50 , adx_6(49) -> 63 , adx_6(54) -> 51 , adx_6(55) -> 56 , adx_6(59) -> 78 , adx_7(59) -> 71 , adx_7(64) -> 65 , adx_7(68) -> 66 , adx_7(75) -> 74 , adx_7(83) -> 86 , adx_7(107) -> 103 , adx_8(82) -> 81 , adx_8(111) -> 110 , adx_8(112) -> 114 , nats_0() -> 8 , nats_1() -> 25 , zeros_0() -> 9 , zeros_1() -> 17 , zeros_2() -> 29 , zeros_3() -> 37 , zeros_4() -> 49 , zeros_5() -> 59 , zeros_6() -> 83 , zeros_7() -> 112 , 0_0() -> 10 , 0_1() -> 18 , 0_2() -> 30 , 0_3() -> 38 , 0_4() -> 48 , 0_5() -> 60 , 0_6() -> 84 , 0_7() -> 108 , head_0(3) -> 11 , head_0(4) -> 11 , head_0(8) -> 11 , head_0(9) -> 11 , head_0(10) -> 11 , head_0(14) -> 11 , head_1(3) -> 23 , head_1(4) -> 23 , head_1(8) -> 23 , head_1(9) -> 23 , head_1(10) -> 23 , head_1(14) -> 23 , tail_0(3) -> 12 , tail_0(4) -> 12 , tail_0(8) -> 12 , tail_0(9) -> 12 , tail_0(10) -> 12 , tail_0(14) -> 12 , tail_1(3) -> 24 , tail_1(4) -> 24 , tail_1(8) -> 24 , tail_1(9) -> 24 , tail_1(10) -> 24 , tail_1(14) -> 24 , proper_0(3) -> 13 , proper_0(4) -> 13 , proper_0(8) -> 13 , proper_0(9) -> 13 , proper_0(10) -> 13 , proper_0(14) -> 13 , proper_1(3) -> 26 , proper_1(4) -> 26 , proper_1(8) -> 26 , proper_1(9) -> 26 , proper_1(10) -> 26 , proper_1(14) -> 26 , proper_2(16) -> 27 , proper_2(17) -> 32 , proper_2(18) -> 31 , proper_3(28) -> 33 , proper_3(29) -> 36 , proper_3(30) -> 35 , proper_4(37) -> 53 , proper_4(38) -> 52 , proper_4(43) -> 44 , proper_5(41) -> 46 , proper_5(48) -> 57 , proper_5(49) -> 58 , proper_5(50) -> 51 , proper_6(47) -> 54 , proper_6(61) -> 66 , proper_7(48) -> 73 , proper_7(49) -> 75 , proper_7(59) -> 107 , proper_7(62) -> 72 , proper_7(63) -> 74 , proper_7(69) -> 76 , proper_8(59) -> 82 , proper_8(60) -> 80 , proper_8(70) -> 79 , proper_8(71) -> 81 , proper_8(78) -> 103 , proper_8(83) -> 111 , proper_8(89) -> 93 , proper_8(90) -> 99 , proper_8(91) -> 100 , proper_9(84) -> 106 , proper_9(86) -> 110 , proper_9(95) -> 101 , proper_9(96) -> 104 , proper_9(97) -> 105 , ok_0(3) -> 14 , ok_0(4) -> 14 , ok_0(8) -> 14 , ok_0(9) -> 14 , ok_0(10) -> 14 , ok_0(14) -> 14 , ok_1(17) -> 13 , ok_1(17) -> 26 , ok_1(18) -> 13 , ok_1(18) -> 26 , ok_1(19) -> 2 , ok_1(19) -> 19 , ok_1(20) -> 5 , ok_1(20) -> 20 , ok_1(21) -> 6 , ok_1(21) -> 21 , ok_1(22) -> 7 , ok_1(22) -> 22 , ok_1(23) -> 11 , ok_1(23) -> 23 , ok_1(24) -> 12 , ok_1(24) -> 24 , ok_1(25) -> 13 , ok_1(25) -> 26 , ok_2(29) -> 32 , ok_2(30) -> 31 , ok_3(34) -> 27 , ok_3(37) -> 36 , ok_3(38) -> 35 , ok_4(42) -> 33 , ok_4(48) -> 52 , ok_4(49) -> 53 , ok_5(55) -> 46 , ok_5(59) -> 58 , ok_5(59) -> 75 , ok_5(60) -> 57 , ok_5(60) -> 73 , ok_6(56) -> 44 , ok_6(64) -> 54 , ok_6(78) -> 74 , ok_6(83) -> 82 , ok_6(83) -> 107 , ok_6(84) -> 80 , ok_6(85) -> 72 , ok_7(65) -> 51 , ok_7(86) -> 81 , ok_7(86) -> 103 , ok_7(87) -> 66 , ok_7(88) -> 79 , ok_7(102) -> 99 , ok_7(108) -> 106 , ok_7(112) -> 111 , ok_8(92) -> 76 , ok_8(97) -> 100 , ok_8(109) -> 104 , ok_8(113) -> 93 , ok_8(114) -> 110 , ok_9(116) -> 105 , ok_9(117) -> 101 , top_0(3) -> 15 , top_0(4) -> 15 , top_0(8) -> 15 , top_0(9) -> 15 , top_0(10) -> 15 , top_0(14) -> 15 , top_1(26) -> 15 , top_2(27) -> 15 , top_3(33) -> 15 , top_4(44) -> 15 , top_5(51) -> 15 , top_6(66) -> 15 , top_7(76) -> 15 , top_8(93) -> 15 , top_9(101) -> 15 , top_10(118) -> 15 } Hurray, we answered YES(?,O(n^1))