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