f(x1) → n(c(c(x1)))
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
↳ QTRS
↳ DependencyPairsProof
f(x1) → n(c(c(x1)))
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
F(x1) → C(c(x1))
C(f(x1)) → C(c(x1))
C(f(x1)) → F(c(c(x1)))
N(f(x1)) → F(n(x1))
C(f(x1)) → C(x1)
F(x1) → C(x1)
N(s(x1)) → F(s(s(x1)))
N(f(x1)) → N(x1)
F(x1) → N(c(c(x1)))
f(x1) → n(c(c(x1)))
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F(x1) → C(c(x1))
C(f(x1)) → C(c(x1))
C(f(x1)) → F(c(c(x1)))
N(f(x1)) → F(n(x1))
C(f(x1)) → C(x1)
F(x1) → C(x1)
N(s(x1)) → F(s(s(x1)))
N(f(x1)) → N(x1)
F(x1) → N(c(c(x1)))
f(x1) → n(c(c(x1)))
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
N(s(x1)) → F(s(s(x1)))
Used ordering: Polynomial interpretation [25,35]:
F(x1) → C(c(x1))
C(f(x1)) → C(c(x1))
C(f(x1)) → F(c(c(x1)))
N(f(x1)) → F(n(x1))
C(f(x1)) → C(x1)
F(x1) → C(x1)
N(f(x1)) → N(x1)
F(x1) → N(c(c(x1)))
The value of delta used in the strict ordering is 16.
POL(C(x1)) = 0
POL(N(x1)) = (4)x_1
POL(c(x1)) = 0
POL(f(x1)) = (4)x_1
POL(n(x1)) = (4)x_1
POL(s(x1)) = 4
POL(F(x1)) = 0
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(f(x1)) → f(n(x1))
n(s(x1)) → f(s(s(x1)))
f(x1) → n(c(c(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
F(x1) → C(c(x1))
C(f(x1)) → F(c(c(x1)))
C(f(x1)) → C(c(x1))
C(f(x1)) → C(x1)
N(f(x1)) → F(n(x1))
F(x1) → C(x1)
F(x1) → N(c(c(x1)))
N(f(x1)) → N(x1)
f(x1) → n(c(c(x1)))
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(x1) → C(c(x1))
C(f(x1)) → C(c(x1))
C(f(x1)) → C(x1)
F(x1) → C(x1)
N(f(x1)) → N(x1)
Used ordering: Polynomial interpretation [25,35]:
C(f(x1)) → F(c(c(x1)))
N(f(x1)) → F(n(x1))
F(x1) → N(c(c(x1)))
The value of delta used in the strict ordering is 1.
POL(C(x1)) = x_1
POL(N(x1)) = 1 + (2)x_1
POL(c(x1)) = x_1
POL(f(x1)) = 1 + (2)x_1
POL(n(x1)) = 1 + (2)x_1
POL(s(x1)) = 0
POL(F(x1)) = 1 + (2)x_1
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(f(x1)) → f(n(x1))
n(s(x1)) → f(s(s(x1)))
f(x1) → n(c(c(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
C(f(x1)) → F(c(c(x1)))
N(f(x1)) → F(n(x1))
F(x1) → N(c(c(x1)))
f(x1) → n(c(c(x1)))
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
N(f(x1)) → F(n(x1))
F(x1) → N(c(c(x1)))
f(x1) → n(c(c(x1)))
c(f(x1)) → f(c(c(x1)))
c(c(x1)) → c(x1)
n(s(x1)) → f(s(s(x1)))
n(f(x1)) → f(n(x1))