WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c12() A__ADD(0(),z0) -> c9(MARK(z0)) A__ADD(s(z0),z1) -> c10(A__ADD(mark(z0),mark(z1)),MARK(z0)) A__ADD(s(z0),z1) -> c11(A__ADD(mark(z0),mark(z1)),MARK(z1)) A__DBL(z0) -> c8() A__DBL(0()) -> c6() A__DBL(s(z0)) -> c7(A__DBL(mark(z0)),MARK(z0)) A__FIRST(z0,z1) -> c15() A__FIRST(0(),z0) -> c13() A__FIRST(s(z0),cons(z1,z2)) -> c14(MARK(z1)) A__HALF(z0) -> c20() A__HALF(0()) -> c16() A__HALF(dbl(z0)) -> c19(MARK(z0)) A__HALF(s(0())) -> c17() A__HALF(s(s(z0))) -> c18(A__HALF(mark(z0)),MARK(z0)) A__SQR(z0) -> c5() A__SQR(0()) -> c2() A__SQR(s(z0)) -> c3(A__ADD(a__sqr(mark(z0)),a__dbl(mark(z0))),A__SQR(mark(z0)),MARK(z0)) A__SQR(s(z0)) -> c4(A__ADD(a__sqr(mark(z0)),a__dbl(mark(z0))),A__DBL(mark(z0)),MARK(z0)) A__TERMS(z0) -> c(A__SQR(mark(z0)),MARK(z0)) A__TERMS(z0) -> c1() MARK(0()) -> c32() MARK(add(z0,z1)) -> c23(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c24(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c29(MARK(z0)) MARK(dbl(z0)) -> c25(A__DBL(mark(z0)),MARK(z0)) MARK(first(z0,z1)) -> c26(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c27(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(half(z0)) -> c28(A__HALF(mark(z0)),MARK(z0)) MARK(nil()) -> c33() MARK(recip(z0)) -> c30(MARK(z0)) MARK(s(z0)) -> c31(MARK(z0)) MARK(sqr(z0)) -> c22(A__SQR(mark(z0)),MARK(z0)) MARK(terms(z0)) -> c21(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(a__add(mark(z0),mark(z1))) a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(a__dbl(mark(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__half(z0) -> half(z0) a__half(0()) -> 0() a__half(dbl(z0)) -> mark(z0) a__half(s(0())) -> 0() a__half(s(s(z0))) -> s(a__half(mark(z0))) a__sqr(z0) -> sqr(z0) a__sqr(0()) -> 0() a__sqr(s(z0)) -> s(a__add(a__sqr(mark(z0)),a__dbl(mark(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(half(z0)) -> a__half(mark(z0)) mark(nil()) -> nil() mark(recip(z0)) -> recip(mark(z0)) mark(s(z0)) -> s(mark(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__HALF/1,A__SQR/1,A__TERMS/1,MARK/1,a__add/2,a__dbl/1,a__first/2,a__half/1 ,a__sqr/1,a__terms/1,mark/1} / {0/0,add/2,c/2,c1/0,c10/2,c11/2,c12/0,c13/0,c14/1,c15/0,c16/0,c17/0,c18/2 ,c19/1,c2/0,c20/0,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/2,c29/1,c3/3,c30/1,c31/1,c32/0,c33/0,c4/3 ,c5/0,c6/0,c7/2,c8/0,c9/1,cons/2,dbl/1,first/2,half/1,nil/0,recip/1,s/1,sqr/1,terms/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__DBL,A__FIRST,A__HALF,A__SQR,A__TERMS,MARK ,a__add,a__dbl,a__first,a__half,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,c26,c27,c28,c29,c3,c30,c31,c32,c33,c4,c5,c6,c7,c8,c9,cons,dbl ,first,half,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) -> c12() A__ADD(0(),z0) -> c9(MARK(z0)) A__ADD(s(z0),z1) -> c10(A__ADD(mark(z0),mark(z1)),MARK(z0)) A__ADD(s(z0),z1) -> c11(A__ADD(mark(z0),mark(z1)),MARK(z1)) A__DBL(z0) -> c8() A__DBL(0()) -> c6() A__DBL(s(z0)) -> c7(A__DBL(mark(z0)),MARK(z0)) A__FIRST(z0,z1) -> c15() A__FIRST(0(),z0) -> c13() A__FIRST(s(z0),cons(z1,z2)) -> c14(MARK(z1)) A__HALF(z0) -> c20() A__HALF(0()) -> c16() A__HALF(dbl(z0)) -> c19(MARK(z0)) A__HALF(s(0())) -> c17() A__HALF(s(s(z0))) -> c18(A__HALF(mark(z0)),MARK(z0)) A__SQR(z0) -> c5() A__SQR(0()) -> c2() A__SQR(s(z0)) -> c3(A__ADD(a__sqr(mark(z0)),a__dbl(mark(z0))),A__SQR(mark(z0)),MARK(z0)) A__SQR(s(z0)) -> c4(A__ADD(a__sqr(mark(z0)),a__dbl(mark(z0))),A__DBL(mark(z0)),MARK(z0)) A__TERMS(z0) -> c(A__SQR(mark(z0)),MARK(z0)) A__TERMS(z0) -> c1() MARK(0()) -> c32() MARK(add(z0,z1)) -> c23(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c24(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c29(MARK(z0)) MARK(dbl(z0)) -> c25(A__DBL(mark(z0)),MARK(z0)) MARK(first(z0,z1)) -> c26(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c27(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(half(z0)) -> c28(A__HALF(mark(z0)),MARK(z0)) MARK(nil()) -> c33() MARK(recip(z0)) -> c30(MARK(z0)) MARK(s(z0)) -> c31(MARK(z0)) MARK(sqr(z0)) -> c22(A__SQR(mark(z0)),MARK(z0)) MARK(terms(z0)) -> c21(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(a__add(mark(z0),mark(z1))) a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(a__dbl(mark(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__half(z0) -> half(z0) a__half(0()) -> 0() a__half(dbl(z0)) -> mark(z0) a__half(s(0())) -> 0() a__half(s(s(z0))) -> s(a__half(mark(z0))) a__sqr(z0) -> sqr(z0) a__sqr(0()) -> 0() a__sqr(s(z0)) -> s(a__add(a__sqr(mark(z0)),a__dbl(mark(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(half(z0)) -> a__half(mark(z0)) mark(nil()) -> nil() mark(recip(z0)) -> recip(mark(z0)) mark(s(z0)) -> s(mark(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__HALF/1,A__SQR/1,A__TERMS/1,MARK/1,a__add/2,a__dbl/1,a__first/2,a__half/1 ,a__sqr/1,a__terms/1,mark/1} / {0/0,add/2,c/2,c1/0,c10/2,c11/2,c12/0,c13/0,c14/1,c15/0,c16/0,c17/0,c18/2 ,c19/1,c2/0,c20/0,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/2,c29/1,c3/3,c30/1,c31/1,c32/0,c33/0,c4/3 ,c5/0,c6/0,c7/2,c8/0,c9/1,cons/2,dbl/1,first/2,half/1,nil/0,recip/1,s/1,sqr/1,terms/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__DBL,A__FIRST,A__HALF,A__SQR,A__TERMS,MARK ,a__add,a__dbl,a__first,a__half,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,c26,c27,c28,c29,c3,c30,c31,c32,c33,c4,c5,c6,c7,c8,c9,cons,dbl ,first,half,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) -> c12() A__ADD(0(),z0) -> c9(MARK(z0)) A__ADD(s(z0),z1) -> c10(A__ADD(mark(z0),mark(z1)),MARK(z0)) A__ADD(s(z0),z1) -> c11(A__ADD(mark(z0),mark(z1)),MARK(z1)) A__DBL(z0) -> c8() A__DBL(0()) -> c6() A__DBL(s(z0)) -> c7(A__DBL(mark(z0)),MARK(z0)) A__FIRST(z0,z1) -> c15() A__FIRST(0(),z0) -> c13() A__FIRST(s(z0),cons(z1,z2)) -> c14(MARK(z1)) A__HALF(z0) -> c20() A__HALF(0()) -> c16() A__HALF(dbl(z0)) -> c19(MARK(z0)) A__HALF(s(0())) -> c17() A__HALF(s(s(z0))) -> c18(A__HALF(mark(z0)),MARK(z0)) A__SQR(z0) -> c5() A__SQR(0()) -> c2() A__SQR(s(z0)) -> c3(A__ADD(a__sqr(mark(z0)),a__dbl(mark(z0))),A__SQR(mark(z0)),MARK(z0)) A__SQR(s(z0)) -> c4(A__ADD(a__sqr(mark(z0)),a__dbl(mark(z0))),A__DBL(mark(z0)),MARK(z0)) A__TERMS(z0) -> c(A__SQR(mark(z0)),MARK(z0)) A__TERMS(z0) -> c1() MARK(0()) -> c32() MARK(add(z0,z1)) -> c23(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c24(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c29(MARK(z0)) MARK(dbl(z0)) -> c25(A__DBL(mark(z0)),MARK(z0)) MARK(first(z0,z1)) -> c26(A__FIRST(mark(z0),mark(z1)),MARK(z0)) MARK(first(z0,z1)) -> c27(A__FIRST(mark(z0),mark(z1)),MARK(z1)) MARK(half(z0)) -> c28(A__HALF(mark(z0)),MARK(z0)) MARK(nil()) -> c33() MARK(recip(z0)) -> c30(MARK(z0)) MARK(s(z0)) -> c31(MARK(z0)) MARK(sqr(z0)) -> c22(A__SQR(mark(z0)),MARK(z0)) MARK(terms(z0)) -> c21(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(a__add(mark(z0),mark(z1))) a__dbl(z0) -> dbl(z0) a__dbl(0()) -> 0() a__dbl(s(z0)) -> s(s(a__dbl(mark(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__half(z0) -> half(z0) a__half(0()) -> 0() a__half(dbl(z0)) -> mark(z0) a__half(s(0())) -> 0() a__half(s(s(z0))) -> s(a__half(mark(z0))) a__sqr(z0) -> sqr(z0) a__sqr(0()) -> 0() a__sqr(s(z0)) -> s(a__add(a__sqr(mark(z0)),a__dbl(mark(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(half(z0)) -> a__half(mark(z0)) mark(nil()) -> nil() mark(recip(z0)) -> recip(mark(z0)) mark(s(z0)) -> s(mark(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__HALF/1,A__SQR/1,A__TERMS/1,MARK/1,a__add/2,a__dbl/1,a__first/2,a__half/1 ,a__sqr/1,a__terms/1,mark/1} / {0/0,add/2,c/2,c1/0,c10/2,c11/2,c12/0,c13/0,c14/1,c15/0,c16/0,c17/0,c18/2 ,c19/1,c2/0,c20/0,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/2,c29/1,c3/3,c30/1,c31/1,c32/0,c33/0,c4/3 ,c5/0,c6/0,c7/2,c8/0,c9/1,cons/2,dbl/1,first/2,half/1,nil/0,recip/1,s/1,sqr/1,terms/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__DBL,A__FIRST,A__HALF,A__SQR,A__TERMS,MARK ,a__add,a__dbl,a__first,a__half,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,c26,c27,c28,c29,c3,c30,c31,c32,c33,c4,c5,c6,c7,c8,c9,cons,dbl ,first,half,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)) ->^+ c23(A__ADD(mark(x),mark(y)),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)