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