WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: FACITER(z0,z1) -> c11(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),ISZERO(z0)) FACITER(z0,z1) -> c12(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),MINUS(z0,s(0()))) FACITER(z0,z1) -> c13(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),TIMES(z1,z0)) FACTORIAL(z0) -> c16(FACITER(z0,s(0()))) IF(false(),z0,z1,z2) -> c15(FACITER(z0,z2)) IF(true(),z0,z1,z2) -> c14() ISZERO(0()) -> c9() ISZERO(s(z0)) -> c10() MINUS(z0,0()) -> c6() MINUS(z0,s(z1)) -> c8(P(minus(z0,z1)),MINUS(z0,z1)) MINUS(0(),z0) -> c7() P(0()) -> c5() P(s(z0)) -> c4() PLUS(0(),z0) -> c() PLUS(s(z0),z1) -> c1(PLUS(z0,z1)) TIMES(0(),z0) -> c2() TIMES(s(z0),z1) -> c3(PLUS(z1,times(z0,z1)),TIMES(z0,z1)) - Weak TRS: facIter(z0,z1) -> if(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)) factorial(z0) -> facIter(z0,s(0())) if(false(),z0,z1,z2) -> facIter(z0,z2) if(true(),z0,z1,z2) -> z1 isZero(0()) -> true() isZero(s(z0)) -> false() minus(z0,0()) -> z0 minus(z0,s(z1)) -> p(minus(z0,z1)) minus(0(),z0) -> 0() p(0()) -> 0() p(s(z0)) -> z0 plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) times(0(),z0) -> 0() times(s(z0),z1) -> plus(z1,times(z0,z1)) - Signature: {FACITER/2,FACTORIAL/1,IF/4,ISZERO/1,MINUS/2,P/1,PLUS/2,TIMES/2,facIter/2,factorial/1,if/4,isZero/1,minus/2 ,p/1,plus/2,times/2} / {0/0,c/0,c1/1,c10/0,c11/2,c12/2,c13/2,c14/0,c15/1,c16/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0 ,c8/2,c9/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {FACITER,FACTORIAL,IF,ISZERO,MINUS,P,PLUS,TIMES,facIter ,factorial,if,isZero,minus,p,plus,times} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,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: FACITER(z0,z1) -> c11(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),ISZERO(z0)) FACITER(z0,z1) -> c12(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),MINUS(z0,s(0()))) FACITER(z0,z1) -> c13(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),TIMES(z1,z0)) FACTORIAL(z0) -> c16(FACITER(z0,s(0()))) IF(false(),z0,z1,z2) -> c15(FACITER(z0,z2)) IF(true(),z0,z1,z2) -> c14() ISZERO(0()) -> c9() ISZERO(s(z0)) -> c10() MINUS(z0,0()) -> c6() MINUS(z0,s(z1)) -> c8(P(minus(z0,z1)),MINUS(z0,z1)) MINUS(0(),z0) -> c7() P(0()) -> c5() P(s(z0)) -> c4() PLUS(0(),z0) -> c() PLUS(s(z0),z1) -> c1(PLUS(z0,z1)) TIMES(0(),z0) -> c2() TIMES(s(z0),z1) -> c3(PLUS(z1,times(z0,z1)),TIMES(z0,z1)) - Weak TRS: facIter(z0,z1) -> if(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)) factorial(z0) -> facIter(z0,s(0())) if(false(),z0,z1,z2) -> facIter(z0,z2) if(true(),z0,z1,z2) -> z1 isZero(0()) -> true() isZero(s(z0)) -> false() minus(z0,0()) -> z0 minus(z0,s(z1)) -> p(minus(z0,z1)) minus(0(),z0) -> 0() p(0()) -> 0() p(s(z0)) -> z0 plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) times(0(),z0) -> 0() times(s(z0),z1) -> plus(z1,times(z0,z1)) - Signature: {FACITER/2,FACTORIAL/1,IF/4,ISZERO/1,MINUS/2,P/1,PLUS/2,TIMES/2,facIter/2,factorial/1,if/4,isZero/1,minus/2 ,p/1,plus/2,times/2} / {0/0,c/0,c1/1,c10/0,c11/2,c12/2,c13/2,c14/0,c15/1,c16/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0 ,c8/2,c9/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {FACITER,FACTORIAL,IF,ISZERO,MINUS,P,PLUS,TIMES,facIter ,factorial,if,isZero,minus,p,plus,times} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,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: FACITER(z0,z1) -> c11(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),ISZERO(z0)) FACITER(z0,z1) -> c12(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),MINUS(z0,s(0()))) FACITER(z0,z1) -> c13(IF(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)),TIMES(z1,z0)) FACTORIAL(z0) -> c16(FACITER(z0,s(0()))) IF(false(),z0,z1,z2) -> c15(FACITER(z0,z2)) IF(true(),z0,z1,z2) -> c14() ISZERO(0()) -> c9() ISZERO(s(z0)) -> c10() MINUS(z0,0()) -> c6() MINUS(z0,s(z1)) -> c8(P(minus(z0,z1)),MINUS(z0,z1)) MINUS(0(),z0) -> c7() P(0()) -> c5() P(s(z0)) -> c4() PLUS(0(),z0) -> c() PLUS(s(z0),z1) -> c1(PLUS(z0,z1)) TIMES(0(),z0) -> c2() TIMES(s(z0),z1) -> c3(PLUS(z1,times(z0,z1)),TIMES(z0,z1)) - Weak TRS: facIter(z0,z1) -> if(isZero(z0),minus(z0,s(0())),z1,times(z1,z0)) factorial(z0) -> facIter(z0,s(0())) if(false(),z0,z1,z2) -> facIter(z0,z2) if(true(),z0,z1,z2) -> z1 isZero(0()) -> true() isZero(s(z0)) -> false() minus(z0,0()) -> z0 minus(z0,s(z1)) -> p(minus(z0,z1)) minus(0(),z0) -> 0() p(0()) -> 0() p(s(z0)) -> z0 plus(0(),z0) -> z0 plus(s(z0),z1) -> s(plus(z0,z1)) times(0(),z0) -> 0() times(s(z0),z1) -> plus(z1,times(z0,z1)) - Signature: {FACITER/2,FACTORIAL/1,IF/4,ISZERO/1,MINUS/2,P/1,PLUS/2,TIMES/2,facIter/2,factorial/1,if/4,isZero/1,minus/2 ,p/1,plus/2,times/2} / {0/0,c/0,c1/1,c10/0,c11/2,c12/2,c13/2,c14/0,c15/1,c16/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0 ,c8/2,c9/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {FACITER,FACTORIAL,IF,ISZERO,MINUS,P,PLUS,TIMES,facIter ,factorial,if,isZero,minus,p,plus,times} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6 ,c7,c8,c9,false,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MINUS(x,y){y -> s(y)} = MINUS(x,s(y)) ->^+ c8(P(minus(x,y)),MINUS(x,y)) = C[MINUS(x,y) = MINUS(x,y){}] WORST_CASE(Omega(n^1),?)