YES Time: 0.036946 TRS: { +(x, 0()) -> x, +(minus x, x) -> 0(), minus +(x, y) -> +(minus y, minus x), minus 0() -> 0(), minus minus x -> x, *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(x, 0()) -> 0(), *(x, minus y) -> minus *(x, y), *(x, 1()) -> x} DP: DP: {minus# +(x, y) -> +#(minus y, minus x), minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y, *#(x, +(y, z)) -> +#(*(x, y), *(x, z)), *#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> minus# *(x, y), *#(x, minus y) -> *#(x, y)} TRS: { +(x, 0()) -> x, +(minus x, x) -> 0(), minus +(x, y) -> +(minus y, minus x), minus 0() -> 0(), minus minus x -> x, *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(x, 0()) -> 0(), *(x, minus y) -> minus *(x, y), *(x, 1()) -> x} UR: { +(x, 0()) -> x, +(minus x, x) -> 0(), minus +(x, y) -> +(minus y, minus x), minus 0() -> 0(), minus minus x -> x, *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(x, 0()) -> 0(), *(x, minus y) -> minus *(x, y), *(x, 1()) -> x, a(w, v) -> w, a(w, v) -> v} EDG: {(*#(x, minus y) -> *#(x, y), *#(x, minus y) -> *#(x, y)) (*#(x, minus y) -> *#(x, y), *#(x, minus y) -> minus# *(x, y)) (*#(x, minus y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, minus y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, minus y) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# y) (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# x) (minus# +(x, y) -> minus# y, minus# +(x, y) -> +#(minus y, minus x)) (*#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> minus# *(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> +#(minus y, minus x)) (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> minus# x) (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> minus# y) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(x, minus y) -> minus# *(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, minus y) -> *#(x, y)) (minus# +(x, y) -> minus# x, minus# +(x, y) -> +#(minus y, minus x)) (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# x) (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y)} STATUS: arrows: 0.625000 SCCS (2): Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> *#(x, y)} Scc: {minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y} SCC (3): Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> *#(x, y)} Weak: { +(x, 0()) -> x, +(minus x, x) -> 0(), minus +(x, y) -> +(minus y, minus x), minus 0() -> 0(), minus minus x -> x, *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(x, 0()) -> 0(), *(x, minus y) -> minus *(x, y), *(x, 1()) -> x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1, [*](x0, x1) = x0 + x1, [minus](x0) = x0 + 1, [0] = 1, [1] = 0, [*#](x0, x1) = x0 Strict: *#(x, minus y) -> *#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y *#(x, +(y, z)) -> *#(x, z) 0 + 0x + 1y + 1z >= 0 + 0x + 1z *#(x, +(y, z)) -> *#(x, y) 0 + 0x + 1y + 1z >= 0 + 0x + 1y Weak: *(x, 1()) -> x 0 + 1x >= 1x *(x, minus y) -> minus *(x, y) 1 + 1x + 1y >= 1 + 1x + 1y *(x, 0()) -> 0() 1 + 1x >= 1 *(x, +(y, z)) -> +(*(x, y), *(x, z)) 0 + 1x + 1y + 1z >= 0 + 2x + 1y + 1z minus minus x -> x 2 + 1x >= 1x minus 0() -> 0() 2 >= 1 minus +(x, y) -> +(minus y, minus x) 1 + 1x + 1y >= 2 + 1x + 1y +(minus x, x) -> 0() 1 + 2x >= 1 +(x, 0()) -> x 1 + 1x >= 1x SCCS (1): Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)} SCC (2): Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)} Weak: { +(x, 0()) -> x, +(minus x, x) -> 0(), minus +(x, y) -> +(minus y, minus x), minus 0() -> 0(), minus minus x -> x, *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(x, 0()) -> 0(), *(x, minus y) -> minus *(x, y), *(x, 1()) -> x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [*](x0, x1) = x0 + x1 + 1, [minus](x0) = 0, [0] = 1, [1] = 0, [*#](x0, x1) = x0 Strict: *#(x, +(y, z)) -> *#(x, z) 1 + 0x + 1y + 1z >= 0 + 0x + 1z *#(x, +(y, z)) -> *#(x, y) 1 + 0x + 1y + 1z >= 0 + 0x + 1y Weak: *(x, 1()) -> x 1 + 1x >= 1x *(x, minus y) -> minus *(x, y) 1 + 1x + 0y >= 0 + 0x + 0y *(x, 0()) -> 0() 2 + 1x >= 1 *(x, +(y, z)) -> +(*(x, y), *(x, z)) 2 + 1x + 1y + 1z >= 3 + 2x + 1y + 1z minus minus x -> x 0 + 0x >= 1x minus 0() -> 0() 0 >= 1 minus +(x, y) -> +(minus y, minus x) 0 + 0x + 0y >= 1 + 0x + 0y +(minus x, x) -> 0() 1 + 1x >= 1 +(x, 0()) -> x 2 + 1x >= 1x Qed SCC (2): Strict: {minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y} Weak: { +(x, 0()) -> x, +(minus x, x) -> 0(), minus +(x, y) -> +(minus y, minus x), minus 0() -> 0(), minus minus x -> x, *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(x, 0()) -> 0(), *(x, minus y) -> minus *(x, y), *(x, 1()) -> x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [*](x0, x1) = x0 + x1 + 1, [minus](x0) = 0, [0] = 1, [1] = 0, [minus#](x0) = x0 Strict: minus# +(x, y) -> minus# y 1 + 1x + 1y >= 0 + 1y minus# +(x, y) -> minus# x 1 + 1x + 1y >= 0 + 1x Weak: *(x, 1()) -> x 1 + 1x >= 1x *(x, minus y) -> minus *(x, y) 1 + 1x + 0y >= 0 + 0x + 0y *(x, 0()) -> 0() 2 + 1x >= 1 *(x, +(y, z)) -> +(*(x, y), *(x, z)) 2 + 1x + 1y + 1z >= 3 + 2x + 1y + 1z minus minus x -> x 0 + 0x >= 1x minus 0() -> 0() 0 >= 1 minus +(x, y) -> +(minus y, minus x) 0 + 0x + 0y >= 1 + 0x + 0y +(minus x, x) -> 0() 1 + 1x >= 1 +(x, 0()) -> x 2 + 1x >= 1x Qed