YES Problem: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) Proof: DP Processor: DPs: p#(f(f(x))) -> q#(f(g(x))) p#(g(g(x))) -> q#(g(f(x))) q#(f(f(x))) -> p#(f(g(x))) q#(g(g(x))) -> p#(g(f(x))) TRS: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) TDG Processor: DPs: p#(f(f(x))) -> q#(f(g(x))) p#(g(g(x))) -> q#(g(f(x))) q#(f(f(x))) -> p#(f(g(x))) q#(g(g(x))) -> p#(g(f(x))) TRS: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) graph: q#(g(g(x))) -> p#(g(f(x))) -> p#(g(g(x))) -> q#(g(f(x))) q#(g(g(x))) -> p#(g(f(x))) -> p#(f(f(x))) -> q#(f(g(x))) q#(f(f(x))) -> p#(f(g(x))) -> p#(g(g(x))) -> q#(g(f(x))) q#(f(f(x))) -> p#(f(g(x))) -> p#(f(f(x))) -> q#(f(g(x))) p#(g(g(x))) -> q#(g(f(x))) -> q#(g(g(x))) -> p#(g(f(x))) p#(g(g(x))) -> q#(g(f(x))) -> q#(f(f(x))) -> p#(f(g(x))) p#(f(f(x))) -> q#(f(g(x))) -> q#(g(g(x))) -> p#(g(f(x))) p#(f(f(x))) -> q#(f(g(x))) -> q#(f(f(x))) -> p#(f(g(x))) EDG Processor: DPs: p#(f(f(x))) -> q#(f(g(x))) p#(g(g(x))) -> q#(g(f(x))) q#(f(f(x))) -> p#(f(g(x))) q#(g(g(x))) -> p#(g(f(x))) TRS: p(f(f(x))) -> q(f(g(x))) p(g(g(x))) -> q(g(f(x))) q(f(f(x))) -> p(f(g(x))) q(g(g(x))) -> p(g(f(x))) graph: Qed