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 = 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(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) = x1 + x2 p(dyade) = 4 + 12*x1 + 2*x2 p(mult) = 2*x1 p(nil) = 0 p(s) = x1 p(times) = 0 Following rules are strictly oriented: dyade(nil(),ls) = 4 + 2*ls > 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)) dyade(cons(x,xs),ls) = 4 + 2*ls + 12*x + 12*xs >= 4 + 2*ls + 2*x + 12*xs = cons(mult(x,ls),dyade(xs,ls)) mult(n,cons(x,xs)) = 2*n >= 2*n = cons(times(n,x),mult(n,xs)) mult(n,nil()) = 2*n >= 0 = nil() times(0(),y) = 0 >= 0 = 0() times(s(x),y) = 0 >= 0 = add(y,times(x,y)) * Step 2: Ara 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(0(),y) -> 0() times(s(x),y) -> add(y,times(x,y)) - Weak TRS: dyade(nil(),ls) -> 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: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(0) F (TrsFun "0") :: [] -(0)-> "A"(7) F (TrsFun "add") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "cons") :: ["A"(0) x "A"(15)] -(15)-> "A"(15) F (TrsFun "cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "cons") :: ["A"(0) x "A"(1)] -(1)-> "A"(1) F (TrsFun "dyade") :: ["A"(15) x "A"(11)] -(8)-> "A"(1) F (TrsFun "mult") :: ["A"(0) x "A"(0)] -(1)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(15) F (TrsFun "nil") :: [] -(0)-> "A"(7) F (TrsFun "s") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "s") :: ["A"(0)] -(0)-> "A"(1) F (TrsFun "times") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"cons\")_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"s\")_A" :: ["A"(0)] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: dyade(cons(x,xs),ls) -> cons(mult(x,ls),dyade(xs,ls)) mult(n,nil()) -> nil() 2. Weak: add(0(),y) -> y add(s(x),y) -> s(add(x,y)) mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) times(0(),y) -> 0() times(s(x),y) -> 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)) mult(n,cons(x,xs)) -> cons(times(n,x),mult(n,xs)) 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,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) = x1 + x2 p(cons) = 2 + x1 + x2 p(dyade) = 4 + x1 + 4*x1*x2 + 2*x1^2 + 3*x2 + x2^2 p(mult) = 4*x1*x2 + 5*x2 p(nil) = 1 p(s) = 3 + x1 p(times) = 1 + x1*x2 + x2 Following rules are strictly oriented: mult(n,cons(x,xs)) = 10 + 8*n + 4*n*x + 4*n*xs + 5*x + 5*xs > 3 + n*x + 4*n*xs + x + 5*xs = cons(times(n,x),mult(n,xs)) times(0(),y) = 1 + y > 0 = 0() Following rules are (at-least) weakly oriented: add(0(),y) = y >= y = y add(s(x),y) = 3 + x + y >= 3 + x + y = s(add(x,y)) dyade(cons(x,xs),ls) = 14 + 11*ls + 4*ls*x + 4*ls*xs + ls^2 + 9*x + 4*x*xs + 2*x^2 + 9*xs + 2*xs^2 >= 6 + 8*ls + 4*ls*x + 4*ls*xs + ls^2 + xs + 2*xs^2 = cons(mult(x,ls),dyade(xs,ls)) dyade(nil(),ls) = 7 + 7*ls + ls^2 >= 1 = nil() mult(n,nil()) = 5 + 4*n >= 1 = nil() times(s(x),y) = 1 + x*y + 4*y >= 1 + 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 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 5: 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 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) = 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 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))