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 TDG 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 graph: q#(q(p(x1))) -> q#(q(x1)) -> q#(q(p(x1))) -> p#(q(q(x1))) q#(q(p(x1))) -> q#(q(x1)) -> q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> q#(q(x1)) -> q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> q#(x1) -> q#(q(p(x1))) -> p#(q(q(x1))) q#(q(p(x1))) -> q#(x1) -> q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> q#(x1) -> q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> Q#(p(x1)) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(Q(Q(x1))) -> p#(x1) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(p(x1)) -> q#(q(x1)) q#(q(p(x1))) -> p#(q(q(x1))) -> p#(p(x1)) -> q#(x1) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> p#(q(q(x1))) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> q#(q(x1)) Q#(p(q(x1))) -> q#(p(Q(x1))) -> q#(q(p(x1))) -> q#(x1) Q#(p(q(x1))) -> Q#(x1) -> Q#(p(q(x1))) -> q#(p(Q(x1))) Q#(p(q(x1))) -> Q#(x1) -> Q#(p(q(x1))) -> p#(Q(x1)) Q#(p(q(x1))) -> Q#(x1) -> Q#(p(q(x1))) -> Q#(x1) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> Q#(p(x1)) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(Q(Q(x1))) -> p#(x1) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(p(x1)) -> q#(q(x1)) Q#(p(q(x1))) -> p#(Q(x1)) -> p#(p(x1)) -> q#(x1) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> q#(p(Q(x1))) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> Q#(x1) p#(Q(Q(x1))) -> Q#(p(x1)) -> Q#(p(q(x1))) -> q#(p(Q(x1))) p#(Q(Q(x1))) -> Q#(p(x1)) -> Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(p(x1)) -> Q#(p(q(x1))) -> Q#(x1) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(p(x1)) p#(Q(Q(x1))) -> p#(x1) -> p#(Q(Q(x1))) -> p#(x1) p#(Q(Q(x1))) -> p#(x1) -> p#(p(x1)) -> q#(q(x1)) p#(Q(Q(x1))) -> p#(x1) -> p#(p(x1)) -> q#(x1) p#(p(x1)) -> q#(q(x1)) -> q#(q(p(x1))) -> p#(q(q(x1))) p#(p(x1)) -> q#(q(x1)) -> q#(q(p(x1))) -> q#(q(x1)) p#(p(x1)) -> q#(q(x1)) -> q#(q(p(x1))) -> q#(x1) p#(p(x1)) -> q#(x1) -> q#(q(p(x1))) -> p#(q(q(x1))) p#(p(x1)) -> q#(x1) -> q#(q(p(x1))) -> q#(q(x1)) p#(p(x1)) -> q#(x1) -> q#(q(p(x1))) -> q#(x1) P#(x1) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> q#(p(Q(x1))) P#(x1) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> p#(Q(x1)) P#(x1) -> Q#(Q(p(x1))) -> Q#(p(q(x1))) -> Q#(x1) P#(x1) -> Q#(p(x1)) -> Q#(p(q(x1))) -> q#(p(Q(x1))) P#(x1) -> Q#(p(x1)) -> Q#(p(q(x1))) -> p#(Q(x1)) P#(x1) -> Q#(p(x1)) -> Q#(p(q(x1))) -> Q#(x1) P#(x1) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(Q(p(x1))) P#(x1) -> p#(x1) -> p#(Q(Q(x1))) -> Q#(p(x1)) P#(x1) -> p#(x1) -> p#(Q(Q(x1))) -> p#(x1) P#(x1) -> p#(x1) -> p#(p(x1)) -> q#(q(x1)) P#(x1) -> p#(x1) -> p#(p(x1)) -> q#(x1) SCC Processor: #sccs: 1 #rules: 11 #arcs: 50/196 DPs: q#(q(p(x1))) -> q#(q(x1)) q#(q(p(x1))) -> q#(x1) q#(q(p(x1))) -> p#(q(q(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)) Q#(p(q(x1))) -> Q#(x1) Q#(p(q(x1))) -> p#(Q(x1)) p#(Q(Q(x1))) -> Q#(Q(p(x1))) Q#(p(q(x1))) -> q#(p(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 Matrix Interpretation Processor: dim=2 interpretation: [q#](x0) = [1 2]x0 + [2], [Q#](x0) = [2 0]x0 + [4], [p#](x0) = [2 2]x0 + [3], [0 2] [q](x0) = [1 0]x0, [0 1] [0] [Q](x0) = [2 0]x0 + [1], [1 2] [1] [p](x0) = [1 0]x0 + [0], [2 4] [3] [P](x0) = [2 0]x0 + [1] orientation: q#(q(p(x1))) = [4 4]x1 + [4] >= [2 2]x1 + [2] = q#(q(x1)) q#(q(p(x1))) = [4 4]x1 + [4] >= [1 2]x1 + [2] = q#(x1) q#(q(p(x1))) = [4 4]x1 + [4] >= [4 4]x1 + [3] = p#(q(q(x1))) p#(p(x1)) = [4 4]x1 + [5] >= [1 2]x1 + [2] = q#(x1) p#(p(x1)) = [4 4]x1 + [5] >= [2 2]x1 + [2] = q#(q(x1)) p#(Q(Q(x1))) = [4 4]x1 + [7] >= [2 2]x1 + [3] = p#(x1) p#(Q(Q(x1))) = [4 4]x1 + [7] >= [2 4]x1 + [6] = Q#(p(x1)) Q#(p(q(x1))) = [4 4]x1 + [6] >= [2 0]x1 + [4] = Q#(x1) Q#(p(q(x1))) = [4 4]x1 + [6] >= [4 2]x1 + [5] = p#(Q(x1)) p#(Q(Q(x1))) = [4 4]x1 + [7] >= [2 0]x1 + [4] = Q#(Q(p(x1))) Q#(p(q(x1))) = [4 4]x1 + [6] >= [4 3]x1 + [5] = q#(p(Q(x1))) [2 4] [3] [2 4] [3] P(x1) = [2 0]x1 + [1] >= [2 0]x1 + [1] = Q(Q(p(x1))) [3 2] [2] [2 0] p(p(x1)) = [1 2]x1 + [1] >= [0 2]x1 = q(q(x1)) [2 4] [4] [2 4] [3] p(Q(Q(x1))) = [2 0]x1 + [1] >= [2 0]x1 + [1] = Q(Q(p(x1))) [0 2] [0] [0 2] [0] Q(p(q(x1))) = [4 4]x1 + [3] >= [4 1]x1 + [3] = q(p(Q(x1))) [2 4] [2] [2 4] [1] q(q(p(x1))) = [2 0]x1 + [0] >= [2 0]x1 + [0] = p(q(q(x1))) [4 0] [2] q(Q(x1)) = [0 1]x1 + [0] >= x1 = x1 [1 0] [0] Q(q(x1)) = [0 4]x1 + [1] >= x1 = x1 [6 4] [6] p(P(x1)) = [2 4]x1 + [3] >= x1 = x1 [6 4] [5] P(p(x1)) = [2 4]x1 + [3] >= x1 = x1 problem: DPs: 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 Qed