YES Time: 0.014364 TRS: {minus minus x -> x, minus *(x, y) -> +(minus minus minus x, minus minus minus y), minus +(x, y) -> *(minus minus minus x, minus minus minus y), f minus x -> minus minus minus f x} DP: DP: {minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus y, f# minus x -> minus# minus minus f x, f# minus x -> minus# minus f x, f# minus x -> minus# f x, f# minus x -> f# x} TRS: {minus minus x -> x, minus *(x, y) -> +(minus minus minus x, minus minus minus y), minus +(x, y) -> *(minus minus minus x, minus minus minus y), f minus x -> minus minus minus f x} EDG: { (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# minus y) (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# minus x) (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y) (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# x) (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# minus y) (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# minus x) (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# y) (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# x) (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus y) (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus x) (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# y) (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# x) (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus y) (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus x) (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# y) (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# x) (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus y) (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus x) (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# y) (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# x) (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus y) (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus x) (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# y) (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# x) (f# minus x -> minus# f x, minus# +(x, y) -> minus# minus minus y) (f# minus x -> minus# f x, minus# +(x, y) -> minus# minus minus x) (f# minus x -> minus# f x, minus# +(x, y) -> minus# minus y) (f# minus x -> minus# f x, minus# +(x, y) -> minus# minus x) (f# minus x -> minus# f x, minus# +(x, y) -> minus# y) (f# minus x -> minus# f x, minus# +(x, y) -> minus# x) (f# minus x -> minus# f x, minus# *(x, y) -> minus# minus minus y) (f# minus x -> minus# f x, minus# *(x, y) -> minus# minus minus x) (f# minus x -> minus# f x, minus# *(x, y) -> minus# minus y) (f# minus x -> minus# f x, minus# *(x, y) -> minus# minus x) (f# minus x -> minus# f x, minus# *(x, y) -> minus# y) (f# minus x -> minus# f x, minus# *(x, y) -> minus# x) (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus y) (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus x) (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# minus minus y) (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# minus y) (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# minus x) (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# y) (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# x) (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus y) (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus x) (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# y) (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# x) (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus y) (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus x) (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# y) (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# x) (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus y) (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus x) (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# y) (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# x) (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus y) (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus x) (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# y) (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# x) (f# minus x -> minus# minus f x, minus# +(x, y) -> minus# minus minus y) (f# minus x -> minus# minus f x, minus# +(x, y) -> minus# minus minus x) (f# minus x -> minus# minus f x, minus# +(x, y) -> minus# minus y) (f# minus x -> minus# minus f x, minus# +(x, y) -> minus# minus x) (f# minus x -> minus# minus f x, minus# +(x, y) -> minus# y) (f# minus x -> minus# minus f x, minus# +(x, y) -> minus# x) (f# minus x -> minus# minus f x, minus# *(x, y) -> minus# minus minus y) (f# minus x -> minus# minus f x, minus# *(x, y) -> minus# minus minus x) (f# minus x -> minus# minus f x, minus# *(x, y) -> minus# minus y) (f# minus x -> minus# minus f x, minus# *(x, y) -> minus# minus x) (f# minus x -> minus# minus f x, minus# *(x, y) -> minus# y) (f# minus x -> minus# minus f x, minus# *(x, y) -> minus# x) (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# x) (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# y) (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus x) (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus y) (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# x) (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# y) (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus x) (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus y) (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# x) (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# y) (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus x) (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus y) (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# x) (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# y) (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus x) (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus y) (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus minus y) (f# minus x -> minus# minus minus f x, minus# *(x, y) -> minus# x) (f# minus x -> minus# minus minus f x, minus# *(x, y) -> minus# y) (f# minus x -> minus# minus minus f x, minus# *(x, y) -> minus# minus x) (f# minus x -> minus# minus minus f x, minus# *(x, y) -> minus# minus y) (f# minus x -> minus# minus minus f x, minus# *(x, y) -> minus# minus minus x) (f# minus x -> minus# minus minus f x, minus# *(x, y) -> minus# minus minus y) (f# minus x -> minus# minus minus f x, minus# +(x, y) -> minus# x) (f# minus x -> minus# minus minus f x, minus# +(x, y) -> minus# y) (f# minus x -> minus# minus minus f x, minus# +(x, y) -> minus# minus x) (f# minus x -> minus# minus minus f x, minus# +(x, y) -> minus# minus y) (f# minus x -> minus# minus minus f x, minus# +(x, y) -> minus# minus minus x) (f# minus x -> minus# minus minus f x, minus# +(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# x) (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# y) (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus x) (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus y) (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# x) (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# y) (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# minus x) (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# minus y) (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# x) (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# y) (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus x) (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus y) (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# x) (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# y) (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus x) (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus y) (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# x) (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# y) (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus x) (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus y) (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus y) (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# x) (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# y) (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus x) (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus y) (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus x) (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus y) (f# minus x -> f# x, f# minus x -> minus# minus minus f x) (f# minus x -> f# x, f# minus x -> minus# minus f x) (f# minus x -> f# x, f# minus x -> minus# f x) (f# minus x -> f# x, f# minus x -> f# x) (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# x) (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# y) (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# minus x) (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# minus y) (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# minus minus y) (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# x) (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# y) (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# minus x) (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# minus y) (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# minus minus x) (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# minus minus y) } SCCS (2): Scc: {f# minus x -> f# x} Scc: {minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus y} SCC (1): Strict: {f# minus x -> f# x} Weak: {minus minus x -> x, minus *(x, y) -> +(minus minus minus x, minus minus minus y), minus +(x, y) -> *(minus minus minus x, minus minus minus y), f minus x -> minus minus minus f x} SPSC: Simple Projection: pi(f#) = 0 Strict: {} Qed SCC (12): Strict: {minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus y} Weak: {minus minus x -> x, minus *(x, y) -> +(minus minus minus x, minus minus minus y), minus +(x, y) -> *(minus minus minus x, minus minus minus y), f minus x -> minus minus minus f 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) = x0, [f](x0) = 0, [minus#](x0) = x0 Strict: minus# +(x, y) -> minus# minus minus y 1 + 1x + 1y >= 0 + 1y minus# +(x, y) -> minus# minus minus x 1 + 1x + 1y >= 0 + 1x minus# +(x, y) -> minus# minus y 1 + 1x + 1y >= 0 + 1y minus# +(x, y) -> minus# minus x 1 + 1x + 1y >= 0 + 1x minus# +(x, y) -> minus# y 1 + 1x + 1y >= 0 + 1y minus# +(x, y) -> minus# x 1 + 1x + 1y >= 0 + 1x minus# *(x, y) -> minus# minus minus y 1 + 1x + 1y >= 0 + 1y minus# *(x, y) -> minus# minus minus x 1 + 1x + 1y >= 0 + 1x minus# *(x, y) -> minus# minus y 1 + 1x + 1y >= 0 + 1y minus# *(x, y) -> minus# minus x 1 + 1x + 1y >= 0 + 1x minus# *(x, y) -> minus# y 1 + 1x + 1y >= 0 + 1y minus# *(x, y) -> minus# x 1 + 1x + 1y >= 0 + 1x Weak: Qed