WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__LENGTH(z0) -> c14() A__LENGTH(cons(z0,z1)) -> c13(A__U11(tt(),z1)) A__LENGTH(nil()) -> c12() A__TAKE(z0,z1) -> c17() A__TAKE(0(),z0) -> c15() A__TAKE(s(z0),cons(z1,z2)) -> c16(A__U21(tt(),z2,z0,z1)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__U12(tt(),z0)) A__U12(z0,z1) -> c5() A__U12(tt(),z0) -> c4(A__LENGTH(mark(z0)),MARK(z0)) A__U21(z0,z1,z2,z3) -> c7() A__U21(tt(),z0,z1,z2) -> c6(A__U22(tt(),z0,z1,z2)) A__U22(z0,z1,z2,z3) -> c9() A__U22(tt(),z0,z1,z2) -> c8(A__U23(tt(),z0,z1,z2)) A__U23(z0,z1,z2,z3) -> c11() A__U23(tt(),z0,z1,z2) -> c10(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c28() MARK(U11(z0,z1)) -> c19(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0,z1)) -> c20(A__U12(mark(z0),z1),MARK(z0)) MARK(U21(z0,z1,z2,z3)) -> c22(A__U21(mark(z0),z1,z2,z3),MARK(z0)) MARK(U22(z0,z1,z2,z3)) -> c23(A__U22(mark(z0),z1,z2,z3),MARK(z0)) MARK(U23(z0,z1,z2,z3)) -> c24(A__U23(mark(z0),z1,z2,z3),MARK(z0)) MARK(cons(z0,z1)) -> c27(MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c31() MARK(s(z0)) -> c30(MARK(z0)) MARK(take(z0,z1)) -> c25(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c26(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c29() MARK(zeros()) -> c18(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(tt(),z0) a__U12(z0,z1) -> U12(z0,z1) a__U12(tt(),z0) -> s(a__length(mark(z0))) a__U21(z0,z1,z2,z3) -> U21(z0,z1,z2,z3) a__U21(tt(),z0,z1,z2) -> a__U22(tt(),z0,z1,z2) a__U22(z0,z1,z2,z3) -> U22(z0,z1,z2,z3) a__U22(tt(),z0,z1,z2) -> a__U23(tt(),z0,z1,z2) a__U23(z0,z1,z2,z3) -> U23(z0,z1,z2,z3) a__U23(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U11(tt(),z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> a__U21(tt(),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0,z1)) -> a__U12(mark(z0),z1) mark(U21(z0,z1,z2,z3)) -> a__U21(mark(z0),z1,z2,z3) mark(U22(z0,z1,z2,z3)) -> a__U22(mark(z0),z1,z2,z3) mark(U23(z0,z1,z2,z3)) -> a__U23(mark(z0),z1,z2,z3) 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__LENGTH/1,A__TAKE/2,A__U11/2,A__U12/2,A__U21/4,A__U22/4,A__U23/4,A__ZEROS/0,MARK/1,a__U11/2,a__U12/2 ,a__U21/4,a__U22/4,a__U23/4,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,U21/4,U22/4,U23/4 ,c/0,c1/0,c10/1,c11/0,c12/0,c13/1,c14/0,c15/0,c16/1,c17/0,c18/1,c19/2,c2/1,c20/2,c21/2,c22/2,c23/2,c24/2 ,c25/2,c26/2,c27/1,c28/0,c29/0,c3/0,c30/1,c31/0,c4/2,c5/0,c6/1,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__LENGTH,A__TAKE,A__U11,A__U12,A__U21,A__U22,A__U23 ,A__ZEROS,MARK,a__U11,a__U12,a__U21,a__U22,a__U23,a__length,a__take,a__zeros,mark} and constructors {0,U11 ,U12,U21,U22,U23,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,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__LENGTH(z0) -> c14() A__LENGTH(cons(z0,z1)) -> c13(A__U11(tt(),z1)) A__LENGTH(nil()) -> c12() A__TAKE(z0,z1) -> c17() A__TAKE(0(),z0) -> c15() A__TAKE(s(z0),cons(z1,z2)) -> c16(A__U21(tt(),z2,z0,z1)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__U12(tt(),z0)) A__U12(z0,z1) -> c5() A__U12(tt(),z0) -> c4(A__LENGTH(mark(z0)),MARK(z0)) A__U21(z0,z1,z2,z3) -> c7() A__U21(tt(),z0,z1,z2) -> c6(A__U22(tt(),z0,z1,z2)) A__U22(z0,z1,z2,z3) -> c9() A__U22(tt(),z0,z1,z2) -> c8(A__U23(tt(),z0,z1,z2)) A__U23(z0,z1,z2,z3) -> c11() A__U23(tt(),z0,z1,z2) -> c10(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c28() MARK(U11(z0,z1)) -> c19(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0,z1)) -> c20(A__U12(mark(z0),z1),MARK(z0)) MARK(U21(z0,z1,z2,z3)) -> c22(A__U21(mark(z0),z1,z2,z3),MARK(z0)) MARK(U22(z0,z1,z2,z3)) -> c23(A__U22(mark(z0),z1,z2,z3),MARK(z0)) MARK(U23(z0,z1,z2,z3)) -> c24(A__U23(mark(z0),z1,z2,z3),MARK(z0)) MARK(cons(z0,z1)) -> c27(MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c31() MARK(s(z0)) -> c30(MARK(z0)) MARK(take(z0,z1)) -> c25(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c26(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c29() MARK(zeros()) -> c18(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(tt(),z0) a__U12(z0,z1) -> U12(z0,z1) a__U12(tt(),z0) -> s(a__length(mark(z0))) a__U21(z0,z1,z2,z3) -> U21(z0,z1,z2,z3) a__U21(tt(),z0,z1,z2) -> a__U22(tt(),z0,z1,z2) a__U22(z0,z1,z2,z3) -> U22(z0,z1,z2,z3) a__U22(tt(),z0,z1,z2) -> a__U23(tt(),z0,z1,z2) a__U23(z0,z1,z2,z3) -> U23(z0,z1,z2,z3) a__U23(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U11(tt(),z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> a__U21(tt(),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0,z1)) -> a__U12(mark(z0),z1) mark(U21(z0,z1,z2,z3)) -> a__U21(mark(z0),z1,z2,z3) mark(U22(z0,z1,z2,z3)) -> a__U22(mark(z0),z1,z2,z3) mark(U23(z0,z1,z2,z3)) -> a__U23(mark(z0),z1,z2,z3) 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__LENGTH/1,A__TAKE/2,A__U11/2,A__U12/2,A__U21/4,A__U22/4,A__U23/4,A__ZEROS/0,MARK/1,a__U11/2,a__U12/2 ,a__U21/4,a__U22/4,a__U23/4,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,U21/4,U22/4,U23/4 ,c/0,c1/0,c10/1,c11/0,c12/0,c13/1,c14/0,c15/0,c16/1,c17/0,c18/1,c19/2,c2/1,c20/2,c21/2,c22/2,c23/2,c24/2 ,c25/2,c26/2,c27/1,c28/0,c29/0,c3/0,c30/1,c31/0,c4/2,c5/0,c6/1,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__LENGTH,A__TAKE,A__U11,A__U12,A__U21,A__U22,A__U23 ,A__ZEROS,MARK,a__U11,a__U12,a__U21,a__U22,a__U23,a__length,a__take,a__zeros,mark} and constructors {0,U11 ,U12,U21,U22,U23,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,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__LENGTH(z0) -> c14() A__LENGTH(cons(z0,z1)) -> c13(A__U11(tt(),z1)) A__LENGTH(nil()) -> c12() A__TAKE(z0,z1) -> c17() A__TAKE(0(),z0) -> c15() A__TAKE(s(z0),cons(z1,z2)) -> c16(A__U21(tt(),z2,z0,z1)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__U12(tt(),z0)) A__U12(z0,z1) -> c5() A__U12(tt(),z0) -> c4(A__LENGTH(mark(z0)),MARK(z0)) A__U21(z0,z1,z2,z3) -> c7() A__U21(tt(),z0,z1,z2) -> c6(A__U22(tt(),z0,z1,z2)) A__U22(z0,z1,z2,z3) -> c9() A__U22(tt(),z0,z1,z2) -> c8(A__U23(tt(),z0,z1,z2)) A__U23(z0,z1,z2,z3) -> c11() A__U23(tt(),z0,z1,z2) -> c10(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c28() MARK(U11(z0,z1)) -> c19(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0,z1)) -> c20(A__U12(mark(z0),z1),MARK(z0)) MARK(U21(z0,z1,z2,z3)) -> c22(A__U21(mark(z0),z1,z2,z3),MARK(z0)) MARK(U22(z0,z1,z2,z3)) -> c23(A__U22(mark(z0),z1,z2,z3),MARK(z0)) MARK(U23(z0,z1,z2,z3)) -> c24(A__U23(mark(z0),z1,z2,z3),MARK(z0)) MARK(cons(z0,z1)) -> c27(MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c31() MARK(s(z0)) -> c30(MARK(z0)) MARK(take(z0,z1)) -> c25(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c26(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c29() MARK(zeros()) -> c18(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(tt(),z0) a__U12(z0,z1) -> U12(z0,z1) a__U12(tt(),z0) -> s(a__length(mark(z0))) a__U21(z0,z1,z2,z3) -> U21(z0,z1,z2,z3) a__U21(tt(),z0,z1,z2) -> a__U22(tt(),z0,z1,z2) a__U22(z0,z1,z2,z3) -> U22(z0,z1,z2,z3) a__U22(tt(),z0,z1,z2) -> a__U23(tt(),z0,z1,z2) a__U23(z0,z1,z2,z3) -> U23(z0,z1,z2,z3) a__U23(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U11(tt(),z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> a__U21(tt(),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0,z1)) -> a__U12(mark(z0),z1) mark(U21(z0,z1,z2,z3)) -> a__U21(mark(z0),z1,z2,z3) mark(U22(z0,z1,z2,z3)) -> a__U22(mark(z0),z1,z2,z3) mark(U23(z0,z1,z2,z3)) -> a__U23(mark(z0),z1,z2,z3) 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__LENGTH/1,A__TAKE/2,A__U11/2,A__U12/2,A__U21/4,A__U22/4,A__U23/4,A__ZEROS/0,MARK/1,a__U11/2,a__U12/2 ,a__U21/4,a__U22/4,a__U23/4,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U12/2,U21/4,U22/4,U23/4 ,c/0,c1/0,c10/1,c11/0,c12/0,c13/1,c14/0,c15/0,c16/1,c17/0,c18/1,c19/2,c2/1,c20/2,c21/2,c22/2,c23/2,c24/2 ,c25/2,c26/2,c27/1,c28/0,c29/0,c3/0,c30/1,c31/0,c4/2,c5/0,c6/1,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__LENGTH,A__TAKE,A__U11,A__U12,A__U21,A__U22,A__U23 ,A__ZEROS,MARK,a__U11,a__U12,a__U21,a__U22,a__U23,a__length,a__take,a__zeros,mark} and constructors {0,U11 ,U12,U21,U22,U23,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,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 -> U11(x,y)} = MARK(U11(x,y)) ->^+ c19(A__U11(mark(x),y),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)