WORST_CASE(?,O(n^2)) * Step 1: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) dyade(cons(x,xs),ls) -> cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) -> nil() mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) mult(n,nil()) -> nil() times(0(),y) -> 0() times(s(x),y) -> add(y,times(x,y)) - Signature: {add/2,dyade/2,mult/2,times/2} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dyade,mult,times} and constructors {0,cons,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(cons) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(add) = [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(dyade) = [8] x1 + [2] p(mult) = [0] p(nil) = [2] p(s) = [1] x1 + [3] p(times) = [2] Following rules are strictly oriented: dyade(nil(),ls) = [18] > [2] = nil() times(0(),y) = [2] > [0] = 0() Following rules are (at-least) weakly oriented: add(0(),y) = [1] y + [0] >= [1] y + [0] = y add(s(x),y) = [1] y + [0] >= [1] y + [3] = s(add(x,y)) dyade(cons(x,xs),ls) = [8] x + [8] xs + [2] >= [8] xs + [2] = cons(mult(x,ls),dyade(xs,ls)) mult(n,cons(x,xs)) = [0] >= [2] = cons(times(n,x),mult(n,xs)) mult(n,nil()) = [0] >= [2] = nil() times(s(x),y) = [2] >= [2] = add(y,times(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) dyade(cons(x,xs),ls) -> cons(mult(x,ls),dyade(xs,ls)) mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) mult(n,nil()) -> nil() times(s(x),y) -> add(y,times(x,y)) - Weak TRS: dyade(nil(),ls) -> nil() times(0(),y) -> 0() - Signature: {add/2,dyade/2,mult/2,times/2} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dyade,mult,times} and constructors {0,cons,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(cons) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(add) = [1] x2 + [2] p(cons) = [1] x1 + [1] x2 + [1] p(dyade) = [13] x1 + [4] x2 + [0] p(mult) = [0] p(nil) = [2] p(s) = [1] x1 + [8] p(times) = [0] Following rules are strictly oriented: add(0(),y) = [1] y + [2] > [1] y + [0] = y dyade(cons(x,xs),ls) = [4] ls + [13] x + [13] xs + [13] > [4] ls + [13] xs + [1] = cons(mult(x,ls),dyade(xs,ls)) Following rules are (at-least) weakly oriented: add(s(x),y) = [1] y + [2] >= [1] y + [10] = s(add(x,y)) dyade(nil(),ls) = [4] ls + [26] >= [2] = nil() mult(n,cons(x,xs)) = [0] >= [1] = cons(times(n,x),mult(n,xs)) mult(n,nil()) = [0] >= [2] = nil() times(0(),y) = [0] >= [0] = 0() times(s(x),y) = [0] >= [2] = add(y,times(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(s(x),y) -> s(add(x,y)) mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) mult(n,nil()) -> nil() times(s(x),y) -> add(y,times(x,y)) - Weak TRS: add(0(),y) -> y dyade(cons(x,xs),ls) -> cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) -> nil() times(0(),y) -> 0() - Signature: {add/2,dyade/2,mult/2,times/2} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dyade,mult,times} and constructors {0,cons,nil,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(cons) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(add) = [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [13] p(dyade) = [2] x1 + [2] x2 + [0] p(mult) = [4] p(nil) = [0] p(s) = [1] x1 + [1] p(times) = [0] Following rules are strictly oriented: mult(n,nil()) = [4] > [0] = nil() Following rules are (at-least) weakly oriented: add(0(),y) = [1] y + [0] >= [1] y + [0] = y add(s(x),y) = [1] y + [0] >= [1] y + [1] = s(add(x,y)) dyade(cons(x,xs),ls) = [2] ls + [2] x + [2] xs + [26] >= [2] ls + [2] xs + [17] = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = [2] ls + [0] >= [0] = nil() mult(n,cons(x,xs)) = [4] >= [17] = cons(times(n,x),mult(n,xs)) times(0(),y) = [0] >= [0] = 0() times(s(x),y) = [0] >= [0] = add(y,times(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(s(x),y) -> s(add(x,y)) mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) times(s(x),y) -> add(y,times(x,y)) - Weak TRS: add(0(),y) -> y dyade(cons(x,xs),ls) -> cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) -> nil() mult(n,nil()) -> nil() times(0(),y) -> 0() - Signature: {add/2,dyade/2,mult/2,times/2} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dyade,mult,times} and constructors {0,cons,nil,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(add) = {2}, uargs(cons) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {add,dyade,mult,times} TcT has computed the following interpretation: p(0) = 0 p(add) = x2 p(cons) = 2 + x1 + x2 p(dyade) = 1 + 7*x1*x2 + x1^2 p(mult) = 1 + 4*x1 + 4*x1*x2 + 3*x2 p(nil) = 2 p(s) = x1 p(times) = x1 + x2 Following rules are strictly oriented: mult(n,cons(x,xs)) = 7 + 12*n + 4*n*x + 4*n*xs + 3*x + 3*xs > 3 + 5*n + 4*n*xs + x + 3*xs = cons(times(n,x),mult(n,xs)) Following rules are (at-least) weakly oriented: add(0(),y) = y >= y = y add(s(x),y) = y >= y = s(add(x,y)) dyade(cons(x,xs),ls) = 5 + 14*ls + 7*ls*x + 7*ls*xs + 4*x + 2*x*xs + x^2 + 4*xs + xs^2 >= 4 + 3*ls + 4*ls*x + 7*ls*xs + 4*x + xs^2 = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 5 + 14*ls >= 2 = nil() mult(n,nil()) = 7 + 12*n >= 2 = nil() times(0(),y) = y >= 0 = 0() times(s(x),y) = x + y >= x + y = add(y,times(x,y)) * Step 5: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(s(x),y) -> s(add(x,y)) times(s(x),y) -> add(y,times(x,y)) - Weak TRS: add(0(),y) -> y dyade(cons(x,xs),ls) -> cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) -> nil() mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) mult(n,nil()) -> nil() times(0(),y) -> 0() - Signature: {add/2,dyade/2,mult/2,times/2} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dyade,mult,times} and constructors {0,cons,nil,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(add) = {2}, uargs(cons) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {add,dyade,mult,times} TcT has computed the following interpretation: p(0) = 0 p(add) = 4*x1 + x2 p(cons) = 3 + x1 + x2 p(dyade) = 2*x1 + 5*x1*x2 + x1^2 p(mult) = 6 + 5*x1*x2 + 2*x2 p(nil) = 3 p(s) = 2 + x1 p(times) = 3*x1*x2 + 2*x2 Following rules are strictly oriented: add(s(x),y) = 8 + 4*x + y > 2 + 4*x + y = s(add(x,y)) Following rules are (at-least) weakly oriented: add(0(),y) = y >= y = y dyade(cons(x,xs),ls) = 15 + 15*ls + 5*ls*x + 5*ls*xs + 8*x + 2*x*xs + x^2 + 8*xs + xs^2 >= 9 + 2*ls + 5*ls*x + 5*ls*xs + 2*xs + xs^2 = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 15 + 15*ls >= 3 = nil() mult(n,cons(x,xs)) = 12 + 15*n + 5*n*x + 5*n*xs + 2*x + 2*xs >= 9 + 3*n*x + 5*n*xs + 2*x + 2*xs = cons(times(n,x),mult(n,xs)) mult(n,nil()) = 12 + 15*n >= 3 = nil() times(0(),y) = 2*y >= 0 = 0() times(s(x),y) = 3*x*y + 8*y >= 3*x*y + 6*y = add(y,times(x,y)) * Step 6: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: times(s(x),y) -> add(y,times(x,y)) - Weak TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) dyade(cons(x,xs),ls) -> cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) -> nil() mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) mult(n,nil()) -> nil() times(0(),y) -> 0() - Signature: {add/2,dyade/2,mult/2,times/2} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dyade,mult,times} and constructors {0,cons,nil,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(add) = {2}, uargs(cons) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {add,dyade,mult,times} TcT has computed the following interpretation: p(0) = 0 p(add) = 2*x1 + x2 p(cons) = 2 + x1 + x2 p(dyade) = 6*x1*x2 + 2*x1^2 + 2*x2 + 2*x2^2 p(mult) = 1 + 5*x1*x2 + 2*x1^2 + 3*x2 p(nil) = 0 p(s) = 1 + x1 p(times) = 2 + 3*x1 + 2*x1*x2 Following rules are strictly oriented: times(s(x),y) = 5 + 3*x + 2*x*y + 2*y > 2 + 3*x + 2*x*y + 2*y = add(y,times(x,y)) Following rules are (at-least) weakly oriented: add(0(),y) = y >= y = y add(s(x),y) = 2 + 2*x + y >= 1 + 2*x + y = s(add(x,y)) dyade(cons(x,xs),ls) = 8 + 14*ls + 6*ls*x + 6*ls*xs + 2*ls^2 + 8*x + 4*x*xs + 2*x^2 + 8*xs + 2*xs^2 >= 3 + 5*ls + 5*ls*x + 6*ls*xs + 2*ls^2 + 2*x^2 + 2*xs^2 = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 2*ls + 2*ls^2 >= 0 = nil() mult(n,cons(x,xs)) = 7 + 10*n + 5*n*x + 5*n*xs + 2*n^2 + 3*x + 3*xs >= 5 + 3*n + 2*n*x + 5*n*xs + 2*n^2 + 3*xs = cons(times(n,x),mult(n,xs)) mult(n,nil()) = 1 + 2*n^2 >= 0 = nil() times(0(),y) = 2 >= 0 = 0() * Step 7: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) dyade(cons(x,xs),ls) -> cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) -> nil() mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) mult(n,nil()) -> nil() times(0(),y) -> 0() times(s(x),y) -> add(y,times(x,y)) - Signature: {add/2,dyade/2,mult/2,times/2} / {0/0,cons/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dyade,mult,times} and constructors {0,cons,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))