YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { app(l, nil()) -> l , app(nil(), k) -> k , app(cons(x, l), k) -> cons(x, app(l, k)) , sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))) , sum(cons(x, nil())) -> cons(x, nil()) , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add the following dependency tuples: Strict DPs: { app^#(l, nil()) -> c_1() , app^#(nil(), k) -> c_2() , app^#(cons(x, l), k) -> c_3(app^#(l, k)) , sum^#(app(l, cons(x, cons(y, k)))) -> c_4(sum^#(app(l, sum(cons(x, cons(y, k))))), app^#(l, sum(cons(x, cons(y, k)))), sum^#(cons(x, cons(y, k)))) , sum^#(cons(x, nil())) -> c_5() , sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , plus^#(0(), y) -> c_7() , plus^#(s(x), y) -> c_8(plus^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { app^#(l, nil()) -> c_1() , app^#(nil(), k) -> c_2() , app^#(cons(x, l), k) -> c_3(app^#(l, k)) , sum^#(app(l, cons(x, cons(y, k)))) -> c_4(sum^#(app(l, sum(cons(x, cons(y, k))))), app^#(l, sum(cons(x, cons(y, k)))), sum^#(cons(x, cons(y, k)))) , sum^#(cons(x, nil())) -> c_5() , sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , plus^#(0(), y) -> c_7() , plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak Trs: { app(l, nil()) -> l , app(nil(), k) -> k , app(cons(x, l), k) -> cons(x, app(l, k)) , sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))) , sum(cons(x, nil())) -> cons(x, nil()) , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Consider the dependency graph: 1: app^#(l, nil()) -> c_1() 2: app^#(nil(), k) -> c_2() 3: app^#(cons(x, l), k) -> c_3(app^#(l, k)) -->_1 app^#(cons(x, l), k) -> c_3(app^#(l, k)) :3 -->_1 app^#(nil(), k) -> c_2() :2 -->_1 app^#(l, nil()) -> c_1() :1 4: sum^#(app(l, cons(x, cons(y, k)))) -> c_4(sum^#(app(l, sum(cons(x, cons(y, k))))), app^#(l, sum(cons(x, cons(y, k)))), sum^#(cons(x, cons(y, k)))) -->_3 sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6 -->_1 sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6 -->_1 sum^#(cons(x, nil())) -> c_5() :5 -->_1 sum^#(app(l, cons(x, cons(y, k)))) -> c_4(sum^#(app(l, sum(cons(x, cons(y, k))))), app^#(l, sum(cons(x, cons(y, k)))), sum^#(cons(x, cons(y, k)))) :4 -->_2 app^#(l, nil()) -> c_1() :1 5: sum^#(cons(x, nil())) -> c_5() 6: sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) -->_2 plus^#(s(x), y) -> c_8(plus^#(x, y)) :8 -->_2 plus^#(0(), y) -> c_7() :7 -->_1 sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6 -->_1 sum^#(cons(x, nil())) -> c_5() :5 7: plus^#(0(), y) -> c_7() 8: plus^#(s(x), y) -> c_8(plus^#(x, y)) -->_1 plus^#(s(x), y) -> c_8(plus^#(x, y)) :8 -->_1 plus^#(0(), y) -> c_7() :7 Only the nodes {1,2,3,5,6,8,7} are reachable from nodes {1,2,3,5,6,7,8} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { app^#(l, nil()) -> c_1() , app^#(nil(), k) -> c_2() , app^#(cons(x, l), k) -> c_3(app^#(l, k)) , sum^#(cons(x, nil())) -> c_5() , sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , plus^#(0(), y) -> c_7() , plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak Trs: { app(l, nil()) -> l , app(nil(), k) -> k , app(cons(x, l), k) -> cons(x, app(l, k)) , sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))) , sum(cons(x, nil())) -> cons(x, nil()) , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,2,4,6} by applications of Pre({1,2,4,6}) = {3,5,7}. Here rules are labeled as follows: DPs: { 1: app^#(l, nil()) -> c_1() , 2: app^#(nil(), k) -> c_2() , 3: app^#(cons(x, l), k) -> c_3(app^#(l, k)) , 4: sum^#(cons(x, nil())) -> c_5() , 5: sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , 6: plus^#(0(), y) -> c_7() , 7: plus^#(s(x), y) -> c_8(plus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { app^#(cons(x, l), k) -> c_3(app^#(l, k)) , sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak DPs: { app^#(l, nil()) -> c_1() , app^#(nil(), k) -> c_2() , sum^#(cons(x, nil())) -> c_5() , plus^#(0(), y) -> c_7() } Weak Trs: { app(l, nil()) -> l , app(nil(), k) -> k , app(cons(x, l), k) -> cons(x, app(l, k)) , sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))) , sum(cons(x, nil())) -> cons(x, nil()) , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { app^#(l, nil()) -> c_1() , app^#(nil(), k) -> c_2() , sum^#(cons(x, nil())) -> c_5() , plus^#(0(), y) -> c_7() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { app^#(cons(x, l), k) -> c_3(app^#(l, k)) , sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak Trs: { app(l, nil()) -> l , app(nil(), k) -> k , app(cons(x, l), k) -> cons(x, app(l, k)) , sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k))))) , sum(cons(x, nil())) -> cons(x, nil()) , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { app^#(cons(x, l), k) -> c_3(app^#(l, k)) , sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: app^#(cons(x, l), k) -> c_3(app^#(l, k)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_8) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [app](x1, x2) = [7] x1 + [7] x2 + [0] [nil] = [0] [cons](x1, x2) = [1] x2 + [1] [sum](x1) = [7] x1 + [0] [plus](x1, x2) = [2] x2 + [0] [0] = [7] [s](x1) = [0] [app^#](x1, x2) = [1] x1 + [7] x2 + [0] [c_1] = [0] [c_2] = [0] [c_3](x1) = [1] x1 + [0] [sum^#](x1) = [0] [c_4](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_5] = [0] [c_6](x1, x2) = [4] x1 + [4] x2 + [0] [plus^#](x1, x2) = [0] [c_7] = [0] [c_8](x1) = [1] x1 + [0] The following symbols are considered usable {plus, app^#, sum^#, plus^#} The order satisfies the following ordering constraints: [plus(0(), y)] = [2] y + [0] >= [1] y + [0] = [y] [plus(s(x), y)] = [2] y + [0] >= [0] = [s(plus(x, y))] [app^#(cons(x, l), k)] = [7] k + [1] l + [1] > [7] k + [1] l + [0] = [c_3(app^#(l, k))] [sum^#(cons(x, cons(y, l)))] = [0] >= [0] = [c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))] [plus^#(s(x), y)] = [0] >= [0] = [c_8(plus^#(x, y))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak DPs: { app^#(cons(x, l), k) -> c_3(app^#(l, k)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { app^#(cons(x, l), k) -> c_3(app^#(l, k)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) , plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } and lower component { plus^#(s(x), y) -> c_8(plus^#(x, y)) } Further, following extension rules are added to the lower component. { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } Trs: { plus(s(x), y) -> s(plus(x, y)) } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(app) = {}, safe(nil) = {}, safe(cons) = {1, 2}, safe(sum) = {}, safe(plus) = {1}, safe(0) = {}, safe(s) = {1}, safe(app^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(sum^#) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(plus^#) = {}, safe(c_7) = {}, safe(c_8) = {} and precedence plus ~ sum^# . Following symbols are considered recursive: {plus, sum^#} The recursion depth is 1. Further, following argument filtering is employed: pi(app) = [], pi(nil) = [], pi(cons) = [2], pi(sum) = [], pi(plus) = [1], pi(0) = [], pi(s) = [], pi(app^#) = [], pi(c_1) = [], pi(c_2) = [], pi(c_3) = [], pi(sum^#) = [1], pi(c_4) = [], pi(c_5) = [], pi(c_6) = [1, 2], pi(plus^#) = [], pi(c_7) = [], pi(c_8) = [] Usable defined function symbols are a subset of: {app^#, sum^#, plus^#} For your convenience, here are the satisfied ordering constraints: pi(sum^#(cons(x, cons(y, l)))) = sum^#(cons(; cons(; l));) > c_6(sum^#(cons(; l);), plus^#();) = pi(c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { sum^#(cons(x, cons(y, l))) -> c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak DPs: { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: plus^#(s(x), y) -> c_8(plus^#(x, y)) } Trs: { plus(0(), y) -> y } Sub-proof: ---------- The following argument positions are usable: Uargs(c_8) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [app](x1, x2) = [7] x1 + [7] x2 + [0] [nil] = [0] [cons](x1, x2) = [1] x1 + [1] x2 + [0] [sum](x1) = [7] x1 + [0] [plus](x1, x2) = [1] x1 + [1] x2 + [0] [0] = [1] [s](x1) = [1] x1 + [1] [app^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [c_2] = [0] [c_3](x1) = [7] x1 + [0] [sum^#](x1) = [2] x1 + [0] [c_4](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_5] = [0] [c_6](x1, x2) = [7] x1 + [7] x2 + [0] [plus^#](x1, x2) = [1] x1 + [2] x2 + [0] [c_7] = [0] [c_8](x1) = [1] x1 + [0] The following symbols are considered usable {plus, sum^#, plus^#} The order satisfies the following ordering constraints: [plus(0(), y)] = [1] y + [1] > [1] y + [0] = [y] [plus(s(x), y)] = [1] x + [1] y + [1] >= [1] x + [1] y + [1] = [s(plus(x, y))] [sum^#(cons(x, cons(y, l)))] = [2] l + [2] x + [2] y + [0] >= [2] l + [2] x + [2] y + [0] = [sum^#(cons(plus(x, y), l))] [sum^#(cons(x, cons(y, l)))] = [2] l + [2] x + [2] y + [0] >= [1] x + [2] y + [0] = [plus^#(x, y)] [plus^#(s(x), y)] = [1] x + [2] y + [1] > [1] x + [2] y + [0] = [c_8(plus^#(x, y))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) , plus^#(s(x), y) -> c_8(plus^#(x, y)) } Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) , plus^#(s(x), y) -> c_8(plus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))