YES Time: 0.022479 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)} 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)} 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)} UR: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), double 0() -> 0(), double s x -> s s double x, a(z, w) -> z, a(z, w) -> w} EDG: {(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)) (double# s x -> double# x, double# s x -> double# x) (plus#(s x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> minus#(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) -> plus#(x, 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#(minus(x, y), double y)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> double# y, double# s x -> double# x) (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))} EDG: {(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)) (double# s x -> double# x, double# s x -> double# x) (plus#(s x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> minus#(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) -> plus#(x, 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#(minus(x, y), double y)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> double# y, double# s x -> double# x) (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))} EDG: {(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)) (double# s x -> double# x, double# s x -> double# x) (plus#(s x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> minus#(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) -> plus#(x, 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#(minus(x, y), double y)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> double# y, double# s x -> double# x) (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))} EDG: {(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)) (double# s x -> double# x, double# s x -> double# x) (plus#(s x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> minus#(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) -> plus#(x, 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#(minus(x, y), double y)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (plus#(s x, y) -> double# y, double# s x -> double# x) (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))} STATUS: arrows: 0.612245 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)} Scc: {double# s x -> double# x} Scc: {minus#(s x, s y) -> minus#(x, y)} SCC (3): 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)} 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [minus](x0, x1) = x0, [plus](x0, x1) = 0, [s](x0) = x0 + 1, [double](x0) = x0 + 1, [0] = 1, [plus#](x0, x1) = x0 Strict: plus#(s x, y) -> plus#(minus(x, y), double y) 1 + 1x + 0y >= 0 + 1x + 0y plus#(s x, y) -> plus#(x, s y) 1 + 1x + 0y >= 0 + 1x + 0y plus#(s x, y) -> plus#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: 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) 1 + 1x + 0y >= 0 + 1x + 0y minus(x, 0()) -> x 0 + 1x >= 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [minus](x0, x1) = x0 + x1 + 1, [plus](x0, x1) = x0 + x1, [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 x, y) -> plus(x, s y) 1 + 1x + 1y >= 1 + 1x + 1y plus(s x, y) -> s plus(minus(x, y), double y) 1 + 1x + 1y >= 3 + 1x + 2y plus(s x, y) -> s plus(x, y) 1 + 1x + 1y >= 1 + 1x + 1y plus(0(), y) -> y 1 + 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) 3 + 1x + 1y >= 1 + 1x + 1y minus(x, 0()) -> x 2 + 1x >= 1x Qed 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [minus](x0, x1) = x0 + 1, [plus](x0, x1) = x0, [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 x, y) -> plus(x, s y) 0 + 0x + 1y >= 1 + 0x + 1y plus(s x, y) -> s plus(minus(x, y), double y) 0 + 0x + 1y >= 2 + 0x + 1y plus(s x, y) -> s plus(x, y) 0 + 0x + 1y >= 1 + 0x + 1y plus(0(), y) -> y 0 + 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