WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AFTERNTH(z0,z1) -> c23(A__SND(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) A__AFTERNTH(z0,z1) -> c24(A__SND(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) A__AFTERNTH(z0,z1) -> c25() A__FST(z0) -> c3() A__FST(pair(z0,z1)) -> c2(MARK(z0)) A__HEAD(z0) -> c14() A__HEAD(cons(z0,z1)) -> c13(MARK(z0)) A__NATSFROM(z0) -> c(MARK(z0)) A__NATSFROM(z0) -> c1() A__SEL(z0,z1) -> c17(A__HEAD(a__afterNth(mark(z0),mark(z1))),A__AFTERNTH(mark(z0),mark(z1)),MARK(z0)) A__SEL(z0,z1) -> c18(A__HEAD(a__afterNth(mark(z0),mark(z1))),A__AFTERNTH(mark(z0),mark(z1)),MARK(z1)) A__SEL(z0,z1) -> c19() A__SND(z0) -> c5() A__SND(pair(z0,z1)) -> c4(MARK(z1)) A__SPLITAT(z0,z1) -> c9() A__SPLITAT(0(),z0) -> c6(MARK(z0)) A__SPLITAT(s(z0),cons(z1,z2)) -> c7(A__U(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) ,A__SPLITAT(mark(z0),mark(z2)) ,MARK(z0)) A__SPLITAT(s(z0),cons(z1,z2)) -> c8(A__U(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) ,A__SPLITAT(mark(z0),mark(z2)) ,MARK(z2)) A__TAIL(z0) -> c16() A__TAIL(cons(z0,z1)) -> c15(MARK(z1)) A__TAKE(z0,z1) -> c20(A__FST(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) A__TAKE(z0,z1) -> c21(A__FST(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) A__TAKE(z0,z1) -> c22() A__U(z0,z1,z2,z3) -> c12() A__U(pair(z0,z1),z2,z3,z4) -> c10(MARK(z3)) A__U(pair(z0,z1),z2,z3,z4) -> c11(MARK(z1)) MARK(0()) -> c44() MARK(afterNth(z0,z1)) -> c36(A__AFTERNTH(mark(z0),mark(z1)),MARK(z0)) MARK(afterNth(z0,z1)) -> c37(A__AFTERNTH(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c40(MARK(z0)) MARK(fst(z0)) -> c27(A__FST(mark(z0)),MARK(z0)) MARK(head(z0)) -> c32(A__HEAD(mark(z0)),MARK(z0)) MARK(natsFrom(z0)) -> c26(A__NATSFROM(mark(z0)),MARK(z0)) MARK(nil()) -> c45() MARK(pair(z0,z1)) -> c42(MARK(z0)) MARK(pair(z0,z1)) -> c43(MARK(z1)) MARK(s(z0)) -> c41(MARK(z0)) MARK(sel(z0,z1)) -> c34(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c35(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(snd(z0)) -> c28(A__SND(mark(z0)),MARK(z0)) MARK(splitAt(z0,z1)) -> c29(A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) MARK(splitAt(z0,z1)) -> c30(A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) MARK(tail(z0)) -> c33(A__TAIL(mark(z0)),MARK(z0)) MARK(take(z0,z1)) -> c38(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c39(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(u(z0,z1,z2,z3)) -> c31(A__U(mark(z0),z1,z2,z3),MARK(z0)) - Weak TRS: a__afterNth(z0,z1) -> a__snd(a__splitAt(mark(z0),mark(z1))) a__afterNth(z0,z1) -> afterNth(z0,z1) a__fst(z0) -> fst(z0) a__fst(pair(z0,z1)) -> mark(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__natsFrom(z0) -> cons(mark(z0),natsFrom(s(z0))) a__natsFrom(z0) -> natsFrom(z0) a__sel(z0,z1) -> a__head(a__afterNth(mark(z0),mark(z1))) a__sel(z0,z1) -> sel(z0,z1) a__snd(z0) -> snd(z0) a__snd(pair(z0,z1)) -> mark(z1) a__splitAt(z0,z1) -> splitAt(z0,z1) a__splitAt(0(),z0) -> pair(nil(),mark(z0)) a__splitAt(s(z0),cons(z1,z2)) -> a__u(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) a__take(z0,z1) -> a__fst(a__splitAt(mark(z0),mark(z1))) a__take(z0,z1) -> take(z0,z1) a__u(z0,z1,z2,z3) -> u(z0,z1,z2,z3) a__u(pair(z0,z1),z2,z3,z4) -> pair(cons(mark(z3),z0),mark(z1)) mark(0()) -> 0() mark(afterNth(z0,z1)) -> a__afterNth(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(fst(z0)) -> a__fst(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(natsFrom(z0)) -> a__natsFrom(mark(z0)) mark(nil()) -> nil() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(snd(z0)) -> a__snd(mark(z0)) mark(splitAt(z0,z1)) -> a__splitAt(mark(z0),mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(u(z0,z1,z2,z3)) -> a__u(mark(z0),z1,z2,z3) - Signature: {A__AFTERNTH/2,A__FST/1,A__HEAD/1,A__NATSFROM/1,A__SEL/2,A__SND/1,A__SPLITAT/2,A__TAIL/1,A__TAKE/2,A__U/4 ,MARK/1,a__afterNth/2,a__fst/1,a__head/1,a__natsFrom/1,a__sel/2,a__snd/1,a__splitAt/2,a__tail/1,a__take/2 ,a__u/4,mark/1} / {0/0,afterNth/2,c/1,c1/0,c10/1,c11/1,c12/0,c13/1,c14/0,c15/1,c16/0,c17/3,c18/3,c19/0,c2/1 ,c20/3,c21/3,c22/0,c23/3,c24/3,c25/0,c26/2,c27/2,c28/2,c29/2,c3/0,c30/2,c31/2,c32/2,c33/2,c34/2,c35/2,c36/2 ,c37/2,c38/2,c39/2,c4/1,c40/1,c41/1,c42/1,c43/1,c44/0,c45/0,c5/0,c6/1,c7/3,c8/3,c9/0,cons/2,fst/1,head/1 ,natsFrom/1,nil/0,pair/2,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} - Obligation: innermost runtime complexity wrt. defined symbols {A__AFTERNTH,A__FST,A__HEAD,A__NATSFROM,A__SEL,A__SND ,A__SPLITAT,A__TAIL,A__TAKE,A__U,MARK,a__afterNth,a__fst,a__head,a__natsFrom,a__sel,a__snd,a__splitAt ,a__tail,a__take,a__u,mark} and constructors {0,afterNth,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45 ,c5,c6,c7,c8,c9,cons,fst,head,natsFrom,nil,pair,s,sel,snd,splitAt,tail,take,u} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AFTERNTH(z0,z1) -> c23(A__SND(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) A__AFTERNTH(z0,z1) -> c24(A__SND(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) A__AFTERNTH(z0,z1) -> c25() A__FST(z0) -> c3() A__FST(pair(z0,z1)) -> c2(MARK(z0)) A__HEAD(z0) -> c14() A__HEAD(cons(z0,z1)) -> c13(MARK(z0)) A__NATSFROM(z0) -> c(MARK(z0)) A__NATSFROM(z0) -> c1() A__SEL(z0,z1) -> c17(A__HEAD(a__afterNth(mark(z0),mark(z1))),A__AFTERNTH(mark(z0),mark(z1)),MARK(z0)) A__SEL(z0,z1) -> c18(A__HEAD(a__afterNth(mark(z0),mark(z1))),A__AFTERNTH(mark(z0),mark(z1)),MARK(z1)) A__SEL(z0,z1) -> c19() A__SND(z0) -> c5() A__SND(pair(z0,z1)) -> c4(MARK(z1)) A__SPLITAT(z0,z1) -> c9() A__SPLITAT(0(),z0) -> c6(MARK(z0)) A__SPLITAT(s(z0),cons(z1,z2)) -> c7(A__U(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) ,A__SPLITAT(mark(z0),mark(z2)) ,MARK(z0)) A__SPLITAT(s(z0),cons(z1,z2)) -> c8(A__U(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) ,A__SPLITAT(mark(z0),mark(z2)) ,MARK(z2)) A__TAIL(z0) -> c16() A__TAIL(cons(z0,z1)) -> c15(MARK(z1)) A__TAKE(z0,z1) -> c20(A__FST(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) A__TAKE(z0,z1) -> c21(A__FST(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) A__TAKE(z0,z1) -> c22() A__U(z0,z1,z2,z3) -> c12() A__U(pair(z0,z1),z2,z3,z4) -> c10(MARK(z3)) A__U(pair(z0,z1),z2,z3,z4) -> c11(MARK(z1)) MARK(0()) -> c44() MARK(afterNth(z0,z1)) -> c36(A__AFTERNTH(mark(z0),mark(z1)),MARK(z0)) MARK(afterNth(z0,z1)) -> c37(A__AFTERNTH(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c40(MARK(z0)) MARK(fst(z0)) -> c27(A__FST(mark(z0)),MARK(z0)) MARK(head(z0)) -> c32(A__HEAD(mark(z0)),MARK(z0)) MARK(natsFrom(z0)) -> c26(A__NATSFROM(mark(z0)),MARK(z0)) MARK(nil()) -> c45() MARK(pair(z0,z1)) -> c42(MARK(z0)) MARK(pair(z0,z1)) -> c43(MARK(z1)) MARK(s(z0)) -> c41(MARK(z0)) MARK(sel(z0,z1)) -> c34(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c35(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(snd(z0)) -> c28(A__SND(mark(z0)),MARK(z0)) MARK(splitAt(z0,z1)) -> c29(A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) MARK(splitAt(z0,z1)) -> c30(A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) MARK(tail(z0)) -> c33(A__TAIL(mark(z0)),MARK(z0)) MARK(take(z0,z1)) -> c38(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c39(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(u(z0,z1,z2,z3)) -> c31(A__U(mark(z0),z1,z2,z3),MARK(z0)) - Weak TRS: a__afterNth(z0,z1) -> a__snd(a__splitAt(mark(z0),mark(z1))) a__afterNth(z0,z1) -> afterNth(z0,z1) a__fst(z0) -> fst(z0) a__fst(pair(z0,z1)) -> mark(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__natsFrom(z0) -> cons(mark(z0),natsFrom(s(z0))) a__natsFrom(z0) -> natsFrom(z0) a__sel(z0,z1) -> a__head(a__afterNth(mark(z0),mark(z1))) a__sel(z0,z1) -> sel(z0,z1) a__snd(z0) -> snd(z0) a__snd(pair(z0,z1)) -> mark(z1) a__splitAt(z0,z1) -> splitAt(z0,z1) a__splitAt(0(),z0) -> pair(nil(),mark(z0)) a__splitAt(s(z0),cons(z1,z2)) -> a__u(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) a__take(z0,z1) -> a__fst(a__splitAt(mark(z0),mark(z1))) a__take(z0,z1) -> take(z0,z1) a__u(z0,z1,z2,z3) -> u(z0,z1,z2,z3) a__u(pair(z0,z1),z2,z3,z4) -> pair(cons(mark(z3),z0),mark(z1)) mark(0()) -> 0() mark(afterNth(z0,z1)) -> a__afterNth(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(fst(z0)) -> a__fst(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(natsFrom(z0)) -> a__natsFrom(mark(z0)) mark(nil()) -> nil() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(snd(z0)) -> a__snd(mark(z0)) mark(splitAt(z0,z1)) -> a__splitAt(mark(z0),mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(u(z0,z1,z2,z3)) -> a__u(mark(z0),z1,z2,z3) - Signature: {A__AFTERNTH/2,A__FST/1,A__HEAD/1,A__NATSFROM/1,A__SEL/2,A__SND/1,A__SPLITAT/2,A__TAIL/1,A__TAKE/2,A__U/4 ,MARK/1,a__afterNth/2,a__fst/1,a__head/1,a__natsFrom/1,a__sel/2,a__snd/1,a__splitAt/2,a__tail/1,a__take/2 ,a__u/4,mark/1} / {0/0,afterNth/2,c/1,c1/0,c10/1,c11/1,c12/0,c13/1,c14/0,c15/1,c16/0,c17/3,c18/3,c19/0,c2/1 ,c20/3,c21/3,c22/0,c23/3,c24/3,c25/0,c26/2,c27/2,c28/2,c29/2,c3/0,c30/2,c31/2,c32/2,c33/2,c34/2,c35/2,c36/2 ,c37/2,c38/2,c39/2,c4/1,c40/1,c41/1,c42/1,c43/1,c44/0,c45/0,c5/0,c6/1,c7/3,c8/3,c9/0,cons/2,fst/1,head/1 ,natsFrom/1,nil/0,pair/2,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} - Obligation: innermost runtime complexity wrt. defined symbols {A__AFTERNTH,A__FST,A__HEAD,A__NATSFROM,A__SEL,A__SND ,A__SPLITAT,A__TAIL,A__TAKE,A__U,MARK,a__afterNth,a__fst,a__head,a__natsFrom,a__sel,a__snd,a__splitAt ,a__tail,a__take,a__u,mark} and constructors {0,afterNth,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45 ,c5,c6,c7,c8,c9,cons,fst,head,natsFrom,nil,pair,s,sel,snd,splitAt,tail,take,u} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AFTERNTH(z0,z1) -> c23(A__SND(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) A__AFTERNTH(z0,z1) -> c24(A__SND(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) A__AFTERNTH(z0,z1) -> c25() A__FST(z0) -> c3() A__FST(pair(z0,z1)) -> c2(MARK(z0)) A__HEAD(z0) -> c14() A__HEAD(cons(z0,z1)) -> c13(MARK(z0)) A__NATSFROM(z0) -> c(MARK(z0)) A__NATSFROM(z0) -> c1() A__SEL(z0,z1) -> c17(A__HEAD(a__afterNth(mark(z0),mark(z1))),A__AFTERNTH(mark(z0),mark(z1)),MARK(z0)) A__SEL(z0,z1) -> c18(A__HEAD(a__afterNth(mark(z0),mark(z1))),A__AFTERNTH(mark(z0),mark(z1)),MARK(z1)) A__SEL(z0,z1) -> c19() A__SND(z0) -> c5() A__SND(pair(z0,z1)) -> c4(MARK(z1)) A__SPLITAT(z0,z1) -> c9() A__SPLITAT(0(),z0) -> c6(MARK(z0)) A__SPLITAT(s(z0),cons(z1,z2)) -> c7(A__U(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) ,A__SPLITAT(mark(z0),mark(z2)) ,MARK(z0)) A__SPLITAT(s(z0),cons(z1,z2)) -> c8(A__U(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) ,A__SPLITAT(mark(z0),mark(z2)) ,MARK(z2)) A__TAIL(z0) -> c16() A__TAIL(cons(z0,z1)) -> c15(MARK(z1)) A__TAKE(z0,z1) -> c20(A__FST(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) A__TAKE(z0,z1) -> c21(A__FST(a__splitAt(mark(z0),mark(z1))),A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) A__TAKE(z0,z1) -> c22() A__U(z0,z1,z2,z3) -> c12() A__U(pair(z0,z1),z2,z3,z4) -> c10(MARK(z3)) A__U(pair(z0,z1),z2,z3,z4) -> c11(MARK(z1)) MARK(0()) -> c44() MARK(afterNth(z0,z1)) -> c36(A__AFTERNTH(mark(z0),mark(z1)),MARK(z0)) MARK(afterNth(z0,z1)) -> c37(A__AFTERNTH(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c40(MARK(z0)) MARK(fst(z0)) -> c27(A__FST(mark(z0)),MARK(z0)) MARK(head(z0)) -> c32(A__HEAD(mark(z0)),MARK(z0)) MARK(natsFrom(z0)) -> c26(A__NATSFROM(mark(z0)),MARK(z0)) MARK(nil()) -> c45() MARK(pair(z0,z1)) -> c42(MARK(z0)) MARK(pair(z0,z1)) -> c43(MARK(z1)) MARK(s(z0)) -> c41(MARK(z0)) MARK(sel(z0,z1)) -> c34(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c35(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(snd(z0)) -> c28(A__SND(mark(z0)),MARK(z0)) MARK(splitAt(z0,z1)) -> c29(A__SPLITAT(mark(z0),mark(z1)),MARK(z0)) MARK(splitAt(z0,z1)) -> c30(A__SPLITAT(mark(z0),mark(z1)),MARK(z1)) MARK(tail(z0)) -> c33(A__TAIL(mark(z0)),MARK(z0)) MARK(take(z0,z1)) -> c38(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c39(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(u(z0,z1,z2,z3)) -> c31(A__U(mark(z0),z1,z2,z3),MARK(z0)) - Weak TRS: a__afterNth(z0,z1) -> a__snd(a__splitAt(mark(z0),mark(z1))) a__afterNth(z0,z1) -> afterNth(z0,z1) a__fst(z0) -> fst(z0) a__fst(pair(z0,z1)) -> mark(z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> mark(z0) a__natsFrom(z0) -> cons(mark(z0),natsFrom(s(z0))) a__natsFrom(z0) -> natsFrom(z0) a__sel(z0,z1) -> a__head(a__afterNth(mark(z0),mark(z1))) a__sel(z0,z1) -> sel(z0,z1) a__snd(z0) -> snd(z0) a__snd(pair(z0,z1)) -> mark(z1) a__splitAt(z0,z1) -> splitAt(z0,z1) a__splitAt(0(),z0) -> pair(nil(),mark(z0)) a__splitAt(s(z0),cons(z1,z2)) -> a__u(a__splitAt(mark(z0),mark(z2)),z0,z1,z2) a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) a__take(z0,z1) -> a__fst(a__splitAt(mark(z0),mark(z1))) a__take(z0,z1) -> take(z0,z1) a__u(z0,z1,z2,z3) -> u(z0,z1,z2,z3) a__u(pair(z0,z1),z2,z3,z4) -> pair(cons(mark(z3),z0),mark(z1)) mark(0()) -> 0() mark(afterNth(z0,z1)) -> a__afterNth(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(fst(z0)) -> a__fst(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(natsFrom(z0)) -> a__natsFrom(mark(z0)) mark(nil()) -> nil() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(snd(z0)) -> a__snd(mark(z0)) mark(splitAt(z0,z1)) -> a__splitAt(mark(z0),mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(u(z0,z1,z2,z3)) -> a__u(mark(z0),z1,z2,z3) - Signature: {A__AFTERNTH/2,A__FST/1,A__HEAD/1,A__NATSFROM/1,A__SEL/2,A__SND/1,A__SPLITAT/2,A__TAIL/1,A__TAKE/2,A__U/4 ,MARK/1,a__afterNth/2,a__fst/1,a__head/1,a__natsFrom/1,a__sel/2,a__snd/1,a__splitAt/2,a__tail/1,a__take/2 ,a__u/4,mark/1} / {0/0,afterNth/2,c/1,c1/0,c10/1,c11/1,c12/0,c13/1,c14/0,c15/1,c16/0,c17/3,c18/3,c19/0,c2/1 ,c20/3,c21/3,c22/0,c23/3,c24/3,c25/0,c26/2,c27/2,c28/2,c29/2,c3/0,c30/2,c31/2,c32/2,c33/2,c34/2,c35/2,c36/2 ,c37/2,c38/2,c39/2,c4/1,c40/1,c41/1,c42/1,c43/1,c44/0,c45/0,c5/0,c6/1,c7/3,c8/3,c9/0,cons/2,fst/1,head/1 ,natsFrom/1,nil/0,pair/2,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} - Obligation: innermost runtime complexity wrt. defined symbols {A__AFTERNTH,A__FST,A__HEAD,A__NATSFROM,A__SEL,A__SND ,A__SPLITAT,A__TAIL,A__TAKE,A__U,MARK,a__afterNth,a__fst,a__head,a__natsFrom,a__sel,a__snd,a__splitAt ,a__tail,a__take,a__u,mark} and constructors {0,afterNth,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45 ,c5,c6,c7,c8,c9,cons,fst,head,natsFrom,nil,pair,s,sel,snd,splitAt,tail,take,u} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> afterNth(x,y)} = MARK(afterNth(x,y)) ->^+ c36(A__AFTERNTH(mark(x),mark(y)),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)