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