WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: -'(z0,0()) -> c6() -'(s(z0),s(z1)) -> c7(-'(z0,z1)) GCD(z0,0(),0()) -> c17() GCD(z0,s(z1),s(z2)) -> c11(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) ,-'(max(z1,z2),min(z1,z2)) ,MAX(z1,z2)) GCD(z0,s(z1),s(z2)) -> c12(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) ,-'(max(z1,z2),min(z1,z2)) ,MIN(z1,z2)) GCD(z0,s(z1),s(z2)) -> c13(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))),MIN(z1,z2)) GCD(0(),z0,0()) -> c18() GCD(0(),0(),z0) -> c19() GCD(s(z0),z1,s(z2)) -> c14(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) ,-'(max(z0,z2),min(z0,z2)) ,MAX(z0,z2)) GCD(s(z0),z1,s(z2)) -> c15(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) ,-'(max(z0,z2),min(z0,z2)) ,MIN(z0,z2)) GCD(s(z0),z1,s(z2)) -> c16(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))),MIN(z0,z2)) GCD(s(z0),s(z1),z2) -> c10(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2),MIN(z0,z1)) GCD(s(z0),s(z1),z2) -> c8(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2) ,-'(max(z0,z1),min(z0,z1)) ,MAX(z0,z1)) GCD(s(z0),s(z1),z2) -> c9(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2) ,-'(max(z0,z1),min(z0,z1)) ,MIN(z0,z1)) MAX(z0,0()) -> c3() MAX(0(),z0) -> c4() MAX(s(z0),s(z1)) -> c5(MAX(z0,z1)) MIN(z0,0()) -> c() MIN(0(),z0) -> c1() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) gcd(z0,0(),0()) -> z0 gcd(z0,s(z1),s(z2)) -> gcd(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) gcd(0(),z0,0()) -> z0 gcd(0(),0(),z0) -> z0 gcd(s(z0),z1,s(z2)) -> gcd(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) gcd(s(z0),s(z1),z2) -> gcd(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),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)) - Signature: {-/2,-'/2,GCD/3,MAX/2,MIN/2,gcd/3,max/2,min/2} / {0/0,c/0,c1/0,c10/2,c11/3,c12/3,c13/2,c14/3,c15/3,c16/2 ,c17/0,c18/0,c19/0,c2/1,c3/0,c4/0,c5/1,c6/0,c7/1,c8/3,c9/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',GCD,MAX,MIN,gcd,max,min} and constructors {0,c,c1 ,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,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: -'(z0,0()) -> c6() -'(s(z0),s(z1)) -> c7(-'(z0,z1)) GCD(z0,0(),0()) -> c17() GCD(z0,s(z1),s(z2)) -> c11(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) ,-'(max(z1,z2),min(z1,z2)) ,MAX(z1,z2)) GCD(z0,s(z1),s(z2)) -> c12(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) ,-'(max(z1,z2),min(z1,z2)) ,MIN(z1,z2)) GCD(z0,s(z1),s(z2)) -> c13(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))),MIN(z1,z2)) GCD(0(),z0,0()) -> c18() GCD(0(),0(),z0) -> c19() GCD(s(z0),z1,s(z2)) -> c14(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) ,-'(max(z0,z2),min(z0,z2)) ,MAX(z0,z2)) GCD(s(z0),z1,s(z2)) -> c15(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) ,-'(max(z0,z2),min(z0,z2)) ,MIN(z0,z2)) GCD(s(z0),z1,s(z2)) -> c16(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))),MIN(z0,z2)) GCD(s(z0),s(z1),z2) -> c10(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2),MIN(z0,z1)) GCD(s(z0),s(z1),z2) -> c8(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2) ,-'(max(z0,z1),min(z0,z1)) ,MAX(z0,z1)) GCD(s(z0),s(z1),z2) -> c9(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2) ,-'(max(z0,z1),min(z0,z1)) ,MIN(z0,z1)) MAX(z0,0()) -> c3() MAX(0(),z0) -> c4() MAX(s(z0),s(z1)) -> c5(MAX(z0,z1)) MIN(z0,0()) -> c() MIN(0(),z0) -> c1() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) gcd(z0,0(),0()) -> z0 gcd(z0,s(z1),s(z2)) -> gcd(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) gcd(0(),z0,0()) -> z0 gcd(0(),0(),z0) -> z0 gcd(s(z0),z1,s(z2)) -> gcd(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) gcd(s(z0),s(z1),z2) -> gcd(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),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)) - Signature: {-/2,-'/2,GCD/3,MAX/2,MIN/2,gcd/3,max/2,min/2} / {0/0,c/0,c1/0,c10/2,c11/3,c12/3,c13/2,c14/3,c15/3,c16/2 ,c17/0,c18/0,c19/0,c2/1,c3/0,c4/0,c5/1,c6/0,c7/1,c8/3,c9/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',GCD,MAX,MIN,gcd,max,min} and constructors {0,c,c1 ,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,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: -'(z0,0()) -> c6() -'(s(z0),s(z1)) -> c7(-'(z0,z1)) GCD(z0,0(),0()) -> c17() GCD(z0,s(z1),s(z2)) -> c11(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) ,-'(max(z1,z2),min(z1,z2)) ,MAX(z1,z2)) GCD(z0,s(z1),s(z2)) -> c12(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) ,-'(max(z1,z2),min(z1,z2)) ,MIN(z1,z2)) GCD(z0,s(z1),s(z2)) -> c13(GCD(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))),MIN(z1,z2)) GCD(0(),z0,0()) -> c18() GCD(0(),0(),z0) -> c19() GCD(s(z0),z1,s(z2)) -> c14(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) ,-'(max(z0,z2),min(z0,z2)) ,MAX(z0,z2)) GCD(s(z0),z1,s(z2)) -> c15(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) ,-'(max(z0,z2),min(z0,z2)) ,MIN(z0,z2)) GCD(s(z0),z1,s(z2)) -> c16(GCD(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))),MIN(z0,z2)) GCD(s(z0),s(z1),z2) -> c10(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2),MIN(z0,z1)) GCD(s(z0),s(z1),z2) -> c8(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2) ,-'(max(z0,z1),min(z0,z1)) ,MAX(z0,z1)) GCD(s(z0),s(z1),z2) -> c9(GCD(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),z2) ,-'(max(z0,z1),min(z0,z1)) ,MIN(z0,z1)) MAX(z0,0()) -> c3() MAX(0(),z0) -> c4() MAX(s(z0),s(z1)) -> c5(MAX(z0,z1)) MIN(z0,0()) -> c() MIN(0(),z0) -> c1() MIN(s(z0),s(z1)) -> c2(MIN(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(s(z0),s(z1)) -> -(z0,z1) gcd(z0,0(),0()) -> z0 gcd(z0,s(z1),s(z2)) -> gcd(z0,-(max(z1,z2),min(z1,z2)),s(min(z1,z2))) gcd(0(),z0,0()) -> z0 gcd(0(),0(),z0) -> z0 gcd(s(z0),z1,s(z2)) -> gcd(-(max(z0,z2),min(z0,z2)),z1,s(min(z0,z2))) gcd(s(z0),s(z1),z2) -> gcd(-(max(z0,z1),min(z0,z1)),s(min(z0,z1)),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)) - Signature: {-/2,-'/2,GCD/3,MAX/2,MIN/2,gcd/3,max/2,min/2} / {0/0,c/0,c1/0,c10/2,c11/3,c12/3,c13/2,c14/3,c15/3,c16/2 ,c17/0,c18/0,c19/0,c2/1,c3/0,c4/0,c5/1,c6/0,c7/1,c8/3,c9/3,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',GCD,MAX,MIN,gcd,max,min} and constructors {0,c,c1 ,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c3,c4,c5,c6,c7,c8,c9,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: -'(x,y){x -> s(x),y -> s(y)} = -'(s(x),s(y)) ->^+ c7(-'(x,y)) = C[-'(x,y) = -'(x,y){}] WORST_CASE(Omega(n^1),?)