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))) Usable Rule 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: 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: 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))) Restore Modifier: 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))) SCC Processor: #sccs: 1 #rules: 4 #arcs: 8/16 DPs: 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))) 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))) Matrix Interpretation Processor: dimension: 1 interpretation: [q#](x0) = x0, [p#](x0) = x0, [q](x0) = 0, [g](x0) = 0, [p](x0) = 0, [f](x0) = x0 + 1 orientation: q#(g(g(x))) = 0 >= 0 = p#(g(f(x))) p#(f(f(x))) = x + 2 >= 1 = q#(f(g(x))) q#(f(f(x))) = x + 2 >= 1 = p#(f(g(x))) p#(g(g(x))) = 0 >= 0 = q#(g(f(x))) p(f(f(x))) = 0 >= 0 = q(f(g(x))) p(g(g(x))) = 0 >= 0 = q(g(f(x))) q(f(f(x))) = 0 >= 0 = p(f(g(x))) q(g(g(x))) = 0 >= 0 = p(g(f(x))) problem: DPs: q#(g(g(x))) -> p#(g(f(x))) p#(g(g(x))) -> q#(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))) Matrix Interpretation Processor: dimension: 1 interpretation: [q#](x0) = x0, [p#](x0) = x0 + 1, [q](x0) = 1, [g](x0) = x0 + 1, [p](x0) = 1, [f](x0) = 0 orientation: q#(g(g(x))) = x + 2 >= 2 = p#(g(f(x))) p#(g(g(x))) = x + 3 >= 1 = q#(g(f(x))) p(f(f(x))) = 1 >= 1 = q(f(g(x))) p(g(g(x))) = 1 >= 1 = q(g(f(x))) q(f(f(x))) = 1 >= 1 = p(f(g(x))) q(g(g(x))) = 1 >= 1 = p(g(f(x))) problem: DPs: 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))) Matrix Interpretation Processor: dimension: 1 interpretation: [q#](x0) = 1, [p#](x0) = 0, [q](x0) = 0, [g](x0) = 0, [p](x0) = 0, [f](x0) = 0 orientation: q#(g(g(x))) = 1 >= 0 = p#(g(f(x))) p(f(f(x))) = 0 >= 0 = q(f(g(x))) p(g(g(x))) = 0 >= 0 = q(g(f(x))) q(f(f(x))) = 0 >= 0 = p(f(g(x))) q(g(g(x))) = 0 >= 0 = p(g(f(x))) problem: DPs: 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))) Qed