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