Certification Problem

Input (TPDB SRS_Standard/Zantema_06/beans1)

The rewrite relation of the following TRS is considered.

1(2(1(x1))) → 2(0(2(x1))) (1)
0(2(1(x1))) → 1(0(2(x1))) (2)
L(2(1(x1))) → L(1(0(2(x1)))) (3)
1(2(0(x1))) → 2(0(1(x1))) (4)
1(2(R(x1))) → 2(0(1(R(x1)))) (5)
0(2(0(x1))) → 1(0(1(x1))) (6)
L(2(0(x1))) → L(1(0(1(x1)))) (7)
0(2(R(x1))) → 1(0(1(R(x1)))) (8)

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
1(2(1(x1))) → 2(0(2(x1))) (1)
1(2(0(x1))) → 2(0(1(x1))) (4)
1(2(L(x1))) → 2(0(1(L(x1)))) (9)
0(2(1(x1))) → 1(0(2(x1))) (2)
R(2(1(x1))) → R(1(0(2(x1)))) (10)
0(2(0(x1))) → 1(0(1(x1))) (6)
0(2(L(x1))) → 1(0(1(L(x1)))) (11)
R(2(0(x1))) → R(1(0(1(x1)))) (12)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
1#(2(1(x1))) → 0#(2(x1)) (13)
1#(2(0(x1))) → 0#(1(x1)) (14)
1#(2(0(x1))) → 1#(x1) (15)
1#(2(L(x1))) → 0#(1(L(x1))) (16)
1#(2(L(x1))) → 1#(L(x1)) (17)
0#(2(1(x1))) → 1#(0(2(x1))) (18)
0#(2(1(x1))) → 0#(2(x1)) (19)
R#(2(1(x1))) → R#(1(0(2(x1)))) (20)
R#(2(1(x1))) → 1#(0(2(x1))) (21)
R#(2(1(x1))) → 0#(2(x1)) (22)
0#(2(0(x1))) → 1#(0(1(x1))) (23)
0#(2(0(x1))) → 0#(1(x1)) (24)
0#(2(0(x1))) → 1#(x1) (25)
0#(2(L(x1))) → 1#(0(1(L(x1)))) (26)
0#(2(L(x1))) → 0#(1(L(x1))) (27)
0#(2(L(x1))) → 1#(L(x1)) (28)
R#(2(0(x1))) → R#(1(0(1(x1)))) (29)
R#(2(0(x1))) → 1#(0(1(x1))) (30)
R#(2(0(x1))) → 0#(1(x1)) (31)
R#(2(0(x1))) → 1#(x1) (32)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.