WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c25() A() -> c26() DIV(z0,z1,0()) -> c22(DIVISIBLE(z0,z1)) DIV(0(),z0,s(z1)) -> c23() DIV(s(z0),z1,s(z2)) -> c24(DIV(z0,z1,z2)) DIVISIBLE(0(),s(z0)) -> c20() DIVISIBLE(s(z0),s(z1)) -> c21(DIV(s(z0),s(z1),s(z1))) GE(z0,0()) -> c15() GE(0(),s(z0)) -> c16() GE(s(z0),s(z1)) -> c17(GE(z0,z1)) IF(false(),z0,z1,z2,z3) -> c5(IF2(divisible(z2,z1),z0,z1,z2,z3),DIVISIBLE(z2,z1)) IF(true(),z0,z1,z2,z3) -> c4() IF2(false(),z0,z1,z2,z3) -> c7(LCMITER(z0,z1,plus(z0,z2),z3),PLUS(z0,z2)) IF2(true(),z0,z1,z2,z3) -> c6() IFTIMES(false(),z0,z1) -> c12(PLUS(z1,times(z1,p(z0))),TIMES(z1,p(z0)),P(z0)) IFTIMES(true(),z0,z1) -> c11() LCM(z0,z1) -> c1(LCMITER(z0,z1,0(),times(z0,z1)),TIMES(z0,z1)) LCMITER(z0,z1,z2,z3) -> c2(IF(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3),OR(ge(0(),z0),ge(z2,z3)),GE(0(),z0)) LCMITER(z0,z1,z2,z3) -> c3(IF(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3),OR(ge(0(),z0),ge(z2,z3)),GE(z2,z3)) OR(false(),z0) -> c19() OR(true(),z0) -> c18() P(0()) -> c14() P(s(z0)) -> c13() PLUS(0(),z0) -> c8() PLUS(s(z0),z1) -> c9(PLUS(z0,z1)) TIMES(z0,z1) -> c10(IFTIMES(ge(0(),z0),z0,z1),GE(0(),z0)) - Weak TRS: a() -> b() a() -> c() div(z0,z1,0()) -> divisible(z0,z1) div(0(),z0,s(z1)) -> false() div(s(z0),z1,s(z2)) -> div(z0,z1,z2) divisible(0(),s(z0)) -> true() divisible(s(z0),s(z1)) -> div(s(z0),s(z1),s(z1)) ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) if(false(),z0,z1,z2,z3) -> if2(divisible(z2,z1),z0,z1,z2,z3) if(true(),z0,z1,z2,z3) -> z2 if2(false(),z0,z1,z2,z3) -> lcmIter(z0,z1,plus(z0,z2),z3) if2(true(),z0,z1,z2,z3) -> z2 ifTimes(false(),z0,z1) -> plus(z1,times(z1,p(z0))) ifTimes(true(),z0,z1) -> 0() lcm(z0,z1) -> lcmIter(z0,z1,0(),times(z0,z1)) lcmIter(z0,z1,z2,z3) -> if(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3) or(false(),z0) -> z0 or(true(),z0) -> true() p(0()) -> s(s(0())) p(s(z0)) -> z0 plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) times(z0,z1) -> ifTimes(ge(0(),z0),z0,z1) - Signature: {A/0,DIV/3,DIVISIBLE/2,GE/2,IF/5,IF2/5,IFTIMES/3,LCM/2,LCMITER/4,OR/2,P/1,PLUS/2,TIMES/2,a/0,div/3 ,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2} / {0/0,b/0,c/0,c1/2,c10/2 ,c11/0,c12/3,c13/0,c14/0,c15/0,c16/0,c17/1,c18/0,c19/0,c2/3,c20/0,c21/1,c22/1,c23/0,c24/1,c25/0,c26/0,c3/3 ,c4/0,c5/2,c6/0,c7/2,c8/0,c9/1,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,DIV,DIVISIBLE,GE,IF,IF2,IFTIMES,LCM,LCMITER,OR,P,PLUS ,TIMES,a,div,divisible,ge,if,if2,ifTimes,lcm,lcmIter,or,p,plus,times} and constructors {0,b,c,c1,c10,c11,c12 ,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c25() A() -> c26() DIV(z0,z1,0()) -> c22(DIVISIBLE(z0,z1)) DIV(0(),z0,s(z1)) -> c23() DIV(s(z0),z1,s(z2)) -> c24(DIV(z0,z1,z2)) DIVISIBLE(0(),s(z0)) -> c20() DIVISIBLE(s(z0),s(z1)) -> c21(DIV(s(z0),s(z1),s(z1))) GE(z0,0()) -> c15() GE(0(),s(z0)) -> c16() GE(s(z0),s(z1)) -> c17(GE(z0,z1)) IF(false(),z0,z1,z2,z3) -> c5(IF2(divisible(z2,z1),z0,z1,z2,z3),DIVISIBLE(z2,z1)) IF(true(),z0,z1,z2,z3) -> c4() IF2(false(),z0,z1,z2,z3) -> c7(LCMITER(z0,z1,plus(z0,z2),z3),PLUS(z0,z2)) IF2(true(),z0,z1,z2,z3) -> c6() IFTIMES(false(),z0,z1) -> c12(PLUS(z1,times(z1,p(z0))),TIMES(z1,p(z0)),P(z0)) IFTIMES(true(),z0,z1) -> c11() LCM(z0,z1) -> c1(LCMITER(z0,z1,0(),times(z0,z1)),TIMES(z0,z1)) LCMITER(z0,z1,z2,z3) -> c2(IF(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3),OR(ge(0(),z0),ge(z2,z3)),GE(0(),z0)) LCMITER(z0,z1,z2,z3) -> c3(IF(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3),OR(ge(0(),z0),ge(z2,z3)),GE(z2,z3)) OR(false(),z0) -> c19() OR(true(),z0) -> c18() P(0()) -> c14() P(s(z0)) -> c13() PLUS(0(),z0) -> c8() PLUS(s(z0),z1) -> c9(PLUS(z0,z1)) TIMES(z0,z1) -> c10(IFTIMES(ge(0(),z0),z0,z1),GE(0(),z0)) - Weak TRS: a() -> b() a() -> c() div(z0,z1,0()) -> divisible(z0,z1) div(0(),z0,s(z1)) -> false() div(s(z0),z1,s(z2)) -> div(z0,z1,z2) divisible(0(),s(z0)) -> true() divisible(s(z0),s(z1)) -> div(s(z0),s(z1),s(z1)) ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) if(false(),z0,z1,z2,z3) -> if2(divisible(z2,z1),z0,z1,z2,z3) if(true(),z0,z1,z2,z3) -> z2 if2(false(),z0,z1,z2,z3) -> lcmIter(z0,z1,plus(z0,z2),z3) if2(true(),z0,z1,z2,z3) -> z2 ifTimes(false(),z0,z1) -> plus(z1,times(z1,p(z0))) ifTimes(true(),z0,z1) -> 0() lcm(z0,z1) -> lcmIter(z0,z1,0(),times(z0,z1)) lcmIter(z0,z1,z2,z3) -> if(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3) or(false(),z0) -> z0 or(true(),z0) -> true() p(0()) -> s(s(0())) p(s(z0)) -> z0 plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) times(z0,z1) -> ifTimes(ge(0(),z0),z0,z1) - Signature: {A/0,DIV/3,DIVISIBLE/2,GE/2,IF/5,IF2/5,IFTIMES/3,LCM/2,LCMITER/4,OR/2,P/1,PLUS/2,TIMES/2,a/0,div/3 ,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2} / {0/0,b/0,c/0,c1/2,c10/2 ,c11/0,c12/3,c13/0,c14/0,c15/0,c16/0,c17/1,c18/0,c19/0,c2/3,c20/0,c21/1,c22/1,c23/0,c24/1,c25/0,c26/0,c3/3 ,c4/0,c5/2,c6/0,c7/2,c8/0,c9/1,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,DIV,DIVISIBLE,GE,IF,IF2,IFTIMES,LCM,LCMITER,OR,P,PLUS ,TIMES,a,div,divisible,ge,if,if2,ifTimes,lcm,lcmIter,or,p,plus,times} and constructors {0,b,c,c1,c10,c11,c12 ,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c25() A() -> c26() DIV(z0,z1,0()) -> c22(DIVISIBLE(z0,z1)) DIV(0(),z0,s(z1)) -> c23() DIV(s(z0),z1,s(z2)) -> c24(DIV(z0,z1,z2)) DIVISIBLE(0(),s(z0)) -> c20() DIVISIBLE(s(z0),s(z1)) -> c21(DIV(s(z0),s(z1),s(z1))) GE(z0,0()) -> c15() GE(0(),s(z0)) -> c16() GE(s(z0),s(z1)) -> c17(GE(z0,z1)) IF(false(),z0,z1,z2,z3) -> c5(IF2(divisible(z2,z1),z0,z1,z2,z3),DIVISIBLE(z2,z1)) IF(true(),z0,z1,z2,z3) -> c4() IF2(false(),z0,z1,z2,z3) -> c7(LCMITER(z0,z1,plus(z0,z2),z3),PLUS(z0,z2)) IF2(true(),z0,z1,z2,z3) -> c6() IFTIMES(false(),z0,z1) -> c12(PLUS(z1,times(z1,p(z0))),TIMES(z1,p(z0)),P(z0)) IFTIMES(true(),z0,z1) -> c11() LCM(z0,z1) -> c1(LCMITER(z0,z1,0(),times(z0,z1)),TIMES(z0,z1)) LCMITER(z0,z1,z2,z3) -> c2(IF(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3),OR(ge(0(),z0),ge(z2,z3)),GE(0(),z0)) LCMITER(z0,z1,z2,z3) -> c3(IF(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3),OR(ge(0(),z0),ge(z2,z3)),GE(z2,z3)) OR(false(),z0) -> c19() OR(true(),z0) -> c18() P(0()) -> c14() P(s(z0)) -> c13() PLUS(0(),z0) -> c8() PLUS(s(z0),z1) -> c9(PLUS(z0,z1)) TIMES(z0,z1) -> c10(IFTIMES(ge(0(),z0),z0,z1),GE(0(),z0)) - Weak TRS: a() -> b() a() -> c() div(z0,z1,0()) -> divisible(z0,z1) div(0(),z0,s(z1)) -> false() div(s(z0),z1,s(z2)) -> div(z0,z1,z2) divisible(0(),s(z0)) -> true() divisible(s(z0),s(z1)) -> div(s(z0),s(z1),s(z1)) ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) if(false(),z0,z1,z2,z3) -> if2(divisible(z2,z1),z0,z1,z2,z3) if(true(),z0,z1,z2,z3) -> z2 if2(false(),z0,z1,z2,z3) -> lcmIter(z0,z1,plus(z0,z2),z3) if2(true(),z0,z1,z2,z3) -> z2 ifTimes(false(),z0,z1) -> plus(z1,times(z1,p(z0))) ifTimes(true(),z0,z1) -> 0() lcm(z0,z1) -> lcmIter(z0,z1,0(),times(z0,z1)) lcmIter(z0,z1,z2,z3) -> if(or(ge(0(),z0),ge(z2,z3)),z0,z1,z2,z3) or(false(),z0) -> z0 or(true(),z0) -> true() p(0()) -> s(s(0())) p(s(z0)) -> z0 plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) times(z0,z1) -> ifTimes(ge(0(),z0),z0,z1) - Signature: {A/0,DIV/3,DIVISIBLE/2,GE/2,IF/5,IF2/5,IFTIMES/3,LCM/2,LCMITER/4,OR/2,P/1,PLUS/2,TIMES/2,a/0,div/3 ,divisible/2,ge/2,if/5,if2/5,ifTimes/3,lcm/2,lcmIter/4,or/2,p/1,plus/2,times/2} / {0/0,b/0,c/0,c1/2,c10/2 ,c11/0,c12/3,c13/0,c14/0,c15/0,c16/0,c17/1,c18/0,c19/0,c2/3,c20/0,c21/1,c22/1,c23/0,c24/1,c25/0,c26/0,c3/3 ,c4/0,c5/2,c6/0,c7/2,c8/0,c9/1,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,DIV,DIVISIBLE,GE,IF,IF2,IFTIMES,LCM,LCMITER,OR,P,PLUS ,TIMES,a,div,divisible,ge,if,if2,ifTimes,lcm,lcmIter,or,p,plus,times} and constructors {0,b,c,c1,c10,c11,c12 ,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: DIV(x,y,z){x -> s(x),z -> s(z)} = DIV(s(x),y,s(z)) ->^+ c24(DIV(x,y,z)) = C[DIV(x,y,z) = DIV(x,y,z){}] WORST_CASE(Omega(n^1),?)