WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum WORST_CASE(Omega(n^1),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: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + 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: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: map#2(plus_x(x),z){z -> Cons(y,z)} = map#2(plus_x(x),Cons(y,z)) ->^+ Cons(plus_x#1(x,y),map#2(plus_x(x),z)) = C[map#2(plus_x(x),z) = map#2(plus_x(x),z){}] ** Step 1.b: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 = 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(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) = 8 + 8*x1 p(map#2) = 8*x2 p(plus_x) = x1 p(plus_x#1) = 8*x2 Following rules are strictly oriented: main(x5,x12) = 8 + 8*x5 > 8*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)) = 8*x2 + 8*x4 >= 8*x2 + 8*x4 = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = 8*x8 >= x8 = x8 plus_x#1(S(x12),x14) = 8*x14 >= 8*x14 = S(plus_x#1(x12,x14)) ** Step 1.b: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 = 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(S) = {1} Following symbols are considered usable: {main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 8 p(Cons) = 15 + x1 + x2 p(Nil) = 0 p(S) = x1 p(main) = 9 + 8*x1 + x2 p(map#2) = 2*x2 p(plus_x) = 2 p(plus_x#1) = 1 + x2 Following rules are strictly oriented: map#2(plus_x(x6),Cons(x4,x2)) = 30 + 2*x2 + 2*x4 > 16 + 2*x2 + x4 = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = 1 + x8 > x8 = x8 Following rules are (at-least) weakly oriented: main(x5,x12) = 9 + x12 + 8*x5 >= 2*x5 = map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) = 0 >= 0 = Nil() plus_x#1(S(x12),x14) = 1 + x14 >= 1 + x14 = S(plus_x#1(x12,x14)) ** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: map#2(plus_x(x2),Nil()) -> Nil() 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(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) -> x8 - 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 = 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(S) = {1} Following symbols are considered usable: {main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 1 p(Cons) = 1 + x1 + x2 p(Nil) = 2 p(S) = x1 p(main) = 8 + 10*x1 + 6*x2 p(map#2) = 8 + 3*x1 + 8*x2 p(plus_x) = x1 p(plus_x#1) = 5 + 8*x2 Following rules are strictly oriented: map#2(plus_x(x2),Nil()) = 24 + 3*x2 > 2 = Nil() Following rules are (at-least) weakly oriented: main(x5,x12) = 8 + 6*x12 + 10*x5 >= 8 + 3*x12 + 8*x5 = map#2(plus_x(x12),x5) map#2(plus_x(x6),Cons(x4,x2)) = 16 + 8*x2 + 8*x4 + 3*x6 >= 14 + 8*x2 + 8*x4 + 3*x6 = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = 5 + 8*x8 >= x8 = x8 plus_x#1(S(x12),x14) = 5 + 8*x14 >= 5 + 8*x14 = S(plus_x#1(x12,x14)) ** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: 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() 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 - 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) = 1 p(Cons) = 2 + x1 + x2 p(Nil) = 0 p(S) = 1 + x1 p(main) = 1 + 4*x1 + 4*x1*x2 + 2*x1^2 + 4*x2 + 4*x2^2 p(map#2) = 1 + 4*x1 + 4*x1*x2 + 2*x1^2 + x2 + 2*x2^2 p(plus_x) = x1 p(plus_x#1) = 3*x1 + 4*x1*x2 Following rules are strictly oriented: plus_x#1(S(x12),x14) = 3 + 3*x12 + 4*x12*x14 + 4*x14 > 1 + 3*x12 + 4*x12*x14 = S(plus_x#1(x12,x14)) Following rules are (at-least) weakly oriented: main(x5,x12) = 1 + 4*x12 + 4*x12*x5 + 4*x12^2 + 4*x5 + 2*x5^2 >= 1 + 4*x12 + 4*x12*x5 + 2*x12^2 + x5 + 2*x5^2 = map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) = 1 + 4*x2 + 2*x2^2 >= 0 = Nil() map#2(plus_x(x6),Cons(x4,x2)) = 11 + 9*x2 + 4*x2*x4 + 4*x2*x6 + 2*x2^2 + 9*x4 + 4*x4*x6 + 2*x4^2 + 12*x6 + 2*x6^2 >= 3 + x2 + 4*x2*x6 + 2*x2^2 + 4*x4*x6 + 7*x6 + 2*x6^2 = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = 3 + 4*x8 >= x8 = x8 ** Step 1.b:5: 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(Omega(n^1),O(n^2))