plus(s(X), plus(Y, Z)) → plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) → plus(X1, plus(X3, plus(X2, X4)))
↳ QTRS
↳ DependencyPairsProof
plus(s(X), plus(Y, Z)) → plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) → plus(X1, plus(X3, plus(X2, X4)))
PLUS(s(X), plus(Y, Z)) → PLUS(s(s(Y)), Z)
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X3, plus(X2, X4))
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(X), plus(Y, Z)) → PLUS(X, plus(s(s(Y)), Z))
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X2, X4)
plus(s(X), plus(Y, Z)) → plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) → plus(X1, plus(X3, plus(X2, X4)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
PLUS(s(X), plus(Y, Z)) → PLUS(s(s(Y)), Z)
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X3, plus(X2, X4))
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(X), plus(Y, Z)) → PLUS(X, plus(s(s(Y)), Z))
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X2, X4)
plus(s(X), plus(Y, Z)) → plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) → plus(X1, plus(X3, plus(X2, X4)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(X), plus(Y, Z)) → PLUS(s(s(Y)), Z)
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X3, plus(X2, X4))
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X2, X4)
Used ordering: Polynomial interpretation [25,35]:
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(X), plus(Y, Z)) → PLUS(X, plus(s(s(Y)), Z))
The value of delta used in the strict ordering is 3.
POL(PLUS(x1, x2)) = x_1 + x_2
POL(plus(x1, x2)) = 3 + (2)x_1 + x_2
POL(s(x1)) = x_1
plus(s(X1), plus(X2, plus(X3, X4))) → plus(X1, plus(X3, plus(X2, X4)))
plus(s(X), plus(Y, Z)) → plus(X, plus(s(s(Y)), Z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(X), plus(Y, Z)) → PLUS(X, plus(s(s(Y)), Z))
plus(s(X), plus(Y, Z)) → plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) → plus(X1, plus(X3, plus(X2, X4)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(X1), plus(X2, plus(X3, X4))) → PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(X), plus(Y, Z)) → PLUS(X, plus(s(s(Y)), Z))
The value of delta used in the strict ordering is 1.
POL(PLUS(x1, x2)) = x_1
POL(plus(x1, x2)) = x_2
POL(s(x1)) = 1 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
plus(s(X), plus(Y, Z)) → plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) → plus(X1, plus(X3, plus(X2, X4)))