WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c5() A__ADD(0(),z0) -> c2(MARK(z0)) A__ADD(s(z0),z1) -> c3(A__ADD(mark(z0),mark(z1)),MARK(z0)) A__ADD(s(z0),z1) -> c4(A__ADD(mark(z0),mark(z1)),MARK(z1)) A__FACT(z0) -> c(A__IF(a__zero(mark(z0)),s(0()),prod(z0,fact(p(z0)))),A__ZERO(mark(z0)),MARK(z0)) A__FACT(z0) -> c1() A__IF(z0,z1,z2) -> c13() A__IF(false(),z0,z1) -> c12(MARK(z1)) A__IF(true(),z0,z1) -> c11(MARK(z0)) A__P(z0) -> c18() A__P(s(z0)) -> c17(MARK(z0)) A__PROD(z0,z1) -> c10() A__PROD(0(),z0) -> c6() A__PROD(s(z0),z1) -> c7(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),MARK(z1)) A__PROD(s(z0),z1) -> c8(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),A__PROD(mark(z0),mark(z1)),MARK(z0)) A__PROD(s(z0),z1) -> c9(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),A__PROD(mark(z0),mark(z1)),MARK(z1)) A__ZERO(z0) -> c16() A__ZERO(0()) -> c14() A__ZERO(s(z0)) -> c15() MARK(0()) -> c28() MARK(add(z0,z1)) -> c25(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c26(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(fact(z0)) -> c19(A__FACT(mark(z0)),MARK(z0)) MARK(false()) -> c30() MARK(if(z0,z1,z2)) -> c20(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(p(z0)) -> c24(A__P(mark(z0)),MARK(z0)) MARK(prod(z0,z1)) -> c22(A__PROD(mark(z0),mark(z1)),MARK(z0)) MARK(prod(z0,z1)) -> c23(A__PROD(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c27(MARK(z0)) MARK(true()) -> c29() MARK(zero(z0)) -> c21(A__ZERO(mark(z0)),MARK(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(a__add(mark(z0),mark(z1))) a__fact(z0) -> a__if(a__zero(mark(z0)),s(0()),prod(z0,fact(p(z0)))) a__fact(z0) -> fact(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__p(z0) -> p(z0) a__p(s(z0)) -> mark(z0) a__prod(z0,z1) -> prod(z0,z1) a__prod(0(),z0) -> 0() a__prod(s(z0),z1) -> a__add(mark(z1),a__prod(mark(z0),mark(z1))) a__zero(z0) -> zero(z0) a__zero(0()) -> true() a__zero(s(z0)) -> false() mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),mark(z1)) mark(fact(z0)) -> a__fact(mark(z0)) mark(false()) -> false() mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(p(z0)) -> a__p(mark(z0)) mark(prod(z0,z1)) -> a__prod(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(true()) -> true() mark(zero(z0)) -> a__zero(mark(z0)) - Signature: {A__ADD/2,A__FACT/1,A__IF/3,A__P/1,A__PROD/2,A__ZERO/1,MARK/1,a__add/2,a__fact/1,a__if/3,a__p/1,a__prod/2 ,a__zero/1,mark/1} / {0/0,add/2,c/3,c1/0,c10/0,c11/1,c12/1,c13/0,c14/0,c15/0,c16/0,c17/1,c18/0,c19/2,c2/1 ,c20/2,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/1,c28/0,c29/0,c3/2,c30/0,c4/2,c5/0,c6/0,c7/2,c8/3,c9/3,fact/1 ,false/0,if/3,p/1,prod/2,s/1,true/0,zero/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__FACT,A__IF,A__P,A__PROD,A__ZERO,MARK,a__add ,a__fact,a__if,a__p,a__prod,a__zero,mark} and constructors {0,add,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,fact,false,if,p,prod,s,true,zero} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c5() A__ADD(0(),z0) -> c2(MARK(z0)) A__ADD(s(z0),z1) -> c3(A__ADD(mark(z0),mark(z1)),MARK(z0)) A__ADD(s(z0),z1) -> c4(A__ADD(mark(z0),mark(z1)),MARK(z1)) A__FACT(z0) -> c(A__IF(a__zero(mark(z0)),s(0()),prod(z0,fact(p(z0)))),A__ZERO(mark(z0)),MARK(z0)) A__FACT(z0) -> c1() A__IF(z0,z1,z2) -> c13() A__IF(false(),z0,z1) -> c12(MARK(z1)) A__IF(true(),z0,z1) -> c11(MARK(z0)) A__P(z0) -> c18() A__P(s(z0)) -> c17(MARK(z0)) A__PROD(z0,z1) -> c10() A__PROD(0(),z0) -> c6() A__PROD(s(z0),z1) -> c7(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),MARK(z1)) A__PROD(s(z0),z1) -> c8(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),A__PROD(mark(z0),mark(z1)),MARK(z0)) A__PROD(s(z0),z1) -> c9(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),A__PROD(mark(z0),mark(z1)),MARK(z1)) A__ZERO(z0) -> c16() A__ZERO(0()) -> c14() A__ZERO(s(z0)) -> c15() MARK(0()) -> c28() MARK(add(z0,z1)) -> c25(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c26(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(fact(z0)) -> c19(A__FACT(mark(z0)),MARK(z0)) MARK(false()) -> c30() MARK(if(z0,z1,z2)) -> c20(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(p(z0)) -> c24(A__P(mark(z0)),MARK(z0)) MARK(prod(z0,z1)) -> c22(A__PROD(mark(z0),mark(z1)),MARK(z0)) MARK(prod(z0,z1)) -> c23(A__PROD(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c27(MARK(z0)) MARK(true()) -> c29() MARK(zero(z0)) -> c21(A__ZERO(mark(z0)),MARK(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(a__add(mark(z0),mark(z1))) a__fact(z0) -> a__if(a__zero(mark(z0)),s(0()),prod(z0,fact(p(z0)))) a__fact(z0) -> fact(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__p(z0) -> p(z0) a__p(s(z0)) -> mark(z0) a__prod(z0,z1) -> prod(z0,z1) a__prod(0(),z0) -> 0() a__prod(s(z0),z1) -> a__add(mark(z1),a__prod(mark(z0),mark(z1))) a__zero(z0) -> zero(z0) a__zero(0()) -> true() a__zero(s(z0)) -> false() mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),mark(z1)) mark(fact(z0)) -> a__fact(mark(z0)) mark(false()) -> false() mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(p(z0)) -> a__p(mark(z0)) mark(prod(z0,z1)) -> a__prod(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(true()) -> true() mark(zero(z0)) -> a__zero(mark(z0)) - Signature: {A__ADD/2,A__FACT/1,A__IF/3,A__P/1,A__PROD/2,A__ZERO/1,MARK/1,a__add/2,a__fact/1,a__if/3,a__p/1,a__prod/2 ,a__zero/1,mark/1} / {0/0,add/2,c/3,c1/0,c10/0,c11/1,c12/1,c13/0,c14/0,c15/0,c16/0,c17/1,c18/0,c19/2,c2/1 ,c20/2,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/1,c28/0,c29/0,c3/2,c30/0,c4/2,c5/0,c6/0,c7/2,c8/3,c9/3,fact/1 ,false/0,if/3,p/1,prod/2,s/1,true/0,zero/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__FACT,A__IF,A__P,A__PROD,A__ZERO,MARK,a__add ,a__fact,a__if,a__p,a__prod,a__zero,mark} and constructors {0,add,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,fact,false,if,p,prod,s,true,zero} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ADD(z0,z1) -> c5() A__ADD(0(),z0) -> c2(MARK(z0)) A__ADD(s(z0),z1) -> c3(A__ADD(mark(z0),mark(z1)),MARK(z0)) A__ADD(s(z0),z1) -> c4(A__ADD(mark(z0),mark(z1)),MARK(z1)) A__FACT(z0) -> c(A__IF(a__zero(mark(z0)),s(0()),prod(z0,fact(p(z0)))),A__ZERO(mark(z0)),MARK(z0)) A__FACT(z0) -> c1() A__IF(z0,z1,z2) -> c13() A__IF(false(),z0,z1) -> c12(MARK(z1)) A__IF(true(),z0,z1) -> c11(MARK(z0)) A__P(z0) -> c18() A__P(s(z0)) -> c17(MARK(z0)) A__PROD(z0,z1) -> c10() A__PROD(0(),z0) -> c6() A__PROD(s(z0),z1) -> c7(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),MARK(z1)) A__PROD(s(z0),z1) -> c8(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),A__PROD(mark(z0),mark(z1)),MARK(z0)) A__PROD(s(z0),z1) -> c9(A__ADD(mark(z1),a__prod(mark(z0),mark(z1))),A__PROD(mark(z0),mark(z1)),MARK(z1)) A__ZERO(z0) -> c16() A__ZERO(0()) -> c14() A__ZERO(s(z0)) -> c15() MARK(0()) -> c28() MARK(add(z0,z1)) -> c25(A__ADD(mark(z0),mark(z1)),MARK(z0)) MARK(add(z0,z1)) -> c26(A__ADD(mark(z0),mark(z1)),MARK(z1)) MARK(fact(z0)) -> c19(A__FACT(mark(z0)),MARK(z0)) MARK(false()) -> c30() MARK(if(z0,z1,z2)) -> c20(A__IF(mark(z0),z1,z2),MARK(z0)) MARK(p(z0)) -> c24(A__P(mark(z0)),MARK(z0)) MARK(prod(z0,z1)) -> c22(A__PROD(mark(z0),mark(z1)),MARK(z0)) MARK(prod(z0,z1)) -> c23(A__PROD(mark(z0),mark(z1)),MARK(z1)) MARK(s(z0)) -> c27(MARK(z0)) MARK(true()) -> c29() MARK(zero(z0)) -> c21(A__ZERO(mark(z0)),MARK(z0)) - Weak TRS: a__add(z0,z1) -> add(z0,z1) a__add(0(),z0) -> mark(z0) a__add(s(z0),z1) -> s(a__add(mark(z0),mark(z1))) a__fact(z0) -> a__if(a__zero(mark(z0)),s(0()),prod(z0,fact(p(z0)))) a__fact(z0) -> fact(z0) a__if(z0,z1,z2) -> if(z0,z1,z2) a__if(false(),z0,z1) -> mark(z1) a__if(true(),z0,z1) -> mark(z0) a__p(z0) -> p(z0) a__p(s(z0)) -> mark(z0) a__prod(z0,z1) -> prod(z0,z1) a__prod(0(),z0) -> 0() a__prod(s(z0),z1) -> a__add(mark(z1),a__prod(mark(z0),mark(z1))) a__zero(z0) -> zero(z0) a__zero(0()) -> true() a__zero(s(z0)) -> false() mark(0()) -> 0() mark(add(z0,z1)) -> a__add(mark(z0),mark(z1)) mark(fact(z0)) -> a__fact(mark(z0)) mark(false()) -> false() mark(if(z0,z1,z2)) -> a__if(mark(z0),z1,z2) mark(p(z0)) -> a__p(mark(z0)) mark(prod(z0,z1)) -> a__prod(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(true()) -> true() mark(zero(z0)) -> a__zero(mark(z0)) - Signature: {A__ADD/2,A__FACT/1,A__IF/3,A__P/1,A__PROD/2,A__ZERO/1,MARK/1,a__add/2,a__fact/1,a__if/3,a__p/1,a__prod/2 ,a__zero/1,mark/1} / {0/0,add/2,c/3,c1/0,c10/0,c11/1,c12/1,c13/0,c14/0,c15/0,c16/0,c17/1,c18/0,c19/2,c2/1 ,c20/2,c21/2,c22/2,c23/2,c24/2,c25/2,c26/2,c27/1,c28/0,c29/0,c3/2,c30/0,c4/2,c5/0,c6/0,c7/2,c8/3,c9/3,fact/1 ,false/0,if/3,p/1,prod/2,s/1,true/0,zero/1} - Obligation: innermost runtime complexity wrt. defined symbols {A__ADD,A__FACT,A__IF,A__P,A__PROD,A__ZERO,MARK,a__add ,a__fact,a__if,a__p,a__prod,a__zero,mark} and constructors {0,add,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,fact,false,if,p,prod,s,true,zero} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MARK(x){x -> add(x,y)} = MARK(add(x,y)) ->^+ c25(A__ADD(mark(x),mark(y)),MARK(x)) = C[MARK(x) = MARK(x){}] WORST_CASE(Omega(n^1),?)