div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
↳ QTRS
↳ DependencyPairsProof
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
DIV(div(X, Y), Z) → DIV(Y, div(i(X), Z))
I(div(X, Y)) → DIV(Y, X)
DIV(div(X, Y), Z) → DIV(i(X), Z)
DIV(X, e) → I(X)
DIV(div(X, Y), Z) → I(X)
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
DIV(div(X, Y), Z) → DIV(Y, div(i(X), Z))
I(div(X, Y)) → DIV(Y, X)
DIV(div(X, Y), Z) → DIV(i(X), Z)
DIV(X, e) → I(X)
DIV(div(X, Y), Z) → I(X)
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
I(div(X, Y)) → DIV(Y, X)
DIV(div(X, Y), Z) → DIV(i(X), Z)
DIV(X, e) → I(X)
DIV(div(X, Y), Z) → I(X)
Used ordering: Polynomial interpretation [25,35]:
DIV(div(X, Y), Z) → DIV(Y, div(i(X), Z))
The value of delta used in the strict ordering is 1.
POL(i(x1)) = x_1
POL(div(x1, x2)) = 2 + x_1 + x_2
POL(e) = 2
POL(DIV(x1, x2)) = 1 + (2)x_1 + (2)x_2
POL(I(x1)) = 4 + (2)x_1
div(X, e) → i(X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
i(div(X, Y)) → div(Y, X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
DIV(div(X, Y), Z) → DIV(Y, div(i(X), Z))
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(div(X, Y), Z) → DIV(Y, div(i(X), Z))
The value of delta used in the strict ordering is 9.
POL(i(x1)) = 3
POL(div(x1, x2)) = 3 + x_2
POL(e) = 3
POL(DIV(x1, x2)) = (3)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))