R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
R2(P(P(x1))) → P2(P(r(x1)))
R2(p(x1)) → P2(x1)
R2(P(P(x1))) → P2(r(x1))
R2(p(x1)) → P1(r(P(x1)))
R2(P(P(x1))) → R2(x1)
R2(p(x1)) → R2(P(x1))
R2(p(x1)) → P1(p(r(P(x1))))
R1(x1) → R2(x1)
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
R2(P(P(x1))) → P2(P(r(x1)))
R2(p(x1)) → P2(x1)
R2(P(P(x1))) → P2(r(x1))
R2(p(x1)) → P1(r(P(x1)))
R2(P(P(x1))) → R2(x1)
R2(p(x1)) → R2(P(x1))
R2(p(x1)) → P1(p(r(P(x1))))
R1(x1) → R2(x1)
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
R2(P(P(x1))) → R2(x1)
R2(p(x1)) → R2(P(x1))
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R2(P(P(x1))) → R2(x1)
Used ordering: Polynomial interpretation [25,35]:
R2(p(x1)) → R2(P(x1))
The value of delta used in the strict ordering is 80.
POL(P(x1)) = 4 + (4)x_1
POL(R2(x1)) = (4)x_1
POL(p(x1)) = 4 + (4)x_1
P(p(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
R2(p(x1)) → R2(P(x1))
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R2(p(x1)) → R2(P(x1))
The value of delta used in the strict ordering is 3.
POL(P(x1)) = 2 + (2)x_1
POL(R2(x1)) = (3)x_1
POL(p(x1)) = 3 + (3)x_1
P(p(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1