WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c22() A() -> c23() DIV(z0,z1) -> c1(DIV2(z0,z1,0())) DIV2(z0,z1,z2) -> c2(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),LE(z1,0())) DIV2(z0,z1,z2) -> c3(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),LE(z1,z0)) DIV2(z0,z1,z2) -> c4(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),PLUS(z2,0())) DIV2(z0,z1,z2) -> c5(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),INC(z2)) IF1(false(),z0,z1,z2,z3,z4) -> c7(IF2(z0,z1,z2,z3,z4)) IF1(true(),z0,z1,z2,z3,z4) -> c6() IF2(false(),z0,z1,z2,z3) -> c9() IF2(true(),z0,z1,z2,z3) -> c8(DIV2(minus(z0,z1),z1,z3),MINUS(z0,z1)) IFPLUS(false(),z0,z1,z2) -> c21(PLUSITER(z0,s(z1),s(z2))) IFPLUS(true(),z0,z1,z2) -> c20() INC(0()) -> c10() INC(s(z0)) -> c11(INC(z0)) LE(0(),z0) -> c13() LE(s(z0),0()) -> c12() LE(s(z0),s(z1)) -> c14(LE(z0,z1)) MINUS(z0,0()) -> c15() MINUS(0(),z0) -> c16() MINUS(s(z0),s(z1)) -> c17(MINUS(z0,z1)) PLUS(z0,z1) -> c18(PLUSITER(z0,z1,0())) PLUSITER(z0,z1,z2) -> c19(IFPLUS(le(z0,z2),z0,z1,z2),LE(z0,z2)) - Weak TRS: a() -> c() a() -> d() div(z0,z1) -> div2(z0,z1,0()) div2(z0,z1,z2) -> if1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)) if1(false(),z0,z1,z2,z3,z4) -> if2(z0,z1,z2,z3,z4) if1(true(),z0,z1,z2,z3,z4) -> divZeroError() if2(false(),z0,z1,z2,z3) -> z2 if2(true(),z0,z1,z2,z3) -> div2(minus(z0,z1),z1,z3) ifPlus(false(),z0,z1,z2) -> plusIter(z0,s(z1),s(z2)) ifPlus(true(),z0,z1,z2) -> z1 inc(0()) -> 0() inc(s(z0)) -> s(inc(z0)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) minus(z0,0()) -> z0 minus(0(),z0) -> 0() minus(s(z0),s(z1)) -> minus(z0,z1) plus(z0,z1) -> plusIter(z0,z1,0()) plusIter(z0,z1,z2) -> ifPlus(le(z0,z2),z0,z1,z2) - Signature: {A/0,DIV/2,DIV2/3,IF1/6,IF2/5,IFPLUS/4,INC/1,LE/2,MINUS/2,PLUS/2,PLUSITER/3,a/0,div/2,div2/3,if1/6,if2/5 ,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3} / {0/0,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/1,c15/0,c16/0 ,c17/1,c18/1,c19/2,c2/2,c20/0,c21/1,c22/0,c23/0,c3/2,c4/2,c5/2,c6/0,c7/1,c8/2,c9/0,d/0,divZeroError/0 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,DIV,DIV2,IF1,IF2,IFPLUS,INC,LE,MINUS,PLUS,PLUSITER,a ,div,div2,if1,if2,ifPlus,inc,le,minus,plus,plusIter} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9,d,divZeroError,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c22() A() -> c23() DIV(z0,z1) -> c1(DIV2(z0,z1,0())) DIV2(z0,z1,z2) -> c2(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),LE(z1,0())) DIV2(z0,z1,z2) -> c3(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),LE(z1,z0)) DIV2(z0,z1,z2) -> c4(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),PLUS(z2,0())) DIV2(z0,z1,z2) -> c5(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),INC(z2)) IF1(false(),z0,z1,z2,z3,z4) -> c7(IF2(z0,z1,z2,z3,z4)) IF1(true(),z0,z1,z2,z3,z4) -> c6() IF2(false(),z0,z1,z2,z3) -> c9() IF2(true(),z0,z1,z2,z3) -> c8(DIV2(minus(z0,z1),z1,z3),MINUS(z0,z1)) IFPLUS(false(),z0,z1,z2) -> c21(PLUSITER(z0,s(z1),s(z2))) IFPLUS(true(),z0,z1,z2) -> c20() INC(0()) -> c10() INC(s(z0)) -> c11(INC(z0)) LE(0(),z0) -> c13() LE(s(z0),0()) -> c12() LE(s(z0),s(z1)) -> c14(LE(z0,z1)) MINUS(z0,0()) -> c15() MINUS(0(),z0) -> c16() MINUS(s(z0),s(z1)) -> c17(MINUS(z0,z1)) PLUS(z0,z1) -> c18(PLUSITER(z0,z1,0())) PLUSITER(z0,z1,z2) -> c19(IFPLUS(le(z0,z2),z0,z1,z2),LE(z0,z2)) - Weak TRS: a() -> c() a() -> d() div(z0,z1) -> div2(z0,z1,0()) div2(z0,z1,z2) -> if1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)) if1(false(),z0,z1,z2,z3,z4) -> if2(z0,z1,z2,z3,z4) if1(true(),z0,z1,z2,z3,z4) -> divZeroError() if2(false(),z0,z1,z2,z3) -> z2 if2(true(),z0,z1,z2,z3) -> div2(minus(z0,z1),z1,z3) ifPlus(false(),z0,z1,z2) -> plusIter(z0,s(z1),s(z2)) ifPlus(true(),z0,z1,z2) -> z1 inc(0()) -> 0() inc(s(z0)) -> s(inc(z0)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) minus(z0,0()) -> z0 minus(0(),z0) -> 0() minus(s(z0),s(z1)) -> minus(z0,z1) plus(z0,z1) -> plusIter(z0,z1,0()) plusIter(z0,z1,z2) -> ifPlus(le(z0,z2),z0,z1,z2) - Signature: {A/0,DIV/2,DIV2/3,IF1/6,IF2/5,IFPLUS/4,INC/1,LE/2,MINUS/2,PLUS/2,PLUSITER/3,a/0,div/2,div2/3,if1/6,if2/5 ,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3} / {0/0,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/1,c15/0,c16/0 ,c17/1,c18/1,c19/2,c2/2,c20/0,c21/1,c22/0,c23/0,c3/2,c4/2,c5/2,c6/0,c7/1,c8/2,c9/0,d/0,divZeroError/0 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,DIV,DIV2,IF1,IF2,IFPLUS,INC,LE,MINUS,PLUS,PLUSITER,a ,div,div2,if1,if2,ifPlus,inc,le,minus,plus,plusIter} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9,d,divZeroError,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c22() A() -> c23() DIV(z0,z1) -> c1(DIV2(z0,z1,0())) DIV2(z0,z1,z2) -> c2(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),LE(z1,0())) DIV2(z0,z1,z2) -> c3(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),LE(z1,z0)) DIV2(z0,z1,z2) -> c4(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),PLUS(z2,0())) DIV2(z0,z1,z2) -> c5(IF1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)),INC(z2)) IF1(false(),z0,z1,z2,z3,z4) -> c7(IF2(z0,z1,z2,z3,z4)) IF1(true(),z0,z1,z2,z3,z4) -> c6() IF2(false(),z0,z1,z2,z3) -> c9() IF2(true(),z0,z1,z2,z3) -> c8(DIV2(minus(z0,z1),z1,z3),MINUS(z0,z1)) IFPLUS(false(),z0,z1,z2) -> c21(PLUSITER(z0,s(z1),s(z2))) IFPLUS(true(),z0,z1,z2) -> c20() INC(0()) -> c10() INC(s(z0)) -> c11(INC(z0)) LE(0(),z0) -> c13() LE(s(z0),0()) -> c12() LE(s(z0),s(z1)) -> c14(LE(z0,z1)) MINUS(z0,0()) -> c15() MINUS(0(),z0) -> c16() MINUS(s(z0),s(z1)) -> c17(MINUS(z0,z1)) PLUS(z0,z1) -> c18(PLUSITER(z0,z1,0())) PLUSITER(z0,z1,z2) -> c19(IFPLUS(le(z0,z2),z0,z1,z2),LE(z0,z2)) - Weak TRS: a() -> c() a() -> d() div(z0,z1) -> div2(z0,z1,0()) div2(z0,z1,z2) -> if1(le(z1,0()),le(z1,z0),z0,z1,plus(z2,0()),inc(z2)) if1(false(),z0,z1,z2,z3,z4) -> if2(z0,z1,z2,z3,z4) if1(true(),z0,z1,z2,z3,z4) -> divZeroError() if2(false(),z0,z1,z2,z3) -> z2 if2(true(),z0,z1,z2,z3) -> div2(minus(z0,z1),z1,z3) ifPlus(false(),z0,z1,z2) -> plusIter(z0,s(z1),s(z2)) ifPlus(true(),z0,z1,z2) -> z1 inc(0()) -> 0() inc(s(z0)) -> s(inc(z0)) le(0(),z0) -> true() le(s(z0),0()) -> false() le(s(z0),s(z1)) -> le(z0,z1) minus(z0,0()) -> z0 minus(0(),z0) -> 0() minus(s(z0),s(z1)) -> minus(z0,z1) plus(z0,z1) -> plusIter(z0,z1,0()) plusIter(z0,z1,z2) -> ifPlus(le(z0,z2),z0,z1,z2) - Signature: {A/0,DIV/2,DIV2/3,IF1/6,IF2/5,IFPLUS/4,INC/1,LE/2,MINUS/2,PLUS/2,PLUSITER/3,a/0,div/2,div2/3,if1/6,if2/5 ,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3} / {0/0,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/1,c15/0,c16/0 ,c17/1,c18/1,c19/2,c2/2,c20/0,c21/1,c22/0,c23/0,c3/2,c4/2,c5/2,c6/0,c7/1,c8/2,c9/0,d/0,divZeroError/0 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,DIV,DIV2,IF1,IF2,IFPLUS,INC,LE,MINUS,PLUS,PLUSITER,a ,div,div2,if1,if2,ifPlus,inc,le,minus,plus,plusIter} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c20,c21,c22,c23,c3,c4,c5,c6,c7,c8,c9,d,divZeroError,false,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: INC(x){x -> s(x)} = INC(s(x)) ->^+ c11(INC(x)) = C[INC(x) = INC(x){}] WORST_CASE(Omega(n^1),?)