Certification Problem

Input (TPDB SRS_Standard/Trafo_06/dup01)

The rewrite relation of the following TRS is considered.

a12(a12(a12(a12(x1)))) → x1 (1)
a13(a13(a13(a13(x1)))) → x1 (2)
a14(a14(a14(a14(x1)))) → x1 (3)
a15(a15(a15(a15(x1)))) → x1 (4)
a16(a16(a16(a16(x1)))) → x1 (5)
a23(a23(a23(a23(x1)))) → x1 (6)
a24(a24(a24(a24(x1)))) → x1 (7)
a25(a25(a25(a25(x1)))) → x1 (8)
a26(a26(a26(a26(x1)))) → x1 (9)
a34(a34(a34(a34(x1)))) → x1 (10)
a35(a35(a35(a35(x1)))) → x1 (11)
a36(a36(a36(a36(x1)))) → x1 (12)
a45(a45(a45(a45(x1)))) → x1 (13)
a46(a46(a46(a46(x1)))) → x1 (14)
a56(a56(a56(a56(x1)))) → x1 (15)
a13(a13(x1)) → a12(a12(a23(a23(a12(a12(x1)))))) (16)
a14(a14(x1)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) (17)
a15(a15(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) (18)
a16(a16(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) (19)
a24(a24(x1)) → a23(a23(a34(a34(a23(a23(x1)))))) (20)
a25(a25(x1)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) (21)
a26(a26(x1)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) (22)
a35(a35(x1)) → a34(a34(a45(a45(a34(a34(x1)))))) (23)
a36(a36(x1)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) (24)
a46(a46(x1)) → a45(a45(a56(a56(a45(a45(x1)))))) (25)
a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) → x1 (26)
a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) → x1 (27)
a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) → x1 (28)
a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) → x1 (29)
a12(a12(a34(a34(x1)))) → a34(a34(a12(a12(x1)))) (30)
a12(a12(a45(a45(x1)))) → a45(a45(a12(a12(x1)))) (31)
a12(a12(a56(a56(x1)))) → a56(a56(a12(a12(x1)))) (32)
a23(a23(a45(a45(x1)))) → a45(a45(a23(a23(x1)))) (33)
a23(a23(a56(a56(x1)))) → a56(a56(a23(a23(x1)))) (34)
a34(a34(a56(a56(x1)))) → a56(a56(a34(a34(x1)))) (35)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a12(a12(a12(a12(x1)))) → x1 (1)
a13(a13(a13(a13(x1)))) → x1 (2)
a14(a14(a14(a14(x1)))) → x1 (3)
a15(a15(a15(a15(x1)))) → x1 (4)
a16(a16(a16(a16(x1)))) → x1 (5)
a23(a23(a23(a23(x1)))) → x1 (6)
a24(a24(a24(a24(x1)))) → x1 (7)
a25(a25(a25(a25(x1)))) → x1 (8)
a26(a26(a26(a26(x1)))) → x1 (9)
a34(a34(a34(a34(x1)))) → x1 (10)
a35(a35(a35(a35(x1)))) → x1 (11)
a36(a36(a36(a36(x1)))) → x1 (12)
a45(a45(a45(a45(x1)))) → x1 (13)
a46(a46(a46(a46(x1)))) → x1 (14)
a56(a56(a56(a56(x1)))) → x1 (15)
a13(a13(x1)) → a12(a12(a23(a23(a12(a12(x1)))))) (16)
a14(a14(x1)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) (17)
a15(a15(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) (18)
a16(a16(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) (19)
a24(a24(x1)) → a23(a23(a34(a34(a23(a23(x1)))))) (20)
a25(a25(x1)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) (21)
a26(a26(x1)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) (22)
a35(a35(x1)) → a34(a34(a45(a45(a34(a34(x1)))))) (23)
a36(a36(x1)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) (24)
a46(a46(x1)) → a45(a45(a56(a56(a45(a45(x1)))))) (25)
a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(x1)))))))))))) → x1 (36)
a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(x1)))))))))))) → x1 (37)
a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(x1)))))))))))) → x1 (38)
a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(x1)))))))))))) → x1 (39)
a34(a34(a12(a12(x1)))) → a12(a12(a34(a34(x1)))) (40)
a45(a45(a12(a12(x1)))) → a12(a12(a45(a45(x1)))) (41)
a56(a56(a12(a12(x1)))) → a12(a12(a56(a56(x1)))) (42)
a45(a45(a23(a23(x1)))) → a23(a23(a45(a45(x1)))) (43)
a56(a56(a23(a23(x1)))) → a23(a23(a56(a56(x1)))) (44)
a56(a56(a34(a34(x1)))) → a34(a34(a56(a56(x1)))) (45)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(a56) = 13 weight(a56) = 1
prec(a46) = 6 weight(a46) = 2
prec(a45) = 15 weight(a45) = 0
prec(a36) = 3 weight(a36) = 4
prec(a35) = 1 weight(a35) = 3
prec(a34) = 7 weight(a34) = 1
prec(a26) = 9 weight(a26) = 5
prec(a25) = 12 weight(a25) = 4
prec(a24) = 0 weight(a24) = 4
prec(a23) = 8 weight(a23) = 1
prec(a16) = 10 weight(a16) = 7
prec(a15) = 5 weight(a15) = 6
prec(a14) = 4 weight(a14) = 6
prec(a13) = 11 weight(a13) = 4
prec(a12) = 2 weight(a12) = 1
all of the following rules can be deleted.
a12(a12(a12(a12(x1)))) → x1 (1)
a13(a13(a13(a13(x1)))) → x1 (2)
a14(a14(a14(a14(x1)))) → x1 (3)
a15(a15(a15(a15(x1)))) → x1 (4)
a16(a16(a16(a16(x1)))) → x1 (5)
a23(a23(a23(a23(x1)))) → x1 (6)
a24(a24(a24(a24(x1)))) → x1 (7)
a25(a25(a25(a25(x1)))) → x1 (8)
a26(a26(a26(a26(x1)))) → x1 (9)
a34(a34(a34(a34(x1)))) → x1 (10)
a35(a35(a35(a35(x1)))) → x1 (11)
a36(a36(a36(a36(x1)))) → x1 (12)
a45(a45(a45(a45(x1)))) → x1 (13)
a46(a46(a46(a46(x1)))) → x1 (14)
a56(a56(a56(a56(x1)))) → x1 (15)
a13(a13(x1)) → a12(a12(a23(a23(a12(a12(x1)))))) (16)
a14(a14(x1)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1)))))))))) (17)
a15(a15(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))) (18)
a16(a16(x1)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1)))))))))))))))))) (19)
a24(a24(x1)) → a23(a23(a34(a34(a23(a23(x1)))))) (20)
a25(a25(x1)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1)))))))))) (21)
a26(a26(x1)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1)))))))))))))) (22)
a35(a35(x1)) → a34(a34(a45(a45(a34(a34(x1)))))) (23)
a36(a36(x1)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1)))))))))) (24)
a46(a46(x1)) → a45(a45(a56(a56(a45(a45(x1)))))) (25)
a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(x1)))))))))))) → x1 (36)
a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(x1)))))))))))) → x1 (37)
a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(x1)))))))))))) → x1 (38)
a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(x1)))))))))))) → x1 (39)
a34(a34(a12(a12(x1)))) → a12(a12(a34(a34(x1)))) (40)
a45(a45(a12(a12(x1)))) → a12(a12(a45(a45(x1)))) (41)
a56(a56(a12(a12(x1)))) → a12(a12(a56(a56(x1)))) (42)
a45(a45(a23(a23(x1)))) → a23(a23(a45(a45(x1)))) (43)
a56(a56(a23(a23(x1)))) → a23(a23(a56(a56(x1)))) (44)
a56(a56(a34(a34(x1)))) → a34(a34(a56(a56(x1)))) (45)

1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.