MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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(incr) = {1}, Uargs(cons) = {2}, Uargs(adx) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [incr](x1) = [1] x1 + [7] [nil] = [7] [cons](x1, x2) = [1] x1 + [1] x2 + [3] [s](x1) = [1] x1 + [5] [adx](x1) = [1] x1 + [3] [nats] = [7] [zeros] = [7] [0] = [0] [head](x1) = [1] x1 + [3] [tail](x1) = [1] x1 + [7] The following symbols are considered usable {incr, adx, nats, zeros, head, tail} The order satisfies the following ordering constraints: [incr(nil())] = [14] > [7] = [nil()] [incr(cons(X, L))] = [1] X + [1] L + [10] ? [1] X + [1] L + [15] = [cons(s(X), incr(L))] [adx(nil())] = [10] > [7] = [nil()] [adx(cons(X, L))] = [1] X + [1] L + [6] ? [1] X + [1] L + [13] = [incr(cons(X, adx(L)))] [nats()] = [7] ? [10] = [adx(zeros())] [zeros()] = [7] ? [10] = [cons(0(), zeros())] [head(cons(X, L))] = [1] X + [1] L + [6] > [1] X + [0] = [X] [tail(cons(X, L))] = [1] X + [1] L + [10] > [1] L + [0] = [L] 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: { incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) } Weak Trs: { incr(nil()) -> nil() , adx(nil()) -> nil() , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(incr) = {1}, Uargs(cons) = {2}, Uargs(adx) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [incr](x1) = [1] x1 + [0] [nil] = [7] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [s](x1) = [1] x1 + [0] [adx](x1) = [1] x1 + [0] [nats] = [7] [zeros] = [4] [0] = [4] [head](x1) = [1] x1 + [7] [tail](x1) = [1] x1 + [7] The following symbols are considered usable {incr, adx, nats, zeros, head, tail} The order satisfies the following ordering constraints: [incr(nil())] = [7] >= [7] = [nil()] [incr(cons(X, L))] = [1] X + [1] L + [0] >= [1] X + [1] L + [0] = [cons(s(X), incr(L))] [adx(nil())] = [7] >= [7] = [nil()] [adx(cons(X, L))] = [1] X + [1] L + [0] >= [1] X + [1] L + [0] = [incr(cons(X, adx(L)))] [nats()] = [7] > [4] = [adx(zeros())] [zeros()] = [4] ? [8] = [cons(0(), zeros())] [head(cons(X, L))] = [1] X + [1] L + [7] > [1] X + [0] = [X] [tail(cons(X, L))] = [1] X + [1] L + [7] > [1] L + [0] = [L] 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: { incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(cons(X, L)) -> incr(cons(X, adx(L))) , zeros() -> cons(0(), zeros()) } Weak Trs: { incr(nil()) -> nil() , adx(nil()) -> nil() , nats() -> adx(zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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(incr) = {1}, Uargs(cons) = {2}, Uargs(adx) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [incr](x1) = [1 0] x1 + [0] [0 0] [0] [nil] = [0] [0] [cons](x1, x2) = [0 1] x1 + [1 0] x2 + [0] [1 0] [0 1] [1] [s](x1) = [0] [0] [adx](x1) = [1 1] x1 + [0] [0 0] [0] [nats] = [7] [7] [zeros] = [0] [0] [0] = [0] [0] [head](x1) = [0 1] x1 + [7] [1 0] [7] [tail](x1) = [1 0] x1 + [7] [0 1] [7] The following symbols are considered usable {incr, adx, nats, zeros, head, tail} The order satisfies the following ordering constraints: [incr(nil())] = [0] [0] >= [0] [0] = [nil()] [incr(cons(X, L))] = [0 1] X + [1 0] L + [0] [0 0] [0 0] [0] ? [1 0] L + [0] [0 0] [1] = [cons(s(X), incr(L))] [adx(nil())] = [0] [0] >= [0] [0] = [nil()] [adx(cons(X, L))] = [1 1] X + [1 1] L + [1] [0 0] [0 0] [0] > [0 1] X + [1 1] L + [0] [0 0] [0 0] [0] = [incr(cons(X, adx(L)))] [nats()] = [7] [7] > [0] [0] = [adx(zeros())] [zeros()] = [0] [0] ? [0] [1] = [cons(0(), zeros())] [head(cons(X, L))] = [1 0] X + [0 1] L + [8] [0 1] [1 0] [7] > [1 0] X + [0] [0 1] [0] = [X] [tail(cons(X, L))] = [0 1] X + [1 0] L + [7] [1 0] [0 1] [8] > [1 0] L + [0] [0 1] [0] = [L] 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: { incr(cons(X, L)) -> cons(s(X), incr(L)) , zeros() -> cons(0(), zeros()) } Weak Trs: { incr(nil()) -> nil() , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS) (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: { incr^#(nil()) -> c_1() , incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(nil()) -> c_3() , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) , head^#(cons(X, L)) -> c_7() , tail^#(cons(X, L)) -> c_8() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(nil()) -> c_1() , incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(nil()) -> c_3() , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) , head^#(cons(X, L)) -> c_7() , tail^#(cons(X, L)) -> c_8() } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3,7,8} by applications of Pre({1,3,7,8}) = {2,4,5}. Here rules are labeled as follows: DPs: { 1: incr^#(nil()) -> c_1() , 2: incr^#(cons(X, L)) -> c_2(incr^#(L)) , 3: adx^#(nil()) -> c_3() , 4: adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , 5: nats^#() -> c_5(adx^#(zeros()), zeros^#()) , 6: zeros^#() -> c_6(zeros^#()) , 7: head^#(cons(X, L)) -> c_7() , 8: tail^#(cons(X, L)) -> c_8() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak DPs: { incr^#(nil()) -> c_1() , adx^#(nil()) -> c_3() , head^#(cons(X, L)) -> c_7() , tail^#(cons(X, L)) -> c_8() } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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. { incr^#(nil()) -> c_1() , adx^#(nil()) -> c_3() , head^#(cons(X, L)) -> c_7() , tail^#(cons(X, L)) -> c_8() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) , nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } StartTerms: basic terms Defined Symbols: incr^# adx^# nats^# zeros^# head^# tail^# Constructors: nil cons s 0 Strategy: innermost Problem (S): ------------ Strict DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) } Weak DPs: { nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } StartTerms: basic terms Defined Symbols: incr^# adx^# nats^# zeros^# head^# tail^# Constructors: nil cons s 0 Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } StartTerms: basic terms Defined Symbols: incr^# adx^# nats^# zeros^# head^# tail^# Constructors: nil cons s 0 Strategy: innermost This problem remains open. S) Strict DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) } Weak DPs: { nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } StartTerms: basic terms Defined Symbols: incr^# adx^# nats^# zeros^# head^# tail^# Constructors: nil cons s 0 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_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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. { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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_5(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: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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. [incr](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [nil]() = 0 [cons](x1, x2) = x1 + x2 [s](x1) = x1 [adx](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [nats]() = 0 [zeros]() = 0 [0]() = 0 [head](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [tail](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [incr^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [c_1]() = 0 [c_2](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [adx^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [c_3]() = 0 [c_4](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 [nats^#]() = 3 [c_5](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 [zeros^#]() = 1 [c_6](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [head^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [c_7]() = 0 [tail^#](x1) = 3*x1 + 3*x1^2 + 3*x1^3 [c_8]() = 0 [c]() = 0 [c_1](x1) = x1 [c_2](x1) = x1 The following symbols are considered usable {incr^#, adx^#, nats^#, zeros^#, head^#, tail^#} This order satisfies the following ordering constraints. [nats^#()] = 3 > 1 = [c_1(zeros^#())] [zeros^#()] = 1 >= 1 = [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: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) } Weak DPs: { nats^#() -> c_5(adx^#(zeros()), zeros^#()) , zeros^#() -> c_6(zeros^#()) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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_6(zeros^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_2(incr^#(L)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, adx(L))), adx^#(L)) } Weak DPs: { nats^#() -> c_5(adx^#(zeros()), zeros^#()) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } 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_5(adx^#(zeros()), zeros^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_1(incr^#(L)) , adx^#(cons(X, L)) -> c_2(incr^#(cons(X, adx(L))), adx^#(L)) } Weak DPs: { nats^#() -> c_3(adx^#(zeros())) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , nats() -> adx(zeros()) , zeros() -> cons(0(), zeros()) , head(cons(X, L)) -> X , tail(cons(X, L)) -> L } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , zeros() -> cons(0(), zeros()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_1(incr^#(L)) , adx^#(cons(X, L)) -> c_2(incr^#(cons(X, adx(L))), adx^#(L)) } Weak DPs: { nats^#() -> c_3(adx^#(zeros())) } Weak Trs: { incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), incr(L)) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, adx(L))) , zeros() -> cons(0(), zeros()) } Obligation: innermost runtime complexity Answer: MAYBE All rules are usable. No progress on transformation, no sub-problems were generated. Arrrr..