WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c21() A() -> c22() GE(z0,0()) -> c18() GE(0(),s(z0)) -> c19() GE(s(z0),s(z1)) -> c20(GE(z0,z1)) HEAD(cons(z0,z1)) -> c15() HEAD(nil()) -> c14() IFPROD(false(),z0,z1) -> c4(PRODITER(tail(z0),times(z1,head(z0))),TAIL(z0)) IFPROD(false(),z0,z1) -> c5(PRODITER(tail(z0),times(z1,head(z0))),TIMES(z1,head(z0)),HEAD(z0)) IFPROD(true(),z0,z1) -> c3() IFTIMES(false(),z0,z1,z2,z3) -> c11(TIMESITER(z0,z1,plus(z1,z2),s(z3)),PLUS(z1,z2)) IFTIMES(true(),z0,z1,z2,z3) -> c10() ISEMPTY(cons(z0,z1)) -> c13() ISEMPTY(nil()) -> c12() PLUS(0(),z0) -> c6() PLUS(s(z0),z1) -> c7(PLUS(z0,z1)) PROD(z0) -> c1(PRODITER(z0,s(0()))) PRODITER(z0,z1) -> c2(IFPROD(isempty(z0),z0,z1),ISEMPTY(z0)) TAIL(cons(z0,z1)) -> c17() TAIL(nil()) -> c16() TIMES(z0,z1) -> c8(TIMESITER(z0,z1,0(),0())) TIMESITER(z0,z1,z2,z3) -> c9(IFTIMES(ge(z3,z0),z0,z1,z2,z3),GE(z3,z0)) - Weak TRS: a() -> b() a() -> c() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) head(cons(z0,z1)) -> z0 head(nil()) -> error() ifProd(false(),z0,z1) -> prodIter(tail(z0),times(z1,head(z0))) ifProd(true(),z0,z1) -> z1 ifTimes(false(),z0,z1,z2,z3) -> timesIter(z0,z1,plus(z1,z2),s(z3)) ifTimes(true(),z0,z1,z2,z3) -> z2 isempty(cons(z0,z1)) -> false() isempty(nil()) -> true() plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) prod(z0) -> prodIter(z0,s(0())) prodIter(z0,z1) -> ifProd(isempty(z0),z0,z1) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() times(z0,z1) -> timesIter(z0,z1,0(),0()) timesIter(z0,z1,z2,z3) -> ifTimes(ge(z3,z0),z0,z1,z2,z3) - Signature: {A/0,GE/2,HEAD/1,IFPROD/3,IFTIMES/5,ISEMPTY/1,PLUS/2,PROD/1,PRODITER/2,TAIL/1,TIMES/2,TIMESITER/4,a/0,ge/2 ,head/1,ifProd/3,ifTimes/5,isempty/1,plus/2,prod/1,prodIter/2,tail/1,times/2,timesIter/4} / {0/0,b/0,c/0 ,c1/1,c10/0,c11/2,c12/0,c13/0,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/2,c20/1,c21/0,c22/0,c3/0,c4/2,c5/3,c6/0 ,c7/1,c8/1,c9/2,cons/2,error/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,GE,HEAD,IFPROD,IFTIMES,ISEMPTY,PLUS,PROD,PRODITER,TAIL ,TIMES,TIMESITER,a,ge,head,ifProd,ifTimes,isempty,plus,prod,prodIter,tail,times ,timesIter} and constructors {0,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3,c4,c5,c6,c7 ,c8,c9,cons,error,false,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c21() A() -> c22() GE(z0,0()) -> c18() GE(0(),s(z0)) -> c19() GE(s(z0),s(z1)) -> c20(GE(z0,z1)) HEAD(cons(z0,z1)) -> c15() HEAD(nil()) -> c14() IFPROD(false(),z0,z1) -> c4(PRODITER(tail(z0),times(z1,head(z0))),TAIL(z0)) IFPROD(false(),z0,z1) -> c5(PRODITER(tail(z0),times(z1,head(z0))),TIMES(z1,head(z0)),HEAD(z0)) IFPROD(true(),z0,z1) -> c3() IFTIMES(false(),z0,z1,z2,z3) -> c11(TIMESITER(z0,z1,plus(z1,z2),s(z3)),PLUS(z1,z2)) IFTIMES(true(),z0,z1,z2,z3) -> c10() ISEMPTY(cons(z0,z1)) -> c13() ISEMPTY(nil()) -> c12() PLUS(0(),z0) -> c6() PLUS(s(z0),z1) -> c7(PLUS(z0,z1)) PROD(z0) -> c1(PRODITER(z0,s(0()))) PRODITER(z0,z1) -> c2(IFPROD(isempty(z0),z0,z1),ISEMPTY(z0)) TAIL(cons(z0,z1)) -> c17() TAIL(nil()) -> c16() TIMES(z0,z1) -> c8(TIMESITER(z0,z1,0(),0())) TIMESITER(z0,z1,z2,z3) -> c9(IFTIMES(ge(z3,z0),z0,z1,z2,z3),GE(z3,z0)) - Weak TRS: a() -> b() a() -> c() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) head(cons(z0,z1)) -> z0 head(nil()) -> error() ifProd(false(),z0,z1) -> prodIter(tail(z0),times(z1,head(z0))) ifProd(true(),z0,z1) -> z1 ifTimes(false(),z0,z1,z2,z3) -> timesIter(z0,z1,plus(z1,z2),s(z3)) ifTimes(true(),z0,z1,z2,z3) -> z2 isempty(cons(z0,z1)) -> false() isempty(nil()) -> true() plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) prod(z0) -> prodIter(z0,s(0())) prodIter(z0,z1) -> ifProd(isempty(z0),z0,z1) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() times(z0,z1) -> timesIter(z0,z1,0(),0()) timesIter(z0,z1,z2,z3) -> ifTimes(ge(z3,z0),z0,z1,z2,z3) - Signature: {A/0,GE/2,HEAD/1,IFPROD/3,IFTIMES/5,ISEMPTY/1,PLUS/2,PROD/1,PRODITER/2,TAIL/1,TIMES/2,TIMESITER/4,a/0,ge/2 ,head/1,ifProd/3,ifTimes/5,isempty/1,plus/2,prod/1,prodIter/2,tail/1,times/2,timesIter/4} / {0/0,b/0,c/0 ,c1/1,c10/0,c11/2,c12/0,c13/0,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/2,c20/1,c21/0,c22/0,c3/0,c4/2,c5/3,c6/0 ,c7/1,c8/1,c9/2,cons/2,error/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,GE,HEAD,IFPROD,IFTIMES,ISEMPTY,PLUS,PROD,PRODITER,TAIL ,TIMES,TIMESITER,a,ge,head,ifProd,ifTimes,isempty,plus,prod,prodIter,tail,times ,timesIter} and constructors {0,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3,c4,c5,c6,c7 ,c8,c9,cons,error,false,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c21() A() -> c22() GE(z0,0()) -> c18() GE(0(),s(z0)) -> c19() GE(s(z0),s(z1)) -> c20(GE(z0,z1)) HEAD(cons(z0,z1)) -> c15() HEAD(nil()) -> c14() IFPROD(false(),z0,z1) -> c4(PRODITER(tail(z0),times(z1,head(z0))),TAIL(z0)) IFPROD(false(),z0,z1) -> c5(PRODITER(tail(z0),times(z1,head(z0))),TIMES(z1,head(z0)),HEAD(z0)) IFPROD(true(),z0,z1) -> c3() IFTIMES(false(),z0,z1,z2,z3) -> c11(TIMESITER(z0,z1,plus(z1,z2),s(z3)),PLUS(z1,z2)) IFTIMES(true(),z0,z1,z2,z3) -> c10() ISEMPTY(cons(z0,z1)) -> c13() ISEMPTY(nil()) -> c12() PLUS(0(),z0) -> c6() PLUS(s(z0),z1) -> c7(PLUS(z0,z1)) PROD(z0) -> c1(PRODITER(z0,s(0()))) PRODITER(z0,z1) -> c2(IFPROD(isempty(z0),z0,z1),ISEMPTY(z0)) TAIL(cons(z0,z1)) -> c17() TAIL(nil()) -> c16() TIMES(z0,z1) -> c8(TIMESITER(z0,z1,0(),0())) TIMESITER(z0,z1,z2,z3) -> c9(IFTIMES(ge(z3,z0),z0,z1,z2,z3),GE(z3,z0)) - Weak TRS: a() -> b() a() -> c() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) head(cons(z0,z1)) -> z0 head(nil()) -> error() ifProd(false(),z0,z1) -> prodIter(tail(z0),times(z1,head(z0))) ifProd(true(),z0,z1) -> z1 ifTimes(false(),z0,z1,z2,z3) -> timesIter(z0,z1,plus(z1,z2),s(z3)) ifTimes(true(),z0,z1,z2,z3) -> z2 isempty(cons(z0,z1)) -> false() isempty(nil()) -> true() plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) prod(z0) -> prodIter(z0,s(0())) prodIter(z0,z1) -> ifProd(isempty(z0),z0,z1) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() times(z0,z1) -> timesIter(z0,z1,0(),0()) timesIter(z0,z1,z2,z3) -> ifTimes(ge(z3,z0),z0,z1,z2,z3) - Signature: {A/0,GE/2,HEAD/1,IFPROD/3,IFTIMES/5,ISEMPTY/1,PLUS/2,PROD/1,PRODITER/2,TAIL/1,TIMES/2,TIMESITER/4,a/0,ge/2 ,head/1,ifProd/3,ifTimes/5,isempty/1,plus/2,prod/1,prodIter/2,tail/1,times/2,timesIter/4} / {0/0,b/0,c/0 ,c1/1,c10/0,c11/2,c12/0,c13/0,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/2,c20/1,c21/0,c22/0,c3/0,c4/2,c5/3,c6/0 ,c7/1,c8/1,c9/2,cons/2,error/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,GE,HEAD,IFPROD,IFTIMES,ISEMPTY,PLUS,PROD,PRODITER,TAIL ,TIMES,TIMESITER,a,ge,head,ifProd,ifTimes,isempty,plus,prod,prodIter,tail,times ,timesIter} and constructors {0,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3,c4,c5,c6,c7 ,c8,c9,cons,error,false,nil,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: GE(x,y){x -> s(x),y -> s(y)} = GE(s(x),s(y)) ->^+ c20(GE(x,y)) = C[GE(x,y) = GE(x,y){}] WORST_CASE(Omega(n^1),?)