WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c3() A__AND(tt(),z0) -> c2(MARK(z0)) A__LENGTH(z0) -> c6() A__LENGTH(cons(z0,z1)) -> c5(A__LENGTH(mark(z1)),MARK(z1)) A__LENGTH(nil()) -> c4() A__TAKE(z0,z1) -> c9() A__TAKE(0(),z0) -> c7() A__TAKE(s(z0),cons(z1,z2)) -> c8(MARK(z1)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c16() MARK(and(z0,z1)) -> c11(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c15(MARK(z0)) MARK(length(z0)) -> c12(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c18() MARK(s(z0)) -> c19(MARK(z0)) MARK(take(z0,z1)) -> c13(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c14(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c17() MARK(zeros()) -> c10(A__ZEROS()) - Weak TRS: a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(a__length(mark(z1))) a__length(nil()) -> 0() 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__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__LENGTH/1,A__TAKE/2,A__ZEROS/0,MARK/1,a__and/2,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0 ,and/2,c/0,c1/0,c10/1,c11/2,c12/2,c13/2,c14/2,c15/1,c16/0,c17/0,c18/0,c19/1,c2/1,c3/0,c4/0,c5/2,c6/0,c7/0 ,c8/1,c9/0,cons/2,length/1,nil/0,s/1,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__LENGTH,A__TAKE,A__ZEROS,MARK,a__and,a__length ,a__take,a__zeros,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c3,c4,c5,c6 ,c7,c8,c9,cons,length,nil,s,take,tt,zeros} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c3() A__AND(tt(),z0) -> c2(MARK(z0)) A__LENGTH(z0) -> c6() A__LENGTH(cons(z0,z1)) -> c5(A__LENGTH(mark(z1)),MARK(z1)) A__LENGTH(nil()) -> c4() A__TAKE(z0,z1) -> c9() A__TAKE(0(),z0) -> c7() A__TAKE(s(z0),cons(z1,z2)) -> c8(MARK(z1)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c16() MARK(and(z0,z1)) -> c11(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c15(MARK(z0)) MARK(length(z0)) -> c12(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c18() MARK(s(z0)) -> c19(MARK(z0)) MARK(take(z0,z1)) -> c13(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c14(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c17() MARK(zeros()) -> c10(A__ZEROS()) - Weak TRS: a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(a__length(mark(z1))) a__length(nil()) -> 0() 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__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__LENGTH/1,A__TAKE/2,A__ZEROS/0,MARK/1,a__and/2,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0 ,and/2,c/0,c1/0,c10/1,c11/2,c12/2,c13/2,c14/2,c15/1,c16/0,c17/0,c18/0,c19/1,c2/1,c3/0,c4/0,c5/2,c6/0,c7/0 ,c8/1,c9/0,cons/2,length/1,nil/0,s/1,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__LENGTH,A__TAKE,A__ZEROS,MARK,a__and,a__length ,a__take,a__zeros,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c3,c4,c5,c6 ,c7,c8,c9,cons,length,nil,s,take,tt,zeros} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c3() A__AND(tt(),z0) -> c2(MARK(z0)) A__LENGTH(z0) -> c6() A__LENGTH(cons(z0,z1)) -> c5(A__LENGTH(mark(z1)),MARK(z1)) A__LENGTH(nil()) -> c4() A__TAKE(z0,z1) -> c9() A__TAKE(0(),z0) -> c7() A__TAKE(s(z0),cons(z1,z2)) -> c8(MARK(z1)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c16() MARK(and(z0,z1)) -> c11(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c15(MARK(z0)) MARK(length(z0)) -> c12(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c18() MARK(s(z0)) -> c19(MARK(z0)) MARK(take(z0,z1)) -> c13(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c14(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c17() MARK(zeros()) -> c10(A__ZEROS()) - Weak TRS: a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(a__length(mark(z1))) a__length(nil()) -> 0() 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__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__LENGTH/1,A__TAKE/2,A__ZEROS/0,MARK/1,a__and/2,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0 ,and/2,c/0,c1/0,c10/1,c11/2,c12/2,c13/2,c14/2,c15/1,c16/0,c17/0,c18/0,c19/1,c2/1,c3/0,c4/0,c5/2,c6/0,c7/0 ,c8/1,c9/0,cons/2,length/1,nil/0,s/1,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__LENGTH,A__TAKE,A__ZEROS,MARK,a__and,a__length ,a__take,a__zeros,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c3,c4,c5,c6 ,c7,c8,c9,cons,length,nil,s,take,tt,zeros} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> and(x,y)} = MARK(and(x,y)) ->^+ c11(A__AND(mark(x),y),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)