YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(b(c(x0))) → c(b(a(x0)))
C(B(A(x0))) → A(B(C(x0)))
b(a(C(x0))) → C(a(b(x0)))
c(A(B(x0))) → B(A(c(x0)))
A(c(b(x0))) → b(c(A(x0)))
B(C(a(x0))) → a(C(B(x0)))
a(A(x0)) → x0
A(a(x0)) → x0
b(B(x0)) → x0
B(b(x0)) → x0
c(C(x0)) → x0
C(c(x0)) → x0

Proof

1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[B(x1)] = 1 · x1 + -∞
[b(x1)] = 2 · x1 + -∞
[A(x1)] = 1 · x1 + -∞
[C(x1)] = 9 · x1 + -∞
[c(x1)] = 2 · x1 + -∞
[a(x1)] = 4 · x1 + -∞
the rules
a(b(c(x0))) → c(b(a(x0)))
C(B(A(x0))) → A(B(C(x0)))
b(a(C(x0))) → C(a(b(x0)))
c(A(B(x0))) → B(A(c(x0)))
A(c(b(x0))) → b(c(A(x0)))
B(C(a(x0))) → a(C(B(x0)))
remain.

1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
c(b(a(x0))) → a(b(c(x0)))
A(B(C(x0))) → C(B(A(x0)))
C(a(b(x0))) → b(a(C(x0)))
B(A(c(x0))) → c(A(B(x0)))
b(c(A(x0))) → A(c(b(x0)))
a(C(B(x0))) → B(C(a(x0)))

1.1.1 Bounds

The given TRS is match-bounded by 0. This is shown by the following automaton.