WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__MINUS(z0,z1) -> c9() A__MINUS(z0,0()) -> c6() A__MINUS(s(z0),s(z1)) -> c7(A__MINUS(mark(z0),mark(z1)),MARK(z0)) A__MINUS(s(z0),s(z1)) -> c8(A__MINUS(mark(z0),mark(z1)),MARK(z1)) A__QUOT(z0,z1) -> c14() A__QUOT(0(),s(z0)) -> c10() A__QUOT(s(z0),s(z1)) -> c11(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))) ,A__MINUS(mark(z0),mark(z1)) ,MARK(z0)) A__QUOT(s(z0),s(z1)) -> c12(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))) ,A__MINUS(mark(z0),mark(z1)) ,MARK(z1)) A__QUOT(s(z0),s(z1)) -> c13(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))),MARK(z1)) A__SEL(z0,z1) -> c5() A__SEL(0(),cons(z0,z1)) -> c2(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c3(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c4(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__ZWQUOT(z0,z1) -> c19() A__ZWQUOT(z0,nil()) -> c15() A__ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c17(A__QUOT(mark(z0),mark(z2)),MARK(z0)) A__ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c18(A__QUOT(mark(z0),mark(z2)),MARK(z2)) A__ZWQUOT(nil(),z0) -> c16() MARK(0()) -> c31() MARK(cons(z0,z1)) -> c29(MARK(z0)) MARK(from(z0)) -> c20(A__FROM(mark(z0)),MARK(z0)) MARK(minus(z0,z1)) -> c23(A__MINUS(mark(z0),mark(z1)),MARK(z0)) MARK(minus(z0,z1)) -> c24(A__MINUS(mark(z0),mark(z1)),MARK(z1)) MARK(nil()) -> c32() MARK(quot(z0,z1)) -> c25(A__QUOT(mark(z0),mark(z1)),MARK(z0)) MARK(quot(z0,z1)) -> c26(A__QUOT(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c30(MARK(z0)) MARK(sel(z0,z1)) -> c21(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c22(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(zWquot(z0,z1)) -> c27(A__ZWQUOT(mark(z0),mark(z1)),MARK(z0)) MARK(zWquot(z0,z1)) -> c28(A__ZWQUOT(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__minus(z0,z1) -> minus(z0,z1) a__minus(z0,0()) -> 0() a__minus(s(z0),s(z1)) -> a__minus(mark(z0),mark(z1)) a__quot(z0,z1) -> quot(z0,z1) a__quot(0(),s(z0)) -> 0() a__quot(s(z0),s(z1)) -> s(a__quot(a__minus(mark(z0),mark(z1)),s(mark(z1)))) a__sel(z0,z1) -> sel(z0,z1) a__sel(0(),cons(z0,z1)) -> mark(z0) a__sel(s(z0),cons(z1,z2)) -> a__sel(mark(z0),mark(z2)) a__zWquot(z0,z1) -> zWquot(z0,z1) a__zWquot(z0,nil()) -> nil() a__zWquot(cons(z0,z1),cons(z2,z3)) -> cons(a__quot(mark(z0),mark(z2)),zWquot(z1,z3)) a__zWquot(nil(),z0) -> nil() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(minus(z0,z1)) -> a__minus(mark(z0),mark(z1)) mark(nil()) -> nil() mark(quot(z0,z1)) -> a__quot(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(zWquot(z0,z1)) -> a__zWquot(mark(z0),mark(z1)) - Signature: {A__FROM/1,A__MINUS/2,A__QUOT/2,A__SEL/2,A__ZWQUOT/2,MARK/1,a__from/1,a__minus/2,a__quot/2,a__sel/2 ,a__zWquot/2,mark/1} / {0/0,c/1,c1/0,c10/0,c11/3,c12/3,c13/2,c14/0,c15/0,c16/0,c17/2,c18/2,c19/0,c2/1,c20/2 ,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/2,c29/1,c3/2,c30/1,c31/0,c32/0,c4/2,c5/0,c6/0,c7/2,c8/2,c9/0 ,cons/2,from/1,minus/2,nil/0,quot/2,s/1,sel/2,zWquot/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__FROM,A__MINUS,A__QUOT,A__SEL,A__ZWQUOT,MARK,a__from ,a__minus,a__quot,a__sel,a__zWquot,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,c4,c5,c6,c7,c8,c9,cons,from,minus,nil,quot,s,sel ,zWquot} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__MINUS(z0,z1) -> c9() A__MINUS(z0,0()) -> c6() A__MINUS(s(z0),s(z1)) -> c7(A__MINUS(mark(z0),mark(z1)),MARK(z0)) A__MINUS(s(z0),s(z1)) -> c8(A__MINUS(mark(z0),mark(z1)),MARK(z1)) A__QUOT(z0,z1) -> c14() A__QUOT(0(),s(z0)) -> c10() A__QUOT(s(z0),s(z1)) -> c11(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))) ,A__MINUS(mark(z0),mark(z1)) ,MARK(z0)) A__QUOT(s(z0),s(z1)) -> c12(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))) ,A__MINUS(mark(z0),mark(z1)) ,MARK(z1)) A__QUOT(s(z0),s(z1)) -> c13(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))),MARK(z1)) A__SEL(z0,z1) -> c5() A__SEL(0(),cons(z0,z1)) -> c2(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c3(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c4(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__ZWQUOT(z0,z1) -> c19() A__ZWQUOT(z0,nil()) -> c15() A__ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c17(A__QUOT(mark(z0),mark(z2)),MARK(z0)) A__ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c18(A__QUOT(mark(z0),mark(z2)),MARK(z2)) A__ZWQUOT(nil(),z0) -> c16() MARK(0()) -> c31() MARK(cons(z0,z1)) -> c29(MARK(z0)) MARK(from(z0)) -> c20(A__FROM(mark(z0)),MARK(z0)) MARK(minus(z0,z1)) -> c23(A__MINUS(mark(z0),mark(z1)),MARK(z0)) MARK(minus(z0,z1)) -> c24(A__MINUS(mark(z0),mark(z1)),MARK(z1)) MARK(nil()) -> c32() MARK(quot(z0,z1)) -> c25(A__QUOT(mark(z0),mark(z1)),MARK(z0)) MARK(quot(z0,z1)) -> c26(A__QUOT(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c30(MARK(z0)) MARK(sel(z0,z1)) -> c21(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c22(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(zWquot(z0,z1)) -> c27(A__ZWQUOT(mark(z0),mark(z1)),MARK(z0)) MARK(zWquot(z0,z1)) -> c28(A__ZWQUOT(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__minus(z0,z1) -> minus(z0,z1) a__minus(z0,0()) -> 0() a__minus(s(z0),s(z1)) -> a__minus(mark(z0),mark(z1)) a__quot(z0,z1) -> quot(z0,z1) a__quot(0(),s(z0)) -> 0() a__quot(s(z0),s(z1)) -> s(a__quot(a__minus(mark(z0),mark(z1)),s(mark(z1)))) a__sel(z0,z1) -> sel(z0,z1) a__sel(0(),cons(z0,z1)) -> mark(z0) a__sel(s(z0),cons(z1,z2)) -> a__sel(mark(z0),mark(z2)) a__zWquot(z0,z1) -> zWquot(z0,z1) a__zWquot(z0,nil()) -> nil() a__zWquot(cons(z0,z1),cons(z2,z3)) -> cons(a__quot(mark(z0),mark(z2)),zWquot(z1,z3)) a__zWquot(nil(),z0) -> nil() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(minus(z0,z1)) -> a__minus(mark(z0),mark(z1)) mark(nil()) -> nil() mark(quot(z0,z1)) -> a__quot(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(zWquot(z0,z1)) -> a__zWquot(mark(z0),mark(z1)) - Signature: {A__FROM/1,A__MINUS/2,A__QUOT/2,A__SEL/2,A__ZWQUOT/2,MARK/1,a__from/1,a__minus/2,a__quot/2,a__sel/2 ,a__zWquot/2,mark/1} / {0/0,c/1,c1/0,c10/0,c11/3,c12/3,c13/2,c14/0,c15/0,c16/0,c17/2,c18/2,c19/0,c2/1,c20/2 ,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/2,c29/1,c3/2,c30/1,c31/0,c32/0,c4/2,c5/0,c6/0,c7/2,c8/2,c9/0 ,cons/2,from/1,minus/2,nil/0,quot/2,s/1,sel/2,zWquot/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__FROM,A__MINUS,A__QUOT,A__SEL,A__ZWQUOT,MARK,a__from ,a__minus,a__quot,a__sel,a__zWquot,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,c4,c5,c6,c7,c8,c9,cons,from,minus,nil,quot,s,sel ,zWquot} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__FROM(z0) -> c(MARK(z0)) A__FROM(z0) -> c1() A__MINUS(z0,z1) -> c9() A__MINUS(z0,0()) -> c6() A__MINUS(s(z0),s(z1)) -> c7(A__MINUS(mark(z0),mark(z1)),MARK(z0)) A__MINUS(s(z0),s(z1)) -> c8(A__MINUS(mark(z0),mark(z1)),MARK(z1)) A__QUOT(z0,z1) -> c14() A__QUOT(0(),s(z0)) -> c10() A__QUOT(s(z0),s(z1)) -> c11(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))) ,A__MINUS(mark(z0),mark(z1)) ,MARK(z0)) A__QUOT(s(z0),s(z1)) -> c12(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))) ,A__MINUS(mark(z0),mark(z1)) ,MARK(z1)) A__QUOT(s(z0),s(z1)) -> c13(A__QUOT(a__minus(mark(z0),mark(z1)),s(mark(z1))),MARK(z1)) A__SEL(z0,z1) -> c5() A__SEL(0(),cons(z0,z1)) -> c2(MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c3(A__SEL(mark(z0),mark(z2)),MARK(z0)) A__SEL(s(z0),cons(z1,z2)) -> c4(A__SEL(mark(z0),mark(z2)),MARK(z2)) A__ZWQUOT(z0,z1) -> c19() A__ZWQUOT(z0,nil()) -> c15() A__ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c17(A__QUOT(mark(z0),mark(z2)),MARK(z0)) A__ZWQUOT(cons(z0,z1),cons(z2,z3)) -> c18(A__QUOT(mark(z0),mark(z2)),MARK(z2)) A__ZWQUOT(nil(),z0) -> c16() MARK(0()) -> c31() MARK(cons(z0,z1)) -> c29(MARK(z0)) MARK(from(z0)) -> c20(A__FROM(mark(z0)),MARK(z0)) MARK(minus(z0,z1)) -> c23(A__MINUS(mark(z0),mark(z1)),MARK(z0)) MARK(minus(z0,z1)) -> c24(A__MINUS(mark(z0),mark(z1)),MARK(z1)) MARK(nil()) -> c32() MARK(quot(z0,z1)) -> c25(A__QUOT(mark(z0),mark(z1)),MARK(z0)) MARK(quot(z0,z1)) -> c26(A__QUOT(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c30(MARK(z0)) MARK(sel(z0,z1)) -> c21(A__SEL(mark(z0),mark(z1)),MARK(z0)) MARK(sel(z0,z1)) -> c22(A__SEL(mark(z0),mark(z1)),MARK(z1)) MARK(zWquot(z0,z1)) -> c27(A__ZWQUOT(mark(z0),mark(z1)),MARK(z0)) MARK(zWquot(z0,z1)) -> c28(A__ZWQUOT(mark(z0),mark(z1)),MARK(z1)) - Weak TRS: a__from(z0) -> cons(mark(z0),from(s(z0))) a__from(z0) -> from(z0) a__minus(z0,z1) -> minus(z0,z1) a__minus(z0,0()) -> 0() a__minus(s(z0),s(z1)) -> a__minus(mark(z0),mark(z1)) a__quot(z0,z1) -> quot(z0,z1) a__quot(0(),s(z0)) -> 0() a__quot(s(z0),s(z1)) -> s(a__quot(a__minus(mark(z0),mark(z1)),s(mark(z1)))) a__sel(z0,z1) -> sel(z0,z1) a__sel(0(),cons(z0,z1)) -> mark(z0) a__sel(s(z0),cons(z1,z2)) -> a__sel(mark(z0),mark(z2)) a__zWquot(z0,z1) -> zWquot(z0,z1) a__zWquot(z0,nil()) -> nil() a__zWquot(cons(z0,z1),cons(z2,z3)) -> cons(a__quot(mark(z0),mark(z2)),zWquot(z1,z3)) a__zWquot(nil(),z0) -> nil() mark(0()) -> 0() mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(from(z0)) -> a__from(mark(z0)) mark(minus(z0,z1)) -> a__minus(mark(z0),mark(z1)) mark(nil()) -> nil() mark(quot(z0,z1)) -> a__quot(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(zWquot(z0,z1)) -> a__zWquot(mark(z0),mark(z1)) - Signature: {A__FROM/1,A__MINUS/2,A__QUOT/2,A__SEL/2,A__ZWQUOT/2,MARK/1,a__from/1,a__minus/2,a__quot/2,a__sel/2 ,a__zWquot/2,mark/1} / {0/0,c/1,c1/0,c10/0,c11/3,c12/3,c13/2,c14/0,c15/0,c16/0,c17/2,c18/2,c19/0,c2/1,c20/2 ,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/2,c28/2,c29/1,c3/2,c30/1,c31/0,c32/0,c4/2,c5/0,c6/0,c7/2,c8/2,c9/0 ,cons/2,from/1,minus/2,nil/0,quot/2,s/1,sel/2,zWquot/2} - Obligation: innermost runtime complexity wrt. defined symbols {A__FROM,A__MINUS,A__QUOT,A__SEL,A__ZWQUOT,MARK,a__from ,a__minus,a__quot,a__sel,a__zWquot,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,c4,c5,c6,c7,c8,c9,cons,from,minus,nil,quot,s,sel ,zWquot} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> cons(x,y)} = MARK(cons(x,y)) ->^+ c29(MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)