MAYBE Time: 0.045090 TRS: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s x, s y) -> s min(x, y), max(x, 0()) -> x, max(0(), y) -> y, max(s x, s y) -> s max(x, y), -(x, 0()) -> x, -(s x, s y) -> -(x, y), gcd(0(), s x) -> s x, gcd(s x, 0()) -> s x, gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y))} DP: DP: {min#(s x, s y) -> min#(x, y), max#(s x, s y) -> max#(x, y), -#(s x, s y) -> -#(x, y), gcd#(s x, s y) -> min#(x, y), gcd#(s x, s y) -> max#(x, y), gcd#(s x, s y) -> -#(max(x, y), min(x, y)), gcd#(s x, s y) -> gcd#(-(max(x, y), min(x, y)), s min(x, y))} TRS: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s x, s y) -> s min(x, y), max(x, 0()) -> x, max(0(), y) -> y, max(s x, s y) -> s max(x, y), -(x, 0()) -> x, -(s x, s y) -> -(x, y), gcd(0(), s x) -> s x, gcd(s x, 0()) -> s x, gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y))} UR: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s x, s y) -> s min(x, y), max(x, 0()) -> x, max(0(), y) -> y, max(s x, s y) -> s max(x, y), -(x, 0()) -> x, -(s x, s y) -> -(x, y), a(z, w) -> z, a(z, w) -> w} EDG: {(gcd#(s x, s y) -> gcd#(-(max(x, y), min(x, y)), s min(x, y)), gcd#(s x, s y) -> gcd#(-(max(x, y), min(x, y)), s min(x, y))) (gcd#(s x, s y) -> gcd#(-(max(x, y), min(x, y)), s min(x, y)), gcd#(s x, s y) -> -#(max(x, y), min(x, y))) (gcd#(s x, s y) -> gcd#(-(max(x, y), min(x, y)), s min(x, y)), gcd#(s x, s y) -> max#(x, y)) (gcd#(s x, s y) -> gcd#(-(max(x, y), min(x, y)), s min(x, y)), gcd#(s x, s y) -> min#(x, y)) (max#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y)) (gcd#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y)) (gcd#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (min#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y)) (gcd#(s x, s y) -> -#(max(x, y), min(x, y)), -#(s x, s y) -> -#(x, y))} STATUS: arrows: 0.795918 SCCS (4): Scc: {gcd#(s x, s y) -> gcd#(-(max(x, y), min(x, y)), s min(x, y))} Scc: {max#(s x, s y) -> max#(x, y)} Scc: {min#(s x, s y) -> min#(x, y)} Scc: {-#(s x, s y) -> -#(x, y)} SCC (1): Strict: {gcd#(s x, s y) -> gcd#(-(max(x, y), min(x, y)), s min(x, y))} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s x, s y) -> s min(x, y), max(x, 0()) -> x, max(0(), y) -> y, max(s x, s y) -> s max(x, y), -(x, 0()) -> x, -(s x, s y) -> -(x, y), gcd(0(), s x) -> s x, gcd(s x, 0()) -> s x, gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y))} Fail SCC (1): Strict: {max#(s x, s y) -> max#(x, y)} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s x, s y) -> s min(x, y), max(x, 0()) -> x, max(0(), y) -> y, max(s x, s y) -> s max(x, y), -(x, 0()) -> x, -(s x, s y) -> -(x, y), gcd(0(), s x) -> s x, gcd(s x, 0()) -> s x, gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [min](x0, x1) = x0 + x1 + 1, [max](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + 1, [gcd](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [max#](x0, x1) = x0 Strict: max#(s x, s y) -> max#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y)) 2 + 0x + 1y >= 3 + 1x + 1y gcd(s x, 0()) -> s x 2 + 0x >= 1 + 1x gcd(0(), s x) -> s x 2 + 1x >= 1 + 1x -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x max(s x, s y) -> s max(x, y) 3 + 1x + 1y >= 2 + 1x + 1y max(0(), y) -> y 2 + 1y >= 1y max(x, 0()) -> x 2 + 1x >= 1x min(s x, s y) -> s min(x, y) 3 + 1x + 1y >= 2 + 1x + 1y min(0(), y) -> 0() 2 + 1y >= 1 min(x, 0()) -> 0() 2 + 1x >= 1 Qed SCC (1): Strict: {min#(s x, s y) -> min#(x, y)} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s x, s y) -> s min(x, y), max(x, 0()) -> x, max(0(), y) -> y, max(s x, s y) -> s max(x, y), -(x, 0()) -> x, -(s x, s y) -> -(x, y), gcd(0(), s x) -> s x, gcd(s x, 0()) -> s x, gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [min](x0, x1) = x0 + x1 + 1, [max](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + 1, [gcd](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [min#](x0, x1) = x0 Strict: min#(s x, s y) -> min#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y)) 2 + 0x + 1y >= 3 + 1x + 1y gcd(s x, 0()) -> s x 2 + 0x >= 1 + 1x gcd(0(), s x) -> s x 2 + 1x >= 1 + 1x -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x max(s x, s y) -> s max(x, y) 3 + 1x + 1y >= 2 + 1x + 1y max(0(), y) -> y 2 + 1y >= 1y max(x, 0()) -> x 2 + 1x >= 1x min(s x, s y) -> s min(x, y) 3 + 1x + 1y >= 2 + 1x + 1y min(0(), y) -> 0() 2 + 1y >= 1 min(x, 0()) -> 0() 2 + 1x >= 1 Qed SCC (1): Strict: {-#(s x, s y) -> -#(x, y)} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s x, s y) -> s min(x, y), max(x, 0()) -> x, max(0(), y) -> y, max(s x, s y) -> s max(x, y), -(x, 0()) -> x, -(s x, s y) -> -(x, y), gcd(0(), s x) -> s x, gcd(s x, 0()) -> s x, gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [min](x0, x1) = x0 + x1 + 1, [max](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + 1, [gcd](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [-#](x0, x1) = x0 Strict: -#(s x, s y) -> -#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: gcd(s x, s y) -> gcd(-(max(x, y), min(x, y)), s min(x, y)) 2 + 0x + 1y >= 3 + 1x + 1y gcd(s x, 0()) -> s x 2 + 0x >= 1 + 1x gcd(0(), s x) -> s x 2 + 1x >= 1 + 1x -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x max(s x, s y) -> s max(x, y) 3 + 1x + 1y >= 2 + 1x + 1y max(0(), y) -> y 2 + 1y >= 1y max(x, 0()) -> x 2 + 1x >= 1x min(s x, s y) -> s min(x, y) 3 + 1x + 1y >= 2 + 1x + 1y min(0(), y) -> 0() 2 + 1y >= 1 min(x, 0()) -> 0() 2 + 1x >= 1 Qed