YES Problem: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 Proof: DP Processor: DPs: P#(x1) -> p#(x1) P#(x1) -> Q#(p(x1)) P#(x1) -> Q#(Q(p(x1))) p#(p(x1)) -> q#(x1) p#(p(x1)) -> q#(q(x1)) p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> Q#(x1) Q#(p(q(x1))) -> p#(Q(x1)) Q#(p(q(x1))) -> q#(p(Q(x1))) q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> p#(q(q(x1))) TRS: P(x1) -> Q(Q(p(x1))) p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) Q(p(q(x1))) -> q(p(Q(x1))) q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(q(x1)) -> x1 p(P(x1)) -> x1 P(p(x1)) -> x1 Usable Rule Processor: DPs: P#(x1) -> p#(x1) P#(x1) -> Q#(p(x1)) P#(x1) -> Q#(Q(p(x1))) p#(p(x1)) -> q#(x1) p#(p(x1)) -> q#(q(x1)) p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> Q#(x1) Q#(p(q(x1))) -> p#(Q(x1)) Q#(p(q(x1))) -> q#(p(Q(x1))) q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> p#(q(q(x1))) TRS: p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) p(P(x1)) -> x1 q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(p(q(x1))) -> q(p(Q(x1))) Q(q(x1)) -> x1 Matrix Interpretation Processor: dim=2 interpretation: [q#](x0) = [1 1]x0, [Q#](x0) = [1 1]x0 + [2], [p#](x0) = [4 1]x0, [P#](x0) = [7 4]x0 + [6], [0 1] [q](x0) = [1 0]x0, [0 1] [0] [Q](x0) = [1 0]x0 + [1], [0 1] [1] [p](x0) = [4 0]x0 + [0], [0 1] [0] [P](x0) = [4 6]x0 + [4] orientation: P#(x1) = [7 4]x1 + [6] >= [4 1]x1 = p#(x1) P#(x1) = [7 4]x1 + [6] >= [4 1]x1 + [3] = Q#(p(x1)) P#(x1) = [7 4]x1 + [6] >= [4 1]x1 + [4] = Q#(Q(p(x1))) p#(p(x1)) = [4 4]x1 + [4] >= [1 1]x1 = q#(x1) p#(p(x1)) = [4 4]x1 + [4] >= [1 1]x1 = q#(q(x1)) p#(Q(Q(x1))) = [4 1]x1 + [5] >= [4 1]x1 = p#(x1) p#(Q(Q(x1))) = [4 1]x1 + [5] >= [4 1]x1 + [3] = Q#(p(x1)) p#(Q(Q(x1))) = [4 1]x1 + [5] >= [4 1]x1 + [4] = Q#(Q(p(x1))) Q#(p(q(x1))) = [1 4]x1 + [3] >= [1 1]x1 + [2] = Q#(x1) Q#(p(q(x1))) = [1 4]x1 + [3] >= [1 4]x1 + [1] = p#(Q(x1)) Q#(p(q(x1))) = [1 4]x1 + [3] >= [1 4]x1 + [2] = q#(p(Q(x1))) q#(q(p(x1))) = [4 1]x1 + [1] >= [1 1]x1 = q#(x1) q#(q(p(x1))) = [4 1]x1 + [1] >= [1 1]x1 = q#(q(x1)) q#(q(p(x1))) = [4 1]x1 + [1] >= [4 1]x1 = p#(q(q(x1))) [4 0] [1] p(p(x1)) = [0 4]x1 + [4] >= x1 = q(q(x1)) [0 1] [2] [0 1] [2] p(Q(Q(x1))) = [4 0]x1 + [4] >= [4 0]x1 + [1] = Q(Q(p(x1))) [4 6] [5] p(P(x1)) = [0 4]x1 + [0] >= x1 = x1 [0 1] [1] [0 1] [1] q(q(p(x1))) = [4 0]x1 + [0] >= [4 0]x1 + [0] = p(q(q(x1))) [1] q(Q(x1)) = x1 + [0] >= x1 = x1 [0 4] [0] [0 4] [0] Q(p(q(x1))) = [1 0]x1 + [2] >= [1 0]x1 + [2] = q(p(Q(x1))) [0] Q(q(x1)) = x1 + [1] >= x1 = x1 problem: DPs: TRS: p(p(x1)) -> q(q(x1)) p(Q(Q(x1))) -> Q(Q(p(x1))) p(P(x1)) -> x1 q(q(p(x1))) -> p(q(q(x1))) q(Q(x1)) -> x1 Q(p(q(x1))) -> q(p(Q(x1))) Q(q(x1)) -> x1 Qed