WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c10() A__ADD(0(),z0) -> c8(MARK(z0)) A__ADD(s(z0),z1) -> c9() A__DBL(z0) -> c7() A__DBL(0()) -> c5() A__DBL(s(z0)) -> c6() A__FIRST(z0,z1) -> c13() A__FIRST(0(),z0) -> c11() A__FIRST(s(z0),cons(z1,z2)) -> c12(MARK(z1)) A__SQR(z0) -> c4() A__SQR(0()) -> c2() A__SQR(s(z0)) -> c3() A__TERMS(z0) -> c(A__SQR(mark(z0)),MARK(z0)) A__TERMS(z0) -> c1() MARK(0()) -> c24() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c17(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c21(MARK(z0)) MARK(dbl(z0)) -> c18(A__DBL(mark(z0)),MARK(z0)) MARK(first(z0,z1)) -> c19(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c20(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(nil()) -> c25() MARK(recip(z0)) -> c22(MARK(z0)) MARK(s(z0)) -> c23() MARK(sqr(z0)) -> c15(A__SQR(mark(z0)),MARK(z0)) MARK(terms(z0)) -> c14(A__TERMS(mark(z0)),MARK(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(dbl(z0))) 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__sqr(z0) -> sqr(z0) a__sqr(0()) -> 0() a__sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) a__terms(z0) -> cons(recip(a__sqr(mark(z0))),terms(s(z0))) a__terms(z0) -> terms(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(dbl(z0)) -> a__dbl(mark(z0)) mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(nil()) -> nil() mark(recip(z0)) -> recip(mark(z0)) mark(s(z0)) -> s(z0) mark(sqr(z0)) -> a__sqr(mark(z0)) mark(terms(z0)) -> a__terms(mark(z0)) - Signature: {A__ADD/2,A__DBL/1,A__FIRST/2,A__SQR/1,A__TERMS/1,MARK/1,a__add/2,a__dbl/1,a__first/2,a__sqr/1,a__terms/1 ,mark/1} / {0/0,add/2,c/2,c1/0,c10/0,c11/0,c12/1,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/0,c20/2,c21/1 ,c22/1,c23/0,c24/0,c25/0,c3/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,cons/2,dbl/1,first/2,nil/0,recip/1,s/1,sqr/1 ,terms/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__DBL,A__FIRST,A__SQR,A__TERMS,MARK,a__add,a__dbl ,a__first,a__sqr,a__terms,mark} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,dbl,first,nil,recip,s,sqr,terms} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c10() A__ADD(0(),z0) -> c8(MARK(z0)) A__ADD(s(z0),z1) -> c9() A__DBL(z0) -> c7() A__DBL(0()) -> c5() A__DBL(s(z0)) -> c6() A__FIRST(z0,z1) -> c13() A__FIRST(0(),z0) -> c11() A__FIRST(s(z0),cons(z1,z2)) -> c12(MARK(z1)) A__SQR(z0) -> c4() A__SQR(0()) -> c2() A__SQR(s(z0)) -> c3() A__TERMS(z0) -> c(A__SQR(mark(z0)),MARK(z0)) A__TERMS(z0) -> c1() MARK(0()) -> c24() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c17(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c21(MARK(z0)) MARK(dbl(z0)) -> c18(A__DBL(mark(z0)),MARK(z0)) MARK(first(z0,z1)) -> c19(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c20(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(nil()) -> c25() MARK(recip(z0)) -> c22(MARK(z0)) MARK(s(z0)) -> c23() MARK(sqr(z0)) -> c15(A__SQR(mark(z0)),MARK(z0)) MARK(terms(z0)) -> c14(A__TERMS(mark(z0)),MARK(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(dbl(z0))) 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__sqr(z0) -> sqr(z0) a__sqr(0()) -> 0() a__sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) a__terms(z0) -> cons(recip(a__sqr(mark(z0))),terms(s(z0))) a__terms(z0) -> terms(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(dbl(z0)) -> a__dbl(mark(z0)) mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(nil()) -> nil() mark(recip(z0)) -> recip(mark(z0)) mark(s(z0)) -> s(z0) mark(sqr(z0)) -> a__sqr(mark(z0)) mark(terms(z0)) -> a__terms(mark(z0)) - Signature: {A__ADD/2,A__DBL/1,A__FIRST/2,A__SQR/1,A__TERMS/1,MARK/1,a__add/2,a__dbl/1,a__first/2,a__sqr/1,a__terms/1 ,mark/1} / {0/0,add/2,c/2,c1/0,c10/0,c11/0,c12/1,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/0,c20/2,c21/1 ,c22/1,c23/0,c24/0,c25/0,c3/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,cons/2,dbl/1,first/2,nil/0,recip/1,s/1,sqr/1 ,terms/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__DBL,A__FIRST,A__SQR,A__TERMS,MARK,a__add,a__dbl ,a__first,a__sqr,a__terms,mark} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,dbl,first,nil,recip,s,sqr,terms} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c10() A__ADD(0(),z0) -> c8(MARK(z0)) A__ADD(s(z0),z1) -> c9() A__DBL(z0) -> c7() A__DBL(0()) -> c5() A__DBL(s(z0)) -> c6() A__FIRST(z0,z1) -> c13() A__FIRST(0(),z0) -> c11() A__FIRST(s(z0),cons(z1,z2)) -> c12(MARK(z1)) A__SQR(z0) -> c4() A__SQR(0()) -> c2() A__SQR(s(z0)) -> c3() A__TERMS(z0) -> c(A__SQR(mark(z0)),MARK(z0)) A__TERMS(z0) -> c1() MARK(0()) -> c24() MARK(add(z0,z1)) -> c16(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c17(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c21(MARK(z0)) MARK(dbl(z0)) -> c18(A__DBL(mark(z0)),MARK(z0)) MARK(first(z0,z1)) -> c19(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c20(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(nil()) -> c25() MARK(recip(z0)) -> c22(MARK(z0)) MARK(s(z0)) -> c23() MARK(sqr(z0)) -> c15(A__SQR(mark(z0)),MARK(z0)) MARK(terms(z0)) -> c14(A__TERMS(mark(z0)),MARK(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(add(z0,z1)) a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(dbl(z0))) 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__sqr(z0) -> sqr(z0) a__sqr(0()) -> 0() a__sqr(s(z0)) -> s(add(sqr(z0),dbl(z0))) a__terms(z0) -> cons(recip(a__sqr(mark(z0))),terms(s(z0))) a__terms(z0) -> terms(z0) mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(dbl(z0)) -> a__dbl(mark(z0)) mark(first(z0,z1)) -> a__first(mark(z0),mark(z1)) mark(nil()) -> nil() mark(recip(z0)) -> recip(mark(z0)) mark(s(z0)) -> s(z0) mark(sqr(z0)) -> a__sqr(mark(z0)) mark(terms(z0)) -> a__terms(mark(z0)) - Signature: {A__ADD/2,A__DBL/1,A__FIRST/2,A__SQR/1,A__TERMS/1,MARK/1,a__add/2,a__dbl/1,a__first/2,a__sqr/1,a__terms/1 ,mark/1} / {0/0,add/2,c/2,c1/0,c10/0,c11/0,c12/1,c13/0,c14/2,c15/2,c16/2,c17/2,c18/2,c19/2,c2/0,c20/2,c21/1 ,c22/1,c23/0,c24/0,c25/0,c3/0,c4/0,c5/0,c6/0,c7/0,c8/1,c9/0,cons/2,dbl/1,first/2,nil/0,recip/1,s/1,sqr/1 ,terms/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__DBL,A__FIRST,A__SQR,A__TERMS,MARK,a__add,a__dbl ,a__first,a__sqr,a__terms,mark} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20 ,c21,c22,c23,c24,c25,c3,c4,c5,c6,c7,c8,c9,cons,dbl,first,nil,recip,s,sqr,terms} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> add(x,y)} = MARK(add(x,y)) ->^+ c16(A__ADD(mark(x),mark(y)),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)