Certification Problem

Input (TPDB SRS_Standard/Waldmann_06_SRS/pi)

The rewrite relation of the following TRS is considered.

3(1(x1)) → 4(1(x1)) (1)
5(9(x1)) → 2(6(5(x1))) (2)
3(5(x1)) → 8(9(7(x1))) (3)
9(x1) → 3(2(3(x1))) (4)
8(4(x1)) → 6(x1) (5)
2(6(x1)) → 4(3(x1)) (6)
3(8(x1)) → 3(2(7(x1))) (7)
9(x1) → 5(0(2(x1))) (8)
8(8(4(x1))) → 1(9(x1)) (9)
7(1(x1)) → 6(9(x1)) (10)
3(9(x1)) → 9(3(x1)) (11)
7(5(x1)) → 1(0(x1)) (12)

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
1(3(x1)) → 1(4(x1)) (13)
9(5(x1)) → 5(6(2(x1))) (14)
5(3(x1)) → 7(9(8(x1))) (15)
9(x1) → 3(2(3(x1))) (4)
4(8(x1)) → 6(x1) (16)
6(2(x1)) → 3(4(x1)) (17)
8(3(x1)) → 7(2(3(x1))) (18)
9(x1) → 2(0(5(x1))) (19)
4(8(8(x1))) → 9(1(x1)) (20)
1(7(x1)) → 9(6(x1)) (21)
9(3(x1)) → 3(9(x1)) (22)
5(7(x1)) → 0(1(x1)) (23)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[5(x1)] =
1 0 1
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[8(x1)] =
1 1 0
1 1 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[3(x1)] =
1 0 0
0 0 1
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[9(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[6(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[1(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[7(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[0(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[2(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[4(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
4(8(8(x1))) → 9(1(x1)) (20)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[5(x1)] = 1 · x1 + -∞
[8(x1)] = 0 · x1 + -∞
[3(x1)] = 0 · x1 + -∞
[9(x1)] = 1 · x1 + -∞
[6(x1)] = 0 · x1 + -∞
[1(x1)] = 1 · x1 + -∞
[7(x1)] = 0 · x1 + -∞
[0(x1)] = 0 · x1 + -∞
[2(x1)] = 0 · x1 + -∞
[4(x1)] = 0 · x1 + -∞
all of the following rules can be deleted.
9(5(x1)) → 5(6(2(x1))) (14)
9(x1) → 3(2(3(x1))) (4)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[5(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
1 0 0
1 0 0
[8(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[3(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[9(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[6(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[1(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[7(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[2(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[4(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
4(8(x1)) → 6(x1) (16)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[5(x1)] = 0 · x1 + -∞
[8(x1)] = 4 · x1 + -∞
[3(x1)] = 8 · x1 + -∞
[9(x1)] = 0 · x1 + -∞
[6(x1)] = 8 · x1 + -∞
[1(x1)] = 4 · x1 + -∞
[7(x1)] = 4 · x1 + -∞
[0(x1)] = 0 · x1 + -∞
[2(x1)] = 0 · x1 + -∞
[4(x1)] = 0 · x1 + -∞
all of the following rules can be deleted.
1(3(x1)) → 1(4(x1)) (13)

1.1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
5#(3(x1)) → 8#(x1) (24)
5#(3(x1)) → 9#(8(x1)) (25)
9#(x1) → 5#(x1) (26)
1#(7(x1)) → 6#(x1) (27)
1#(7(x1)) → 9#(6(x1)) (28)
9#(3(x1)) → 9#(x1) (29)
5#(7(x1)) → 1#(x1) (30)

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.