WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__APP(z0,z1) -> c2() A__APP(cons(z0,z1),z2) -> c1(MARK(z0)) A__APP(nil(),z0) -> c(MARK(z0)) A__FROM(z0) -> c3(MARK(z0)) A__FROM(z0) -> c4() A__PREFIX(z0) -> c10() A__PREFIX(z0) -> c11() A__ZWADR(z0,z1) -> c9() A__ZWADR(z0,nil()) -> c6() A__ZWADR(cons(z0,z1),cons(z2,z3)) -> c7(A__APP(mark(z2),cons(mark(z0),nil())),MARK(z2)) A__ZWADR(cons(z0,z1),cons(z2,z3)) -> c8(A__APP(mark(z2),cons(mark(z0),nil())),MARK(z0)) A__ZWADR(nil(),z0) -> c5() MARK(app(z0,z1)) -> c12(A__APP(mark(z0),mark(z1)),MARK(z0)) MARK(app(z0,z1)) -> c13(A__APP(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c19(MARK(z0)) MARK(from(z0)) -> c14(A__FROM(mark(z0)),MARK(z0)) MARK(nil()) -> c18() MARK(prefix(z0)) -> c17(A__PREFIX(mark(z0)),MARK(z0)) MARK(s(z0)) -> c20(MARK(z0)) MARK(zWadr(z0,z1)) -> c15(A__ZWADR(mark(z0),mark(z1)),MARK(z0)) MARK(zWadr(z0,z1)) -> c16(A__ZWADR(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__app(z0,z1) -> app(z0,z1) a__app(cons(z0,z1),z2) -> cons(mark(z0),app(z1,z2)) a__app(nil(),z0) -> mark(z0) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__prefix(z0) -> cons(nil(),zWadr(z0,prefix(z0))) a__prefix(z0) -> prefix(z0) a__zWadr(z0,z1) -> zWadr(z0,z1) a__zWadr(z0,nil()) -> nil() a__zWadr(cons(z0,z1),cons(z2,z3)) -> cons(a__app(mark(z2),cons(mark(z0),nil())),zWadr(z1,z3)) a__zWadr(nil(),z0) -> nil() mark(app(z0,z1)) -> a__app(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(nil()) -> nil() mark(prefix(z0)) -> a__prefix(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(zWadr(z0,z1)) -> a__zWadr(mark(z0),mark(z1)) - Signature: {A__APP/2,A__FROM/1,A__PREFIX/1,A__ZWADR/2,MARK/1,a__app/2,a__from/1,a__prefix/1,a__zWadr/2,mark/1} / {app/2 ,c/1,c1/1,c10/0,c11/0,c12/2,c13/2,c14/2,c15/2,c16/2,c17/2,c18/0,c19/1,c2/0,c20/1,c3/1,c4/0,c5/0,c6/0,c7/2 ,c8/2,c9/0,cons/2,from/1,nil/0,prefix/1,s/1,zWadr/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__APP,A__FROM,A__PREFIX,A__ZWADR,MARK,a__app,a__from ,a__prefix,a__zWadr,mark} and constructors {app,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c3,c4,c5 ,c6,c7,c8,c9,cons,from,nil,prefix,s,zWadr} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__APP(z0,z1) -> c2() A__APP(cons(z0,z1),z2) -> c1(MARK(z0)) A__APP(nil(),z0) -> c(MARK(z0)) A__FROM(z0) -> c3(MARK(z0)) A__FROM(z0) -> c4() A__PREFIX(z0) -> c10() A__PREFIX(z0) -> c11() A__ZWADR(z0,z1) -> c9() A__ZWADR(z0,nil()) -> c6() A__ZWADR(cons(z0,z1),cons(z2,z3)) -> c7(A__APP(mark(z2),cons(mark(z0),nil())),MARK(z2)) A__ZWADR(cons(z0,z1),cons(z2,z3)) -> c8(A__APP(mark(z2),cons(mark(z0),nil())),MARK(z0)) A__ZWADR(nil(),z0) -> c5() MARK(app(z0,z1)) -> c12(A__APP(mark(z0),mark(z1)),MARK(z0)) MARK(app(z0,z1)) -> c13(A__APP(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c19(MARK(z0)) MARK(from(z0)) -> c14(A__FROM(mark(z0)),MARK(z0)) MARK(nil()) -> c18() MARK(prefix(z0)) -> c17(A__PREFIX(mark(z0)),MARK(z0)) MARK(s(z0)) -> c20(MARK(z0)) MARK(zWadr(z0,z1)) -> c15(A__ZWADR(mark(z0),mark(z1)),MARK(z0)) MARK(zWadr(z0,z1)) -> c16(A__ZWADR(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__app(z0,z1) -> app(z0,z1) a__app(cons(z0,z1),z2) -> cons(mark(z0),app(z1,z2)) a__app(nil(),z0) -> mark(z0) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__prefix(z0) -> cons(nil(),zWadr(z0,prefix(z0))) a__prefix(z0) -> prefix(z0) a__zWadr(z0,z1) -> zWadr(z0,z1) a__zWadr(z0,nil()) -> nil() a__zWadr(cons(z0,z1),cons(z2,z3)) -> cons(a__app(mark(z2),cons(mark(z0),nil())),zWadr(z1,z3)) a__zWadr(nil(),z0) -> nil() mark(app(z0,z1)) -> a__app(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(nil()) -> nil() mark(prefix(z0)) -> a__prefix(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(zWadr(z0,z1)) -> a__zWadr(mark(z0),mark(z1)) - Signature: {A__APP/2,A__FROM/1,A__PREFIX/1,A__ZWADR/2,MARK/1,a__app/2,a__from/1,a__prefix/1,a__zWadr/2,mark/1} / {app/2 ,c/1,c1/1,c10/0,c11/0,c12/2,c13/2,c14/2,c15/2,c16/2,c17/2,c18/0,c19/1,c2/0,c20/1,c3/1,c4/0,c5/0,c6/0,c7/2 ,c8/2,c9/0,cons/2,from/1,nil/0,prefix/1,s/1,zWadr/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__APP,A__FROM,A__PREFIX,A__ZWADR,MARK,a__app,a__from ,a__prefix,a__zWadr,mark} and constructors {app,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c3,c4,c5 ,c6,c7,c8,c9,cons,from,nil,prefix,s,zWadr} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__APP(z0,z1) -> c2() A__APP(cons(z0,z1),z2) -> c1(MARK(z0)) A__APP(nil(),z0) -> c(MARK(z0)) A__FROM(z0) -> c3(MARK(z0)) A__FROM(z0) -> c4() A__PREFIX(z0) -> c10() A__PREFIX(z0) -> c11() A__ZWADR(z0,z1) -> c9() A__ZWADR(z0,nil()) -> c6() A__ZWADR(cons(z0,z1),cons(z2,z3)) -> c7(A__APP(mark(z2),cons(mark(z0),nil())),MARK(z2)) A__ZWADR(cons(z0,z1),cons(z2,z3)) -> c8(A__APP(mark(z2),cons(mark(z0),nil())),MARK(z0)) A__ZWADR(nil(),z0) -> c5() MARK(app(z0,z1)) -> c12(A__APP(mark(z0),mark(z1)),MARK(z0)) MARK(app(z0,z1)) -> c13(A__APP(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c19(MARK(z0)) MARK(from(z0)) -> c14(A__FROM(mark(z0)),MARK(z0)) MARK(nil()) -> c18() MARK(prefix(z0)) -> c17(A__PREFIX(mark(z0)),MARK(z0)) MARK(s(z0)) -> c20(MARK(z0)) MARK(zWadr(z0,z1)) -> c15(A__ZWADR(mark(z0),mark(z1)),MARK(z0)) MARK(zWadr(z0,z1)) -> c16(A__ZWADR(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__app(z0,z1) -> app(z0,z1) a__app(cons(z0,z1),z2) -> cons(mark(z0),app(z1,z2)) a__app(nil(),z0) -> mark(z0) a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__prefix(z0) -> cons(nil(),zWadr(z0,prefix(z0))) a__prefix(z0) -> prefix(z0) a__zWadr(z0,z1) -> zWadr(z0,z1) a__zWadr(z0,nil()) -> nil() a__zWadr(cons(z0,z1),cons(z2,z3)) -> cons(a__app(mark(z2),cons(mark(z0),nil())),zWadr(z1,z3)) a__zWadr(nil(),z0) -> nil() mark(app(z0,z1)) -> a__app(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(nil()) -> nil() mark(prefix(z0)) -> a__prefix(mark(z0)) mark(s(z0)) -> s(mark(z0)) mark(zWadr(z0,z1)) -> a__zWadr(mark(z0),mark(z1)) - Signature: {A__APP/2,A__FROM/1,A__PREFIX/1,A__ZWADR/2,MARK/1,a__app/2,a__from/1,a__prefix/1,a__zWadr/2,mark/1} / {app/2 ,c/1,c1/1,c10/0,c11/0,c12/2,c13/2,c14/2,c15/2,c16/2,c17/2,c18/0,c19/1,c2/0,c20/1,c3/1,c4/0,c5/0,c6/0,c7/2 ,c8/2,c9/0,cons/2,from/1,nil/0,prefix/1,s/1,zWadr/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__APP,A__FROM,A__PREFIX,A__ZWADR,MARK,a__app,a__from ,a__prefix,a__zWadr,mark} and constructors {app,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c3,c4,c5 ,c6,c7,c8,c9,cons,from,nil,prefix,s,zWadr} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> app(x,y)} = MARK(app(x,y)) ->^+ c12(A__APP(mark(x),mark(y)),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)