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