WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__2ND(z0) -> c5() A__2ND(cons(z0,z1)) -> c4(A__HEAD(mark(z1)),MARK(z1)) A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__HEAD(z0) -> c3() A__HEAD(cons(z0,z1)) -> c2(MARK(z0)) A__SEL(z0,z1) -> c12() A__SEL(0(),cons(z0,z1)) -> c9(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c10(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c11(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7(MARK(z1)) MARK(0()) -> c22() MARK(2nd(z0)) -> c15(A__2ND(mark(z0)),MARK(z0)) MARK(cons(z0,z1)) -> c20(MARK(z0)) MARK(from(z0)) -> c13(A__FROM(mark(z0)),MARK(z0)) MARK(head(z0)) -> c14(A__HEAD(mark(z0)),MARK(z0)) MARK(nil()) -> c23() MARK(s(z0)) -> c21(MARK(z0)) MARK(sel(z0,z1)) -> c18(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c19(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(take(z0,z1)) -> c16(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c17(A__TAKE(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__2nd(z0) -> 2nd(z0) a__2nd(cons(z0,z1)) -> a__head(mark(z1)) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__sel(z0,z1) -> sel(z0,z1) a__sel(0(),cons(z0,z1)) -> mark(z0) a__sel(s(z0),cons(z1,z2)) -> a__sel(mark(z0),mark(z2)) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(mark(z1),take(z0,z2)) mark(0()) -> 0() mark(2nd(z0)) -> a__2nd(mark(z0)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) - Signature: {A__2ND/1,A__FROM/1,A__HEAD/1,A__SEL/2,A__TAKE/2,MARK/1,a__2nd/1,a__from/1,a__head/1,a__sel/2,a__take/2 ,mark/1} / {0/0,2nd/1,c/1,c1/0,c10/2,c11/2,c12/0,c13/2,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/1,c20/1,c21/1 ,c22/0,c23/0,c3/0,c4/2,c5/0,c6/0,c7/1,c8/0,c9/1,cons/2,from/1,head/1,nil/0,s/1,sel/2,take/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__2ND,A__FROM,A__HEAD,A__SEL,A__TAKE,MARK,a__2nd,a__from ,a__head,a__sel,a__take,mark} and constructors {0,2nd,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9,cons,from,head,nil,s,sel,take} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__2ND(z0) -> c5() A__2ND(cons(z0,z1)) -> c4(A__HEAD(mark(z1)),MARK(z1)) A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__HEAD(z0) -> c3() A__HEAD(cons(z0,z1)) -> c2(MARK(z0)) A__SEL(z0,z1) -> c12() A__SEL(0(),cons(z0,z1)) -> c9(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c10(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c11(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7(MARK(z1)) MARK(0()) -> c22() MARK(2nd(z0)) -> c15(A__2ND(mark(z0)),MARK(z0)) MARK(cons(z0,z1)) -> c20(MARK(z0)) MARK(from(z0)) -> c13(A__FROM(mark(z0)),MARK(z0)) MARK(head(z0)) -> c14(A__HEAD(mark(z0)),MARK(z0)) MARK(nil()) -> c23() MARK(s(z0)) -> c21(MARK(z0)) MARK(sel(z0,z1)) -> c18(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c19(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(take(z0,z1)) -> c16(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c17(A__TAKE(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__2nd(z0) -> 2nd(z0) a__2nd(cons(z0,z1)) -> a__head(mark(z1)) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__sel(z0,z1) -> sel(z0,z1) a__sel(0(),cons(z0,z1)) -> mark(z0) a__sel(s(z0),cons(z1,z2)) -> a__sel(mark(z0),mark(z2)) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(mark(z1),take(z0,z2)) mark(0()) -> 0() mark(2nd(z0)) -> a__2nd(mark(z0)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) - Signature: {A__2ND/1,A__FROM/1,A__HEAD/1,A__SEL/2,A__TAKE/2,MARK/1,a__2nd/1,a__from/1,a__head/1,a__sel/2,a__take/2 ,mark/1} / {0/0,2nd/1,c/1,c1/0,c10/2,c11/2,c12/0,c13/2,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/1,c20/1,c21/1 ,c22/0,c23/0,c3/0,c4/2,c5/0,c6/0,c7/1,c8/0,c9/1,cons/2,from/1,head/1,nil/0,s/1,sel/2,take/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__2ND,A__FROM,A__HEAD,A__SEL,A__TAKE,MARK,a__2nd,a__from ,a__head,a__sel,a__take,mark} and constructors {0,2nd,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9,cons,from,head,nil,s,sel,take} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__2ND(z0) -> c5() A__2ND(cons(z0,z1)) -> c4(A__HEAD(mark(z1)),MARK(z1)) A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__HEAD(z0) -> c3() A__HEAD(cons(z0,z1)) -> c2(MARK(z0)) A__SEL(z0,z1) -> c12() A__SEL(0(),cons(z0,z1)) -> c9(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c10(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c11(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7(MARK(z1)) MARK(0()) -> c22() MARK(2nd(z0)) -> c15(A__2ND(mark(z0)),MARK(z0)) MARK(cons(z0,z1)) -> c20(MARK(z0)) MARK(from(z0)) -> c13(A__FROM(mark(z0)),MARK(z0)) MARK(head(z0)) -> c14(A__HEAD(mark(z0)),MARK(z0)) MARK(nil()) -> c23() MARK(s(z0)) -> c21(MARK(z0)) MARK(sel(z0,z1)) -> c18(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c19(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(take(z0,z1)) -> c16(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c17(A__TAKE(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__2nd(z0) -> 2nd(z0) a__2nd(cons(z0,z1)) -> a__head(mark(z1)) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__sel(z0,z1) -> sel(z0,z1) a__sel(0(),cons(z0,z1)) -> mark(z0) a__sel(s(z0),cons(z1,z2)) -> a__sel(mark(z0),mark(z2)) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(mark(z1),take(z0,z2)) mark(0()) -> 0() mark(2nd(z0)) -> a__2nd(mark(z0)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) - Signature: {A__2ND/1,A__FROM/1,A__HEAD/1,A__SEL/2,A__TAKE/2,MARK/1,a__2nd/1,a__from/1,a__head/1,a__sel/2,a__take/2 ,mark/1} / {0/0,2nd/1,c/1,c1/0,c10/2,c11/2,c12/0,c13/2,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/1,c20/1,c21/1 ,c22/0,c23/0,c3/0,c4/2,c5/0,c6/0,c7/1,c8/0,c9/1,cons/2,from/1,head/1,nil/0,s/1,sel/2,take/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__2ND,A__FROM,A__HEAD,A__SEL,A__TAKE,MARK,a__2nd,a__from ,a__head,a__sel,a__take,mark} and constructors {0,2nd,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9,cons,from,head,nil,s,sel,take} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> 2nd(x)} = MARK(2nd(x)) ->^+ c15(A__2ND(mark(x)),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)