c(c(z, y, a), a, a) → b(z, y)
f(c(x, y, z)) → c(z, f(b(y, z)), a)
b(z, b(c(a, y, a), f(f(x)))) → c(c(y, a, z), z, x)
↳ QTRS
↳ DependencyPairsProof
c(c(z, y, a), a, a) → b(z, y)
f(c(x, y, z)) → c(z, f(b(y, z)), a)
b(z, b(c(a, y, a), f(f(x)))) → c(c(y, a, z), z, x)
C(c(z, y, a), a, a) → B(z, y)
B(z, b(c(a, y, a), f(f(x)))) → C(y, a, z)
F(c(x, y, z)) → C(z, f(b(y, z)), a)
F(c(x, y, z)) → B(y, z)
B(z, b(c(a, y, a), f(f(x)))) → C(c(y, a, z), z, x)
F(c(x, y, z)) → F(b(y, z))
c(c(z, y, a), a, a) → b(z, y)
f(c(x, y, z)) → c(z, f(b(y, z)), a)
b(z, b(c(a, y, a), f(f(x)))) → c(c(y, a, z), z, x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
C(c(z, y, a), a, a) → B(z, y)
B(z, b(c(a, y, a), f(f(x)))) → C(y, a, z)
F(c(x, y, z)) → C(z, f(b(y, z)), a)
F(c(x, y, z)) → B(y, z)
B(z, b(c(a, y, a), f(f(x)))) → C(c(y, a, z), z, x)
F(c(x, y, z)) → F(b(y, z))
c(c(z, y, a), a, a) → b(z, y)
f(c(x, y, z)) → c(z, f(b(y, z)), a)
b(z, b(c(a, y, a), f(f(x)))) → c(c(y, a, z), z, x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
C(c(z, y, a), a, a) → B(z, y)
B(z, b(c(a, y, a), f(f(x)))) → C(y, a, z)
B(z, b(c(a, y, a), f(f(x)))) → C(c(y, a, z), z, x)
c(c(z, y, a), a, a) → b(z, y)
f(c(x, y, z)) → c(z, f(b(y, z)), a)
b(z, b(c(a, y, a), f(f(x)))) → c(c(y, a, z), z, x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
C(c(z, y, a), a, a) → B(z, y)
B(z, b(c(a, y, a), f(f(x)))) → C(y, a, z)
B(z, b(c(a, y, a), f(f(x)))) → C(c(y, a, z), z, x)
The value of delta used in the strict ordering is 1.
POL(C(x1, x2, x3)) = 1 + x_1
POL(a) = 0
POL(f(x1)) = 1 + x_1
POL(b(x1, x2)) = (4)x_1 + x_2
POL(c(x1, x2, x3)) = (4)x_1 + (4)x_2
POL(B(x1, x2)) = x_1 + (4)x_2
b(z, b(c(a, y, a), f(f(x)))) → c(c(y, a, z), z, x)
c(c(z, y, a), a, a) → b(z, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
c(c(z, y, a), a, a) → b(z, y)
f(c(x, y, z)) → c(z, f(b(y, z)), a)
b(z, b(c(a, y, a), f(f(x)))) → c(c(y, a, z), z, x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
F(c(x, y, z)) → F(b(y, z))
c(c(z, y, a), a, a) → b(z, y)
f(c(x, y, z)) → c(z, f(b(y, z)), a)
b(z, b(c(a, y, a), f(f(x)))) → c(c(y, a, z), z, x)