WORST_CASE(?,O(n^2)) * Step 1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) mtadd(x,cons(t,ts)) -> cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) -> nil() tadd(x,leaf()) -> leaf() tadd(x,node(y,ts)) -> node(add(x,y),mtadd(x,ts)) - Signature: {add/2,mtadd/2,tadd/2} / {0/0,cons/2,leaf/0,nil/0,node/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,mtadd,tadd} and constructors {0,cons,leaf,nil,node,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(cons) = {1,2}, uargs(node) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {add,mtadd,tadd} TcT has computed the following interpretation: p(0) = [1] p(add) = [2] x2 + [0] p(cons) = [1] x1 + [1] x2 + [10] p(leaf) = [9] p(mtadd) = [2] x2 + [0] p(nil) = [1] p(node) = [1] x1 + [1] x2 + [0] p(s) = [1] x1 + [0] p(tadd) = [2] x2 + [0] Following rules are strictly oriented: mtadd(x,cons(t,ts)) = [2] t + [2] ts + [20] > [2] t + [2] ts + [10] = cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) = [2] > [1] = nil() tadd(x,leaf()) = [18] > [9] = leaf() Following rules are (at-least) weakly oriented: add(0(),y) = [2] y + [0] >= [1] y + [0] = y add(s(x),y) = [2] y + [0] >= [2] y + [0] = s(add(x,y)) tadd(x,node(y,ts)) = [2] ts + [2] y + [0] >= [2] ts + [2] y + [0] = node(add(x,y),mtadd(x,ts)) * Step 2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) tadd(x,node(y,ts)) -> node(add(x,y),mtadd(x,ts)) - Weak TRS: mtadd(x,cons(t,ts)) -> cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) -> nil() tadd(x,leaf()) -> leaf() - Signature: {add/2,mtadd/2,tadd/2} / {0/0,cons/2,leaf/0,nil/0,node/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,mtadd,tadd} and constructors {0,cons,leaf,nil,node,s} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(cons) = {1,2}, uargs(node) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {add,mtadd,tadd} TcT has computed the following interpretation: p(0) = 0 p(add) = x2 p(cons) = x1 + x2 p(leaf) = 0 p(mtadd) = 4*x2 p(nil) = 6 p(node) = 4 + x1 + x2 p(s) = x1 p(tadd) = 4*x2 Following rules are strictly oriented: tadd(x,node(y,ts)) = 16 + 4*ts + 4*y > 4 + 4*ts + y = node(add(x,y),mtadd(x,ts)) Following rules are (at-least) weakly oriented: add(0(),y) = y >= y = y add(s(x),y) = y >= y = s(add(x,y)) mtadd(x,cons(t,ts)) = 4*t + 4*ts >= 4*t + 4*ts = cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) = 24 >= 6 = nil() tadd(x,leaf()) = 0 >= 0 = leaf() * Step 3: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) - Weak TRS: mtadd(x,cons(t,ts)) -> cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) -> nil() tadd(x,leaf()) -> leaf() tadd(x,node(y,ts)) -> node(add(x,y),mtadd(x,ts)) - Signature: {add/2,mtadd/2,tadd/2} / {0/0,cons/2,leaf/0,nil/0,node/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,mtadd,tadd} and constructors {0,cons,leaf,nil,node,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(cons) = {1,2}, uargs(node) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {add,mtadd,tadd} TcT has computed the following interpretation: p(0) = [1] p(add) = [2] x2 + [1] p(cons) = [1] x1 + [1] x2 + [4] p(leaf) = [0] p(mtadd) = [2] x2 + [12] p(nil) = [0] p(node) = [1] x1 + [1] x2 + [9] p(s) = [1] x1 + [0] p(tadd) = [2] x2 + [4] Following rules are strictly oriented: add(0(),y) = [2] y + [1] > [1] y + [0] = y Following rules are (at-least) weakly oriented: add(s(x),y) = [2] y + [1] >= [2] y + [1] = s(add(x,y)) mtadd(x,cons(t,ts)) = [2] t + [2] ts + [20] >= [2] t + [2] ts + [20] = cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) = [12] >= [0] = nil() tadd(x,leaf()) = [4] >= [0] = leaf() tadd(x,node(y,ts)) = [2] ts + [2] y + [22] >= [2] ts + [2] y + [22] = node(add(x,y),mtadd(x,ts)) * Step 4: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(s(x),y) -> s(add(x,y)) - Weak TRS: add(0(),y) -> y mtadd(x,cons(t,ts)) -> cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) -> nil() tadd(x,leaf()) -> leaf() tadd(x,node(y,ts)) -> node(add(x,y),mtadd(x,ts)) - Signature: {add/2,mtadd/2,tadd/2} / {0/0,cons/2,leaf/0,nil/0,node/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,mtadd,tadd} and constructors {0,cons,leaf,nil,node,s} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(cons) = {1,2}, uargs(node) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {add,mtadd,tadd} TcT has computed the following interpretation: p(0) = 2 p(add) = 3*x1 + 2*x2 p(cons) = x1 + x2 p(leaf) = 0 p(mtadd) = 3*x1 + 6*x1*x2 + 4*x2 + x2^2 p(nil) = 2 p(node) = 1 + x1 + x2 p(s) = 1 + x1 p(tadd) = 6*x1*x2 + 2*x2 + x2^2 Following rules are strictly oriented: add(s(x),y) = 3 + 3*x + 2*y > 1 + 3*x + 2*y = s(add(x,y)) Following rules are (at-least) weakly oriented: add(0(),y) = 6 + 2*y >= y = y mtadd(x,cons(t,ts)) = 4*t + 2*t*ts + 6*t*x + t^2 + 4*ts + 6*ts*x + ts^2 + 3*x >= 2*t + 6*t*x + t^2 + 4*ts + 6*ts*x + ts^2 + 3*x = cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) = 12 + 15*x >= 2 = nil() tadd(x,leaf()) = 0 >= 0 = leaf() tadd(x,node(y,ts)) = 3 + 4*ts + 6*ts*x + 2*ts*y + ts^2 + 6*x + 6*x*y + 4*y + y^2 >= 1 + 4*ts + 6*ts*x + ts^2 + 6*x + 2*y = node(add(x,y),mtadd(x,ts)) * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) mtadd(x,cons(t,ts)) -> cons(tadd(x,t),mtadd(x,ts)) mtadd(x,nil()) -> nil() tadd(x,leaf()) -> leaf() tadd(x,node(y,ts)) -> node(add(x,y),mtadd(x,ts)) - Signature: {add/2,mtadd/2,tadd/2} / {0/0,cons/2,leaf/0,nil/0,node/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,mtadd,tadd} and constructors {0,cons,leaf,nil,node,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))