WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ACK(0(),z0) -> c9(PLUS(z0,s(0()))) ACK(s(z0),0()) -> c10(ACK(z0,s(0()))) ACK(s(z0),s(z1)) -> c11(ACK(z0,ack(s(z0),z1)),ACK(s(z0),z1)) DOUBLE(z0) -> c1(PERMUTE(z0,z0,a())) ISZERO(0()) -> c17() ISZERO(s(z0)) -> c18() P(0()) -> c7() P(s(z0)) -> c8() PERMUTE(z0,z1,a()) -> c2(PERMUTE(isZero(z0),z0,b()),ISZERO(z0)) PERMUTE(z0,z1,c()) -> c6(PERMUTE(z1,z0,a())) PERMUTE(false(),z0,b()) -> c3(PERMUTE(ack(z0,z0),p(z0),c()),ACK(z0,z0)) PERMUTE(false(),z0,b()) -> c4(PERMUTE(ack(z0,z0),p(z0),c()),P(z0)) PERMUTE(true(),z0,b()) -> c5() PLUS(z0,0()) -> c16() PLUS(z0,s(0())) -> c15() PLUS(z0,s(s(z1))) -> c14(PLUS(s(z0),z1)) PLUS(0(),z0) -> c12() PLUS(s(z0),z1) -> c13(PLUS(z0,s(z1))) - Weak TRS: ack(0(),z0) -> plus(z0,s(0())) ack(s(z0),0()) -> ack(z0,s(0())) ack(s(z0),s(z1)) -> ack(z0,ack(s(z0),z1)) double(z0) -> permute(z0,z0,a()) isZero(0()) -> true() isZero(s(z0)) -> false() p(0()) -> 0() p(s(z0)) -> z0 permute(z0,z1,a()) -> permute(isZero(z0),z0,b()) permute(z0,z1,c()) -> s(s(permute(z1,z0,a()))) permute(false(),z0,b()) -> permute(ack(z0,z0),p(z0),c()) permute(true(),z0,b()) -> 0() plus(z0,0()) -> z0 plus(z0,s(0())) -> s(z0) plus(z0,s(s(z1))) -> s(plus(s(z0),z1)) plus(0(),z0) -> z0 plus(s(z0),z1) -> plus(z0,s(z1)) - Signature: {ACK/2,DOUBLE/1,ISZERO/1,P/1,PERMUTE/3,PLUS/2,ack/2,double/1,isZero/1,p/1,permute/3,plus/2} / {0/0,a/0,b/0 ,c/0,c1/1,c10/1,c11/2,c12/0,c13/1,c14/1,c15/0,c16/0,c17/0,c18/0,c2/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACK,DOUBLE,ISZERO,P,PERMUTE,PLUS,ack,double,isZero,p ,permute,plus} and constructors {0,a,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,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: ACK(0(),z0) -> c9(PLUS(z0,s(0()))) ACK(s(z0),0()) -> c10(ACK(z0,s(0()))) ACK(s(z0),s(z1)) -> c11(ACK(z0,ack(s(z0),z1)),ACK(s(z0),z1)) DOUBLE(z0) -> c1(PERMUTE(z0,z0,a())) ISZERO(0()) -> c17() ISZERO(s(z0)) -> c18() P(0()) -> c7() P(s(z0)) -> c8() PERMUTE(z0,z1,a()) -> c2(PERMUTE(isZero(z0),z0,b()),ISZERO(z0)) PERMUTE(z0,z1,c()) -> c6(PERMUTE(z1,z0,a())) PERMUTE(false(),z0,b()) -> c3(PERMUTE(ack(z0,z0),p(z0),c()),ACK(z0,z0)) PERMUTE(false(),z0,b()) -> c4(PERMUTE(ack(z0,z0),p(z0),c()),P(z0)) PERMUTE(true(),z0,b()) -> c5() PLUS(z0,0()) -> c16() PLUS(z0,s(0())) -> c15() PLUS(z0,s(s(z1))) -> c14(PLUS(s(z0),z1)) PLUS(0(),z0) -> c12() PLUS(s(z0),z1) -> c13(PLUS(z0,s(z1))) - Weak TRS: ack(0(),z0) -> plus(z0,s(0())) ack(s(z0),0()) -> ack(z0,s(0())) ack(s(z0),s(z1)) -> ack(z0,ack(s(z0),z1)) double(z0) -> permute(z0,z0,a()) isZero(0()) -> true() isZero(s(z0)) -> false() p(0()) -> 0() p(s(z0)) -> z0 permute(z0,z1,a()) -> permute(isZero(z0),z0,b()) permute(z0,z1,c()) -> s(s(permute(z1,z0,a()))) permute(false(),z0,b()) -> permute(ack(z0,z0),p(z0),c()) permute(true(),z0,b()) -> 0() plus(z0,0()) -> z0 plus(z0,s(0())) -> s(z0) plus(z0,s(s(z1))) -> s(plus(s(z0),z1)) plus(0(),z0) -> z0 plus(s(z0),z1) -> plus(z0,s(z1)) - Signature: {ACK/2,DOUBLE/1,ISZERO/1,P/1,PERMUTE/3,PLUS/2,ack/2,double/1,isZero/1,p/1,permute/3,plus/2} / {0/0,a/0,b/0 ,c/0,c1/1,c10/1,c11/2,c12/0,c13/1,c14/1,c15/0,c16/0,c17/0,c18/0,c2/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACK,DOUBLE,ISZERO,P,PERMUTE,PLUS,ack,double,isZero,p ,permute,plus} and constructors {0,a,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,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: ACK(0(),z0) -> c9(PLUS(z0,s(0()))) ACK(s(z0),0()) -> c10(ACK(z0,s(0()))) ACK(s(z0),s(z1)) -> c11(ACK(z0,ack(s(z0),z1)),ACK(s(z0),z1)) DOUBLE(z0) -> c1(PERMUTE(z0,z0,a())) ISZERO(0()) -> c17() ISZERO(s(z0)) -> c18() P(0()) -> c7() P(s(z0)) -> c8() PERMUTE(z0,z1,a()) -> c2(PERMUTE(isZero(z0),z0,b()),ISZERO(z0)) PERMUTE(z0,z1,c()) -> c6(PERMUTE(z1,z0,a())) PERMUTE(false(),z0,b()) -> c3(PERMUTE(ack(z0,z0),p(z0),c()),ACK(z0,z0)) PERMUTE(false(),z0,b()) -> c4(PERMUTE(ack(z0,z0),p(z0),c()),P(z0)) PERMUTE(true(),z0,b()) -> c5() PLUS(z0,0()) -> c16() PLUS(z0,s(0())) -> c15() PLUS(z0,s(s(z1))) -> c14(PLUS(s(z0),z1)) PLUS(0(),z0) -> c12() PLUS(s(z0),z1) -> c13(PLUS(z0,s(z1))) - Weak TRS: ack(0(),z0) -> plus(z0,s(0())) ack(s(z0),0()) -> ack(z0,s(0())) ack(s(z0),s(z1)) -> ack(z0,ack(s(z0),z1)) double(z0) -> permute(z0,z0,a()) isZero(0()) -> true() isZero(s(z0)) -> false() p(0()) -> 0() p(s(z0)) -> z0 permute(z0,z1,a()) -> permute(isZero(z0),z0,b()) permute(z0,z1,c()) -> s(s(permute(z1,z0,a()))) permute(false(),z0,b()) -> permute(ack(z0,z0),p(z0),c()) permute(true(),z0,b()) -> 0() plus(z0,0()) -> z0 plus(z0,s(0())) -> s(z0) plus(z0,s(s(z1))) -> s(plus(s(z0),z1)) plus(0(),z0) -> z0 plus(s(z0),z1) -> plus(z0,s(z1)) - Signature: {ACK/2,DOUBLE/1,ISZERO/1,P/1,PERMUTE/3,PLUS/2,ack/2,double/1,isZero/1,p/1,permute/3,plus/2} / {0/0,a/0,b/0 ,c/0,c1/1,c10/1,c11/2,c12/0,c13/1,c14/1,c15/0,c16/0,c17/0,c18/0,c2/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1 ,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACK,DOUBLE,ISZERO,P,PERMUTE,PLUS,ack,double,isZero,p ,permute,plus} and constructors {0,a,b,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,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: ACK(s(x),y){y -> s(y)} = ACK(s(x),s(y)) ->^+ c11(ACK(x,ack(s(x),y)),ACK(s(x),y)) = C[ACK(s(x),y) = ACK(s(x),y){}] WORST_CASE(Omega(n^1),?)