t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
↳ QTRS
↳ DependencyPairsProof
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
C(n(x1)) → C(x1)
T(f(x1)) → C(n(x1))
C(o(x1)) → O(c(x1))
T(f(x1)) → T(c(n(x1)))
C(o(x1)) → C(x1)
C(f(x1)) → C(x1)
C(n(x1)) → N(c(x1))
O(f(x1)) → O(x1)
N(f(x1)) → N(x1)
T(f(x1)) → N(x1)
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
C(n(x1)) → C(x1)
T(f(x1)) → C(n(x1))
C(o(x1)) → O(c(x1))
T(f(x1)) → T(c(n(x1)))
C(o(x1)) → C(x1)
C(f(x1)) → C(x1)
C(n(x1)) → N(c(x1))
O(f(x1)) → O(x1)
N(f(x1)) → N(x1)
T(f(x1)) → N(x1)
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
O(f(x1)) → O(x1)
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
O(f(x1)) → O(x1)
The value of delta used in the strict ordering is 4.
POL(f(x1)) = 1 + (4)x_1
POL(O(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
N(f(x1)) → N(x1)
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
N(f(x1)) → N(x1)
The value of delta used in the strict ordering is 4.
POL(N(x1)) = (4)x_1
POL(f(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
C(n(x1)) → C(x1)
C(o(x1)) → C(x1)
C(f(x1)) → C(x1)
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
C(n(x1)) → C(x1)
C(o(x1)) → C(x1)
C(f(x1)) → C(x1)
The value of delta used in the strict ordering is 16.
POL(C(x1)) = (4)x_1
POL(n(x1)) = 4 + (4)x_1
POL(f(x1)) = 4 + (3)x_1
POL(o(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
T(f(x1)) → T(c(n(x1)))
t(f(x1)) → t(c(n(x1)))
n(f(x1)) → f(n(x1))
o(f(x1)) → f(o(x1))
n(s(x1)) → f(s(x1))
o(s(x1)) → f(s(x1))
c(f(x1)) → f(c(x1))
c(n(x1)) → n(c(x1))
c(o(x1)) → o(c(x1))
c(o(x1)) → o(x1)