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