a(a(f(x, y))) → f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) → a(f(x, y))
f(b(x), b(y)) → b(f(x, y))
↳ QTRS
↳ DependencyPairsProof
a(a(f(x, y))) → f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) → a(f(x, y))
f(b(x), b(y)) → b(f(x, y))
A(a(f(x, y))) → A(b(a(x)))
A(a(f(x, y))) → A(y)
A(a(f(x, y))) → A(b(a(b(a(y)))))
A(a(f(x, y))) → A(b(a(b(a(x)))))
F(a(x), a(y)) → F(x, y)
F(a(x), a(y)) → A(f(x, y))
A(a(f(x, y))) → A(b(a(y)))
A(a(f(x, y))) → F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
F(b(x), b(y)) → F(x, y)
A(a(f(x, y))) → A(x)
a(a(f(x, y))) → f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) → a(f(x, y))
f(b(x), b(y)) → b(f(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
A(a(f(x, y))) → A(b(a(x)))
A(a(f(x, y))) → A(y)
A(a(f(x, y))) → A(b(a(b(a(y)))))
A(a(f(x, y))) → A(b(a(b(a(x)))))
F(a(x), a(y)) → F(x, y)
F(a(x), a(y)) → A(f(x, y))
A(a(f(x, y))) → A(b(a(y)))
A(a(f(x, y))) → F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
F(b(x), b(y)) → F(x, y)
A(a(f(x, y))) → A(x)
a(a(f(x, y))) → f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) → a(f(x, y))
f(b(x), b(y)) → b(f(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
A(a(f(x, y))) → A(y)
F(a(x), a(y)) → F(x, y)
F(a(x), a(y)) → A(f(x, y))
A(a(f(x, y))) → F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
A(a(f(x, y))) → A(x)
F(b(x), b(y)) → F(x, y)
a(a(f(x, y))) → f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) → a(f(x, y))
f(b(x), b(y)) → b(f(x, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A(a(f(x, y))) → A(y)
A(a(f(x, y))) → A(x)
Used ordering: Polynomial interpretation [25,35]:
F(a(x), a(y)) → F(x, y)
F(a(x), a(y)) → A(f(x, y))
A(a(f(x, y))) → F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
F(b(x), b(y)) → F(x, y)
The value of delta used in the strict ordering is 2.
POL(a(x1)) = x_1
POL(f(x1, x2)) = 1 + (2)x_1 + (2)x_2
POL(A(x1)) = (2)x_1
POL(b(x1)) = x_1
POL(F(x1, x2)) = 2 + (4)x_1 + (4)x_2
a(a(f(x, y))) → f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) → a(f(x, y))
f(b(x), b(y)) → b(f(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(a(x), a(y)) → A(f(x, y))
F(a(x), a(y)) → F(x, y)
A(a(f(x, y))) → F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
F(b(x), b(y)) → F(x, y)
a(a(f(x, y))) → f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) → a(f(x, y))
f(b(x), b(y)) → b(f(x, y))