WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: F(z0,z1,0()) -> c12(MAX(z0,z1)) F(z0,0(),z1) -> c11(MAX(z0,z1)) F(0(),z0,z1) -> c10(MAX(z0,z1)) F(s(z0),s(z1),s(z2)) -> c7(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,MAX(s(z0),max(s(z1),s(z2))) ,MAX(s(z1),s(z2))) F(s(z0),s(z1),s(z2)) -> c8(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,P(min(s(z0),max(s(z1),s(z2)))) ,MIN(s(z0),max(s(z1),s(z2))) ,MAX(s(z1),s(z2))) F(s(z0),s(z1),s(z2)) -> c9(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,MIN(s(z0),min(s(z1),s(z2))) ,MIN(s(z1),s(z2))) MAX(z0,0()) -> c4() MAX(0(),z0) -> c3() MAX(s(z0),s(z1)) -> c5(MAX(z0,z1)) MIN(z0,0()) -> c1() MIN(0(),z0) -> c() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) P(s(z0)) -> c6() - Weak TRS: f(z0,z1,0()) -> max(z0,z1) f(z0,0(),z1) -> max(z0,z1) f(0(),z0,z1) -> max(z0,z1) f(s(z0),s(z1),s(z2)) -> f(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) max(z0,0()) -> z0 max(0(),z0) -> z0 max(s(z0),s(z1)) -> s(max(z0,z1)) min(z0,0()) -> 0() min(0(),z0) -> 0() min(s(z0),s(z1)) -> s(min(z0,z1)) p(s(z0)) -> z0 - Signature: {F/3,MAX/2,MIN/2,P/1,f/3,max/2,min/2,p/1} / {0/0,c/0,c1/0,c10/1,c11/1,c12/1,c2/1,c3/0,c4/0,c5/1,c6/0,c7/3 ,c8/4,c9/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {F,MAX,MIN,P,f,max,min,p} and constructors {0,c,c1,c10,c11 ,c12,c2,c3,c4,c5,c6,c7,c8,c9,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: F(z0,z1,0()) -> c12(MAX(z0,z1)) F(z0,0(),z1) -> c11(MAX(z0,z1)) F(0(),z0,z1) -> c10(MAX(z0,z1)) F(s(z0),s(z1),s(z2)) -> c7(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,MAX(s(z0),max(s(z1),s(z2))) ,MAX(s(z1),s(z2))) F(s(z0),s(z1),s(z2)) -> c8(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,P(min(s(z0),max(s(z1),s(z2)))) ,MIN(s(z0),max(s(z1),s(z2))) ,MAX(s(z1),s(z2))) F(s(z0),s(z1),s(z2)) -> c9(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,MIN(s(z0),min(s(z1),s(z2))) ,MIN(s(z1),s(z2))) MAX(z0,0()) -> c4() MAX(0(),z0) -> c3() MAX(s(z0),s(z1)) -> c5(MAX(z0,z1)) MIN(z0,0()) -> c1() MIN(0(),z0) -> c() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) P(s(z0)) -> c6() - Weak TRS: f(z0,z1,0()) -> max(z0,z1) f(z0,0(),z1) -> max(z0,z1) f(0(),z0,z1) -> max(z0,z1) f(s(z0),s(z1),s(z2)) -> f(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) max(z0,0()) -> z0 max(0(),z0) -> z0 max(s(z0),s(z1)) -> s(max(z0,z1)) min(z0,0()) -> 0() min(0(),z0) -> 0() min(s(z0),s(z1)) -> s(min(z0,z1)) p(s(z0)) -> z0 - Signature: {F/3,MAX/2,MIN/2,P/1,f/3,max/2,min/2,p/1} / {0/0,c/0,c1/0,c10/1,c11/1,c12/1,c2/1,c3/0,c4/0,c5/1,c6/0,c7/3 ,c8/4,c9/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {F,MAX,MIN,P,f,max,min,p} and constructors {0,c,c1,c10,c11 ,c12,c2,c3,c4,c5,c6,c7,c8,c9,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: F(z0,z1,0()) -> c12(MAX(z0,z1)) F(z0,0(),z1) -> c11(MAX(z0,z1)) F(0(),z0,z1) -> c10(MAX(z0,z1)) F(s(z0),s(z1),s(z2)) -> c7(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,MAX(s(z0),max(s(z1),s(z2))) ,MAX(s(z1),s(z2))) F(s(z0),s(z1),s(z2)) -> c8(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,P(min(s(z0),max(s(z1),s(z2)))) ,MIN(s(z0),max(s(z1),s(z2))) ,MAX(s(z1),s(z2))) F(s(z0),s(z1),s(z2)) -> c9(F(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) ,MIN(s(z0),min(s(z1),s(z2))) ,MIN(s(z1),s(z2))) MAX(z0,0()) -> c4() MAX(0(),z0) -> c3() MAX(s(z0),s(z1)) -> c5(MAX(z0,z1)) MIN(z0,0()) -> c1() MIN(0(),z0) -> c() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) P(s(z0)) -> c6() - Weak TRS: f(z0,z1,0()) -> max(z0,z1) f(z0,0(),z1) -> max(z0,z1) f(0(),z0,z1) -> max(z0,z1) f(s(z0),s(z1),s(z2)) -> f(max(s(z0),max(s(z1),s(z2))) ,p(min(s(z0),max(s(z1),s(z2)))) ,min(s(z0),min(s(z1),s(z2)))) max(z0,0()) -> z0 max(0(),z0) -> z0 max(s(z0),s(z1)) -> s(max(z0,z1)) min(z0,0()) -> 0() min(0(),z0) -> 0() min(s(z0),s(z1)) -> s(min(z0,z1)) p(s(z0)) -> z0 - Signature: {F/3,MAX/2,MIN/2,P/1,f/3,max/2,min/2,p/1} / {0/0,c/0,c1/0,c10/1,c11/1,c12/1,c2/1,c3/0,c4/0,c5/1,c6/0,c7/3 ,c8/4,c9/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {F,MAX,MIN,P,f,max,min,p} and constructors {0,c,c1,c10,c11 ,c12,c2,c3,c4,c5,c6,c7,c8,c9,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MAX(x,y){x -> s(x),y -> s(y)} = MAX(s(x),s(y)) ->^+ c5(MAX(x,y)) = C[MAX(x,y) = MAX(x,y){}] WORST_CASE(Omega(n^1),?)