Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/159731)

The rewrite relation of the following TRS is considered.

0(0(1(0(x1)))) → 0(2(0(0(3(1(x1)))))) (1)
0(0(1(0(x1)))) → 0(2(0(4(1(0(x1)))))) (2)
0(0(1(0(x1)))) → 2(0(0(0(2(1(x1)))))) (3)
3(0(1(0(x1)))) → 0(2(3(1(0(x1))))) (4)
3(0(1(0(x1)))) → 3(1(0(0(2(x1))))) (5)
3(0(1(0(x1)))) → 3(1(1(0(0(x1))))) (6)
3(0(1(0(x1)))) → 3(1(2(0(0(x1))))) (7)
3(0(1(0(x1)))) → 3(1(5(0(0(x1))))) (8)
3(0(1(0(x1)))) → 3(5(1(0(0(x1))))) (9)
3(0(1(0(x1)))) → 5(0(3(1(0(x1))))) (10)
3(0(1(0(x1)))) → 2(0(2(3(1(0(x1)))))) (11)
3(0(1(0(x1)))) → 2(2(0(3(1(0(x1)))))) (12)
3(0(1(0(x1)))) → 3(1(5(0(0(0(x1)))))) (13)
3(0(1(0(x1)))) → 3(1(5(0(2(0(x1)))))) (14)
3(0(1(0(x1)))) → 3(1(5(1(0(0(x1)))))) (15)
3(0(1(0(x1)))) → 3(1(5(2(0(0(x1)))))) (16)
3(0(1(0(x1)))) → 3(1(5(5(0(0(x1)))))) (17)
3(0(1(0(x1)))) → 3(2(2(1(0(0(x1)))))) (18)
3(0(1(0(x1)))) → 3(5(1(0(0(2(x1)))))) (19)
3(0(1(0(x1)))) → 3(5(1(5(0(0(x1)))))) (20)
3(0(1(0(x1)))) → 5(1(1(3(0(0(x1)))))) (21)
3(4(1(0(x1)))) → 3(1(2(4(0(x1))))) (22)
3(4(1(0(x1)))) → 3(1(4(0(2(x1))))) (23)
3(4(1(0(x1)))) → 3(1(5(4(0(x1))))) (24)
3(4(1(0(x1)))) → 3(4(2(1(0(x1))))) (25)
3(4(1(0(x1)))) → 3(1(1(5(4(0(x1)))))) (26)
3(4(1(0(x1)))) → 3(1(2(1(4(0(x1)))))) (27)
3(4(1(0(x1)))) → 3(1(2(5(4(0(x1)))))) (28)
3(4(1(0(x1)))) → 3(1(4(2(0(2(x1)))))) (29)
3(4(1(0(x1)))) → 3(1(5(4(0(2(x1)))))) (30)
3(4(1(0(x1)))) → 3(1(5(5(4(0(x1)))))) (31)
3(4(1(0(x1)))) → 3(4(2(1(1(0(x1)))))) (32)
3(4(1(0(x1)))) → 3(4(5(1(2(0(x1)))))) (33)
0(1(4(1(0(x1))))) → 0(1(1(4(0(2(x1)))))) (34)
0(2(0(1(0(x1))))) → 0(2(0(0(3(1(x1)))))) (35)
0(2(0(1(0(x1))))) → 2(0(0(0(3(1(x1)))))) (36)
0(3(0(1(0(x1))))) → 0(0(3(1(3(0(x1)))))) (37)
0(3(0(1(0(x1))))) → 0(0(3(3(1(0(x1)))))) (38)
0(3(0(1(0(x1))))) → 0(0(3(5(1(0(x1)))))) (39)
0(3(0(1(0(x1))))) → 2(0(0(3(1(0(x1)))))) (40)
0(3(4(1(0(x1))))) → 0(2(0(4(3(1(x1)))))) (41)
0(5(0(1(0(x1))))) → 0(0(0(1(5(2(x1)))))) (42)
0(5(0(1(0(x1))))) → 0(0(1(5(1(0(x1)))))) (43)
0(5(0(1(0(x1))))) → 0(2(0(0(1(5(x1)))))) (44)
3(0(1(0(0(x1))))) → 3(1(3(0(0(0(x1)))))) (45)
3(0(1(1(0(x1))))) → 3(1(0(1(2(0(x1)))))) (46)
3(0(2(1(0(x1))))) → 2(0(3(1(1(0(x1)))))) (47)
3(0(2(1(0(x1))))) → 2(3(1(5(0(0(x1)))))) (48)
3(0(2(1(0(x1))))) → 3(1(2(0(1(0(x1)))))) (49)
3(0(2(1(0(x1))))) → 3(1(2(0(5(0(x1)))))) (50)
3(0(5(1(0(x1))))) → 3(1(5(2(0(0(x1)))))) (51)
3(1(0(1(0(x1))))) → 2(0(3(1(1(0(x1)))))) (52)
3(1(0(1(0(x1))))) → 3(1(1(1(0(0(x1)))))) (53)
3(1(0(1(0(x1))))) → 3(1(2(1(0(0(x1)))))) (54)
3(1(4(1(0(x1))))) → 3(1(2(1(4(0(x1)))))) (55)
3(1(4(1(0(x1))))) → 3(1(5(1(4(0(x1)))))) (56)
3(2(0(1(0(x1))))) → 0(2(3(1(5(0(x1)))))) (57)
3(2(0(1(0(x1))))) → 2(0(3(1(1(0(x1)))))) (58)
3(3(0(1(0(x1))))) → 3(1(2(0(3(0(x1)))))) (59)
3(3(0(1(0(x1))))) → 3(1(2(3(0(0(x1)))))) (60)
3(3(4(1(0(x1))))) → 3(1(2(4(3(0(x1)))))) (61)
3(3(4(1(0(x1))))) → 3(1(3(4(0(2(x1)))))) (62)
3(3(4(1(0(x1))))) → 3(1(4(3(1(0(x1)))))) (63)
3(4(0(1(0(x1))))) → 0(2(4(1(3(0(x1)))))) (64)
3(4(0(1(0(x1))))) → 3(1(4(0(0(2(x1)))))) (65)
3(4(0(1(0(x1))))) → 3(2(0(4(1(0(x1)))))) (66)
3(4(4(1(0(x1))))) → 3(1(1(4(4(0(x1)))))) (67)

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
0(1(0(0(x1)))) → 1(3(0(0(2(0(x1)))))) (68)
0(1(0(0(x1)))) → 0(1(4(0(2(0(x1)))))) (69)
0(1(0(0(x1)))) → 1(2(0(0(0(2(x1)))))) (70)
0(1(0(3(x1)))) → 0(1(3(2(0(x1))))) (71)
0(1(0(3(x1)))) → 2(0(0(1(3(x1))))) (72)
0(1(0(3(x1)))) → 0(0(1(1(3(x1))))) (73)
0(1(0(3(x1)))) → 0(0(2(1(3(x1))))) (74)
0(1(0(3(x1)))) → 0(0(5(1(3(x1))))) (75)
0(1(0(3(x1)))) → 0(0(1(5(3(x1))))) (76)
0(1(0(3(x1)))) → 0(1(3(0(5(x1))))) (77)
0(1(0(3(x1)))) → 0(1(3(2(0(2(x1)))))) (78)
0(1(0(3(x1)))) → 0(1(3(0(2(2(x1)))))) (79)
0(1(0(3(x1)))) → 0(0(0(5(1(3(x1)))))) (80)
0(1(0(3(x1)))) → 0(2(0(5(1(3(x1)))))) (81)
0(1(0(3(x1)))) → 0(0(1(5(1(3(x1)))))) (82)
0(1(0(3(x1)))) → 0(0(2(5(1(3(x1)))))) (83)
0(1(0(3(x1)))) → 0(0(5(5(1(3(x1)))))) (84)
0(1(0(3(x1)))) → 0(0(1(2(2(3(x1)))))) (85)
0(1(0(3(x1)))) → 2(0(0(1(5(3(x1)))))) (86)
0(1(0(3(x1)))) → 0(0(5(1(5(3(x1)))))) (87)
0(1(0(3(x1)))) → 0(0(3(1(1(5(x1)))))) (88)
0(1(4(3(x1)))) → 0(4(2(1(3(x1))))) (89)
0(1(4(3(x1)))) → 2(0(4(1(3(x1))))) (90)
0(1(4(3(x1)))) → 0(4(5(1(3(x1))))) (91)
0(1(4(3(x1)))) → 0(1(2(4(3(x1))))) (92)
0(1(4(3(x1)))) → 0(4(5(1(1(3(x1)))))) (93)
0(1(4(3(x1)))) → 0(4(1(2(1(3(x1)))))) (94)
0(1(4(3(x1)))) → 0(4(5(2(1(3(x1)))))) (95)
0(1(4(3(x1)))) → 2(0(2(4(1(3(x1)))))) (96)
0(1(4(3(x1)))) → 2(0(4(5(1(3(x1)))))) (97)
0(1(4(3(x1)))) → 0(4(5(5(1(3(x1)))))) (98)
0(1(4(3(x1)))) → 0(1(1(2(4(3(x1)))))) (99)
0(1(4(3(x1)))) → 0(2(1(5(4(3(x1)))))) (100)
0(1(4(1(0(x1))))) → 2(0(4(1(1(0(x1)))))) (101)
0(1(0(2(0(x1))))) → 1(3(0(0(2(0(x1)))))) (102)
0(1(0(2(0(x1))))) → 1(3(0(0(0(2(x1)))))) (103)
0(1(0(3(0(x1))))) → 0(3(1(3(0(0(x1)))))) (104)
0(1(0(3(0(x1))))) → 0(1(3(3(0(0(x1)))))) (105)
0(1(0(3(0(x1))))) → 0(1(5(3(0(0(x1)))))) (106)
0(1(0(3(0(x1))))) → 0(1(3(0(0(2(x1)))))) (107)
0(1(4(3(0(x1))))) → 1(3(4(0(2(0(x1)))))) (108)
0(1(0(5(0(x1))))) → 2(5(1(0(0(0(x1)))))) (109)
0(1(0(5(0(x1))))) → 0(1(5(1(0(0(x1)))))) (110)
0(1(0(5(0(x1))))) → 5(1(0(0(2(0(x1)))))) (111)
0(0(1(0(3(x1))))) → 0(0(0(3(1(3(x1)))))) (112)
0(1(1(0(3(x1))))) → 0(2(1(0(1(3(x1)))))) (113)
0(1(2(0(3(x1))))) → 0(1(1(3(0(2(x1)))))) (114)
0(1(2(0(3(x1))))) → 0(0(5(1(3(2(x1)))))) (115)
0(1(2(0(3(x1))))) → 0(1(0(2(1(3(x1)))))) (116)
0(1(2(0(3(x1))))) → 0(5(0(2(1(3(x1)))))) (117)
0(1(5(0(3(x1))))) → 0(0(2(5(1(3(x1)))))) (118)
0(1(0(1(3(x1))))) → 0(1(1(3(0(2(x1)))))) (119)
0(1(0(1(3(x1))))) → 0(0(1(1(1(3(x1)))))) (120)
0(1(0(1(3(x1))))) → 0(0(1(2(1(3(x1)))))) (121)
0(1(4(1(3(x1))))) → 0(4(1(2(1(3(x1)))))) (122)
0(1(4(1(3(x1))))) → 0(4(1(5(1(3(x1)))))) (123)
0(1(0(2(3(x1))))) → 0(5(1(3(2(0(x1)))))) (124)
0(1(0(2(3(x1))))) → 0(1(1(3(0(2(x1)))))) (125)
0(1(0(3(3(x1))))) → 0(3(0(2(1(3(x1)))))) (126)
0(1(0(3(3(x1))))) → 0(0(3(2(1(3(x1)))))) (127)
0(1(4(3(3(x1))))) → 0(3(4(2(1(3(x1)))))) (128)
0(1(4(3(3(x1))))) → 2(0(4(3(1(3(x1)))))) (129)
0(1(4(3(3(x1))))) → 0(1(3(4(1(3(x1)))))) (130)
0(1(0(4(3(x1))))) → 0(3(1(4(2(0(x1)))))) (131)
0(1(0(4(3(x1))))) → 2(0(0(4(1(3(x1)))))) (132)
0(1(0(4(3(x1))))) → 0(1(4(0(2(3(x1)))))) (133)
0(1(4(4(3(x1))))) → 0(4(4(1(1(3(x1)))))) (134)

1.1 Closure Under Flat Contexts

Using the flat contexts

{0(☐), 1(☐), 3(☐), 2(☐), 4(☐), 5(☐)}

We obtain the transformed TRS

There are 142 ruless (increase limit for explicit display).

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

There are 852 ruless (increase limit for explicit display).

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1 + 4
[10(x1)] = 1 · x1 + 4
[00(x1)] = 1 · x1 + 4
[14(x1)] = 1 · x1 + 6
[40(x1)] = 1 · x1
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1 + 2
[04(x1)] = 1 · x1 + 6
[03(x1)] = 1 · x1 + 2
[05(x1)] = 1 · x1 + 2
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[31(x1)] = 1 · x1
[34(x1)] = 1 · x1 + 4
[33(x1)] = 1 · x1 + 1
[35(x1)] = 1 · x1 + 2
[11(x1)] = 1 · x1
[21(x1)] = 1 · x1
[51(x1)] = 1 · x1
[15(x1)] = 1 · x1
[53(x1)] = 1 · x1
[50(x1)] = 1 · x1 + 2
[54(x1)] = 1 · x1 + 7
[52(x1)] = 1 · x1 + 2
[55(x1)] = 1 · x1 + 4
[24(x1)] = 1 · x1 + 6
[22(x1)] = 1 · x1
[23(x1)] = 1 · x1
[25(x1)] = 1 · x1
[12(x1)] = 1 · x1
[43(x1)] = 1 · x1
[42(x1)] = 1 · x1
[45(x1)] = 1 · x1
[41(x1)] = 1 · x1 + 2
[44(x1)] = 1 · x1
all of the following rules can be deleted.

There are 672 ruless (increase limit for explicit display).

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1 + 3
[10(x1)] = 1 · x1 + 2
[00(x1)] = 1 · x1 + 3
[14(x1)] = 1 · x1 + 2
[40(x1)] = 1 · x1 + 1
[02(x1)] = 1 · x1 + 1
[20(x1)] = 1 · x1 + 1
[04(x1)] = 1 · x1 + 3
[03(x1)] = 1 · x1 + 2
[05(x1)] = 1 · x1 + 1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[31(x1)] = 1 · x1
[51(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1 + 1
[55(x1)] = 1 · x1 + 3
[43(x1)] = 1 · x1 + 1
[12(x1)] = 1 · x1
[24(x1)] = 1 · x1 + 1
[45(x1)] = 1 · x1
[11(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1 + 2
[15(x1)] = 1 · x1
[21(x1)] = 1 · x1
[23(x1)] = 1 · x1
[42(x1)] = 1 · x1 + 1
[41(x1)] = 1 · x1 + 2
[22(x1)] = 1 · x1
[52(x1)] = 1 · x1 + 2
[53(x1)] = 1 · x1
[25(x1)] = 1 · x1
all of the following rules can be deleted.
01(14(43(30(x1)))) → 01(12(24(43(30(x1))))) (339)
01(14(43(31(x1)))) → 01(12(24(43(31(x1))))) (340)
01(14(43(34(x1)))) → 01(12(24(43(34(x1))))) (341)
01(14(43(32(x1)))) → 01(12(24(43(32(x1))))) (342)
01(14(43(33(x1)))) → 01(12(24(43(33(x1))))) (343)
01(14(43(35(x1)))) → 01(12(24(43(35(x1))))) (344)
01(12(20(03(30(x1))))) → 00(05(51(13(32(20(x1)))))) (429)
01(12(20(03(34(x1))))) → 00(05(51(13(32(24(x1)))))) (431)
01(10(02(23(30(x1))))) → 05(51(13(32(20(00(x1)))))) (483)
01(10(02(23(31(x1))))) → 05(51(13(32(20(01(x1)))))) (484)
40(01(10(00(04(x1))))) → 41(12(20(00(00(02(24(x1))))))) (599)
30(01(14(43(30(x1))))) → 32(20(02(24(41(13(30(x1))))))) (729)
30(01(14(43(31(x1))))) → 32(20(02(24(41(13(31(x1))))))) (730)
30(01(14(43(34(x1))))) → 32(20(02(24(41(13(34(x1))))))) (731)
30(01(14(43(32(x1))))) → 32(20(02(24(41(13(32(x1))))))) (732)
30(01(14(43(33(x1))))) → 32(20(02(24(41(13(33(x1))))))) (733)
30(01(14(43(35(x1))))) → 32(20(02(24(41(13(35(x1))))))) (734)
40(01(14(43(30(x1))))) → 42(20(02(24(41(13(30(x1))))))) (741)
40(01(14(43(31(x1))))) → 42(20(02(24(41(13(31(x1))))))) (742)
40(01(14(43(34(x1))))) → 42(20(02(24(41(13(34(x1))))))) (743)
40(01(14(43(32(x1))))) → 42(20(02(24(41(13(32(x1))))))) (744)
40(01(14(43(33(x1))))) → 42(20(02(24(41(13(33(x1))))))) (745)
40(01(14(43(35(x1))))) → 42(20(02(24(41(13(35(x1))))))) (746)
50(01(14(43(30(x1))))) → 52(20(02(24(41(13(30(x1))))))) (747)
50(01(14(43(31(x1))))) → 52(20(02(24(41(13(31(x1))))))) (748)
50(01(14(43(34(x1))))) → 52(20(02(24(41(13(34(x1))))))) (749)
50(01(14(43(32(x1))))) → 52(20(02(24(41(13(32(x1))))))) (750)
50(01(14(43(33(x1))))) → 52(20(02(24(41(13(33(x1))))))) (751)
50(01(14(43(35(x1))))) → 52(20(02(24(41(13(35(x1))))))) (752)
40(01(10(02(20(04(x1)))))) → 41(13(30(00(00(02(24(x1))))))) (887)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1 + 1
[10(x1)] = 1 · x1
[00(x1)] = 1 · x1
[14(x1)] = 1 · x1
[40(x1)] = 1 · x1
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1
[04(x1)] = 1 · x1
[03(x1)] = 1 · x1
[05(x1)] = 1 · x1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[31(x1)] = 1 · x1 + 1
[51(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1 + 1
[55(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[45(x1)] = 1 · x1
[11(x1)] = 1 · x1
[12(x1)] = 1 · x1
[24(x1)] = 1 · x1
[50(x1)] = 1 · x1
[15(x1)] = 1 · x1
[21(x1)] = 1 · x1
[42(x1)] = 1 · x1
[41(x1)] = 1 · x1 + 1
[22(x1)] = 1 · x1
[52(x1)] = 1 · x1
[53(x1)] = 1 · x1
[25(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
01(10(03(30(x1)))) → 00(00(05(51(13(30(x1)))))) (279)
01(10(03(31(x1)))) → 00(00(05(51(13(31(x1)))))) (280)
01(10(03(34(x1)))) → 00(00(05(51(13(34(x1)))))) (281)
01(10(03(32(x1)))) → 00(00(05(51(13(32(x1)))))) (282)
01(10(03(33(x1)))) → 00(00(05(51(13(33(x1)))))) (283)
01(10(03(35(x1)))) → 00(00(05(51(13(35(x1)))))) (284)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1 + 2
[10(x1)] = 1 · x1 + 2
[00(x1)] = 1 · x1 + 2
[14(x1)] = 1 · x1
[40(x1)] = 1 · x1
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1 + 1
[04(x1)] = 1 · x1
[03(x1)] = 1 · x1 + 1
[05(x1)] = 1 · x1 + 2
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[31(x1)] = 1 · x1
[55(x1)] = 1 · x1 + 1
[51(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[45(x1)] = 1 · x1 + 1
[11(x1)] = 1 · x1
[12(x1)] = 1 · x1
[24(x1)] = 1 · x1
[50(x1)] = 1 · x1
[15(x1)] = 1 · x1
[21(x1)] = 1 · x1
[42(x1)] = 1 · x1
[41(x1)] = 1 · x1 + 1
[22(x1)] = 1 · x1
[52(x1)] = 1 · x1
[53(x1)] = 1 · x1
[25(x1)] = 1 · x1
all of the following rules can be deleted.
01(10(00(00(x1)))) → 01(14(40(02(20(00(x1)))))) (225)
01(10(00(01(x1)))) → 01(14(40(02(20(01(x1)))))) (226)
01(10(00(04(x1)))) → 01(14(40(02(20(04(x1)))))) (227)
01(10(00(02(x1)))) → 01(14(40(02(20(02(x1)))))) (228)
01(10(00(03(x1)))) → 01(14(40(02(20(03(x1)))))) (229)
01(10(00(05(x1)))) → 01(14(40(02(20(05(x1)))))) (230)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[31(x1)] = 1 · x1
[05(x1)] = 1 · x1
[55(x1)] = 1 · x1
[51(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[14(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[04(x1)] = 1 · x1 + 1
[45(x1)] = 1 · x1
[11(x1)] = 1 · x1
[12(x1)] = 1 · x1
[24(x1)] = 1 · x1
[50(x1)] = 1 · x1
[15(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1
[42(x1)] = 1 · x1
[40(x1)] = 1 · x1
[41(x1)] = 1 · x1
[22(x1)] = 1 · x1
[52(x1)] = 1 · x1
[53(x1)] = 1 · x1
[25(x1)] = 1 · x1
all of the following rules can be deleted.
01(14(43(30(x1)))) → 01(11(12(24(43(30(x1)))))) (369)
01(14(43(31(x1)))) → 01(11(12(24(43(31(x1)))))) (370)
01(14(43(34(x1)))) → 01(11(12(24(43(34(x1)))))) (371)
01(14(43(32(x1)))) → 01(11(12(24(43(32(x1)))))) (372)
01(14(43(33(x1)))) → 01(11(12(24(43(33(x1)))))) (373)
01(14(43(35(x1)))) → 01(11(12(24(43(35(x1)))))) (374)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[31(x1)] = 1 · x1
[05(x1)] = 1 · x1
[55(x1)] = 1 · x1
[51(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[14(x1)] = 1 · x1
[43(x1)] = 1 · x1 + 1
[04(x1)] = 1 · x1
[45(x1)] = 1 · x1
[50(x1)] = 1 · x1
[15(x1)] = 1 · x1
[02(x1)] = 1 · x1
[12(x1)] = 1 · x1
[21(x1)] = 1 · x1
[42(x1)] = 1 · x1 + 1
[40(x1)] = 1 · x1 + 1
[41(x1)] = 1 · x1 + 1
[22(x1)] = 1 · x1
[52(x1)] = 1 · x1
[53(x1)] = 1 · x1
[25(x1)] = 1 · x1
all of the following rules can be deleted.
01(14(43(30(x1)))) → 04(45(55(51(13(30(x1)))))) (363)
01(14(43(31(x1)))) → 04(45(55(51(13(31(x1)))))) (364)
01(14(43(34(x1)))) → 04(45(55(51(13(34(x1)))))) (365)
01(14(43(32(x1)))) → 04(45(55(51(13(32(x1)))))) (366)
01(14(43(33(x1)))) → 04(45(55(51(13(33(x1)))))) (367)
01(14(43(35(x1)))) → 04(45(55(51(13(35(x1)))))) (368)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1 + 1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[31(x1)] = 1 · x1 + 1
[05(x1)] = 1 · x1
[55(x1)] = 1 · x1 + 1
[51(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1
[15(x1)] = 1 · x1
[04(x1)] = 1 · x1
[02(x1)] = 1 · x1
[12(x1)] = 1 · x1
[21(x1)] = 1 · x1
[43(x1)] = 1 · x1
[14(x1)] = 1 · x1
[42(x1)] = 1 · x1
[40(x1)] = 1 · x1
[41(x1)] = 1 · x1 + 1
[22(x1)] = 1 · x1
[52(x1)] = 1 · x1
[53(x1)] = 1 · x1
[25(x1)] = 1 · x1
all of the following rules can be deleted.
30(01(10(05(50(00(x1)))))) → 32(25(51(10(00(00(00(x1))))))) (945)
30(01(10(05(50(01(x1)))))) → 32(25(51(10(00(00(01(x1))))))) (946)
30(01(10(05(50(04(x1)))))) → 32(25(51(10(00(00(04(x1))))))) (947)
30(01(10(05(50(02(x1)))))) → 32(25(51(10(00(00(02(x1))))))) (948)
30(01(10(05(50(03(x1)))))) → 32(25(51(10(00(00(03(x1))))))) (949)
30(01(10(05(50(05(x1)))))) → 32(25(51(10(00(00(05(x1))))))) (950)
40(01(10(05(50(00(x1)))))) → 42(25(51(10(00(00(00(x1))))))) (957)
40(01(10(05(50(01(x1)))))) → 42(25(51(10(00(00(01(x1))))))) (958)
40(01(10(05(50(04(x1)))))) → 42(25(51(10(00(00(04(x1))))))) (959)
40(01(10(05(50(02(x1)))))) → 42(25(51(10(00(00(02(x1))))))) (960)
40(01(10(05(50(03(x1)))))) → 42(25(51(10(00(00(03(x1))))))) (961)
40(01(10(05(50(05(x1)))))) → 42(25(51(10(00(00(05(x1))))))) (962)
50(01(10(05(50(00(x1)))))) → 52(25(51(10(00(00(00(x1))))))) (963)
50(01(10(05(50(01(x1)))))) → 52(25(51(10(00(00(01(x1))))))) (964)
50(01(10(05(50(04(x1)))))) → 52(25(51(10(00(00(04(x1))))))) (965)
50(01(10(05(50(02(x1)))))) → 52(25(51(10(00(00(02(x1))))))) (966)
50(01(10(05(50(03(x1)))))) → 52(25(51(10(00(00(03(x1))))))) (967)
50(01(10(05(50(05(x1)))))) → 52(25(51(10(00(00(05(x1))))))) (968)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1 + 1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1 + 1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1 + 1
[31(x1)] = 1 · x1
[05(x1)] = 1 · x1
[55(x1)] = 1 · x1
[51(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[50(x1)] = 1 · x1 + 1
[15(x1)] = 1 · x1
[04(x1)] = 1 · x1 + 1
[02(x1)] = 1 · x1 + 1
[12(x1)] = 1 · x1
[21(x1)] = 1 · x1
[43(x1)] = 1 · x1
[14(x1)] = 1 · x1
[42(x1)] = 1 · x1
[40(x1)] = 1 · x1
[41(x1)] = 1 · x1
[22(x1)] = 1 · x1
[52(x1)] = 1 · x1 + 1
[53(x1)] = 1 · x1
all of the following rules can be deleted.
01(10(03(30(x1)))) → 00(05(55(51(13(30(x1)))))) (303)
01(10(03(31(x1)))) → 00(05(55(51(13(31(x1)))))) (304)
01(10(03(34(x1)))) → 00(05(55(51(13(34(x1)))))) (305)
01(10(03(32(x1)))) → 00(05(55(51(13(32(x1)))))) (306)
01(10(03(33(x1)))) → 00(05(55(51(13(33(x1)))))) (307)
01(10(03(35(x1)))) → 00(05(55(51(13(35(x1)))))) (308)
50(01(10(05(50(00(x1)))))) → 55(51(10(00(02(20(00(x1))))))) (999)
50(01(10(05(50(01(x1)))))) → 55(51(10(00(02(20(01(x1))))))) (1000)
50(01(10(05(50(04(x1)))))) → 55(51(10(00(02(20(04(x1))))))) (1001)
50(01(10(05(50(02(x1)))))) → 55(51(10(00(02(20(02(x1))))))) (1002)
50(01(10(05(50(03(x1)))))) → 55(51(10(00(02(20(03(x1))))))) (1003)
50(01(10(05(50(05(x1)))))) → 55(51(10(00(02(20(05(x1))))))) (1004)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[31(x1)] = 1 · x1
[05(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1
[15(x1)] = 1 · x1
[51(x1)] = 1 · x1
[04(x1)] = 1 · x1
[02(x1)] = 1 · x1
[12(x1)] = 1 · x1
[21(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[14(x1)] = 1 · x1
[42(x1)] = 1 · x1
[40(x1)] = 1 · x1
[41(x1)] = 1 · x1
[22(x1)] = 1 · x1
[52(x1)] = 1 · x1
[53(x1)] = 1 · x1
all of the following rules can be deleted.
01(10(05(50(00(x1))))) → 01(15(51(10(00(00(x1)))))) (405)
01(10(05(50(01(x1))))) → 01(15(51(10(00(01(x1)))))) (406)
01(10(05(50(04(x1))))) → 01(15(51(10(00(04(x1)))))) (407)
01(10(05(50(02(x1))))) → 01(15(51(10(00(02(x1)))))) (408)
01(10(05(50(03(x1))))) → 01(15(51(10(00(03(x1)))))) (409)
01(10(05(50(05(x1))))) → 01(15(51(10(00(05(x1)))))) (410)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[31(x1)] = 1 · x1
[12(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[04(x1)] = 1 · x1
[43(x1)] = 1 · x1
[14(x1)] = 1 · x1
[42(x1)] = 1 · x1
[40(x1)] = 1 · x1
[41(x1)] = 1 · x1
[22(x1)] = 1 · x1
[50(x1)] = 1 · x1
[52(x1)] = 1 · x1
[15(x1)] = 1 · x1
[53(x1)] = 1 · x1
[05(x1)] = 1 · x1 + 1
[51(x1)] = 1 · x1
all of the following rules can be deleted.
30(01(10(05(50(00(x1)))))) → 35(51(10(00(02(20(00(x1))))))) (981)
30(01(10(05(50(01(x1)))))) → 35(51(10(00(02(20(01(x1))))))) (982)
30(01(10(05(50(04(x1)))))) → 35(51(10(00(02(20(04(x1))))))) (983)
30(01(10(05(50(02(x1)))))) → 35(51(10(00(02(20(02(x1))))))) (984)
30(01(10(05(50(03(x1)))))) → 35(51(10(00(02(20(03(x1))))))) (985)
30(01(10(05(50(05(x1)))))) → 35(51(10(00(02(20(05(x1))))))) (986)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1 + 1
[30(x1)] = 1 · x1
[13(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[31(x1)] = 1 · x1
[12(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1 + 1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[04(x1)] = 1 · x1
[43(x1)] = 1 · x1 + 2
[14(x1)] = 1 · x1
[42(x1)] = 1 · x1
[40(x1)] = 1 · x1 + 2
[41(x1)] = 1 · x1 + 2
[22(x1)] = 1 · x1
[50(x1)] = 1 · x1
[52(x1)] = 1 · x1
[15(x1)] = 1 · x1 + 1
[53(x1)] = 1 · x1
all of the following rules can be deleted.
01(10(03(30(x1)))) → 01(13(32(20(00(x1))))) (231)
01(10(03(31(x1)))) → 01(13(32(20(01(x1))))) (232)
01(10(04(43(30(x1))))) → 03(31(14(42(20(00(x1)))))) (519)
01(10(04(43(31(x1))))) → 03(31(14(42(20(01(x1)))))) (520)
30(01(10(03(30(x1))))) → 32(20(00(01(13(30(x1)))))) (621)
30(01(10(03(31(x1))))) → 32(20(00(01(13(31(x1)))))) (622)
30(01(10(03(34(x1))))) → 32(20(00(01(13(34(x1)))))) (623)
30(01(10(03(32(x1))))) → 32(20(00(01(13(32(x1)))))) (624)
30(01(10(03(33(x1))))) → 32(20(00(01(13(33(x1)))))) (625)
30(01(10(03(35(x1))))) → 32(20(00(01(13(35(x1)))))) (626)
40(01(10(03(30(x1))))) → 42(20(00(01(13(30(x1)))))) (633)
40(01(10(03(31(x1))))) → 42(20(00(01(13(31(x1)))))) (634)
40(01(10(03(34(x1))))) → 42(20(00(01(13(34(x1)))))) (635)
40(01(10(03(32(x1))))) → 42(20(00(01(13(32(x1)))))) (636)
40(01(10(03(33(x1))))) → 42(20(00(01(13(33(x1)))))) (637)
40(01(10(03(35(x1))))) → 42(20(00(01(13(35(x1)))))) (638)
50(01(10(03(30(x1))))) → 52(20(00(01(13(30(x1)))))) (639)
50(01(10(03(31(x1))))) → 52(20(00(01(13(31(x1)))))) (640)
50(01(10(03(34(x1))))) → 52(20(00(01(13(34(x1)))))) (641)
50(01(10(03(32(x1))))) → 52(20(00(01(13(32(x1)))))) (642)
50(01(10(03(33(x1))))) → 52(20(00(01(13(33(x1)))))) (643)
50(01(10(03(35(x1))))) → 52(20(00(01(13(35(x1)))))) (644)
40(01(10(03(30(x1))))) → 42(20(00(01(15(53(30(x1))))))) (669)
40(01(10(03(31(x1))))) → 42(20(00(01(15(53(31(x1))))))) (670)
40(01(10(03(34(x1))))) → 42(20(00(01(15(53(34(x1))))))) (671)
40(01(10(03(32(x1))))) → 42(20(00(01(15(53(32(x1))))))) (672)
40(01(10(03(33(x1))))) → 42(20(00(01(15(53(33(x1))))))) (673)
40(01(10(03(35(x1))))) → 42(20(00(01(15(53(35(x1))))))) (674)
40(01(14(43(30(x1))))) → 42(20(04(41(13(30(x1)))))) (705)
40(01(14(43(31(x1))))) → 42(20(04(41(13(31(x1)))))) (706)
40(01(14(43(34(x1))))) → 42(20(04(41(13(34(x1)))))) (707)
40(01(14(43(32(x1))))) → 42(20(04(41(13(32(x1)))))) (708)
40(01(14(43(33(x1))))) → 42(20(04(41(13(33(x1)))))) (709)
40(01(14(43(35(x1))))) → 42(20(04(41(13(35(x1)))))) (710)
40(01(10(04(43(30(x1)))))) → 42(20(00(04(41(13(30(x1))))))) (1065)
40(01(10(04(43(31(x1)))))) → 42(20(00(04(41(13(31(x1))))))) (1066)
40(01(10(04(43(34(x1)))))) → 42(20(00(04(41(13(34(x1))))))) (1067)
40(01(10(04(43(32(x1)))))) → 42(20(00(04(41(13(32(x1))))))) (1068)
40(01(10(04(43(33(x1)))))) → 42(20(00(04(41(13(33(x1))))))) (1069)
40(01(10(04(43(35(x1)))))) → 42(20(00(04(41(13(35(x1))))))) (1070)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[03(x1)] = 1 · x1
[30(x1)] = 1 · x1
[10(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1
[13(x1)] = 1 · x1
[31(x1)] = 1 · x1
[34(x1)] = 1 · x1
[32(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[40(x1)] = 1 · x1 + 1
[00(x1)] = 1 · x1
[41(x1)] = 1 · x1
[22(x1)] = 1 · x1
[15(x1)] = 1 · x1
[53(x1)] = 1 · x1
[50(x1)] = 1 · x1
[52(x1)] = 1 · x1
[14(x1)] = 1 · x1
[43(x1)] = 1 · x1
[04(x1)] = 1 · x1
all of the following rules can be deleted.
40(01(10(00(02(x1))))) → 41(12(20(00(00(02(22(x1))))))) (600)
40(01(10(02(20(02(x1)))))) → 41(13(30(00(00(02(22(x1))))))) (888)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1
[12(x1)] = 1 · x1 + 1
[20(x1)] = 1 · x1
[03(x1)] = 1 · x1
[30(x1)] = 1 · x1
[10(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1
[13(x1)] = 1 · x1
[31(x1)] = 1 · x1
[34(x1)] = 1 · x1
[32(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[00(x1)] = 1 · x1
[15(x1)] = 1 · x1
[53(x1)] = 1 · x1
[50(x1)] = 1 · x1
[52(x1)] = 1 · x1
[14(x1)] = 1 · x1
[43(x1)] = 1 · x1
[04(x1)] = 1 · x1
[41(x1)] = 1 · x1
all of the following rules can be deleted.
01(12(20(03(30(x1))))) → 01(10(02(21(13(30(x1)))))) (435)
01(12(20(03(31(x1))))) → 01(10(02(21(13(31(x1)))))) (436)
01(12(20(03(34(x1))))) → 01(10(02(21(13(34(x1)))))) (437)
01(12(20(03(32(x1))))) → 01(10(02(21(13(32(x1)))))) (438)
01(12(20(03(33(x1))))) → 01(10(02(21(13(33(x1)))))) (439)
01(12(20(03(35(x1))))) → 01(10(02(21(13(35(x1)))))) (440)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[30(x1)] = 1 · x1
[01(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1 + 1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[15(x1)] = 1 · x1
[53(x1)] = 1 · x1
[31(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[50(x1)] = 1 · x1
[52(x1)] = 1 · x1
[14(x1)] = 1 · x1
[43(x1)] = 1 · x1
[04(x1)] = 1 · x1
[41(x1)] = 1 · x1
[13(x1)] = 1 · x1
all of the following rules can be deleted.
30(01(10(03(30(x1))))) → 32(20(00(01(15(53(30(x1))))))) (657)
30(01(10(03(31(x1))))) → 32(20(00(01(15(53(31(x1))))))) (658)
30(01(10(03(34(x1))))) → 32(20(00(01(15(53(34(x1))))))) (659)
30(01(10(03(32(x1))))) → 32(20(00(01(15(53(32(x1))))))) (660)
30(01(10(03(33(x1))))) → 32(20(00(01(15(53(33(x1))))))) (661)
30(01(10(03(35(x1))))) → 32(20(00(01(15(53(35(x1))))))) (662)
50(01(10(03(30(x1))))) → 52(20(00(01(15(53(30(x1))))))) (675)
50(01(10(03(31(x1))))) → 52(20(00(01(15(53(31(x1))))))) (676)
50(01(10(03(34(x1))))) → 52(20(00(01(15(53(34(x1))))))) (677)
50(01(10(03(32(x1))))) → 52(20(00(01(15(53(32(x1))))))) (678)
50(01(10(03(33(x1))))) → 52(20(00(01(15(53(33(x1))))))) (679)
50(01(10(03(35(x1))))) → 52(20(00(01(15(53(35(x1))))))) (680)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[30(x1)] = 1 · x1
[01(x1)] = 1 · x1
[14(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[04(x1)] = 1 · x1
[41(x1)] = 1 · x1
[13(x1)] = 1 · x1
[31(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[50(x1)] = 1 · x1
[52(x1)] = 1 · x1
[10(x1)] = 1 · x1
[00(x1)] = 1 · x1
all of the following rules can be deleted.
30(01(14(43(30(x1))))) → 32(20(04(41(13(30(x1)))))) (693)
30(01(14(43(31(x1))))) → 32(20(04(41(13(31(x1)))))) (694)
30(01(14(43(34(x1))))) → 32(20(04(41(13(34(x1)))))) (695)
30(01(14(43(32(x1))))) → 32(20(04(41(13(32(x1)))))) (696)
30(01(14(43(33(x1))))) → 32(20(04(41(13(33(x1)))))) (697)
30(01(14(43(35(x1))))) → 32(20(04(41(13(35(x1)))))) (698)
50(01(14(43(30(x1))))) → 52(20(04(41(13(30(x1)))))) (711)
50(01(14(43(31(x1))))) → 52(20(04(41(13(31(x1)))))) (712)
50(01(14(43(34(x1))))) → 52(20(04(41(13(34(x1)))))) (713)
50(01(14(43(32(x1))))) → 52(20(04(41(13(32(x1)))))) (714)
50(01(14(43(33(x1))))) → 52(20(04(41(13(33(x1)))))) (715)
50(01(14(43(35(x1))))) → 52(20(04(41(13(35(x1)))))) (716)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[30(x1)] = 1 · x1 + 1
[01(x1)] = 1 · x1
[10(x1)] = 1 · x1
[04(x1)] = 1 · x1
[43(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[41(x1)] = 1 · x1
[13(x1)] = 1 · x1
[31(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
[50(x1)] = 1 · x1
[52(x1)] = 1 · x1
all of the following rules can be deleted.
30(01(10(04(43(30(x1)))))) → 32(20(00(04(41(13(30(x1))))))) (1053)
30(01(10(04(43(31(x1)))))) → 32(20(00(04(41(13(31(x1))))))) (1054)
30(01(10(04(43(34(x1)))))) → 32(20(00(04(41(13(34(x1))))))) (1055)
30(01(10(04(43(32(x1)))))) → 32(20(00(04(41(13(32(x1))))))) (1056)
30(01(10(04(43(33(x1)))))) → 32(20(00(04(41(13(33(x1))))))) (1057)
30(01(10(04(43(35(x1)))))) → 32(20(00(04(41(13(35(x1))))))) (1058)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[50(x1)] = 1 · x1
[01(x1)] = 1 · x1 + 1
[10(x1)] = 1 · x1
[04(x1)] = 1 · x1
[43(x1)] = 1 · x1
[30(x1)] = 1 · x1
[52(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1
[41(x1)] = 1 · x1
[13(x1)] = 1 · x1
[31(x1)] = 1 · x1
[34(x1)] = 1 · x1
[32(x1)] = 1 · x1
[33(x1)] = 1 · x1
[35(x1)] = 1 · x1
all of the following rules can be deleted.
50(01(10(04(43(30(x1)))))) → 52(20(00(04(41(13(30(x1))))))) (1071)
50(01(10(04(43(31(x1)))))) → 52(20(00(04(41(13(31(x1))))))) (1072)
50(01(10(04(43(34(x1)))))) → 52(20(00(04(41(13(34(x1))))))) (1073)
50(01(10(04(43(32(x1)))))) → 52(20(00(04(41(13(32(x1))))))) (1074)
50(01(10(04(43(33(x1)))))) → 52(20(00(04(41(13(33(x1))))))) (1075)
50(01(10(04(43(35(x1)))))) → 52(20(00(04(41(13(35(x1))))))) (1076)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

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