MAYBE Time: 0.484415 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), twice 0() -> 0(), twice s x -> s s twice x, -(x, 0()) -> x, -(s x, s y) -> -(x, y), p s x -> x, f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice min(x, y))} DP: DP: {min#(s x, s y) -> min#(x, y), max#(s x, s y) -> max#(x, y), twice# s x -> twice# x, -#(s x, s y) -> -#(x, y), f#(s x, s y) -> min#(x, y), f#(s x, s y) -> min#(s x, s y), f#(s x, s y) -> max#(s x, s y), f#(s x, s y) -> twice# min(x, y), f#(s x, s y) -> -#(max(s x, s y), min(s x, s y)), f#(s x, s y) -> p# twice min(x, y), f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice 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), twice 0() -> 0(), twice s x -> s s twice x, -(x, 0()) -> x, -(s x, s y) -> -(x, y), p s x -> x, f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice min(x, y))} EDG: {(f#(s x, s y) -> max#(s x, s y), max#(s x, s y) -> max#(x, y)) (f#(s x, s y) -> twice# min(x, y), twice# s x -> twice# x) (f#(s x, s y) -> -#(max(s x, s y), min(s x, s y)), -#(s x, s y) -> -#(x, y)) (min#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (f#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y)) (max#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y)) (f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y)), f#(s x, s y) -> min#(x, y)) (f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y)), f#(s x, s y) -> min#(s x, s y)) (f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y)), f#(s x, s y) -> max#(s x, s y)) (f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y)), f#(s x, s y) -> twice# min(x, y)) (f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y)), f#(s x, s y) -> -#(max(s x, s y), min(s x, s y))) (f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y)), f#(s x, s y) -> p# twice min(x, y)) (f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y)), f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y))) (twice# s x -> twice# x, twice# s x -> twice# x) (f#(s x, s y) -> min#(s x, s y), min#(s x, s y) -> min#(x, y))} STATUS: arrows: 0.867769 SCCS (5): Scc: {f#(s x, s y) -> f#(-(max(s x, s y), min(s x, s y)), p twice min(x, y))} Scc: {-#(s x, s y) -> -#(x, y)} Scc: {twice# s x -> twice# x} 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) -> f#(-(max(s x, s y), min(s x, s y)), p twice 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), twice 0() -> 0(), twice s x -> s s twice x, -(x, 0()) -> x, -(s x, s y) -> -(x, y), p s x -> x, f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice min(x, y))} Fail 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), twice 0() -> 0(), twice s x -> s s twice x, -(x, 0()) -> x, -(s x, s y) -> -(x, y), p s x -> x, f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice 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, [f](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [twice](x0) = x0 + 1, [p](x0) = x0 + 1, [0] = 1, [-#](x0, x1) = x0 + 1 Strict: -#(s x, s y) -> -#(x, y) 2 + 0y + 1x >= 1 + 0y + 1x Weak: f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice min(x, y)) 2 + 0y + 1x >= 5 + 1y + 1x p s x -> x 2 + 1x >= 1x -(s x, s y) -> -(x, y) 2 + 1y + 0x >= 1 + 1y + 0x -(x, 0()) -> x 2 + 0x >= 1x twice s x -> s s twice x 2 + 1x >= 3 + 1x twice 0() -> 0() 2 >= 1 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: {twice# s x -> twice# x} 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), twice 0() -> 0(), twice s x -> s s twice x, -(x, 0()) -> x, -(s x, s y) -> -(x, y), p s x -> x, f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice 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 + 1, [-](x0, x1) = x0 + 1, [f](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [twice](x0) = x0 + 1, [p](x0) = x0 + 1, [0] = 1, [twice#](x0) = x0 + 1 Strict: twice# s x -> twice# x 2 + 1x >= 1 + 1x Weak: f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice min(x, y)) 2 + 0y + 1x >= 5 + 1y + 1x p s x -> x 2 + 1x >= 1x -(s x, s y) -> -(x, y) 2 + 1y + 0x >= 1 + 1y + 0x -(x, 0()) -> x 2 + 0x >= 1x twice s x -> s s twice x 2 + 1x >= 3 + 1x twice 0() -> 0() 2 >= 1 max(s x, s y) -> s max(x, y) 2 + 1y + 0x >= 2 + 1y + 0x max(0(), y) -> y 1 + 1y >= 1y max(x, 0()) -> x 2 + 0x >= 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: {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), twice 0() -> 0(), twice s x -> s s twice x, -(x, 0()) -> x, -(s x, s y) -> -(x, y), p s x -> x, f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice 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, [f](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [twice](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) -> f(-(max(s x, s y), min(s x, s y)), p twice min(x, y)) 2 + 0y + 1x >= 5 + 1y + 1x p s x -> x 2 + 1x >= 1x -(s x, s y) -> -(x, y) 2 + 1y + 0x >= 1 + 1y + 0x -(x, 0()) -> x 2 + 0x >= 1x twice s x -> s s twice x 2 + 1x >= 3 + 1x twice 0() -> 0() 2 >= 1 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), twice 0() -> 0(), twice s x -> s s twice x, -(x, 0()) -> x, -(s x, s y) -> -(x, y), p s x -> x, f(s x, s y) -> f(-(max(s x, s y), min(s x, s y)), p twice 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, [f](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [twice](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) -> f(-(max(s x, s y), min(s x, s y)), p twice min(x, y)) 2 + 0y + 1x >= 5 + 1y + 1x p s x -> x 2 + 1x >= 1x -(s x, s y) -> -(x, y) 2 + 1y + 0x >= 1 + 1y + 0x -(x, 0()) -> x 2 + 0x >= 1x twice s x -> s s twice x 2 + 1x >= 3 + 1x twice 0() -> 0() 2 >= 1 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