YES Time: 0.001357 TRS: {minus minus x -> x, minus h x -> h minus x, minus f(x, y) -> f(minus y, minus x)} DP: DP: { minus# h x -> minus# x, minus# f(x, y) -> minus# x, minus# f(x, y) -> minus# y} TRS: {minus minus x -> x, minus h x -> h minus x, minus f(x, y) -> f(minus y, minus x)} EDG: {(minus# h x -> minus# x, minus# f(x, y) -> minus# y) (minus# h x -> minus# x, minus# f(x, y) -> minus# x) (minus# h x -> minus# x, minus# h x -> minus# x) (minus# f(x, y) -> minus# x, minus# h x -> minus# x) (minus# f(x, y) -> minus# x, minus# f(x, y) -> minus# x) (minus# f(x, y) -> minus# x, minus# f(x, y) -> minus# y) (minus# f(x, y) -> minus# y, minus# h x -> minus# x) (minus# f(x, y) -> minus# y, minus# f(x, y) -> minus# x) (minus# f(x, y) -> minus# y, minus# f(x, y) -> minus# y)} SCCS (1): Scc: { minus# h x -> minus# x, minus# f(x, y) -> minus# x, minus# f(x, y) -> minus# y} SCC (3): Strict: { minus# h x -> minus# x, minus# f(x, y) -> minus# x, minus# f(x, y) -> minus# y} Weak: {minus minus x -> x, minus h x -> h minus x, minus f(x, y) -> f(minus y, minus x)} SPSC: Simple Projection: pi(minus#) = 0 Strict: { minus# h x -> minus# x, minus# f(x, y) -> minus# y} EDG: {(minus# h x -> minus# x, minus# f(x, y) -> minus# y) (minus# h x -> minus# x, minus# h x -> minus# x) (minus# f(x, y) -> minus# y, minus# h x -> minus# x) (minus# f(x, y) -> minus# y, minus# f(x, y) -> minus# y)} SCCS (1): Scc: { minus# h x -> minus# x, minus# f(x, y) -> minus# y} SCC (2): Strict: { minus# h x -> minus# x, minus# f(x, y) -> minus# y} Weak: {minus minus x -> x, minus h x -> h minus x, minus f(x, y) -> f(minus y, minus x)} SPSC: Simple Projection: pi(minus#) = 0 Strict: {minus# f(x, y) -> minus# y} EDG: {(minus# f(x, y) -> minus# y, minus# f(x, y) -> minus# y)} SCCS (1): Scc: {minus# f(x, y) -> minus# y} SCC (1): Strict: {minus# f(x, y) -> minus# y} Weak: {minus minus x -> x, minus h x -> h minus x, minus f(x, y) -> f(minus y, minus x)} SPSC: Simple Projection: pi(minus#) = 0 Strict: {} Qed