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