YES Time: 0.047538 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) } 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) } 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) (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) (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) (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) (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)} 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) (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) (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) (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) (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.437500 SCCS (1): 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 (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