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