WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A() -> c29() A() -> c30() GE(z0,0()) -> c26() GE(0(),s(z0)) -> c27() GE(s(z0),s(z1)) -> c28(GE(z0,z1)) GEN(z0,z1,z2) -> c3(IF(ge(z2,z0),z0,z1,z2),GE(z2,z0)) GENERATE(z0,z1) -> c2(GEN(z0,z1,0())) HEAD(cons(z0,z1)) -> c18() HEAD(nil()) -> c19() IF(false(),z0,z1,z2) -> c5(GEN(z0,z1,s(z2))) IF(true(),z0,z1,z2) -> c4() IFSUM(false(),z0,z1,z2) -> c10(IFSUM2(z0,z1,z2)) IFSUM(true(),z0,z1,z2) -> c9() IFSUM2(false(),z0,z1) -> c12(SUM2(cons(p(head(z0)),tail(z0)),s(z1)),P(head(z0)),HEAD(z0)) IFSUM2(false(),z0,z1) -> c13(SUM2(cons(p(head(z0)),tail(z0)),s(z1)),TAIL(z0)) IFSUM2(true(),z0,z1) -> c11(SUM2(tail(z0),z1),TAIL(z0)) ISNIL(cons(z0,z1)) -> c15() ISNIL(nil()) -> c14() ISZERO(0()) -> c20() ISZERO(s(0())) -> c21() ISZERO(s(s(z0))) -> c22(ISZERO(s(z0))) P(0()) -> c23() P(s(0())) -> c24() P(s(s(z0))) -> c25(P(s(z0))) SUM(z0) -> c6(SUM2(z0,0())) SUM2(z0,z1) -> c7(IFSUM(isNil(z0),isZero(head(z0)),z0,z1),ISNIL(z0)) SUM2(z0,z1) -> c8(IFSUM(isNil(z0),isZero(head(z0)),z0,z1),ISZERO(head(z0)),HEAD(z0)) TAIL(cons(z0,z1)) -> c17() TAIL(nil()) -> c16() TIMES(z0,z1) -> c1(SUM(generate(z0,z1)),GENERATE(z0,z1)) - Weak TRS: a() -> c() a() -> d() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) gen(z0,z1,z2) -> if(ge(z2,z0),z0,z1,z2) generate(z0,z1) -> gen(z0,z1,0()) head(cons(z0,z1)) -> z0 head(nil()) -> error() if(false(),z0,z1,z2) -> cons(z1,gen(z0,z1,s(z2))) if(true(),z0,z1,z2) -> nil() ifsum(false(),z0,z1,z2) -> ifsum2(z0,z1,z2) ifsum(true(),z0,z1,z2) -> z2 ifsum2(false(),z0,z1) -> sum2(cons(p(head(z0)),tail(z0)),s(z1)) ifsum2(true(),z0,z1) -> sum2(tail(z0),z1) isNil(cons(z0,z1)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(z0))) -> isZero(s(z0)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(z0))) -> s(p(s(z0))) sum(z0) -> sum2(z0,0()) sum2(z0,z1) -> ifsum(isNil(z0),isZero(head(z0)),z0,z1) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() times(z0,z1) -> sum(generate(z0,z1)) - Signature: {A/0,GE/2,GEN/3,GENERATE/2,HEAD/1,IF/4,IFSUM/4,IFSUM2/3,ISNIL/1,ISZERO/1,P/1,SUM/1,SUM2/2,TAIL/1,TIMES/2,a/0 ,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2} / {0/0 ,c/0,c1/2,c10/1,c11/2,c12/3,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/1,c20/0,c21/0,c22/1,c23/0,c24/0 ,c25/1,c26/0,c27/0,c28/1,c29/0,c3/2,c30/0,c4/0,c5/1,c6/1,c7/2,c8/3,c9/0,cons/2,d/0,error/0,false/0,nil/0,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,GE,GEN,GENERATE,HEAD,IF,IFSUM,IFSUM2,ISNIL,ISZERO,P,SUM ,SUM2,TAIL,TIMES,a,ge,gen,generate,head,if,ifsum,ifsum2,isNil,isZero,p,sum,sum2,tail ,times} 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,c4,c5,c6,c7,c8,c9,cons,d,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() -> c29() A() -> c30() GE(z0,0()) -> c26() GE(0(),s(z0)) -> c27() GE(s(z0),s(z1)) -> c28(GE(z0,z1)) GEN(z0,z1,z2) -> c3(IF(ge(z2,z0),z0,z1,z2),GE(z2,z0)) GENERATE(z0,z1) -> c2(GEN(z0,z1,0())) HEAD(cons(z0,z1)) -> c18() HEAD(nil()) -> c19() IF(false(),z0,z1,z2) -> c5(GEN(z0,z1,s(z2))) IF(true(),z0,z1,z2) -> c4() IFSUM(false(),z0,z1,z2) -> c10(IFSUM2(z0,z1,z2)) IFSUM(true(),z0,z1,z2) -> c9() IFSUM2(false(),z0,z1) -> c12(SUM2(cons(p(head(z0)),tail(z0)),s(z1)),P(head(z0)),HEAD(z0)) IFSUM2(false(),z0,z1) -> c13(SUM2(cons(p(head(z0)),tail(z0)),s(z1)),TAIL(z0)) IFSUM2(true(),z0,z1) -> c11(SUM2(tail(z0),z1),TAIL(z0)) ISNIL(cons(z0,z1)) -> c15() ISNIL(nil()) -> c14() ISZERO(0()) -> c20() ISZERO(s(0())) -> c21() ISZERO(s(s(z0))) -> c22(ISZERO(s(z0))) P(0()) -> c23() P(s(0())) -> c24() P(s(s(z0))) -> c25(P(s(z0))) SUM(z0) -> c6(SUM2(z0,0())) SUM2(z0,z1) -> c7(IFSUM(isNil(z0),isZero(head(z0)),z0,z1),ISNIL(z0)) SUM2(z0,z1) -> c8(IFSUM(isNil(z0),isZero(head(z0)),z0,z1),ISZERO(head(z0)),HEAD(z0)) TAIL(cons(z0,z1)) -> c17() TAIL(nil()) -> c16() TIMES(z0,z1) -> c1(SUM(generate(z0,z1)),GENERATE(z0,z1)) - Weak TRS: a() -> c() a() -> d() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) gen(z0,z1,z2) -> if(ge(z2,z0),z0,z1,z2) generate(z0,z1) -> gen(z0,z1,0()) head(cons(z0,z1)) -> z0 head(nil()) -> error() if(false(),z0,z1,z2) -> cons(z1,gen(z0,z1,s(z2))) if(true(),z0,z1,z2) -> nil() ifsum(false(),z0,z1,z2) -> ifsum2(z0,z1,z2) ifsum(true(),z0,z1,z2) -> z2 ifsum2(false(),z0,z1) -> sum2(cons(p(head(z0)),tail(z0)),s(z1)) ifsum2(true(),z0,z1) -> sum2(tail(z0),z1) isNil(cons(z0,z1)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(z0))) -> isZero(s(z0)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(z0))) -> s(p(s(z0))) sum(z0) -> sum2(z0,0()) sum2(z0,z1) -> ifsum(isNil(z0),isZero(head(z0)),z0,z1) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() times(z0,z1) -> sum(generate(z0,z1)) - Signature: {A/0,GE/2,GEN/3,GENERATE/2,HEAD/1,IF/4,IFSUM/4,IFSUM2/3,ISNIL/1,ISZERO/1,P/1,SUM/1,SUM2/2,TAIL/1,TIMES/2,a/0 ,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2} / {0/0 ,c/0,c1/2,c10/1,c11/2,c12/3,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/1,c20/0,c21/0,c22/1,c23/0,c24/0 ,c25/1,c26/0,c27/0,c28/1,c29/0,c3/2,c30/0,c4/0,c5/1,c6/1,c7/2,c8/3,c9/0,cons/2,d/0,error/0,false/0,nil/0,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,GE,GEN,GENERATE,HEAD,IF,IFSUM,IFSUM2,ISNIL,ISZERO,P,SUM ,SUM2,TAIL,TIMES,a,ge,gen,generate,head,if,ifsum,ifsum2,isNil,isZero,p,sum,sum2,tail ,times} 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,c4,c5,c6,c7,c8,c9,cons,d,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() -> c29() A() -> c30() GE(z0,0()) -> c26() GE(0(),s(z0)) -> c27() GE(s(z0),s(z1)) -> c28(GE(z0,z1)) GEN(z0,z1,z2) -> c3(IF(ge(z2,z0),z0,z1,z2),GE(z2,z0)) GENERATE(z0,z1) -> c2(GEN(z0,z1,0())) HEAD(cons(z0,z1)) -> c18() HEAD(nil()) -> c19() IF(false(),z0,z1,z2) -> c5(GEN(z0,z1,s(z2))) IF(true(),z0,z1,z2) -> c4() IFSUM(false(),z0,z1,z2) -> c10(IFSUM2(z0,z1,z2)) IFSUM(true(),z0,z1,z2) -> c9() IFSUM2(false(),z0,z1) -> c12(SUM2(cons(p(head(z0)),tail(z0)),s(z1)),P(head(z0)),HEAD(z0)) IFSUM2(false(),z0,z1) -> c13(SUM2(cons(p(head(z0)),tail(z0)),s(z1)),TAIL(z0)) IFSUM2(true(),z0,z1) -> c11(SUM2(tail(z0),z1),TAIL(z0)) ISNIL(cons(z0,z1)) -> c15() ISNIL(nil()) -> c14() ISZERO(0()) -> c20() ISZERO(s(0())) -> c21() ISZERO(s(s(z0))) -> c22(ISZERO(s(z0))) P(0()) -> c23() P(s(0())) -> c24() P(s(s(z0))) -> c25(P(s(z0))) SUM(z0) -> c6(SUM2(z0,0())) SUM2(z0,z1) -> c7(IFSUM(isNil(z0),isZero(head(z0)),z0,z1),ISNIL(z0)) SUM2(z0,z1) -> c8(IFSUM(isNil(z0),isZero(head(z0)),z0,z1),ISZERO(head(z0)),HEAD(z0)) TAIL(cons(z0,z1)) -> c17() TAIL(nil()) -> c16() TIMES(z0,z1) -> c1(SUM(generate(z0,z1)),GENERATE(z0,z1)) - Weak TRS: a() -> c() a() -> d() ge(z0,0()) -> true() ge(0(),s(z0)) -> false() ge(s(z0),s(z1)) -> ge(z0,z1) gen(z0,z1,z2) -> if(ge(z2,z0),z0,z1,z2) generate(z0,z1) -> gen(z0,z1,0()) head(cons(z0,z1)) -> z0 head(nil()) -> error() if(false(),z0,z1,z2) -> cons(z1,gen(z0,z1,s(z2))) if(true(),z0,z1,z2) -> nil() ifsum(false(),z0,z1,z2) -> ifsum2(z0,z1,z2) ifsum(true(),z0,z1,z2) -> z2 ifsum2(false(),z0,z1) -> sum2(cons(p(head(z0)),tail(z0)),s(z1)) ifsum2(true(),z0,z1) -> sum2(tail(z0),z1) isNil(cons(z0,z1)) -> false() isNil(nil()) -> true() isZero(0()) -> true() isZero(s(0())) -> false() isZero(s(s(z0))) -> isZero(s(z0)) p(0()) -> s(s(0())) p(s(0())) -> 0() p(s(s(z0))) -> s(p(s(z0))) sum(z0) -> sum2(z0,0()) sum2(z0,z1) -> ifsum(isNil(z0),isZero(head(z0)),z0,z1) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() times(z0,z1) -> sum(generate(z0,z1)) - Signature: {A/0,GE/2,GEN/3,GENERATE/2,HEAD/1,IF/4,IFSUM/4,IFSUM2/3,ISNIL/1,ISZERO/1,P/1,SUM/1,SUM2/2,TAIL/1,TIMES/2,a/0 ,ge/2,gen/3,generate/2,head/1,if/4,ifsum/4,ifsum2/3,isNil/1,isZero/1,p/1,sum/1,sum2/2,tail/1,times/2} / {0/0 ,c/0,c1/2,c10/1,c11/2,c12/3,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/1,c20/0,c21/0,c22/1,c23/0,c24/0 ,c25/1,c26/0,c27/0,c28/1,c29/0,c3/2,c30/0,c4/0,c5/1,c6/1,c7/2,c8/3,c9/0,cons/2,d/0,error/0,false/0,nil/0,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A,GE,GEN,GENERATE,HEAD,IF,IFSUM,IFSUM2,ISNIL,ISZERO,P,SUM ,SUM2,TAIL,TIMES,a,ge,gen,generate,head,if,ifsum,ifsum2,isNil,isZero,p,sum,sum2,tail ,times} 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,c4,c5,c6,c7,c8,c9,cons,d,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)) ->^+ c28(GE(x,y)) = C[GE(x,y) = GE(x,y){}] WORST_CASE(Omega(n^1),?)