YES Time: 0.026464 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} UR: {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) } STATUS: arrows: 0.281250 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [*](x0, x1) = 0, [+](x0, x1) = x0, [minus](x0) = x0 + 1, [f](x0) = 0, [f#](x0) = x0 Strict: f# minus x -> f# x 1 + 1x >= 0 + 1x Weak: f minus x -> minus minus minus f x 0 + 0x >= 3 + 0x minus +(x, y) -> *(minus minus minus x, minus minus minus y) 1 + 1x + 0y >= 0 + 0x + 0y minus *(x, y) -> +(minus minus minus x, minus minus minus y) 1 + 0x + 0y >= 3 + 1x + 0y minus minus x -> x 2 + 1x >= 1x 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: f minus x -> minus minus minus f x 0 + 0x >= 0 + 0x minus +(x, y) -> *(minus minus minus x, minus minus minus y) 1 + 1x + 1y >= 1 + 1x + 1y minus *(x, y) -> +(minus minus minus x, minus minus minus y) 1 + 1x + 1y >= 1 + 1x + 1y minus minus x -> x 0 + 1x >= 1x Qed