MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(adx) = {1}, Uargs(cons) = {2}, Uargs(incr) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [nats] = [7] [adx](x1) = [1] x1 + [6] [zeros] = [5] [cons](x1, x2) = [1] x1 + [1] x2 + [1] [0] = [7] [incr](x1) = [1] x1 + [7] [s](x1) = [1] x1 + [7] [hd](x1) = [1] x1 + [3] [tl](x1) = [1] x1 + [5] The following symbols are considered usable {nats, adx, zeros, incr, hd, tl} The order satisfies the following ordering constraints: [nats()] = [7] ? [11] = [adx(zeros())] [adx(cons(X, Y))] = [1] X + [1] Y + [7] ? [1] X + [1] Y + [14] = [incr(cons(X, adx(Y)))] [zeros()] = [5] ? [13] = [cons(0(), zeros())] [incr(cons(X, Y))] = [1] X + [1] Y + [8] ? [1] X + [1] Y + [15] = [cons(s(X), incr(Y))] [hd(cons(X, Y))] = [1] X + [1] Y + [4] > [1] X + [0] = [X] [tl(cons(X, Y))] = [1] X + [1] Y + [6] > [1] Y + [0] = [Y] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) } Weak Trs: { hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(adx) = {1}, Uargs(cons) = {2}, Uargs(incr) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [nats] = [7] [adx](x1) = [1] x1 + [0] [zeros] = [4] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [4] [incr](x1) = [1] x1 + [0] [s](x1) = [1] x1 + [0] [hd](x1) = [1] x1 + [7] [tl](x1) = [1] x1 + [7] The following symbols are considered usable {nats, adx, zeros, incr, hd, tl} The order satisfies the following ordering constraints: [nats()] = [7] > [4] = [adx(zeros())] [adx(cons(X, Y))] = [1] X + [1] Y + [0] >= [1] X + [1] Y + [0] = [incr(cons(X, adx(Y)))] [zeros()] = [4] ? [8] = [cons(0(), zeros())] [incr(cons(X, Y))] = [1] X + [1] Y + [0] >= [1] X + [1] Y + [0] = [cons(s(X), incr(Y))] [hd(cons(X, Y))] = [1] X + [1] Y + [7] > [1] X + [0] = [X] [tl(cons(X, Y))] = [1] X + [1] Y + [7] > [1] Y + [0] = [Y] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) } Weak Trs: { nats() -> adx(zeros()) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(adx) = {1}, Uargs(cons) = {2}, Uargs(incr) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [nats] = [7] [7] [adx](x1) = [1 1] x1 + [0] [0 0] [0] [zeros] = [0] [0] [cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [4] [0] = [0] [0] [incr](x1) = [1 0] x1 + [0] [0 0] [0] [s](x1) = [0] [0] [hd](x1) = [1 0] x1 + [7] [0 1] [7] [tl](x1) = [1 0] x1 + [7] [0 1] [7] The following symbols are considered usable {nats, adx, zeros, incr, hd, tl} The order satisfies the following ordering constraints: [nats()] = [7] [7] > [0] [0] = [adx(zeros())] [adx(cons(X, Y))] = [1 1] X + [1 1] Y + [4] [0 0] [0 0] [0] > [1 0] X + [1 1] Y + [0] [0 0] [0 0] [0] = [incr(cons(X, adx(Y)))] [zeros()] = [0] [0] ? [0] [4] = [cons(0(), zeros())] [incr(cons(X, Y))] = [1 0] X + [1 0] Y + [0] [0 0] [0 0] [0] ? [1 0] Y + [0] [0 0] [4] = [cons(s(X), incr(Y))] [hd(cons(X, Y))] = [1 0] X + [1 0] Y + [7] [0 1] [0 1] [11] > [1 0] X + [0] [0 1] [0] = [X] [tl(cons(X, Y))] = [1 0] X + [1 0] Y + [7] [0 1] [0 1] [11] > [1 0] Y + [0] [0 1] [0] = [Y] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 5.0 seconds. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: We add the following dependency tuples: Strict DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , zeros^#() -> c_3(zeros^#()) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) , hd^#(cons(X, Y)) -> c_5() , tl^#(cons(X, Y)) -> c_6() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , zeros^#() -> c_3(zeros^#()) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) , hd^#(cons(X, Y)) -> c_5() , tl^#(cons(X, Y)) -> c_6() } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {5,6} by applications of Pre({5,6}) = {}. Here rules are labeled as follows: DPs: { 1: nats^#() -> c_1(adx^#(zeros()), zeros^#()) , 2: adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , 3: zeros^#() -> c_3(zeros^#()) , 4: incr^#(cons(X, Y)) -> c_4(incr^#(Y)) , 5: hd^#(cons(X, Y)) -> c_5() , 6: tl^#(cons(X, Y)) -> c_6() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , zeros^#() -> c_3(zeros^#()) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak DPs: { hd^#(cons(X, Y)) -> c_5() , tl^#(cons(X, Y)) -> c_6() } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { hd^#(cons(X, Y)) -> c_5() , tl^#(cons(X, Y)) -> c_6() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , zeros^#() -> c_3(zeros^#()) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component: Problem (R): ------------ Strict DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , zeros^#() -> c_3(zeros^#()) } Weak DPs: { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } StartTerms: basic terms Defined Symbols: nats^# adx^# zeros^# incr^# hd^# tl^# Constructors: cons 0 s Strategy: innermost Problem (S): ------------ Strict DPs: { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , zeros^#() -> c_3(zeros^#()) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } StartTerms: basic terms Defined Symbols: nats^# adx^# zeros^# incr^# hd^# tl^# Constructors: cons 0 s Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , zeros^#() -> c_3(zeros^#()) } Weak DPs: { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } StartTerms: basic terms Defined Symbols: nats^# adx^# zeros^# incr^# hd^# tl^# Constructors: cons 0 s Strategy: innermost This problem remains open. S) Strict DPs: { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , zeros^#() -> c_3(zeros^#()) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } StartTerms: basic terms Defined Symbols: nats^# adx^# zeros^# incr^# hd^# tl^# Constructors: cons 0 s Strategy: innermost This problem remains open. Proofs for generated problems: ------------------------------ R) We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , zeros^#() -> c_3(zeros^#()) } Weak DPs: { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , zeros^#() -> c_3(zeros^#()) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(zeros^#()) , zeros^#() -> c_2(zeros^#()) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_1(zeros^#()) , zeros^#() -> c_2(zeros^#()) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: We use the processor 'polynomial interpretation' to orient following rules strictly. DPs: { nats^#() -> c_1(zeros^#()) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^3)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are considered usable: Uargs(c_1) = {1}, Uargs(c_2) = {1} TcT has computed the following constructor-restricted polynomial interpretation. [nats]() = 0 [adx](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [zeros]() = 0 [cons](x1, x2) = x1 + x2 [0]() = 0 [incr](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [s](x1) = x1 [hd](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [tl](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [nats^#]() = 3 [c_1](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1*x2^2 + 3*x1^2 + 3*x1^2*x2 + 3*x1^3 + 3*x2 + 3*x2^2 + 3*x2^3 [adx^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [zeros^#]() = 0 [c_2](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1*x2^2 + 3*x1^2 + 3*x1^2*x2 + 3*x1^3 + 3*x2 + 3*x2^2 + 3*x2^3 [incr^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [c_3](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [c_4](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [hd^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [c_5]() = 0 [tl^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [c_6]() = 0 [c]() = 0 [c_1](x1) = 1 + 3*x1 + 3*x1^2 + 3*x1^3 [c_2](x1) = 3*x1 + 3*x1^2 + 3*x1^3 The following symbols are considered usable {nats^#, adx^#, zeros^#, incr^#, hd^#, tl^#} This order satisfies the following ordering constraints. [nats^#()] = 3 > 1 = [c_1(zeros^#())] [zeros^#()] = >= = [c_2(zeros^#())] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { zeros^#() -> c_2(zeros^#()) } Weak DPs: { nats^#() -> c_1(zeros^#()) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: Computation stopped due to timeout after 5.0 seconds. 3) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible S) We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) , zeros^#() -> c_3(zeros^#()) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { zeros^#() -> c_3(zeros^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { adx^#(cons(X, Y)) -> c_2(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_4(incr^#(Y)) } Weak DPs: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { nats^#() -> c_1(adx^#(zeros()), zeros^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { adx^#(cons(X, Y)) -> c_1(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_2(incr^#(Y)) } Weak DPs: { nats^#() -> c_3(adx^#(zeros())) } Weak Trs: { nats() -> adx(zeros()) , adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) , hd(cons(X, Y)) -> X , tl(cons(X, Y)) -> Y } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { adx^#(cons(X, Y)) -> c_1(incr^#(cons(X, adx(Y))), adx^#(Y)) , incr^#(cons(X, Y)) -> c_2(incr^#(Y)) } Weak DPs: { nats^#() -> c_3(adx^#(zeros())) } Weak Trs: { adx(cons(X, Y)) -> incr(cons(X, adx(Y))) , zeros() -> cons(0(), zeros()) , incr(cons(X, Y)) -> cons(s(X), incr(Y)) } Obligation: innermost runtime complexity Answer: MAYBE All rules are usable. No progress on transformation, no sub-problems were generated. Arrrr..