WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__INCR(z0) -> c5() A__INCR(cons(z0,z1)) -> c4(MARK(z0)) A__ODDNS() -> c2(A__INCR(a__pairNs()),A__PAIRNS()) A__ODDNS() -> c3() A__PAIRNS() -> c() A__PAIRNS() -> c1() A__REPITEMS(z0) -> c18() A__REPITEMS(cons(z0,z1)) -> c17(MARK(z0)) A__REPITEMS(nil()) -> c16() A__TAIL(z0) -> c15() A__TAIL(cons(z0,z1)) -> c14(MARK(z1)) A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7(MARK(z1)) A__ZIP(z0,z1) -> c13() A__ZIP(z0,nil()) -> c10() A__ZIP(cons(z0,z1),cons(z2,z3)) -> c11(MARK(z0)) A__ZIP(cons(z0,z1),cons(z2,z3)) -> c12(MARK(z2)) A__ZIP(nil(),z0) -> c9() MARK(0()) -> c29() MARK(cons(z0,z1)) -> c28(MARK(z0)) MARK(incr(z0)) -> c20(A__INCR(mark(z0)),MARK(z0)) MARK(nil()) -> c31() MARK(oddNs()) -> c21(A__ODDNS()) MARK(pair(z0,z1)) -> c32(MARK(z0)) MARK(pair(z0,z1)) -> c33(MARK(z1)) MARK(pairNs()) -> c19(A__PAIRNS()) MARK(repItems(z0)) -> c27(A__REPITEMS(mark(z0)),MARK(z0)) MARK(s(z0)) -> c30(MARK(z0)) MARK(tail(z0)) -> c26(A__TAIL(mark(z0)),MARK(z0)) MARK(take(z0,z1)) -> c22(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c23(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(zip(z0,z1)) -> c24(A__ZIP(mark(z0),mark(z1)),MARK(z0)) MARK(zip(z0,z1)) -> c25(A__ZIP(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__incr(z0) -> incr(z0) a__incr(cons(z0,z1)) -> cons(s(mark(z0)),incr(z1)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(z0) -> repItems(z0) a__repItems(cons(z0,z1)) -> cons(mark(z0),cons(z0,repItems(z1))) a__repItems(nil()) -> nil() a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(mark(z1),take(z0,z2)) a__zip(z0,z1) -> zip(z0,z1) a__zip(z0,nil()) -> nil() a__zip(cons(z0,z1),cons(z2,z3)) -> cons(pair(mark(z0),mark(z2)),zip(z1,z3)) a__zip(nil(),z0) -> nil() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(incr(z0)) -> a__incr(mark(z0)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(pairNs()) -> a__pairNs() mark(repItems(z0)) -> a__repItems(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(zip(z0,z1)) -> a__zip(mark(z0),mark(z1)) - Signature: {A__INCR/1,A__ODDNS/0,A__PAIRNS/0,A__REPITEMS/1,A__TAIL/1,A__TAKE/2,A__ZIP/2,MARK/1,a__incr/1,a__oddNs/0 ,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1} / {0/0,c/0,c1/0,c10/0,c11/1,c12/1,c13/0 ,c14/1,c15/0,c16/0,c17/1,c18/0,c19/1,c2/2,c20/2,c21/1,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/1,c29/0,c3/0 ,c30/1,c31/0,c32/1,c33/1,c4/1,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,incr/1,nil/0,oddNs/0,pair/2,pairNs/0 ,repItems/1,s/1,tail/1,take/2,zip/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__INCR,A__ODDNS,A__PAIRNS,A__REPITEMS,A__TAIL,A__TAKE ,A__ZIP,MARK,a__incr,a__oddNs,a__pairNs,a__repItems,a__tail,a__take,a__zip,mark} and constructors {0,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,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__INCR(z0) -> c5() A__INCR(cons(z0,z1)) -> c4(MARK(z0)) A__ODDNS() -> c2(A__INCR(a__pairNs()),A__PAIRNS()) A__ODDNS() -> c3() A__PAIRNS() -> c() A__PAIRNS() -> c1() A__REPITEMS(z0) -> c18() A__REPITEMS(cons(z0,z1)) -> c17(MARK(z0)) A__REPITEMS(nil()) -> c16() A__TAIL(z0) -> c15() A__TAIL(cons(z0,z1)) -> c14(MARK(z1)) A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7(MARK(z1)) A__ZIP(z0,z1) -> c13() A__ZIP(z0,nil()) -> c10() A__ZIP(cons(z0,z1),cons(z2,z3)) -> c11(MARK(z0)) A__ZIP(cons(z0,z1),cons(z2,z3)) -> c12(MARK(z2)) A__ZIP(nil(),z0) -> c9() MARK(0()) -> c29() MARK(cons(z0,z1)) -> c28(MARK(z0)) MARK(incr(z0)) -> c20(A__INCR(mark(z0)),MARK(z0)) MARK(nil()) -> c31() MARK(oddNs()) -> c21(A__ODDNS()) MARK(pair(z0,z1)) -> c32(MARK(z0)) MARK(pair(z0,z1)) -> c33(MARK(z1)) MARK(pairNs()) -> c19(A__PAIRNS()) MARK(repItems(z0)) -> c27(A__REPITEMS(mark(z0)),MARK(z0)) MARK(s(z0)) -> c30(MARK(z0)) MARK(tail(z0)) -> c26(A__TAIL(mark(z0)),MARK(z0)) MARK(take(z0,z1)) -> c22(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c23(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(zip(z0,z1)) -> c24(A__ZIP(mark(z0),mark(z1)),MARK(z0)) MARK(zip(z0,z1)) -> c25(A__ZIP(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__incr(z0) -> incr(z0) a__incr(cons(z0,z1)) -> cons(s(mark(z0)),incr(z1)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(z0) -> repItems(z0) a__repItems(cons(z0,z1)) -> cons(mark(z0),cons(z0,repItems(z1))) a__repItems(nil()) -> nil() a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(mark(z1),take(z0,z2)) a__zip(z0,z1) -> zip(z0,z1) a__zip(z0,nil()) -> nil() a__zip(cons(z0,z1),cons(z2,z3)) -> cons(pair(mark(z0),mark(z2)),zip(z1,z3)) a__zip(nil(),z0) -> nil() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(incr(z0)) -> a__incr(mark(z0)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(pairNs()) -> a__pairNs() mark(repItems(z0)) -> a__repItems(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(zip(z0,z1)) -> a__zip(mark(z0),mark(z1)) - Signature: {A__INCR/1,A__ODDNS/0,A__PAIRNS/0,A__REPITEMS/1,A__TAIL/1,A__TAKE/2,A__ZIP/2,MARK/1,a__incr/1,a__oddNs/0 ,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1} / {0/0,c/0,c1/0,c10/0,c11/1,c12/1,c13/0 ,c14/1,c15/0,c16/0,c17/1,c18/0,c19/1,c2/2,c20/2,c21/1,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/1,c29/0,c3/0 ,c30/1,c31/0,c32/1,c33/1,c4/1,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,incr/1,nil/0,oddNs/0,pair/2,pairNs/0 ,repItems/1,s/1,tail/1,take/2,zip/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__INCR,A__ODDNS,A__PAIRNS,A__REPITEMS,A__TAIL,A__TAKE ,A__ZIP,MARK,a__incr,a__oddNs,a__pairNs,a__repItems,a__tail,a__take,a__zip,mark} and constructors {0,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,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__INCR(z0) -> c5() A__INCR(cons(z0,z1)) -> c4(MARK(z0)) A__ODDNS() -> c2(A__INCR(a__pairNs()),A__PAIRNS()) A__ODDNS() -> c3() A__PAIRNS() -> c() A__PAIRNS() -> c1() A__REPITEMS(z0) -> c18() A__REPITEMS(cons(z0,z1)) -> c17(MARK(z0)) A__REPITEMS(nil()) -> c16() A__TAIL(z0) -> c15() A__TAIL(cons(z0,z1)) -> c14(MARK(z1)) A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7(MARK(z1)) A__ZIP(z0,z1) -> c13() A__ZIP(z0,nil()) -> c10() A__ZIP(cons(z0,z1),cons(z2,z3)) -> c11(MARK(z0)) A__ZIP(cons(z0,z1),cons(z2,z3)) -> c12(MARK(z2)) A__ZIP(nil(),z0) -> c9() MARK(0()) -> c29() MARK(cons(z0,z1)) -> c28(MARK(z0)) MARK(incr(z0)) -> c20(A__INCR(mark(z0)),MARK(z0)) MARK(nil()) -> c31() MARK(oddNs()) -> c21(A__ODDNS()) MARK(pair(z0,z1)) -> c32(MARK(z0)) MARK(pair(z0,z1)) -> c33(MARK(z1)) MARK(pairNs()) -> c19(A__PAIRNS()) MARK(repItems(z0)) -> c27(A__REPITEMS(mark(z0)),MARK(z0)) MARK(s(z0)) -> c30(MARK(z0)) MARK(tail(z0)) -> c26(A__TAIL(mark(z0)),MARK(z0)) MARK(take(z0,z1)) -> c22(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c23(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(zip(z0,z1)) -> c24(A__ZIP(mark(z0),mark(z1)),MARK(z0)) MARK(zip(z0,z1)) -> c25(A__ZIP(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__incr(z0) -> incr(z0) a__incr(cons(z0,z1)) -> cons(s(mark(z0)),incr(z1)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(z0) -> repItems(z0) a__repItems(cons(z0,z1)) -> cons(mark(z0),cons(z0,repItems(z1))) a__repItems(nil()) -> nil() a__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> mark(z1) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(mark(z1),take(z0,z2)) a__zip(z0,z1) -> zip(z0,z1) a__zip(z0,nil()) -> nil() a__zip(cons(z0,z1),cons(z2,z3)) -> cons(pair(mark(z0),mark(z2)),zip(z1,z3)) a__zip(nil(),z0) -> nil() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(incr(z0)) -> a__incr(mark(z0)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(pairNs()) -> a__pairNs() mark(repItems(z0)) -> a__repItems(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(zip(z0,z1)) -> a__zip(mark(z0),mark(z1)) - Signature: {A__INCR/1,A__ODDNS/0,A__PAIRNS/0,A__REPITEMS/1,A__TAIL/1,A__TAKE/2,A__ZIP/2,MARK/1,a__incr/1,a__oddNs/0 ,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1} / {0/0,c/0,c1/0,c10/0,c11/1,c12/1,c13/0 ,c14/1,c15/0,c16/0,c17/1,c18/0,c19/1,c2/2,c20/2,c21/1,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/1,c29/0,c3/0 ,c30/1,c31/0,c32/1,c33/1,c4/1,c5/0,c6/0,c7/1,c8/0,c9/0,cons/2,incr/1,nil/0,oddNs/0,pair/2,pairNs/0 ,repItems/1,s/1,tail/1,take/2,zip/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__INCR,A__ODDNS,A__PAIRNS,A__REPITEMS,A__TAIL,A__TAKE ,A__ZIP,MARK,a__incr,a__oddNs,a__pairNs,a__repItems,a__tail,a__take,a__zip,mark} and constructors {0,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,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> cons(x,y)} = MARK(cons(x,y)) ->^+ c28(MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)