Certification Problem

Input (TPDB SRS_Standard/Mixed_SRS/s6)

The rewrite relation of the following TRS is considered.

a12(a12(x1)) → x1 (1)
a13(a13(x1)) → x1 (2)
a14(a14(x1)) → x1 (3)
a15(a15(x1)) → x1 (4)
a16(a16(x1)) → x1 (5)
a23(a23(x1)) → x1 (6)
a24(a24(x1)) → x1 (7)
a25(a25(x1)) → x1 (8)
a26(a26(x1)) → x1 (9)
a34(a34(x1)) → x1 (10)
a35(a35(x1)) → x1 (11)
a36(a36(x1)) → x1 (12)
a45(a45(x1)) → x1 (13)
a46(a46(x1)) → x1 (14)
a56(a56(x1)) → x1 (15)
a13(x1) → a12(a23(a12(x1))) (16)
a14(x1) → a12(a23(a34(a23(a12(x1))))) (17)
a15(x1) → a12(a23(a34(a45(a34(a23(a12(x1))))))) (18)
a16(x1) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) (19)
a24(x1) → a23(a34(a23(x1))) (20)
a25(x1) → a23(a34(a45(a34(a23(x1))))) (21)
a26(x1) → a23(a34(a45(a56(a45(a34(a23(x1))))))) (22)
a35(x1) → a34(a45(a34(x1))) (23)
a36(x1) → a34(a45(a56(a45(a34(x1))))) (24)
a46(x1) → a45(a56(a45(x1))) (25)
a12(a23(a12(a23(a12(a23(x1)))))) → x1 (26)
a23(a34(a23(a34(a23(a34(x1)))))) → x1 (27)
a34(a45(a34(a45(a34(a45(x1)))))) → x1 (28)
a45(a56(a45(a56(a45(a56(x1)))))) → x1 (29)
a12(a34(x1)) → a34(a12(x1)) (30)
a12(a45(x1)) → a45(a12(x1)) (31)
a12(a56(x1)) → a56(a12(x1)) (32)
a23(a45(x1)) → a45(a23(x1)) (33)
a23(a56(x1)) → a56(a23(x1)) (34)
a34(a56(x1)) → a56(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(x1)) → x1 (1)
a13(a13(x1)) → x1 (2)
a14(a14(x1)) → x1 (3)
a15(a15(x1)) → x1 (4)
a16(a16(x1)) → x1 (5)
a23(a23(x1)) → x1 (6)
a24(a24(x1)) → x1 (7)
a25(a25(x1)) → x1 (8)
a26(a26(x1)) → x1 (9)
a34(a34(x1)) → x1 (10)
a35(a35(x1)) → x1 (11)
a36(a36(x1)) → x1 (12)
a45(a45(x1)) → x1 (13)
a46(a46(x1)) → x1 (14)
a56(a56(x1)) → x1 (15)
a13(x1) → a12(a23(a12(x1))) (16)
a14(x1) → a12(a23(a34(a23(a12(x1))))) (17)
a15(x1) → a12(a23(a34(a45(a34(a23(a12(x1))))))) (18)
a16(x1) → a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) (19)
a24(x1) → a23(a34(a23(x1))) (20)
a25(x1) → a23(a34(a45(a34(a23(x1))))) (21)
a26(x1) → a23(a34(a45(a56(a45(a34(a23(x1))))))) (22)
a35(x1) → a34(a45(a34(x1))) (23)
a36(x1) → a34(a45(a56(a45(a34(x1))))) (24)
a46(x1) → a45(a56(a45(x1))) (25)
a23(a12(a23(a12(a23(a12(x1)))))) → x1 (36)
a34(a23(a34(a23(a34(a23(x1)))))) → x1 (37)
a45(a34(a45(a34(a45(a34(x1)))))) → x1 (38)
a56(a45(a56(a45(a56(a45(x1)))))) → x1 (39)
a34(a12(x1)) → a12(a34(x1)) (40)
a45(a12(x1)) → a12(a45(x1)) (41)
a56(a12(x1)) → a12(a56(x1)) (42)
a45(a23(x1)) → a23(a45(x1)) (43)
a56(a23(x1)) → a23(a56(x1)) (44)
a56(a34(x1)) → a34(a56(x1)) (45)

1.1 Rule Removal

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

1.1.1 R is empty

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