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