Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z033)

The rewrite relation of the following TRS is considered.

b(a(b(b(a(b(a(x1))))))) → a(b(a(a(b(b(a(b(b(a(x1)))))))))) (1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a(b(a(b(b(a(b(x1))))))) → a(b(b(a(b(b(a(a(b(a(x1)))))))))) (2)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
ab(ba(ab(bb(ba(ab(ba(x1))))))) → ab(bb(ba(ab(bb(ba(aa(ab(ba(aa(x1)))))))))) (3)
ab(ba(ab(bb(ba(ab(bb(x1))))))) → ab(bb(ba(ab(bb(ba(aa(ab(ba(ab(x1)))))))))) (4)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
ab#(ba(ab(bb(ba(ab(ba(x1))))))) → ab#(bb(ba(ab(bb(ba(aa(ab(ba(aa(x1)))))))))) (5)
ab#(ba(ab(bb(ba(ab(ba(x1))))))) → ab#(bb(ba(aa(ab(ba(aa(x1))))))) (6)
ab#(ba(ab(bb(ba(ab(ba(x1))))))) → ab#(ba(aa(x1))) (7)
ab#(ba(ab(bb(ba(ab(bb(x1))))))) → ab#(bb(ba(ab(bb(ba(aa(ab(ba(ab(x1)))))))))) (8)
ab#(ba(ab(bb(ba(ab(bb(x1))))))) → ab#(bb(ba(aa(ab(ba(ab(x1))))))) (9)
ab#(ba(ab(bb(ba(ab(bb(x1))))))) → ab#(ba(ab(x1))) (10)
ab#(ba(ab(bb(ba(ab(bb(x1))))))) → ab#(x1) (11)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.