YES TRS: { f(x) -> g(x), f(a()) -> f(b()), g(b()) -> g(a())} DP: Strict: { f#(x) -> g#(x), f#(a()) -> f#(b()), g#(b()) -> g#(a())} Weak: { f(x) -> g(x), f(a()) -> f(b()), g(b()) -> g(a())} EDG: {(f#(x) -> g#(x), g#(b()) -> g#(a())) (f#(a()) -> f#(b()), f#(x) -> g#(x))} SCCS: Qed