WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__DBL(z0) -> c2() A__DBL(0()) -> c() A__DBL(s(z0)) -> c1() A__DBL1(z0) -> c17() A__DBL1(0()) -> c15() A__DBL1(s(z0)) -> c16(A__DBL1(mark(z0)),MARK(z0)) A__DBLS(z0) -> c5() A__DBLS(cons(z0,z1)) -> c4() A__DBLS(nil()) -> c3() A__FROM(z0) -> c13() A__FROM(z0) -> c14() A__INDX(z0,z1) -> c12() A__INDX(cons(z0,z1),z2) -> c11() A__INDX(nil(),z0) -> c10() A__QUOTE(z0) -> c27() A__QUOTE(0()) -> c22() A__QUOTE(dbl(z0)) -> c24(A__DBL1(mark(z0)),MARK(z0)) A__QUOTE(s(z0)) -> c23(A__QUOTE(mark(z0)),MARK(z0)) A__QUOTE(sel(z0,z1)) -> c25(A__SEL1(mark(z0),mark(z1)),MARK(z0)) A__QUOTE(sel(z0,z1)) -> c26(A__SEL1(mark(z0),mark(z1)),MARK(z1)) A__SEL(z0,z1) -> c9() A__SEL(0(),cons(z0,z1)) -> c6(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c7(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c8(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__SEL1(z0,z1) -> c21() A__SEL1(0(),cons(z0,z1)) -> c18(MARK(z0)) A__SEL1(s(z0),cons(z1,z2)) -> c19(A__SEL1(mark(z0),mark(z2)),MARK(z0)) A__SEL1(s(z0),cons(z1,z2)) -> c20(A__SEL1(mark(z0),mark(z2)),MARK(z2)) MARK(0()) -> c38() MARK(01()) -> c42() MARK(cons(z0,z1)) -> c41() MARK(dbl(z0)) -> c28(A__DBL(mark(z0)),MARK(z0)) MARK(dbl1(z0)) -> c34(A__DBL1(mark(z0)),MARK(z0)) MARK(dbls(z0)) -> c29(A__DBLS(mark(z0)),MARK(z0)) MARK(from(z0)) -> c33(A__FROM(z0)) MARK(indx(z0,z1)) -> c32(A__INDX(mark(z0),z1),MARK(z0)) MARK(nil()) -> c40() MARK(quote(z0)) -> c37(A__QUOTE(mark(z0)),MARK(z0)) MARK(s(z0)) -> c39() MARK(s1(z0)) -> c43(MARK(z0)) MARK(sel(z0,z1)) -> c30(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c31(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(sel1(z0,z1)) -> c35(A__SEL1(mark(z0),mark(z1)),MARK(z0)) MARK(sel1(z0,z1)) -> c36(A__SEL1(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(dbl(z0))) a__dbl1(z0) -> dbl1(z0) a__dbl1(0()) -> 01() a__dbl1(s(z0)) -> s1(s1(a__dbl1(mark(z0)))) a__dbls(z0) -> dbls(z0) a__dbls(cons(z0,z1)) -> cons(dbl(z0),dbls(z1)) a__dbls(nil()) -> nil() a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__indx(z0,z1) -> indx(z0,z1) a__indx(cons(z0,z1),z2) -> cons(sel(z0,z2),indx(z1,z2)) a__indx(nil(),z0) -> nil() a__quote(z0) -> quote(z0) a__quote(0()) -> 01() a__quote(dbl(z0)) -> a__dbl1(mark(z0)) a__quote(s(z0)) -> s1(a__quote(mark(z0))) a__quote(sel(z0,z1)) -> a__sel1(mark(z0),mark(z1)) 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__sel1(z0,z1) -> sel1(z0,z1) a__sel1(0(),cons(z0,z1)) -> mark(z0) a__sel1(s(z0),cons(z1,z2)) -> a__sel1(mark(z0),mark(z2)) mark(0()) -> 0() mark(01()) -> 01() mark(cons(z0,z1)) -> cons(z0,z1) mark(dbl(z0)) -> a__dbl(mark(z0)) mark(dbl1(z0)) -> a__dbl1(mark(z0)) mark(dbls(z0)) -> a__dbls(mark(z0)) mark(from(z0)) -> a__from(z0) mark(indx(z0,z1)) -> a__indx(mark(z0),z1) mark(nil()) -> nil() mark(quote(z0)) -> a__quote(mark(z0)) mark(s(z0)) -> s(z0) mark(s1(z0)) -> s1(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(sel1(z0,z1)) -> a__sel1(mark(z0),mark(z1)) - Signature: {A__DBL/1,A__DBL1/1,A__DBLS/1,A__FROM/1,A__INDX/2,A__QUOTE/1,A__SEL/2,A__SEL1/2,MARK/1,a__dbl/1,a__dbl1/1 ,a__dbls/1,a__from/1,a__indx/2,a__quote/1,a__sel/2,a__sel1/2,mark/1} / {0/0,01/0,c/0,c1/0,c10/0,c11/0,c12/0 ,c13/0,c14/0,c15/0,c16/2,c17/0,c18/1,c19/2,c2/0,c20/2,c21/0,c22/0,c23/2,c24/2,c25/2,c26/2,c27/0,c28/2,c29/2 ,c3/0,c30/2,c31/2,c32/2,c33/1,c34/2,c35/2,c36/2,c37/2,c38/0,c39/0,c4/0,c40/0,c41/0,c42/0,c43/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,cons/2,dbl/1,dbl1/1,dbls/1,from/1,indx/2,nil/0,quote/1,s/1,s1/1,sel/2,sel1/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__DBL,A__DBL1,A__DBLS,A__FROM,A__INDX,A__QUOTE,A__SEL ,A__SEL1,MARK,a__dbl,a__dbl1,a__dbls,a__from,a__indx,a__quote,a__sel,a__sel1,mark} and constructors {0,01,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,c5,c6,c7,c8,c9,cons,dbl,dbl1,dbls,from,indx,nil,quote,s,s1,sel ,sel1} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__DBL(z0) -> c2() A__DBL(0()) -> c() A__DBL(s(z0)) -> c1() A__DBL1(z0) -> c17() A__DBL1(0()) -> c15() A__DBL1(s(z0)) -> c16(A__DBL1(mark(z0)),MARK(z0)) A__DBLS(z0) -> c5() A__DBLS(cons(z0,z1)) -> c4() A__DBLS(nil()) -> c3() A__FROM(z0) -> c13() A__FROM(z0) -> c14() A__INDX(z0,z1) -> c12() A__INDX(cons(z0,z1),z2) -> c11() A__INDX(nil(),z0) -> c10() A__QUOTE(z0) -> c27() A__QUOTE(0()) -> c22() A__QUOTE(dbl(z0)) -> c24(A__DBL1(mark(z0)),MARK(z0)) A__QUOTE(s(z0)) -> c23(A__QUOTE(mark(z0)),MARK(z0)) A__QUOTE(sel(z0,z1)) -> c25(A__SEL1(mark(z0),mark(z1)),MARK(z0)) A__QUOTE(sel(z0,z1)) -> c26(A__SEL1(mark(z0),mark(z1)),MARK(z1)) A__SEL(z0,z1) -> c9() A__SEL(0(),cons(z0,z1)) -> c6(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c7(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c8(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__SEL1(z0,z1) -> c21() A__SEL1(0(),cons(z0,z1)) -> c18(MARK(z0)) A__SEL1(s(z0),cons(z1,z2)) -> c19(A__SEL1(mark(z0),mark(z2)),MARK(z0)) A__SEL1(s(z0),cons(z1,z2)) -> c20(A__SEL1(mark(z0),mark(z2)),MARK(z2)) MARK(0()) -> c38() MARK(01()) -> c42() MARK(cons(z0,z1)) -> c41() MARK(dbl(z0)) -> c28(A__DBL(mark(z0)),MARK(z0)) MARK(dbl1(z0)) -> c34(A__DBL1(mark(z0)),MARK(z0)) MARK(dbls(z0)) -> c29(A__DBLS(mark(z0)),MARK(z0)) MARK(from(z0)) -> c33(A__FROM(z0)) MARK(indx(z0,z1)) -> c32(A__INDX(mark(z0),z1),MARK(z0)) MARK(nil()) -> c40() MARK(quote(z0)) -> c37(A__QUOTE(mark(z0)),MARK(z0)) MARK(s(z0)) -> c39() MARK(s1(z0)) -> c43(MARK(z0)) MARK(sel(z0,z1)) -> c30(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c31(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(sel1(z0,z1)) -> c35(A__SEL1(mark(z0),mark(z1)),MARK(z0)) MARK(sel1(z0,z1)) -> c36(A__SEL1(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(dbl(z0))) a__dbl1(z0) -> dbl1(z0) a__dbl1(0()) -> 01() a__dbl1(s(z0)) -> s1(s1(a__dbl1(mark(z0)))) a__dbls(z0) -> dbls(z0) a__dbls(cons(z0,z1)) -> cons(dbl(z0),dbls(z1)) a__dbls(nil()) -> nil() a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__indx(z0,z1) -> indx(z0,z1) a__indx(cons(z0,z1),z2) -> cons(sel(z0,z2),indx(z1,z2)) a__indx(nil(),z0) -> nil() a__quote(z0) -> quote(z0) a__quote(0()) -> 01() a__quote(dbl(z0)) -> a__dbl1(mark(z0)) a__quote(s(z0)) -> s1(a__quote(mark(z0))) a__quote(sel(z0,z1)) -> a__sel1(mark(z0),mark(z1)) 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__sel1(z0,z1) -> sel1(z0,z1) a__sel1(0(),cons(z0,z1)) -> mark(z0) a__sel1(s(z0),cons(z1,z2)) -> a__sel1(mark(z0),mark(z2)) mark(0()) -> 0() mark(01()) -> 01() mark(cons(z0,z1)) -> cons(z0,z1) mark(dbl(z0)) -> a__dbl(mark(z0)) mark(dbl1(z0)) -> a__dbl1(mark(z0)) mark(dbls(z0)) -> a__dbls(mark(z0)) mark(from(z0)) -> a__from(z0) mark(indx(z0,z1)) -> a__indx(mark(z0),z1) mark(nil()) -> nil() mark(quote(z0)) -> a__quote(mark(z0)) mark(s(z0)) -> s(z0) mark(s1(z0)) -> s1(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(sel1(z0,z1)) -> a__sel1(mark(z0),mark(z1)) - Signature: {A__DBL/1,A__DBL1/1,A__DBLS/1,A__FROM/1,A__INDX/2,A__QUOTE/1,A__SEL/2,A__SEL1/2,MARK/1,a__dbl/1,a__dbl1/1 ,a__dbls/1,a__from/1,a__indx/2,a__quote/1,a__sel/2,a__sel1/2,mark/1} / {0/0,01/0,c/0,c1/0,c10/0,c11/0,c12/0 ,c13/0,c14/0,c15/0,c16/2,c17/0,c18/1,c19/2,c2/0,c20/2,c21/0,c22/0,c23/2,c24/2,c25/2,c26/2,c27/0,c28/2,c29/2 ,c3/0,c30/2,c31/2,c32/2,c33/1,c34/2,c35/2,c36/2,c37/2,c38/0,c39/0,c4/0,c40/0,c41/0,c42/0,c43/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,cons/2,dbl/1,dbl1/1,dbls/1,from/1,indx/2,nil/0,quote/1,s/1,s1/1,sel/2,sel1/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__DBL,A__DBL1,A__DBLS,A__FROM,A__INDX,A__QUOTE,A__SEL ,A__SEL1,MARK,a__dbl,a__dbl1,a__dbls,a__from,a__indx,a__quote,a__sel,a__sel1,mark} and constructors {0,01,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,c5,c6,c7,c8,c9,cons,dbl,dbl1,dbls,from,indx,nil,quote,s,s1,sel ,sel1} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__DBL(z0) -> c2() A__DBL(0()) -> c() A__DBL(s(z0)) -> c1() A__DBL1(z0) -> c17() A__DBL1(0()) -> c15() A__DBL1(s(z0)) -> c16(A__DBL1(mark(z0)),MARK(z0)) A__DBLS(z0) -> c5() A__DBLS(cons(z0,z1)) -> c4() A__DBLS(nil()) -> c3() A__FROM(z0) -> c13() A__FROM(z0) -> c14() A__INDX(z0,z1) -> c12() A__INDX(cons(z0,z1),z2) -> c11() A__INDX(nil(),z0) -> c10() A__QUOTE(z0) -> c27() A__QUOTE(0()) -> c22() A__QUOTE(dbl(z0)) -> c24(A__DBL1(mark(z0)),MARK(z0)) A__QUOTE(s(z0)) -> c23(A__QUOTE(mark(z0)),MARK(z0)) A__QUOTE(sel(z0,z1)) -> c25(A__SEL1(mark(z0),mark(z1)),MARK(z0)) A__QUOTE(sel(z0,z1)) -> c26(A__SEL1(mark(z0),mark(z1)),MARK(z1)) A__SEL(z0,z1) -> c9() A__SEL(0(),cons(z0,z1)) -> c6(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c7(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c8(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__SEL1(z0,z1) -> c21() A__SEL1(0(),cons(z0,z1)) -> c18(MARK(z0)) A__SEL1(s(z0),cons(z1,z2)) -> c19(A__SEL1(mark(z0),mark(z2)),MARK(z0)) A__SEL1(s(z0),cons(z1,z2)) -> c20(A__SEL1(mark(z0),mark(z2)),MARK(z2)) MARK(0()) -> c38() MARK(01()) -> c42() MARK(cons(z0,z1)) -> c41() MARK(dbl(z0)) -> c28(A__DBL(mark(z0)),MARK(z0)) MARK(dbl1(z0)) -> c34(A__DBL1(mark(z0)),MARK(z0)) MARK(dbls(z0)) -> c29(A__DBLS(mark(z0)),MARK(z0)) MARK(from(z0)) -> c33(A__FROM(z0)) MARK(indx(z0,z1)) -> c32(A__INDX(mark(z0),z1),MARK(z0)) MARK(nil()) -> c40() MARK(quote(z0)) -> c37(A__QUOTE(mark(z0)),MARK(z0)) MARK(s(z0)) -> c39() MARK(s1(z0)) -> c43(MARK(z0)) MARK(sel(z0,z1)) -> c30(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c31(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(sel1(z0,z1)) -> c35(A__SEL1(mark(z0),mark(z1)),MARK(z0)) MARK(sel1(z0,z1)) -> c36(A__SEL1(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(dbl(z0))) a__dbl1(z0) -> dbl1(z0) a__dbl1(0()) -> 01() a__dbl1(s(z0)) -> s1(s1(a__dbl1(mark(z0)))) a__dbls(z0) -> dbls(z0) a__dbls(cons(z0,z1)) -> cons(dbl(z0),dbls(z1)) a__dbls(nil()) -> nil() a__from(z0) -> cons(z0,from(s(z0))) a__from(z0) -> from(z0) a__indx(z0,z1) -> indx(z0,z1) a__indx(cons(z0,z1),z2) -> cons(sel(z0,z2),indx(z1,z2)) a__indx(nil(),z0) -> nil() a__quote(z0) -> quote(z0) a__quote(0()) -> 01() a__quote(dbl(z0)) -> a__dbl1(mark(z0)) a__quote(s(z0)) -> s1(a__quote(mark(z0))) a__quote(sel(z0,z1)) -> a__sel1(mark(z0),mark(z1)) 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__sel1(z0,z1) -> sel1(z0,z1) a__sel1(0(),cons(z0,z1)) -> mark(z0) a__sel1(s(z0),cons(z1,z2)) -> a__sel1(mark(z0),mark(z2)) mark(0()) -> 0() mark(01()) -> 01() mark(cons(z0,z1)) -> cons(z0,z1) mark(dbl(z0)) -> a__dbl(mark(z0)) mark(dbl1(z0)) -> a__dbl1(mark(z0)) mark(dbls(z0)) -> a__dbls(mark(z0)) mark(from(z0)) -> a__from(z0) mark(indx(z0,z1)) -> a__indx(mark(z0),z1) mark(nil()) -> nil() mark(quote(z0)) -> a__quote(mark(z0)) mark(s(z0)) -> s(z0) mark(s1(z0)) -> s1(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(sel1(z0,z1)) -> a__sel1(mark(z0),mark(z1)) - Signature: {A__DBL/1,A__DBL1/1,A__DBLS/1,A__FROM/1,A__INDX/2,A__QUOTE/1,A__SEL/2,A__SEL1/2,MARK/1,a__dbl/1,a__dbl1/1 ,a__dbls/1,a__from/1,a__indx/2,a__quote/1,a__sel/2,a__sel1/2,mark/1} / {0/0,01/0,c/0,c1/0,c10/0,c11/0,c12/0 ,c13/0,c14/0,c15/0,c16/2,c17/0,c18/1,c19/2,c2/0,c20/2,c21/0,c22/0,c23/2,c24/2,c25/2,c26/2,c27/0,c28/2,c29/2 ,c3/0,c30/2,c31/2,c32/2,c33/1,c34/2,c35/2,c36/2,c37/2,c38/0,c39/0,c4/0,c40/0,c41/0,c42/0,c43/1,c5/0,c6/1 ,c7/2,c8/2,c9/0,cons/2,dbl/1,dbl1/1,dbls/1,from/1,indx/2,nil/0,quote/1,s/1,s1/1,sel/2,sel1/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__DBL,A__DBL1,A__DBLS,A__FROM,A__INDX,A__QUOTE,A__SEL ,A__SEL1,MARK,a__dbl,a__dbl1,a__dbls,a__from,a__indx,a__quote,a__sel,a__sel1,mark} and constructors {0,01,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,c5,c6,c7,c8,c9,cons,dbl,dbl1,dbls,from,indx,nil,quote,s,s1,sel ,sel1} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> dbl(x)} = MARK(dbl(x)) ->^+ c28(A__DBL(mark(x)),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)