MAYBE Time: 0.033196 TRS: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), double 0() -> 0(), double s x -> s s double x, plus(0(), y) -> y, plus(s x, y) -> s plus(x, y), plus(s x, y) -> s plus(minus(x, y), double y), plus(s x, y) -> plus(x, s y), plus(s plus(x, y), z) -> s plus(plus(x, y), z)} DP: DP: { minus#(s x, s y) -> minus#(x, y), double# s x -> double# x, plus#(s x, y) -> minus#(x, y), plus#(s x, y) -> double# y, plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z)} TRS: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), double 0() -> 0(), double s x -> s s double x, plus(0(), y) -> y, plus(s x, y) -> s plus(x, y), plus(s x, y) -> s plus(minus(x, y), double y), plus(s x, y) -> plus(x, s y), plus(s plus(x, y), z) -> s plus(plus(x, y), z)} EDG: {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> plus#(x, y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(minus(x, y), double y)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, s y)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> double# y) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> minus#(x, y)) (plus#(s x, y) -> double# y, double# s x -> double# x) (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z)) (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(minus(x, y), double y)) (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(x, s y)) (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(x, y)) (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> double# y) (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> minus#(x, y)) (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> minus#(x, y)) (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> double# y) (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, y)) (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, s y)) (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(minus(x, y), double y)) (plus#(s x, y) -> plus#(x, s y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z)) (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> minus#(x, y)) (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> double# y) (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> plus#(x, y)) (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> plus#(x, s y)) (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> plus#(minus(x, y), double y)) (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s plus(x, y), z) -> plus#(plus(x, y), z)) (plus#(s x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (double# s x -> double# x, double# s x -> double# x)} STATUS: arrows: 0.562500 SCCS (3): Scc: { plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z)} Scc: {minus#(s x, s y) -> minus#(x, y)} Scc: {double# s x -> double# x} SCC (4): Strict: { plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), double 0() -> 0(), double s x -> s s double x, plus(0(), y) -> y, plus(s x, y) -> s plus(x, y), plus(s x, y) -> s plus(minus(x, y), double y), plus(s x, y) -> plus(x, s y), plus(s plus(x, y), z) -> s plus(plus(x, y), z)} Fail SCC (1): Strict: {minus#(s x, s y) -> minus#(x, y)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), double 0() -> 0(), double s x -> s s double x, plus(0(), y) -> y, plus(s x, y) -> s plus(x, y), plus(s x, y) -> s plus(minus(x, y), double y), plus(s x, y) -> plus(x, s y), plus(s plus(x, y), z) -> s plus(plus(x, y), z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [minus](x0, x1) = x0 + 1, [plus](x0, x1) = 0, [s](x0) = x0 + 1, [double](x0) = x0 + 1, [0] = 1, [minus#](x0, x1) = x0 Strict: minus#(s x, s y) -> minus#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: plus(s plus(x, y), z) -> s plus(plus(x, y), z) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z plus(s x, y) -> plus(x, s y) 0 + 0x + 0y >= 0 + 0x + 0y plus(s x, y) -> s plus(minus(x, y), double y) 0 + 0x + 0y >= 1 + 0x + 0y plus(s x, y) -> s plus(x, y) 0 + 0x + 0y >= 1 + 0x + 0y plus(0(), y) -> y 0 + 0y >= 1y double s x -> s s double x 2 + 1x >= 3 + 1x double 0() -> 0() 2 >= 1 minus(s x, s y) -> minus(x, y) 2 + 0x + 1y >= 1 + 0x + 1y minus(x, 0()) -> x 2 + 0x >= 1x Qed SCC (1): Strict: {double# s x -> double# x} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), double 0() -> 0(), double s x -> s s double x, plus(0(), y) -> y, plus(s x, y) -> s plus(x, y), plus(s x, y) -> s plus(minus(x, y), double y), plus(s x, y) -> plus(x, s y), plus(s plus(x, y), z) -> s plus(plus(x, y), z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [minus](x0, x1) = x0 + 1, [plus](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [double](x0) = x0 + 1, [0] = 1, [double#](x0) = x0 Strict: double# s x -> double# x 1 + 1x >= 0 + 1x Weak: plus(s plus(x, y), z) -> s plus(plus(x, y), z) 3 + 1x + 1y + 1z >= 3 + 1x + 1y + 1z plus(s x, y) -> plus(x, s y) 2 + 1x + 1y >= 2 + 1x + 1y plus(s x, y) -> s plus(minus(x, y), double y) 2 + 1x + 1y >= 4 + 0x + 2y plus(s x, y) -> s plus(x, y) 2 + 1x + 1y >= 2 + 1x + 1y plus(0(), y) -> y 2 + 1y >= 1y double s x -> s s double x 2 + 1x >= 3 + 1x double 0() -> 0() 2 >= 1 minus(s x, s y) -> minus(x, y) 2 + 0x + 1y >= 1 + 0x + 1y minus(x, 0()) -> x 2 + 0x >= 1x Qed