p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
HALF(s(s(x1))) → P(s(s(x1)))
HALF(s(s(x1))) → P(p(s(s(x1))))
HALF(0(x1)) → HALF(p(s(p(s(x1)))))
P(p(s(x1))) → P(x1)
RD(0(x1)) → RD(x1)
HALF(0(x1)) → P(s(p(s(x1))))
P(0(x1)) → P(x1)
G(s(x1)) → P(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
J(s(x1)) → P(s(p(p(s(x1)))))
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
J(s(x1)) → F(p(s(p(p(s(x1))))))
J(s(x1)) → P(s(x1))
F(s(x1)) → G(p(s(s(x1))))
G(s(x1)) → P(s(p(s(x1))))
J(s(x1)) → P(s(f(p(s(p(p(s(x1))))))))
G(s(x1)) → J(s(p(s(p(s(x1))))))
F(s(x1)) → P(s(s(x1)))
J(s(x1)) → P(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
HALF(0(x1)) → P(s(x1))
G(s(x1)) → P(s(x1))
J(s(x1)) → P(p(s(x1)))
F(s(x1)) → P(s(g(p(s(s(x1))))))
G(s(x1)) → P(s(s(s(j(s(p(s(p(s(x1))))))))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
HALF(s(s(x1))) → P(s(s(x1)))
HALF(s(s(x1))) → P(p(s(s(x1))))
HALF(0(x1)) → HALF(p(s(p(s(x1)))))
P(p(s(x1))) → P(x1)
RD(0(x1)) → RD(x1)
HALF(0(x1)) → P(s(p(s(x1))))
P(0(x1)) → P(x1)
G(s(x1)) → P(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
J(s(x1)) → P(s(p(p(s(x1)))))
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
J(s(x1)) → F(p(s(p(p(s(x1))))))
J(s(x1)) → P(s(x1))
F(s(x1)) → G(p(s(s(x1))))
G(s(x1)) → P(s(p(s(x1))))
J(s(x1)) → P(s(f(p(s(p(p(s(x1))))))))
G(s(x1)) → J(s(p(s(p(s(x1))))))
F(s(x1)) → P(s(s(x1)))
J(s(x1)) → P(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
HALF(0(x1)) → P(s(x1))
G(s(x1)) → P(s(x1))
J(s(x1)) → P(p(s(x1)))
F(s(x1)) → P(s(g(p(s(s(x1))))))
G(s(x1)) → P(s(s(s(j(s(p(s(p(s(x1))))))))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
RD(0(x1)) → RD(x1)
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
RD(0(x1)) → RD(x1)
The value of delta used in the strict ordering is 4.
POL(RD(x1)) = (4)x_1
POL(0(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
P(p(s(x1))) → P(x1)
P(0(x1)) → P(x1)
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(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)
P(0(x1)) → P(x1)
The value of delta used in the strict ordering is 16.
POL(P(x1)) = (4)x_1
POL(p(x1)) = 4 + (4)x_1
POL(s(x1)) = 4 + (4)x_1
POL(0(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
HALF(0(x1)) → HALF(p(s(p(s(x1)))))
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HALF(0(x1)) → HALF(p(s(p(s(x1)))))
Used ordering: Polynomial interpretation [25,35]:
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
The value of delta used in the strict ordering is 12.
POL(HALF(x1)) = (4)x_1
POL(p(x1)) = x_1
POL(s(x1)) = x_1
POL(0(x1)) = 3 + (2)x_1
p(s(x1)) → x1
p(0(x1)) → 0(s(s(p(x1))))
p(p(s(x1))) → p(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
HALF(s(s(x1))) → HALF(p(p(s(s(x1)))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
J(s(x1)) → F(p(s(p(p(s(x1))))))
F(s(x1)) → G(p(s(s(x1))))
G(s(x1)) → J(s(p(s(p(s(x1))))))
p(0(x1)) → 0(s(s(p(x1))))
p(s(x1)) → x1
p(p(s(x1))) → p(x1)
f(s(x1)) → p(s(g(p(s(s(x1))))))
g(s(x1)) → p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
j(s(x1)) → p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
half(0(x1)) → 0(s(s(half(p(s(p(s(x1))))))))
half(s(s(x1))) → s(half(p(p(s(s(x1))))))
rd(0(x1)) → 0(s(0(0(0(0(s(0(rd(x1)))))))))