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