Certification Problem

Input (TPDB SRS_Standard/Wenzel_16/abababaab-aabaabababab.srs)

The rewrite relation of the following TRS is considered.

a(b(a(b(a(b(a(a(b(x1))))))))) → a(a(b(a(a(b(a(b(a(b(a(b(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
b(a(a(b(a(b(a(b(a(x1))))))))) → b(a(b(a(b(a(b(a(a(b(a(a(x1)))))))))))) (2)

1.1 Semantic Labeling

Root-labeling is applied.

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

1.1.1 Dependency Pair Transformation

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

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.