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