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