WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FIRST(z0,z1) -> c4() A__FIRST(0(),z0) -> c2() A__FIRST(s(z0),cons(z1,z2)) -> c3(MARK(z1)) A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__SEL(z0,z1) -> c8() A__SEL(0(),cons(z0,z1)) -> c5(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c6(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c7(A__SEL(mark(z0),mark(z2)),MARK(z2)) MARK(0()) -> c16() MARK(cons(z0,z1)) -> c14(MARK(z0)) MARK(first(z0,z1)) -> c10(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c11(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c9(A__FROM(mark(z0)),MARK(z0)) MARK(nil()) -> c17() MARK(s(z0)) -> c15(MARK(z0)) MARK(sel(z0,z1)) -> c12(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c13(A__SEL(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(mark(z1),first(z0,z2)) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(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)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) - Signature: {A__FIRST/2,A__FROM/1,A__SEL/2,MARK/1,a__first/2,a__from/1,a__sel/2,mark/1} / {0/0,c/1,c1/0,c10/2,c11/2 ,c12/2,c13/2,c14/1,c15/1,c16/0,c17/0,c2/0,c3/1,c4/0,c5/1,c6/2,c7/2,c8/0,c9/2,cons/2,first/2,from/1,nil/0,s/1 ,sel/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__FIRST,A__FROM,A__SEL,MARK,a__first,a__from,a__sel ,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,cons,first,from,nil ,s,sel} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FIRST(z0,z1) -> c4() A__FIRST(0(),z0) -> c2() A__FIRST(s(z0),cons(z1,z2)) -> c3(MARK(z1)) A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__SEL(z0,z1) -> c8() A__SEL(0(),cons(z0,z1)) -> c5(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c6(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c7(A__SEL(mark(z0),mark(z2)),MARK(z2)) MARK(0()) -> c16() MARK(cons(z0,z1)) -> c14(MARK(z0)) MARK(first(z0,z1)) -> c10(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c11(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c9(A__FROM(mark(z0)),MARK(z0)) MARK(nil()) -> c17() MARK(s(z0)) -> c15(MARK(z0)) MARK(sel(z0,z1)) -> c12(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c13(A__SEL(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(mark(z1),first(z0,z2)) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(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)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) - Signature: {A__FIRST/2,A__FROM/1,A__SEL/2,MARK/1,a__first/2,a__from/1,a__sel/2,mark/1} / {0/0,c/1,c1/0,c10/2,c11/2 ,c12/2,c13/2,c14/1,c15/1,c16/0,c17/0,c2/0,c3/1,c4/0,c5/1,c6/2,c7/2,c8/0,c9/2,cons/2,first/2,from/1,nil/0,s/1 ,sel/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__FIRST,A__FROM,A__SEL,MARK,a__first,a__from,a__sel ,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,cons,first,from,nil ,s,sel} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FIRST(z0,z1) -> c4() A__FIRST(0(),z0) -> c2() A__FIRST(s(z0),cons(z1,z2)) -> c3(MARK(z1)) A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__SEL(z0,z1) -> c8() A__SEL(0(),cons(z0,z1)) -> c5(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c6(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c7(A__SEL(mark(z0),mark(z2)),MARK(z2)) MARK(0()) -> c16() MARK(cons(z0,z1)) -> c14(MARK(z0)) MARK(first(z0,z1)) -> c10(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c11(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(from(z0)) -> c9(A__FROM(mark(z0)),MARK(z0)) MARK(nil()) -> c17() MARK(s(z0)) -> c15(MARK(z0)) MARK(sel(z0,z1)) -> c12(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c13(A__SEL(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__first(z0,z1) -> first(z0,z1) a__first(0(),z0) -> nil() a__first(s(z0),cons(z1,z2)) -> cons(mark(z1),first(z0,z2)) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(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)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(from(z0)) -> a__from(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) - Signature: {A__FIRST/2,A__FROM/1,A__SEL/2,MARK/1,a__first/2,a__from/1,a__sel/2,mark/1} / {0/0,c/1,c1/0,c10/2,c11/2 ,c12/2,c13/2,c14/1,c15/1,c16/0,c17/0,c2/0,c3/1,c4/0,c5/1,c6/2,c7/2,c8/0,c9/2,cons/2,first/2,from/1,nil/0,s/1 ,sel/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__FIRST,A__FROM,A__SEL,MARK,a__first,a__from,a__sel ,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,cons,first,from,nil ,s,sel} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> cons(x,y)} = MARK(cons(x,y)) ->^+ c14(MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)