WORST_CASE(?,O(n^2)) * Step 1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: main(x5,x12) -> map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) -> Nil() map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) -> x8 plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14)) - Signature: {main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,plus_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main,map#2,plus_x#1} and constructors {0,Cons,Nil,S ,plus_x} + 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(S) = {1} Following symbols are considered usable: {main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 0 p(Cons) = x1 + x2 p(Nil) = 0 p(S) = x1 p(main) = 4 + x1 p(map#2) = x2 p(plus_x) = 0 p(plus_x#1) = x2 Following rules are strictly oriented: main(x5,x12) = 4 + x5 > x5 = map#2(plus_x(x12),x5) Following rules are (at-least) weakly oriented: map#2(plus_x(x2),Nil()) = 0 >= 0 = Nil() map#2(plus_x(x6),Cons(x4,x2)) = x2 + x4 >= x2 + x4 = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = x8 >= x8 = x8 plus_x#1(S(x12),x14) = x14 >= x14 = S(plus_x#1(x12,x14)) * Step 2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: map#2(plus_x(x2),Nil()) -> Nil() map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) -> x8 plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14)) - Weak TRS: main(x5,x12) -> map#2(plus_x(x12),x5) - Signature: {main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,plus_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main,map#2,plus_x#1} and constructors {0,Cons,Nil,S ,plus_x} + 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(S) = {1} Following symbols are considered usable: {main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 0 p(Cons) = 1 + x1 + x2 p(Nil) = 0 p(S) = x1 p(main) = 2 + x1 p(map#2) = 2 + x1*x2 + x2 p(plus_x) = 0 p(plus_x#1) = x2 Following rules are strictly oriented: map#2(plus_x(x2),Nil()) = 2 > 0 = Nil() Following rules are (at-least) weakly oriented: main(x5,x12) = 2 + x5 >= 2 + x5 = map#2(plus_x(x12),x5) map#2(plus_x(x6),Cons(x4,x2)) = 3 + x2 + x4 >= 3 + x2 + x4 = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = x8 >= x8 = x8 plus_x#1(S(x12),x14) = x14 >= x14 = S(plus_x#1(x12,x14)) * Step 3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) -> x8 plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14)) - Weak TRS: main(x5,x12) -> map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) -> Nil() - Signature: {main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,plus_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main,map#2,plus_x#1} and constructors {0,Cons,Nil,S ,plus_x} + 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(S) = {1} Following symbols are considered usable: {main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 2 p(Cons) = 2 + x1 + x2 p(Nil) = 0 p(S) = 2 + x1 p(main) = 2 + 5*x1 + 4*x1*x2 + 6*x1^2 + 2*x2 + 4*x2^2 p(map#2) = 1 + x1 + 4*x1*x2 + 4*x1^2 + 2*x2^2 p(plus_x) = x1 p(plus_x#1) = 5*x1 + 2*x2 Following rules are strictly oriented: map#2(plus_x(x6),Cons(x4,x2)) = 9 + 8*x2 + 4*x2*x4 + 4*x2*x6 + 2*x2^2 + 8*x4 + 4*x4*x6 + 2*x4^2 + 9*x6 + 4*x6^2 > 3 + 4*x2*x6 + 2*x2^2 + 2*x4 + 6*x6 + 4*x6^2 = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = 10 + 2*x8 > x8 = x8 plus_x#1(S(x12),x14) = 10 + 5*x12 + 2*x14 > 2 + 5*x12 + 2*x14 = S(plus_x#1(x12,x14)) Following rules are (at-least) weakly oriented: main(x5,x12) = 2 + 2*x12 + 4*x12*x5 + 4*x12^2 + 5*x5 + 6*x5^2 >= 1 + x12 + 4*x12*x5 + 4*x12^2 + 2*x5^2 = map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) = 1 + x2 + 4*x2^2 >= 0 = Nil() * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: main(x5,x12) -> map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) -> Nil() map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) -> x8 plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14)) - Signature: {main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,plus_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main,map#2,plus_x#1} and constructors {0,Cons,Nil,S ,plus_x} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))