MAYBE Time: 0.129379 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), p s x -> x, f(x, y, 0()) -> max(x, y), f(x, 0(), z) -> max(x, z), f(0(), y, z) -> max(y, z), f(s x, s y, s z) -> f(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))} DP: DP: { min#(s x, s y) -> min#(x, y), max#(s x, s y) -> max#(x, y), f#(x, y, 0()) -> max#(x, y), f#(x, 0(), z) -> max#(x, z), f#(0(), y, z) -> max#(y, z), f#(s x, s y, s z) -> min#(s y, s z), f#(s x, s y, s z) -> min#(s x, min(s y, s z)), f#(s x, s y, s z) -> min#(s x, max(s y, s z)), f#(s x, s y, s z) -> max#(s y, s z), f#(s x, s y, s z) -> max#(s x, max(s y, s z)), f#(s x, s y, s z) -> p# min(s x, max(s y, s z)), f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))} 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), p s x -> x, f(x, y, 0()) -> max(x, y), f(x, 0(), z) -> max(x, z), f(0(), y, z) -> max(y, z), f(s x, s y, s z) -> f(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))} 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), p s x -> x, a(w, v) -> w, a(w, v) -> v} EDG: {(f#(s x, s y, s z) -> max#(s y, s z), max#(s x, s y) -> max#(x, y)) (f#(x, 0(), z) -> max#(x, z), max#(s x, s y) -> max#(x, y)) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(s x, s y, s z) -> p# min(s x, max(s y, s z))) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(s x, s y, s z) -> max#(s x, max(s y, s z))) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(s x, s y, s z) -> max#(s y, s z)) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(s x, s y, s z) -> min#(s x, max(s y, s z))) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(s x, s y, s z) -> min#(s x, min(s y, s z))) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(s x, s y, s z) -> min#(s y, s z)) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(0(), y, z) -> max#(y, z)) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(x, 0(), z) -> max#(x, z)) (f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))), f#(x, y, 0()) -> max#(x, y)) (max#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y)) (f#(s x, s y, s z) -> min#(s x, min(s y, s z)), min#(s x, s y) -> min#(x, y)) (f#(s x, s y, s z) -> max#(s x, max(s y, s z)), max#(s x, s y) -> max#(x, y)) (f#(s x, s y, s z) -> min#(s x, max(s y, s z)), min#(s x, s y) -> min#(x, y)) (f#(x, y, 0()) -> max#(x, y), max#(s x, s y) -> max#(x, y)) (min#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y)) (f#(0(), y, z) -> max#(y, z), max#(s x, s y) -> max#(x, y)) (f#(s x, s y, s z) -> min#(s y, s z), min#(s x, s y) -> min#(x, y))} STATUS: arrows: 0.861111 SCCS (3): Scc: {f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))} Scc: {max#(s x, s y) -> max#(x, y)} Scc: {min#(s x, s y) -> min#(x, y)} SCC (1): Strict: {f#(s x, s y, s z) -> f#(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))} 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), p s x -> x, f(x, y, 0()) -> max(x, y), f(x, 0(), z) -> max(x, z), f(0(), y, z) -> max(y, z), f(s x, s y, s z) -> f(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))} 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), p s x -> x, f(x, y, 0()) -> max(x, y), f(x, 0(), z) -> max(x, z), f(0(), y, z) -> max(y, z), f(s x, s y, s z) -> f(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + 1, [min](x0, x1) = x0 + x1 + 1, [max](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [p](x0) = x0 + 1, [0] = 1, [max#](x0, x1) = x0 + 1 Strict: max#(s x, s y) -> max#(x, y) 2 + 0y + 1x >= 1 + 0y + 1x Weak: f(s x, s y, s z) -> f(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))) 3 + 1y + 0x + 1z >= 12 + 2y + 2x + 2z f(0(), y, z) -> max(y, z) 1 + 1y + 1z >= 1 + 1y + 1z f(x, 0(), z) -> max(x, z) 2 + 0x + 1z >= 1 + 1x + 1z f(x, y, 0()) -> max(x, y) 2 + 1y + 0x >= 1 + 1y + 1x p s x -> x 2 + 1x >= 1x max(s x, s y) -> s max(x, y) 3 + 1y + 1x >= 2 + 1y + 1x max(0(), y) -> y 2 + 1y >= 1y max(x, 0()) -> x 2 + 1x >= 1x min(s x, s y) -> s min(x, y) 3 + 1y + 1x >= 2 + 1y + 1x 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), p s x -> x, f(x, y, 0()) -> max(x, y), f(x, 0(), z) -> max(x, z), f(0(), y, z) -> max(y, z), f(s x, s y, s z) -> f(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + 1, [min](x0, x1) = x0 + x1 + 1, [max](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [p](x0) = x0 + 1, [0] = 1, [min#](x0, x1) = x0 + 1 Strict: min#(s x, s y) -> min#(x, y) 2 + 0y + 1x >= 1 + 0y + 1x Weak: f(s x, s y, s z) -> f(max(s x, max(s y, s z)), p min(s x, max(s y, s z)), min(s x, min(s y, s z))) 3 + 1y + 0x + 1z >= 12 + 2y + 2x + 2z f(0(), y, z) -> max(y, z) 1 + 1y + 1z >= 1 + 1y + 1z f(x, 0(), z) -> max(x, z) 2 + 0x + 1z >= 1 + 1x + 1z f(x, y, 0()) -> max(x, y) 2 + 1y + 0x >= 1 + 1y + 1x p s x -> x 2 + 1x >= 1x max(s x, s y) -> s max(x, y) 3 + 1y + 1x >= 2 + 1y + 1x max(0(), y) -> y 2 + 1y >= 1y max(x, 0()) -> x 2 + 1x >= 1x min(s x, s y) -> s min(x, y) 3 + 1y + 1x >= 2 + 1y + 1x min(0(), y) -> 0() 2 + 1y >= 1 min(x, 0()) -> 0() 2 + 1x >= 1 Qed