g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))
↳ QTRS
↳ DependencyPairsProof
g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))
F(0, 1, x) → F(s(x), x, x)
F(x, y, s(z)) → F(0, 1, z)
g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F(0, 1, x) → F(s(x), x, x)
F(x, y, s(z)) → F(0, 1, z)
g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(x, y, s(z)) → F(0, 1, z)
Used ordering: Polynomial interpretation [25,35]:
F(0, 1, x) → F(s(x), x, x)
The value of delta used in the strict ordering is 12.
POL(s(x1)) = 4 + (2)x_1
POL(F(x1, x2, x3)) = (3)x_3
POL(0) = 3
POL(1) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
F(0, 1, x) → F(s(x), x, x)
g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))