Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/212421)

The rewrite relation of the following TRS is considered.

0(1(2(x1))) → 0(1(3(2(x1)))) (1)
0(1(2(x1))) → 0(2(1(0(x1)))) (2)
0(1(2(x1))) → 0(2(1(3(x1)))) (3)
0(1(2(x1))) → 0(2(2(1(x1)))) (4)
0(1(2(x1))) → 0(2(2(1(4(x1))))) (5)
0(1(2(x1))) → 5(1(0(5(2(3(x1)))))) (6)
0(2(4(x1))) → 0(2(1(4(3(x1))))) (7)
0(4(2(x1))) → 4(0(2(3(x1)))) (8)
0(4(2(x1))) → 4(0(5(5(2(x1))))) (9)
0(0(4(2(x1)))) → 0(0(2(2(3(4(x1)))))) (10)
0(1(2(2(x1)))) → 0(2(1(0(2(x1))))) (11)
0(1(2(2(x1)))) → 1(3(0(2(2(x1))))) (12)
0(1(2(4(x1)))) → 0(1(4(2(3(x1))))) (13)
0(1(2(4(x1)))) → 4(0(2(2(1(1(x1)))))) (14)
0(1(2(4(x1)))) → 4(0(5(5(2(1(x1)))))) (15)
0(1(2(5(x1)))) → 3(5(5(2(1(0(x1)))))) (16)
0(1(4(2(x1)))) → 0(5(2(1(4(x1))))) (17)
0(1(5(2(x1)))) → 1(5(0(2(3(x1))))) (18)
0(1(5(2(x1)))) → 0(2(2(1(0(5(x1)))))) (19)
0(1(5(2(x1)))) → 5(5(0(2(1(3(x1)))))) (20)
0(2(4(2(x1)))) → 0(5(4(3(2(2(x1)))))) (21)
0(3(1(2(x1)))) → 0(2(1(3(2(x1))))) (22)
0(3(1(2(x1)))) → 1(0(2(5(3(x1))))) (23)
0(3(1(2(x1)))) → 1(5(0(2(3(x1))))) (24)
0(3(1(2(x1)))) → 3(0(2(2(1(x1))))) (25)
0(3(1(2(x1)))) → 3(2(2(1(0(x1))))) (26)
0(3(1(2(x1)))) → 0(3(2(3(1(3(x1)))))) (27)
0(3(4(2(x1)))) → 0(2(2(3(4(x1))))) (28)
5(0(1(2(x1)))) → 1(3(2(5(0(x1))))) (29)
5(0(1(2(x1)))) → 5(0(2(1(3(3(x1)))))) (30)
0(1(1(2(5(x1))))) → 5(0(2(5(1(1(x1)))))) (31)
0(2(3(4(2(x1))))) → 3(2(2(3(4(0(x1)))))) (32)
0(3(1(2(5(x1))))) → 2(3(1(3(0(5(x1)))))) (33)
0(3(1(5(2(x1))))) → 0(3(2(5(1(2(x1)))))) (34)
0(3(4(1(4(x1))))) → 0(5(3(1(4(4(x1)))))) (35)
0(3(5(1(2(x1))))) → 5(5(3(2(1(0(x1)))))) (36)
0(4(0(4(2(x1))))) → 4(4(0(0(2(2(x1)))))) (37)
0(4(1(1(2(x1))))) → 3(1(4(0(2(1(x1)))))) (38)
0(4(1(2(2(x1))))) → 4(1(0(2(2(3(x1)))))) (39)
0(4(1(2(5(x1))))) → 3(4(1(0(2(5(x1)))))) (40)
0(4(2(1(2(x1))))) → 4(1(3(2(0(2(x1)))))) (41)
0(4(2(1(4(x1))))) → 0(2(1(4(4(4(x1)))))) (42)
0(4(2(5(2(x1))))) → 5(4(3(2(2(0(x1)))))) (43)
0(4(5(1(2(x1))))) → 1(4(2(0(5(5(x1)))))) (44)
0(4(5(1(2(x1))))) → 4(0(2(5(1(1(x1)))))) (45)
5(0(1(2(2(x1))))) → 5(0(2(2(1(2(x1)))))) (46)
5(0(2(4(2(x1))))) → 0(2(2(5(1(4(x1)))))) (47)
5(0(4(4(2(x1))))) → 0(5(2(5(4(4(x1)))))) (48)

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
2(1(0(x1))) → 2(3(1(0(x1)))) (49)
2(1(0(x1))) → 0(1(2(0(x1)))) (50)
2(1(0(x1))) → 3(1(2(0(x1)))) (51)
2(1(0(x1))) → 1(2(2(0(x1)))) (52)
2(1(0(x1))) → 4(1(2(2(0(x1))))) (53)
2(1(0(x1))) → 3(2(5(0(1(5(x1)))))) (54)
4(2(0(x1))) → 3(4(1(2(0(x1))))) (55)
2(4(0(x1))) → 3(2(0(4(x1)))) (56)
2(4(0(x1))) → 2(5(5(0(4(x1))))) (57)
2(4(0(0(x1)))) → 4(3(2(2(0(0(x1)))))) (58)
2(2(1(0(x1)))) → 2(0(1(2(0(x1))))) (59)
2(2(1(0(x1)))) → 2(2(0(3(1(x1))))) (60)
4(2(1(0(x1)))) → 3(2(4(1(0(x1))))) (61)
4(2(1(0(x1)))) → 1(1(2(2(0(4(x1)))))) (62)
4(2(1(0(x1)))) → 1(2(5(5(0(4(x1)))))) (63)
5(2(1(0(x1)))) → 0(1(2(5(5(3(x1)))))) (64)
2(4(1(0(x1)))) → 4(1(2(5(0(x1))))) (65)
2(5(1(0(x1)))) → 3(2(0(5(1(x1))))) (66)
2(5(1(0(x1)))) → 5(0(1(2(2(0(x1)))))) (67)
2(5(1(0(x1)))) → 3(1(2(0(5(5(x1)))))) (68)
2(4(2(0(x1)))) → 2(2(3(4(5(0(x1)))))) (69)
2(1(3(0(x1)))) → 2(3(1(2(0(x1))))) (70)
2(1(3(0(x1)))) → 3(5(2(0(1(x1))))) (71)
2(1(3(0(x1)))) → 3(2(0(5(1(x1))))) (72)
2(1(3(0(x1)))) → 1(2(2(0(3(x1))))) (73)
2(1(3(0(x1)))) → 0(1(2(2(3(x1))))) (74)
2(1(3(0(x1)))) → 3(1(3(2(3(0(x1)))))) (75)
2(4(3(0(x1)))) → 4(3(2(2(0(x1))))) (76)
2(1(0(5(x1)))) → 0(5(2(3(1(x1))))) (77)
2(1(0(5(x1)))) → 3(3(1(2(0(5(x1)))))) (78)
5(2(1(1(0(x1))))) → 1(1(5(2(0(5(x1)))))) (79)
2(4(3(2(0(x1))))) → 0(4(3(2(2(3(x1)))))) (80)
5(2(1(3(0(x1))))) → 5(0(3(1(3(2(x1)))))) (81)
2(5(1(3(0(x1))))) → 2(1(5(2(3(0(x1)))))) (82)
4(1(4(3(0(x1))))) → 4(4(1(3(5(0(x1)))))) (83)
2(1(5(3(0(x1))))) → 0(1(2(3(5(5(x1)))))) (84)
2(4(0(4(0(x1))))) → 2(2(0(0(4(4(x1)))))) (85)
2(1(1(4(0(x1))))) → 1(2(0(4(1(3(x1)))))) (86)
2(2(1(4(0(x1))))) → 3(2(2(0(1(4(x1)))))) (87)
5(2(1(4(0(x1))))) → 5(2(0(1(4(3(x1)))))) (88)
2(1(2(4(0(x1))))) → 2(0(2(3(1(4(x1)))))) (89)
4(1(2(4(0(x1))))) → 4(4(4(1(2(0(x1)))))) (90)
2(5(2(4(0(x1))))) → 0(2(2(3(4(5(x1)))))) (91)
2(1(5(4(0(x1))))) → 5(5(0(2(4(1(x1)))))) (92)
2(1(5(4(0(x1))))) → 1(1(5(2(0(4(x1)))))) (93)
2(2(1(0(5(x1))))) → 2(1(2(2(0(5(x1)))))) (94)
2(4(2(0(5(x1))))) → 4(1(5(2(2(0(x1)))))) (95)
2(4(4(0(5(x1))))) → 4(4(5(2(5(0(x1)))))) (96)

1.1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS

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

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1.1 Rule Removal

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

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

1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[25(x1)] = 1 · x1
[51(x1)] = 1 · x1
[13(x1)] = 1 · x1
[30(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1
[15(x1)] = 1 · x1
[52(x1)] = 1 · x1
[23(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1
[41(x1)] = 1 · x1
[14(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[44(x1)] = 1 · x1
[35(x1)] = 1 · x1
[50(x1)] = 1 · x1
[22(x1)] = 1 · x1
[10(x1)] = 1 · x1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[24(x1)] = 1 · x1
[32(x1)] = 1 · x1
[42(x1)] = 1 · x1
[34(x1)] = 1 · x1
[33(x1)] = 1 · x1
[11(x1)] = 1 · x1
all of the following rules can be deleted.
41(14(43(30(02(x1))))) → 44(41(13(35(50(02(x1)))))) (348)
41(14(43(30(01(x1))))) → 44(41(13(35(50(01(x1)))))) (349)
41(14(43(30(00(x1))))) → 44(41(13(35(50(00(x1)))))) (350)
41(14(43(30(03(x1))))) → 44(41(13(35(50(03(x1)))))) (351)
41(14(43(30(04(x1))))) → 44(41(13(35(50(04(x1)))))) (352)
41(14(43(30(05(x1))))) → 44(41(13(35(50(05(x1)))))) (353)
14(42(20(02(x1)))) → 13(34(41(12(20(02(x1)))))) (564)
14(42(20(01(x1)))) → 13(34(41(12(20(01(x1)))))) (565)
14(42(20(00(x1)))) → 13(34(41(12(20(00(x1)))))) (566)
14(42(20(03(x1)))) → 13(34(41(12(20(03(x1)))))) (567)
14(42(20(04(x1)))) → 13(34(41(12(20(04(x1)))))) (568)
14(42(20(05(x1)))) → 13(34(41(12(20(05(x1)))))) (569)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[25(x1)] = 1 · x1
[51(x1)] = 1 · x1
[13(x1)] = 1 · x1 + 1
[30(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1 + 1
[15(x1)] = 1 · x1
[52(x1)] = 1 · x1
[23(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1
[22(x1)] = 1 · x1
[10(x1)] = 1 · x1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[50(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[24(x1)] = 1 · x1
[41(x1)] = 1 · x1
[32(x1)] = 1 · x1
[34(x1)] = 1 · x1
[42(x1)] = 1 · x1
[33(x1)] = 1 · x1
[44(x1)] = 1 · x1
[43(x1)] = 1 · x1
[11(x1)] = 1 · x1
[35(x1)] = 1 · x1
all of the following rules can be deleted.
22(21(10(02(x1)))) → 24(41(12(22(20(02(x1)))))) (486)
22(21(10(01(x1)))) → 24(41(12(22(20(01(x1)))))) (487)
22(21(10(00(x1)))) → 24(41(12(22(20(00(x1)))))) (488)
22(21(10(03(x1)))) → 24(41(12(22(20(03(x1)))))) (489)
22(21(10(04(x1)))) → 24(41(12(22(20(04(x1)))))) (490)
22(21(10(05(x1)))) → 24(41(12(22(20(05(x1)))))) (491)
02(21(10(02(x1)))) → 04(41(12(22(20(02(x1)))))) (498)
02(21(10(01(x1)))) → 04(41(12(22(20(01(x1)))))) (499)
02(21(10(00(x1)))) → 04(41(12(22(20(00(x1)))))) (500)
02(21(10(03(x1)))) → 04(41(12(22(20(03(x1)))))) (501)
02(21(10(04(x1)))) → 04(41(12(22(20(04(x1)))))) (502)
02(21(10(05(x1)))) → 04(41(12(22(20(05(x1)))))) (503)
52(21(10(02(x1)))) → 54(41(12(22(20(02(x1)))))) (516)
52(21(10(01(x1)))) → 54(41(12(22(20(01(x1)))))) (517)
52(21(10(00(x1)))) → 54(41(12(22(20(00(x1)))))) (518)
52(21(10(03(x1)))) → 54(41(12(22(20(03(x1)))))) (519)
52(21(10(04(x1)))) → 54(41(12(22(20(04(x1)))))) (520)
52(21(10(05(x1)))) → 54(41(12(22(20(05(x1)))))) (521)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[25(x1)] = 1 · x1
[51(x1)] = 1 · x1
[13(x1)] = 1 · x1
[30(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1
[15(x1)] = 1 · x1
[52(x1)] = 1 · x1
[23(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1
[22(x1)] = 1 · x1
[10(x1)] = 1 · x1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[50(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[32(x1)] = 1 · x1
[34(x1)] = 1 · x1
[42(x1)] = 1 · x1
[33(x1)] = 1 · x1
[41(x1)] = 1 · x1
[44(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[24(x1)] = 1 · x1
[11(x1)] = 1 · x1
[35(x1)] = 1 · x1
all of the following rules can be deleted.
44(42(20(02(x1)))) → 43(34(41(12(20(02(x1)))))) (582)
44(42(20(01(x1)))) → 43(34(41(12(20(01(x1)))))) (583)
44(42(20(00(x1)))) → 43(34(41(12(20(00(x1)))))) (584)
44(42(20(03(x1)))) → 43(34(41(12(20(03(x1)))))) (585)
44(42(20(04(x1)))) → 43(34(41(12(20(04(x1)))))) (586)
44(42(20(05(x1)))) → 43(34(41(12(20(05(x1)))))) (587)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[25(x1)] = 1 · x1
[51(x1)] = 1 · x1 + 1
[13(x1)] = 1 · x1
[30(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1 + 1
[15(x1)] = 1 · x1
[52(x1)] = 1 · x1
[23(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1
[22(x1)] = 1 · x1
[10(x1)] = 1 · x1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[50(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[32(x1)] = 1 · x1
[34(x1)] = 1 · x1
[42(x1)] = 1 · x1
[33(x1)] = 1 · x1
[41(x1)] = 1 · x1
[24(x1)] = 1 · x1
[11(x1)] = 1 · x1
[43(x1)] = 1 · x1
[35(x1)] = 1 · x1
all of the following rules can be deleted.
52(25(51(10(02(x1))))) → 55(50(01(12(22(20(02(x1))))))) (912)
52(25(51(10(01(x1))))) → 55(50(01(12(22(20(01(x1))))))) (913)
52(25(51(10(00(x1))))) → 55(50(01(12(22(20(00(x1))))))) (914)
52(25(51(10(03(x1))))) → 55(50(01(12(22(20(03(x1))))))) (915)
52(25(51(10(04(x1))))) → 55(50(01(12(22(20(04(x1))))))) (916)
52(25(51(10(05(x1))))) → 55(50(01(12(22(20(05(x1))))))) (917)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[25(x1)] = 1 · x1
[51(x1)] = 1 · x1
[13(x1)] = 1 · x1
[30(x1)] = 1 · x1 + 3
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1
[15(x1)] = 1 · x1
[52(x1)] = 1 · x1
[23(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1 + 2
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1 + 3
[22(x1)] = 1 · x1
[10(x1)] = 1 · x1 + 2
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1 + 2
[50(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1 + 1
[55(x1)] = 1 · x1
[32(x1)] = 1 · x1 + 1
[34(x1)] = 1 · x1
[42(x1)] = 1 · x1
[33(x1)] = 1 · x1
[41(x1)] = 1 · x1
[24(x1)] = 1 · x1 + 1
[11(x1)] = 1 · x1
[43(x1)] = 1 · x1
[35(x1)] = 1 · x1 + 4
all of the following rules can be deleted.
12(21(10(01(x1)))) → 13(32(25(50(01(15(51(x1))))))) (529)
24(42(21(10(02(x1))))) → 21(11(12(22(20(04(42(x1))))))) (702)
02(24(43(30(02(x1))))) → 04(43(32(22(20(02(x1)))))) (1146)
02(24(43(30(01(x1))))) → 04(43(32(22(20(01(x1)))))) (1147)
02(24(43(30(00(x1))))) → 04(43(32(22(20(00(x1)))))) (1148)
02(24(43(30(03(x1))))) → 04(43(32(22(20(03(x1)))))) (1149)
02(24(43(30(04(x1))))) → 04(43(32(22(20(04(x1)))))) (1150)
02(24(43(30(05(x1))))) → 04(43(32(22(20(05(x1)))))) (1151)
52(24(43(32(20(02(x1)))))) → 50(04(43(32(22(23(32(x1))))))) (1308)
52(24(43(32(20(00(x1)))))) → 50(04(43(32(22(23(30(x1))))))) (1310)
52(24(43(32(20(05(x1)))))) → 50(04(43(32(22(23(35(x1))))))) (1313)
22(24(42(20(05(52(x1)))))) → 24(41(15(52(22(20(02(x1))))))) (1530)
22(24(42(20(05(50(x1)))))) → 24(41(15(52(22(20(00(x1))))))) (1532)
22(24(42(20(05(54(x1)))))) → 24(41(15(52(22(20(04(x1))))))) (1534)
02(24(42(20(05(52(x1)))))) → 04(41(15(52(22(20(02(x1))))))) (1542)
02(24(42(20(05(50(x1)))))) → 04(41(15(52(22(20(00(x1))))))) (1544)
02(24(42(20(05(54(x1)))))) → 04(41(15(52(22(20(04(x1))))))) (1546)
52(24(42(20(05(52(x1)))))) → 54(41(15(52(22(20(02(x1))))))) (1560)
52(24(42(20(05(50(x1)))))) → 54(41(15(52(22(20(00(x1))))))) (1562)
52(24(42(20(05(54(x1)))))) → 54(41(15(52(22(20(04(x1))))))) (1564)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[25(x1)] = 1 · x1
[51(x1)] = 1 · x1
[13(x1)] = 1 · x1
[30(x1)] = 1 · x1
[02(x1)] = 1 · x1 + 1
[21(x1)] = 1 · x1
[15(x1)] = 1 · x1
[52(x1)] = 1 · x1
[23(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1 + 1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1 + 1
[22(x1)] = 1 · x1
[10(x1)] = 1 · x1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[50(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[34(x1)] = 1 · x1
[42(x1)] = 1 · x1
[33(x1)] = 1 · x1
[41(x1)] = 1 · x1
[24(x1)] = 1 · x1
[43(x1)] = 1 · x1
[32(x1)] = 1 · x1
[35(x1)] = 1 · x1
all of the following rules can be deleted.
12(24(43(32(20(02(x1)))))) → 10(04(43(32(22(23(32(x1))))))) (1284)
12(24(43(32(20(00(x1)))))) → 10(04(43(32(22(23(30(x1))))))) (1286)
12(24(43(32(20(05(x1)))))) → 10(04(43(32(22(23(35(x1))))))) (1289)
02(24(43(32(20(02(x1)))))) → 00(04(43(32(22(23(32(x1))))))) (1290)
02(24(43(32(20(00(x1)))))) → 00(04(43(32(22(23(30(x1))))))) (1292)
02(24(43(32(20(05(x1)))))) → 00(04(43(32(22(23(35(x1))))))) (1295)
32(24(43(32(20(02(x1)))))) → 30(04(43(32(22(23(32(x1))))))) (1296)
32(24(43(32(20(00(x1)))))) → 30(04(43(32(22(23(30(x1))))))) (1298)
32(24(43(32(20(05(x1)))))) → 30(04(43(32(22(23(35(x1))))))) (1301)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[25(x1)] = 1 · x1
[51(x1)] = 1 · x1 + 1
[13(x1)] = 1 · x1
[30(x1)] = 1 · x1
[02(x1)] = 1 · x1
[21(x1)] = 1 · x1
[15(x1)] = 1 · x1
[52(x1)] = 1 · x1
[23(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1
[22(x1)] = 1 · x1
[10(x1)] = 1 · x1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[50(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[34(x1)] = 1 · x1
[42(x1)] = 1 · x1
[33(x1)] = 1 · x1
[41(x1)] = 1 · x1
[24(x1)] = 1 · x1
[43(x1)] = 1 · x1
[32(x1)] = 1 · x1
all of the following rules can be deleted.
25(51(13(30(02(x1))))) → 21(15(52(23(30(02(x1)))))) (342)
25(51(13(30(01(x1))))) → 21(15(52(23(30(01(x1)))))) (343)
25(51(13(30(00(x1))))) → 21(15(52(23(30(00(x1)))))) (344)
25(51(13(30(03(x1))))) → 21(15(52(23(30(03(x1)))))) (345)
25(51(13(30(04(x1))))) → 21(15(52(23(30(04(x1)))))) (346)
25(51(13(30(05(x1))))) → 21(15(52(23(30(05(x1)))))) (347)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[22(x1)] = 1 · x1
[21(x1)] = 1 · x1
[10(x1)] = 1 · x1 + 1
[05(x1)] = 1 · x1
[52(x1)] = 1 · x1
[12(x1)] = 1 · x1
[20(x1)] = 1 · x1
[51(x1)] = 1 · x1
[50(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[02(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[34(x1)] = 1 · x1
[42(x1)] = 1 · x1
[33(x1)] = 1 · x1
[41(x1)] = 1 · x1
[24(x1)] = 1 · x1
[43(x1)] = 1 · x1
[30(x1)] = 1 · x1
[32(x1)] = 1 · x1
all of the following rules can be deleted.
22(21(10(05(52(x1))))) → 21(12(22(20(05(52(x1)))))) (378)
22(21(10(05(51(x1))))) → 21(12(22(20(05(51(x1)))))) (379)
22(21(10(05(50(x1))))) → 21(12(22(20(05(50(x1)))))) (380)
22(21(10(05(53(x1))))) → 21(12(22(20(05(53(x1)))))) (381)
22(21(10(05(54(x1))))) → 21(12(22(20(05(54(x1)))))) (382)
22(21(10(05(55(x1))))) → 21(12(22(20(05(55(x1)))))) (383)
22(21(10(02(x1)))) → 21(12(22(20(02(x1))))) (450)
22(21(10(01(x1)))) → 21(12(22(20(01(x1))))) (451)
22(21(10(00(x1)))) → 21(12(22(20(00(x1))))) (452)
22(21(10(03(x1)))) → 21(12(22(20(03(x1))))) (453)
22(21(10(04(x1)))) → 21(12(22(20(04(x1))))) (454)
22(21(10(05(x1)))) → 21(12(22(20(05(x1))))) (455)

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
[34(x1)] = 1 · x1
[42(x1)] = 1 · x1 + 1
[20(x1)] = 1 · x1
[02(x1)] = 1 · x1
[33(x1)] = 1 · x1
[41(x1)] = 1 · x1
[12(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1
[22(x1)] = 1 · x1
[24(x1)] = 1 · x1
[43(x1)] = 1 · x1
[30(x1)] = 1 · x1
[32(x1)] = 1 · x1
[52(x1)] = 1 · x1
[54(x1)] = 1 · x1
all of the following rules can be deleted.
34(42(20(02(x1)))) → 33(34(41(12(20(02(x1)))))) (576)
34(42(20(01(x1)))) → 33(34(41(12(20(01(x1)))))) (577)
34(42(20(00(x1)))) → 33(34(41(12(20(00(x1)))))) (578)
34(42(20(03(x1)))) → 33(34(41(12(20(03(x1)))))) (579)
34(42(20(04(x1)))) → 33(34(41(12(20(04(x1)))))) (580)
34(42(20(05(x1)))) → 33(34(41(12(20(05(x1)))))) (581)

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
[22(x1)] = 1 · x1
[24(x1)] = 1 · x1
[43(x1)] = 1 · x1
[30(x1)] = 1 · x1 + 1
[02(x1)] = 1 · x1
[32(x1)] = 1 · x1
[20(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1
[52(x1)] = 1 · x1
[54(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
22(24(43(30(02(x1))))) → 24(43(32(22(20(02(x1)))))) (1134)
22(24(43(30(01(x1))))) → 24(43(32(22(20(01(x1)))))) (1135)
22(24(43(30(00(x1))))) → 24(43(32(22(20(00(x1)))))) (1136)
22(24(43(30(03(x1))))) → 24(43(32(22(20(03(x1)))))) (1137)
22(24(43(30(04(x1))))) → 24(43(32(22(20(04(x1)))))) (1138)
22(24(43(30(05(x1))))) → 24(43(32(22(20(05(x1)))))) (1139)

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
[52(x1)] = 1 · x1
[24(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[30(x1)] = 1 · x1
[02(x1)] = 1 · x1
[54(x1)] = 1 · x1
[32(x1)] = 1 · x1
[22(x1)] = 1 · x1
[20(x1)] = 1 · x1
[01(x1)] = 1 · x1
[00(x1)] = 1 · x1
[03(x1)] = 1 · x1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1
all of the following rules can be deleted.
52(24(43(30(02(x1))))) → 54(43(32(22(20(02(x1)))))) (1164)
52(24(43(30(01(x1))))) → 54(43(32(22(20(01(x1)))))) (1165)
52(24(43(30(00(x1))))) → 54(43(32(22(20(00(x1)))))) (1166)
52(24(43(30(03(x1))))) → 54(43(32(22(20(03(x1)))))) (1167)
52(24(43(30(04(x1))))) → 54(43(32(22(20(04(x1)))))) (1168)
52(24(43(30(05(x1))))) → 54(43(32(22(20(05(x1)))))) (1169)

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.