YES Time: 0.001536 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: DP: {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))} 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))} EDG: {(g#(h(x, y), z) -> g#(x, f(y, z)), 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#(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#(f(x, y), z) -> g#(y, z), g#(x, h(y, z)) -> g#(x, y)) (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#(h(x, y), z) -> g#(x, f(y, z)))} SCCS (1): 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 (3): 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 (2): Scc: {g#(h(x, y), z) -> g#(x, f(y, z))} Scc: {g#(x, h(y, z)) -> g#(x, y)} SCC (1): 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 (1): 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