WORST_CASE(?,O(n^2)) * Step 1: NaturalPI 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: 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*x2 p(cons) = 1 + x1 + x2 p(dyade) = 4 + 2*x1 + 4*x1*x2 + 6*x1^2 + x2^2 p(mult) = 2 + x1^2 + 4*x2 p(nil) = 0 p(s) = x1 p(times) = 0 Following rules are strictly oriented: dyade(cons(x,xs),ls) = 12 + 4*ls + 4*ls*x + 4*ls*xs + ls^2 + 14*x + 12*x*xs + 6*x^2 + 14*xs + 6*xs^2 > 7 + 4*ls + 4*ls*xs + ls^2 + x^2 + 2*xs + 6*xs^2 = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 4 + ls^2 > 0 = nil() mult(n,cons(x,xs)) = 6 + n^2 + 4*x + 4*xs > 3 + n^2 + 4*xs = cons(times(n,x),mult(n,xs)) mult(n,nil()) = 2 + n^2 > 0 = nil() Following rules are (at-least) weakly oriented: add(0(),y) = 2*y >= y = y add(s(x),y) = 2*y >= 2*y = s(add(x,y)) times(0(),y) = 0 >= 0 = 0() times(s(x),y) = 0 >= 0 = add(y,times(x,y)) * Step 2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) times(0(),y) -> 0() times(s(x),y) -> add(y,times(x,y)) - Weak TRS: 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() - 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) = 1 + x1 + x2 p(dyade) = 6*x1 + 6*x1*x2 + 4*x1^2 + 2*x2^2 p(mult) = 4 + x1 + 4*x1^2 + 4*x2 p(nil) = 1 p(s) = x1 p(times) = 2 Following rules are strictly oriented: times(0(),y) = 2 > 0 = 0() 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) = 10 + 6*ls + 6*ls*x + 6*ls*xs + 2*ls^2 + 14*x + 8*x*xs + 4*x^2 + 14*xs + 4*xs^2 >= 5 + 4*ls + 6*ls*xs + 2*ls^2 + x + 4*x^2 + 6*xs + 4*xs^2 = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 10 + 6*ls + 2*ls^2 >= 1 = nil() mult(n,cons(x,xs)) = 8 + n + 4*n^2 + 4*x + 4*xs >= 7 + n + 4*n^2 + 4*xs = cons(times(n,x),mult(n,xs)) mult(n,nil()) = 8 + n + 4*n^2 >= 1 = nil() times(s(x),y) = 2 >= 2 = add(y,times(x,y)) * Step 3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) times(s(x),y) -> add(y,times(x,y)) - Weak TRS: 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) = x1 + x2 p(dyade) = 6*x1 + 2*x1*x2 + 6*x1^2 + 4*x2 + 7*x2^2 p(mult) = 5*x1 + 2*x1*x2 + 5*x1^2 p(nil) = 0 p(s) = 2 + x1 p(times) = 2*x1*x2 Following rules are strictly oriented: add(s(x),y) = 4 + 2*x + y > 2 + 2*x + y = s(add(x,y)) Following rules are (at-least) weakly oriented: add(0(),y) = y >= y = y dyade(cons(x,xs),ls) = 4*ls + 2*ls*x + 2*ls*xs + 7*ls^2 + 6*x + 12*x*xs + 6*x^2 + 6*xs + 6*xs^2 >= 4*ls + 2*ls*x + 2*ls*xs + 7*ls^2 + 5*x + 5*x^2 + 6*xs + 6*xs^2 = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 4*ls + 7*ls^2 >= 0 = nil() mult(n,cons(x,xs)) = 5*n + 2*n*x + 2*n*xs + 5*n^2 >= 5*n + 2*n*x + 2*n*xs + 5*n^2 = cons(times(n,x),mult(n,xs)) mult(n,nil()) = 5*n + 5*n^2 >= 0 = nil() times(0(),y) = 0 >= 0 = 0() times(s(x),y) = 2*x*y + 4*y >= 2*x*y + 2*y = add(y,times(x,y)) * Step 4: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: add(0(),y) -> y times(s(x),y) -> add(y,times(x,y)) - Weak TRS: 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) = 4 + x1 + x2 p(cons) = 2 + x1 + x2 p(dyade) = 4*x1 + 4*x1*x2 + x1^2 + 2*x2^2 p(mult) = 1 + 3*x1*x2 + x1^2 + x2 p(nil) = 0 p(s) = 2 + x1 p(times) = 2*x1 + 2*x1*x2 Following rules are strictly oriented: add(0(),y) = 4 + y > y = y Following rules are (at-least) weakly oriented: add(s(x),y) = 6 + x + y >= 6 + x + y = s(add(x,y)) dyade(cons(x,xs),ls) = 12 + 8*ls + 4*ls*x + 4*ls*xs + 2*ls^2 + 8*x + 2*x*xs + x^2 + 8*xs + xs^2 >= 3 + ls + 3*ls*x + 4*ls*xs + 2*ls^2 + x^2 + 4*xs + xs^2 = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 2*ls^2 >= 0 = nil() mult(n,cons(x,xs)) = 3 + 6*n + 3*n*x + 3*n*xs + n^2 + x + xs >= 3 + 2*n + 2*n*x + 3*n*xs + n^2 + xs = cons(times(n,x),mult(n,xs)) mult(n,nil()) = 1 + n^2 >= 0 = nil() times(0(),y) = 0 >= 0 = 0() times(s(x),y) = 4 + 2*x + 2*x*y + 4*y >= 4 + 2*x + 2*x*y + y = add(y,times(x,y)) * Step 5: 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) = x1 + x2 p(cons) = 2 + x1 + x2 p(dyade) = 5*x1 + 3*x1*x2 + 6*x2 p(mult) = 7 + 5*x1 + 2*x1*x2 + x2 p(nil) = 0 p(s) = 2 + x1 p(times) = x1 + x1*x2 Following rules are strictly oriented: times(s(x),y) = 2 + x + x*y + 2*y > x + x*y + y = add(y,times(x,y)) Following rules are (at-least) weakly oriented: add(0(),y) = y >= y = y add(s(x),y) = 2 + x + y >= 2 + x + y = s(add(x,y)) dyade(cons(x,xs),ls) = 10 + 12*ls + 3*ls*x + 3*ls*xs + 5*x + 5*xs >= 9 + 7*ls + 2*ls*x + 3*ls*xs + 5*x + 5*xs = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 6*ls >= 0 = nil() mult(n,cons(x,xs)) = 9 + 9*n + 2*n*x + 2*n*xs + x + xs >= 9 + 6*n + n*x + 2*n*xs + xs = cons(times(n,x),mult(n,xs)) mult(n,nil()) = 7 + 5*n >= 0 = nil() times(0(),y) = 0 >= 0 = 0() * Step 6: 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))