v(s(x1)) → s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) → p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) → s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) → p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(p(s(x1))))))))))
↳ QTRS
↳ DependencyPairsProof
v(s(x1)) → s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) → p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) → s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) → p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(p(s(x1))))))))))
V(s(x1)) → P(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))
V(0(x1)) → P(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
V(s(x1)) → P(s(p(s(x1))))
V(0(x1)) → P(s(s(s(s(s(x1))))))
W(s(x1)) → P(s(s(x1)))
W(s(x1)) → V(p(p(s(s(s(p(p(s(s(x1))))))))))
W(0(x1)) → P(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))
W(s(x1)) → P(s(s(v(p(p(s(s(s(p(p(s(s(x1)))))))))))))
V(0(x1)) → P(p(s(s(s(s(s(x1)))))))
W(s(x1)) → P(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))
V(0(x1)) → P(s(s(0(p(p(s(s(s(s(s(x1)))))))))))
W(0(x1)) → P(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1))))))))))))))))
V(s(x1)) → P(s(x1))
W(0(x1)) → P(s(s(0(s(s(s(s(s(s(x1))))))))))
W(s(x1)) → P(p(s(s(s(p(p(s(s(x1)))))))))
W(0(x1)) → P(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))
W(0(x1)) → P(p(p(s(s(0(s(s(s(s(s(s(x1))))))))))))
V(s(x1)) → P(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1)))))))))))))))))))
W(0(x1)) → P(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
V(s(x1)) → P(s(s(p(s(p(s(x1)))))))
P(p(s(x1))) → P(x1)
W(s(x1)) → P(s(s(s(p(p(s(s(x1))))))))
W(0(x1)) → P(p(s(s(0(s(s(s(s(s(s(x1)))))))))))
W(0(x1)) → P(p(p(p(p(s(s(0(s(s(s(s(s(s(x1))))))))))))))
W(s(x1)) → P(p(s(s(x1))))
V(s(x1)) → P(p(s(s(p(s(p(s(x1))))))))
W(0(x1)) → P(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))
V(s(x1)) → W(p(p(s(s(p(s(p(s(x1)))))))))
P(0(x1)) → P(s(x1))
v(s(x1)) → s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) → p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) → s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) → p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(p(s(x1))))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
V(s(x1)) → P(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))
V(0(x1)) → P(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
V(s(x1)) → P(s(p(s(x1))))
V(0(x1)) → P(s(s(s(s(s(x1))))))
W(s(x1)) → P(s(s(x1)))
W(s(x1)) → V(p(p(s(s(s(p(p(s(s(x1))))))))))
W(0(x1)) → P(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))
W(s(x1)) → P(s(s(v(p(p(s(s(s(p(p(s(s(x1)))))))))))))
V(0(x1)) → P(p(s(s(s(s(s(x1)))))))
W(s(x1)) → P(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))
V(0(x1)) → P(s(s(0(p(p(s(s(s(s(s(x1)))))))))))
W(0(x1)) → P(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1))))))))))))))))
V(s(x1)) → P(s(x1))
W(0(x1)) → P(s(s(0(s(s(s(s(s(s(x1))))))))))
W(s(x1)) → P(p(s(s(s(p(p(s(s(x1)))))))))
W(0(x1)) → P(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))
W(0(x1)) → P(p(p(s(s(0(s(s(s(s(s(s(x1))))))))))))
V(s(x1)) → P(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1)))))))))))))))))))
W(0(x1)) → P(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
V(s(x1)) → P(s(s(p(s(p(s(x1)))))))
P(p(s(x1))) → P(x1)
W(s(x1)) → P(s(s(s(p(p(s(s(x1))))))))
W(0(x1)) → P(p(s(s(0(s(s(s(s(s(s(x1)))))))))))
W(0(x1)) → P(p(p(p(p(s(s(0(s(s(s(s(s(s(x1))))))))))))))
W(s(x1)) → P(p(s(s(x1))))
V(s(x1)) → P(p(s(s(p(s(p(s(x1))))))))
W(0(x1)) → P(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))
V(s(x1)) → W(p(p(s(s(p(s(p(s(x1)))))))))
P(0(x1)) → P(s(x1))
v(s(x1)) → s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) → p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) → s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) → p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(p(s(x1))))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
P(p(s(x1))) → P(x1)
v(s(x1)) → s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) → p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) → s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) → p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(p(s(x1))))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(p(s(x1))) → P(x1)
The value of delta used in the strict ordering is 2.
POL(P(x1)) = (2)x_1
POL(p(x1)) = 1 + x_1
POL(s(x1)) = x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
v(s(x1)) → s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) → p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) → s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) → p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(p(s(x1))))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
V(s(x1)) → W(p(p(s(s(p(s(p(s(x1)))))))))
W(s(x1)) → V(p(p(s(s(s(p(p(s(s(x1))))))))))
v(s(x1)) → s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) → p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) → s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) → p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(p(s(x1))))))))))