YES Time: 0.000407 TRS: {f(f(x, a()), a()) -> f(f(f(x, a()), f(a(), a())), a())} DP: DP: {f#(f(x, a()), a()) -> f#(f(x, a()), f(a(), a())), f#(f(x, a()), a()) -> f#(f(f(x, a()), f(a(), a())), a()), f#(f(x, a()), a()) -> f#(a(), a())} TRS: {f(f(x, a()), a()) -> f(f(f(x, a()), f(a(), a())), a())} EDG: {} SCCS (0): Qed