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