Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3385)

The rewrite relation of the following TRS is considered.

0(4(x1)) → 0(1(4(2(3(3(x1)))))) (1)
0(4(x1)) → 0(2(1(4(3(4(x1)))))) (2)
0(0(4(x1))) → 1(1(5(2(3(4(x1)))))) (3)
0(1(1(x1))) → 0(2(2(1(1(1(x1)))))) (4)
0(1(3(x1))) → 0(2(4(3(4(4(x1)))))) (5)
0(2(4(x1))) → 1(5(4(3(4(4(x1)))))) (6)
0(4(0(x1))) → 0(1(2(1(0(3(x1)))))) (7)
1(2(3(x1))) → 5(1(4(1(4(4(x1)))))) (8)
1(3(3(x1))) → 0(2(1(1(0(5(x1)))))) (9)
1(3(3(x1))) → 5(4(0(3(2(3(x1)))))) (10)
1(3(5(x1))) → 1(1(4(3(3(2(x1)))))) (11)
2(0(0(x1))) → 2(4(3(4(4(4(x1)))))) (12)
2(0(1(x1))) → 2(1(5(1(0(1(x1)))))) (13)
2(0(1(x1))) → 2(4(3(5(2(3(x1)))))) (14)
2(0(4(x1))) → 2(0(2(1(4(3(x1)))))) (15)
2(0(4(x1))) → 2(4(1(4(3(1(x1)))))) (16)
3(0(1(x1))) → 3(1(4(3(4(1(x1)))))) (17)
3(0(5(x1))) → 3(1(0(2(3(2(x1)))))) (18)
4(0(0(x1))) → 2(5(2(1(1(1(x1)))))) (19)
4(0(5(x1))) → 4(1(4(5(1(4(x1)))))) (20)
4(0(5(x1))) → 4(2(1(4(3(5(x1)))))) (21)
5(0(2(x1))) → 1(5(2(1(0(2(x1)))))) (22)
5(0(4(x1))) → 1(0(3(2(4(4(x1)))))) (23)
5(0(4(x1))) → 1(5(1(0(3(4(x1)))))) (24)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS
0(4(x1)) → 0(1(4(2(3(3(x1)))))) (1)
0(4(x1)) → 0(2(1(4(3(4(x1)))))) (2)
0(1(1(x1))) → 0(2(2(1(1(1(x1)))))) (4)
0(1(3(x1))) → 0(2(4(3(4(4(x1)))))) (5)
0(4(0(x1))) → 0(1(2(1(0(3(x1)))))) (7)
1(3(5(x1))) → 1(1(4(3(3(2(x1)))))) (11)
2(0(0(x1))) → 2(4(3(4(4(4(x1)))))) (12)
2(0(1(x1))) → 2(1(5(1(0(1(x1)))))) (13)
2(0(1(x1))) → 2(4(3(5(2(3(x1)))))) (14)
2(0(4(x1))) → 2(0(2(1(4(3(x1)))))) (15)
2(0(4(x1))) → 2(4(1(4(3(1(x1)))))) (16)
3(0(1(x1))) → 3(1(4(3(4(1(x1)))))) (17)
3(0(5(x1))) → 3(1(0(2(3(2(x1)))))) (18)
4(0(5(x1))) → 4(1(4(5(1(4(x1)))))) (20)
4(0(5(x1))) → 4(2(1(4(3(5(x1)))))) (21)
0(0(0(4(x1)))) → 0(1(1(5(2(3(4(x1))))))) (25)
4(0(0(4(x1)))) → 4(1(1(5(2(3(4(x1))))))) (26)
1(0(0(4(x1)))) → 1(1(1(5(2(3(4(x1))))))) (27)
2(0(0(4(x1)))) → 2(1(1(5(2(3(4(x1))))))) (28)
3(0(0(4(x1)))) → 3(1(1(5(2(3(4(x1))))))) (29)
5(0(0(4(x1)))) → 5(1(1(5(2(3(4(x1))))))) (30)
0(0(2(4(x1)))) → 0(1(5(4(3(4(4(x1))))))) (31)
4(0(2(4(x1)))) → 4(1(5(4(3(4(4(x1))))))) (32)
1(0(2(4(x1)))) → 1(1(5(4(3(4(4(x1))))))) (33)
2(0(2(4(x1)))) → 2(1(5(4(3(4(4(x1))))))) (34)
3(0(2(4(x1)))) → 3(1(5(4(3(4(4(x1))))))) (35)
5(0(2(4(x1)))) → 5(1(5(4(3(4(4(x1))))))) (36)
0(1(2(3(x1)))) → 0(5(1(4(1(4(4(x1))))))) (37)
4(1(2(3(x1)))) → 4(5(1(4(1(4(4(x1))))))) (38)
1(1(2(3(x1)))) → 1(5(1(4(1(4(4(x1))))))) (39)
2(1(2(3(x1)))) → 2(5(1(4(1(4(4(x1))))))) (40)
3(1(2(3(x1)))) → 3(5(1(4(1(4(4(x1))))))) (41)
5(1(2(3(x1)))) → 5(5(1(4(1(4(4(x1))))))) (42)
0(1(3(3(x1)))) → 0(0(2(1(1(0(5(x1))))))) (43)
4(1(3(3(x1)))) → 4(0(2(1(1(0(5(x1))))))) (44)
1(1(3(3(x1)))) → 1(0(2(1(1(0(5(x1))))))) (45)
2(1(3(3(x1)))) → 2(0(2(1(1(0(5(x1))))))) (46)
3(1(3(3(x1)))) → 3(0(2(1(1(0(5(x1))))))) (47)
5(1(3(3(x1)))) → 5(0(2(1(1(0(5(x1))))))) (48)
0(1(3(3(x1)))) → 0(5(4(0(3(2(3(x1))))))) (49)
4(1(3(3(x1)))) → 4(5(4(0(3(2(3(x1))))))) (50)
1(1(3(3(x1)))) → 1(5(4(0(3(2(3(x1))))))) (51)
2(1(3(3(x1)))) → 2(5(4(0(3(2(3(x1))))))) (52)
3(1(3(3(x1)))) → 3(5(4(0(3(2(3(x1))))))) (53)
5(1(3(3(x1)))) → 5(5(4(0(3(2(3(x1))))))) (54)
0(4(0(0(x1)))) → 0(2(5(2(1(1(1(x1))))))) (55)
4(4(0(0(x1)))) → 4(2(5(2(1(1(1(x1))))))) (56)
1(4(0(0(x1)))) → 1(2(5(2(1(1(1(x1))))))) (57)
2(4(0(0(x1)))) → 2(2(5(2(1(1(1(x1))))))) (58)
3(4(0(0(x1)))) → 3(2(5(2(1(1(1(x1))))))) (59)
5(4(0(0(x1)))) → 5(2(5(2(1(1(1(x1))))))) (60)
0(5(0(2(x1)))) → 0(1(5(2(1(0(2(x1))))))) (61)
4(5(0(2(x1)))) → 4(1(5(2(1(0(2(x1))))))) (62)
1(5(0(2(x1)))) → 1(1(5(2(1(0(2(x1))))))) (63)
2(5(0(2(x1)))) → 2(1(5(2(1(0(2(x1))))))) (64)
3(5(0(2(x1)))) → 3(1(5(2(1(0(2(x1))))))) (65)
5(5(0(2(x1)))) → 5(1(5(2(1(0(2(x1))))))) (66)
0(5(0(4(x1)))) → 0(1(0(3(2(4(4(x1))))))) (67)
4(5(0(4(x1)))) → 4(1(0(3(2(4(4(x1))))))) (68)
1(5(0(4(x1)))) → 1(1(0(3(2(4(4(x1))))))) (69)
2(5(0(4(x1)))) → 2(1(0(3(2(4(4(x1))))))) (70)
3(5(0(4(x1)))) → 3(1(0(3(2(4(4(x1))))))) (71)
5(5(0(4(x1)))) → 5(1(0(3(2(4(4(x1))))))) (72)
0(5(0(4(x1)))) → 0(1(5(1(0(3(4(x1))))))) (73)
4(5(0(4(x1)))) → 4(1(5(1(0(3(4(x1))))))) (74)
1(5(0(4(x1)))) → 1(1(5(1(0(3(4(x1))))))) (75)
2(5(0(4(x1)))) → 2(1(5(1(0(3(4(x1))))))) (76)
3(5(0(4(x1)))) → 3(1(5(1(0(3(4(x1))))))) (77)
5(5(0(4(x1)))) → 5(1(5(1(0(3(4(x1))))))) (78)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1 Rule Removal

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

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

1.1.1.1 Rule Removal

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

1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[01(x1)] = 1 · x1
[13(x1)] = 1 · x1
[33(x1)] = 1 · x1 + 1
[30(x1)] = 1 · x1
[05(x1)] = 1 · x1
[54(x1)] = 1 · x1
[40(x1)] = 1 · x1
[03(x1)] = 1 · x1
[32(x1)] = 1 · x1
[23(x1)] = 1 · x1
[34(x1)] = 1 · x1
[31(x1)] = 1 · x1
[35(x1)] = 1 · x1
[41(x1)] = 1 · x1
[45(x1)] = 1 · x1
[11(x1)] = 1 · x1
[15(x1)] = 1 · x1
[21(x1)] = 1 · x1
[25(x1)] = 1 · x1
[51(x1)] = 1 · x1
[55(x1)] = 1 · x1
[50(x1)] = 1 · x1
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1
[52(x1)] = 1 · x1
[10(x1)] = 1 · x1
[24(x1)] = 1 · x1
[22(x1)] = 1 · x1
[04(x1)] = 1 · x1
[44(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
all of the following rules can be deleted.
01(13(33(30(x1)))) → 05(54(40(03(32(23(30(x1))))))) (313)
01(13(33(34(x1)))) → 05(54(40(03(32(23(34(x1))))))) (314)
01(13(33(31(x1)))) → 05(54(40(03(32(23(31(x1))))))) (315)
01(13(33(32(x1)))) → 05(54(40(03(32(23(32(x1))))))) (316)
01(13(33(33(x1)))) → 05(54(40(03(32(23(33(x1))))))) (317)
01(13(33(35(x1)))) → 05(54(40(03(32(23(35(x1))))))) (318)
41(13(33(30(x1)))) → 45(54(40(03(32(23(30(x1))))))) (319)
41(13(33(34(x1)))) → 45(54(40(03(32(23(34(x1))))))) (320)
41(13(33(31(x1)))) → 45(54(40(03(32(23(31(x1))))))) (321)
41(13(33(32(x1)))) → 45(54(40(03(32(23(32(x1))))))) (322)
41(13(33(33(x1)))) → 45(54(40(03(32(23(33(x1))))))) (323)
41(13(33(35(x1)))) → 45(54(40(03(32(23(35(x1))))))) (324)
11(13(33(30(x1)))) → 15(54(40(03(32(23(30(x1))))))) (325)
11(13(33(34(x1)))) → 15(54(40(03(32(23(34(x1))))))) (326)
11(13(33(31(x1)))) → 15(54(40(03(32(23(31(x1))))))) (327)
11(13(33(32(x1)))) → 15(54(40(03(32(23(32(x1))))))) (328)
11(13(33(33(x1)))) → 15(54(40(03(32(23(33(x1))))))) (329)
11(13(33(35(x1)))) → 15(54(40(03(32(23(35(x1))))))) (330)
21(13(33(30(x1)))) → 25(54(40(03(32(23(30(x1))))))) (331)
21(13(33(34(x1)))) → 25(54(40(03(32(23(34(x1))))))) (332)
21(13(33(31(x1)))) → 25(54(40(03(32(23(31(x1))))))) (333)
21(13(33(32(x1)))) → 25(54(40(03(32(23(32(x1))))))) (334)
21(13(33(33(x1)))) → 25(54(40(03(32(23(33(x1))))))) (335)
21(13(33(35(x1)))) → 25(54(40(03(32(23(35(x1))))))) (336)
31(13(33(30(x1)))) → 35(54(40(03(32(23(30(x1))))))) (337)
31(13(33(34(x1)))) → 35(54(40(03(32(23(34(x1))))))) (338)
31(13(33(31(x1)))) → 35(54(40(03(32(23(31(x1))))))) (339)
31(13(33(32(x1)))) → 35(54(40(03(32(23(32(x1))))))) (340)
31(13(33(33(x1)))) → 35(54(40(03(32(23(33(x1))))))) (341)
31(13(33(35(x1)))) → 35(54(40(03(32(23(35(x1))))))) (342)
51(13(33(30(x1)))) → 55(54(40(03(32(23(30(x1))))))) (343)
51(13(33(34(x1)))) → 55(54(40(03(32(23(34(x1))))))) (344)
51(13(33(31(x1)))) → 55(54(40(03(32(23(31(x1))))))) (345)
51(13(33(32(x1)))) → 55(54(40(03(32(23(32(x1))))))) (346)
51(13(33(33(x1)))) → 55(54(40(03(32(23(33(x1))))))) (347)
51(13(33(35(x1)))) → 55(54(40(03(32(23(35(x1))))))) (348)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[05(x1)] = 1 · x1
[50(x1)] = 1 · x1 + 1
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1
[01(x1)] = 1 · x1
[15(x1)] = 1 · x1
[52(x1)] = 1 · x1
[21(x1)] = 1 · x1
[10(x1)] = 1 · x1
[24(x1)] = 1 · x1
[22(x1)] = 1 · x1
[23(x1)] = 1 · x1
[25(x1)] = 1 · x1
[45(x1)] = 1 · x1
[41(x1)] = 1 · x1
[11(x1)] = 1 · x1
[35(x1)] = 1 · x1
[31(x1)] = 1 · x1
[55(x1)] = 1 · x1
[51(x1)] = 1 · x1
[04(x1)] = 1 · x1
[40(x1)] = 1 · x1
[03(x1)] = 1 · x1
[32(x1)] = 1 · x1 + 1
[44(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
[34(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
05(50(02(20(x1)))) → 01(15(52(21(10(02(20(x1))))))) (385)
05(50(02(24(x1)))) → 01(15(52(21(10(02(24(x1))))))) (386)
05(50(02(21(x1)))) → 01(15(52(21(10(02(21(x1))))))) (387)
05(50(02(22(x1)))) → 01(15(52(21(10(02(22(x1))))))) (388)
05(50(02(23(x1)))) → 01(15(52(21(10(02(23(x1))))))) (389)
05(50(02(25(x1)))) → 01(15(52(21(10(02(25(x1))))))) (390)
45(50(02(20(x1)))) → 41(15(52(21(10(02(20(x1))))))) (391)
45(50(02(24(x1)))) → 41(15(52(21(10(02(24(x1))))))) (392)
45(50(02(21(x1)))) → 41(15(52(21(10(02(21(x1))))))) (393)
45(50(02(22(x1)))) → 41(15(52(21(10(02(22(x1))))))) (394)
45(50(02(23(x1)))) → 41(15(52(21(10(02(23(x1))))))) (395)
45(50(02(25(x1)))) → 41(15(52(21(10(02(25(x1))))))) (396)
15(50(02(20(x1)))) → 11(15(52(21(10(02(20(x1))))))) (397)
15(50(02(24(x1)))) → 11(15(52(21(10(02(24(x1))))))) (398)
15(50(02(21(x1)))) → 11(15(52(21(10(02(21(x1))))))) (399)
15(50(02(22(x1)))) → 11(15(52(21(10(02(22(x1))))))) (400)
15(50(02(23(x1)))) → 11(15(52(21(10(02(23(x1))))))) (401)
15(50(02(25(x1)))) → 11(15(52(21(10(02(25(x1))))))) (402)
25(50(02(20(x1)))) → 21(15(52(21(10(02(20(x1))))))) (403)
25(50(02(24(x1)))) → 21(15(52(21(10(02(24(x1))))))) (404)
25(50(02(21(x1)))) → 21(15(52(21(10(02(21(x1))))))) (405)
25(50(02(22(x1)))) → 21(15(52(21(10(02(22(x1))))))) (406)
25(50(02(23(x1)))) → 21(15(52(21(10(02(23(x1))))))) (407)
25(50(02(25(x1)))) → 21(15(52(21(10(02(25(x1))))))) (408)
35(50(02(20(x1)))) → 31(15(52(21(10(02(20(x1))))))) (409)
35(50(02(24(x1)))) → 31(15(52(21(10(02(24(x1))))))) (410)
35(50(02(21(x1)))) → 31(15(52(21(10(02(21(x1))))))) (411)
35(50(02(22(x1)))) → 31(15(52(21(10(02(22(x1))))))) (412)
35(50(02(23(x1)))) → 31(15(52(21(10(02(23(x1))))))) (413)
35(50(02(25(x1)))) → 31(15(52(21(10(02(25(x1))))))) (414)
55(50(02(20(x1)))) → 51(15(52(21(10(02(20(x1))))))) (415)
55(50(02(24(x1)))) → 51(15(52(21(10(02(24(x1))))))) (416)
55(50(02(21(x1)))) → 51(15(52(21(10(02(21(x1))))))) (417)
55(50(02(22(x1)))) → 51(15(52(21(10(02(22(x1))))))) (418)
55(50(02(23(x1)))) → 51(15(52(21(10(02(23(x1))))))) (419)
55(50(02(25(x1)))) → 51(15(52(21(10(02(25(x1))))))) (420)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[05(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1
[04(x1)] = 1 · x1
[40(x1)] = 1 · x1
[01(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[32(x1)] = 1 · x1
[24(x1)] = 1 · x1
[44(x1)] = 1 · x1
[41(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
[45(x1)] = 1 · x1 + 1
[15(x1)] = 1 · x1 + 1
[11(x1)] = 1 · x1
[25(x1)] = 1 · x1 + 1
[21(x1)] = 1 · x1
[35(x1)] = 1 · x1 + 1
[31(x1)] = 1 · x1
[55(x1)] = 1 · x1 + 1
[51(x1)] = 1 · x1
[34(x1)] = 1 · x1
all of the following rules can be deleted.
05(50(04(40(x1)))) → 01(10(03(32(24(44(40(x1))))))) (421)
05(50(04(44(x1)))) → 01(10(03(32(24(44(44(x1))))))) (422)
05(50(04(41(x1)))) → 01(10(03(32(24(44(41(x1))))))) (423)
05(50(04(42(x1)))) → 01(10(03(32(24(44(42(x1))))))) (424)
05(50(04(43(x1)))) → 01(10(03(32(24(44(43(x1))))))) (425)
05(50(04(45(x1)))) → 01(10(03(32(24(44(45(x1))))))) (426)
45(50(04(40(x1)))) → 41(10(03(32(24(44(40(x1))))))) (427)
45(50(04(44(x1)))) → 41(10(03(32(24(44(44(x1))))))) (428)
45(50(04(41(x1)))) → 41(10(03(32(24(44(41(x1))))))) (429)
45(50(04(42(x1)))) → 41(10(03(32(24(44(42(x1))))))) (430)
45(50(04(43(x1)))) → 41(10(03(32(24(44(43(x1))))))) (431)
45(50(04(45(x1)))) → 41(10(03(32(24(44(45(x1))))))) (432)
15(50(04(40(x1)))) → 11(10(03(32(24(44(40(x1))))))) (433)
15(50(04(44(x1)))) → 11(10(03(32(24(44(44(x1))))))) (434)
15(50(04(41(x1)))) → 11(10(03(32(24(44(41(x1))))))) (435)
15(50(04(42(x1)))) → 11(10(03(32(24(44(42(x1))))))) (436)
15(50(04(43(x1)))) → 11(10(03(32(24(44(43(x1))))))) (437)
15(50(04(45(x1)))) → 11(10(03(32(24(44(45(x1))))))) (438)
25(50(04(40(x1)))) → 21(10(03(32(24(44(40(x1))))))) (439)
25(50(04(44(x1)))) → 21(10(03(32(24(44(44(x1))))))) (440)
25(50(04(41(x1)))) → 21(10(03(32(24(44(41(x1))))))) (441)
25(50(04(42(x1)))) → 21(10(03(32(24(44(42(x1))))))) (442)
25(50(04(43(x1)))) → 21(10(03(32(24(44(43(x1))))))) (443)
25(50(04(45(x1)))) → 21(10(03(32(24(44(45(x1))))))) (444)
35(50(04(40(x1)))) → 31(10(03(32(24(44(40(x1))))))) (445)
35(50(04(44(x1)))) → 31(10(03(32(24(44(44(x1))))))) (446)
35(50(04(41(x1)))) → 31(10(03(32(24(44(41(x1))))))) (447)
35(50(04(42(x1)))) → 31(10(03(32(24(44(42(x1))))))) (448)
35(50(04(43(x1)))) → 31(10(03(32(24(44(43(x1))))))) (449)
35(50(04(45(x1)))) → 31(10(03(32(24(44(45(x1))))))) (450)
55(50(04(40(x1)))) → 51(10(03(32(24(44(40(x1))))))) (451)
55(50(04(44(x1)))) → 51(10(03(32(24(44(44(x1))))))) (452)
55(50(04(41(x1)))) → 51(10(03(32(24(44(41(x1))))))) (453)
55(50(04(42(x1)))) → 51(10(03(32(24(44(42(x1))))))) (454)
55(50(04(43(x1)))) → 51(10(03(32(24(44(43(x1))))))) (455)
55(50(04(45(x1)))) → 51(10(03(32(24(44(45(x1))))))) (456)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[05(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1
[04(x1)] = 1 · x1
[40(x1)] = 1 · x1
[01(x1)] = 1 · x1
[15(x1)] = 1 · x1
[51(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[34(x1)] = 1 · x1
[44(x1)] = 1 · x1
[41(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
[45(x1)] = 1 · x1
[11(x1)] = 1 · x1
[25(x1)] = 1 · x1
[21(x1)] = 1 · x1
[35(x1)] = 1 · x1
[31(x1)] = 1 · x1
[55(x1)] = 1 · x1
all of the following rules can be deleted.
05(50(04(40(x1)))) → 01(15(51(10(03(34(40(x1))))))) (457)
05(50(04(44(x1)))) → 01(15(51(10(03(34(44(x1))))))) (458)
05(50(04(41(x1)))) → 01(15(51(10(03(34(41(x1))))))) (459)
05(50(04(42(x1)))) → 01(15(51(10(03(34(42(x1))))))) (460)
05(50(04(43(x1)))) → 01(15(51(10(03(34(43(x1))))))) (461)
05(50(04(45(x1)))) → 01(15(51(10(03(34(45(x1))))))) (462)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[45(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1
[04(x1)] = 1 · x1
[40(x1)] = 1 · x1
[41(x1)] = 1 · x1
[15(x1)] = 1 · x1
[51(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[34(x1)] = 1 · x1
[44(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
[11(x1)] = 1 · x1
[25(x1)] = 1 · x1
[21(x1)] = 1 · x1
[35(x1)] = 1 · x1
[31(x1)] = 1 · x1
[55(x1)] = 1 · x1
all of the following rules can be deleted.
45(50(04(40(x1)))) → 41(15(51(10(03(34(40(x1))))))) (463)
45(50(04(44(x1)))) → 41(15(51(10(03(34(44(x1))))))) (464)
45(50(04(41(x1)))) → 41(15(51(10(03(34(41(x1))))))) (465)
45(50(04(42(x1)))) → 41(15(51(10(03(34(42(x1))))))) (466)
45(50(04(43(x1)))) → 41(15(51(10(03(34(43(x1))))))) (467)
45(50(04(45(x1)))) → 41(15(51(10(03(34(45(x1))))))) (468)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[15(x1)] = 1 · x1
[50(x1)] = 1 · x1
[04(x1)] = 1 · x1 + 2
[40(x1)] = 1 · x1
[11(x1)] = 1 · x1
[51(x1)] = 1 · x1 + 1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[34(x1)] = 1 · x1
[44(x1)] = 1 · x1
[41(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
[45(x1)] = 1 · x1
[25(x1)] = 1 · x1
[21(x1)] = 1 · x1 + 1
[35(x1)] = 1 · x1
[31(x1)] = 1 · x1 + 1
[55(x1)] = 1 · x1
all of the following rules can be deleted.
15(50(04(40(x1)))) → 11(15(51(10(03(34(40(x1))))))) (469)
15(50(04(44(x1)))) → 11(15(51(10(03(34(44(x1))))))) (470)
15(50(04(41(x1)))) → 11(15(51(10(03(34(41(x1))))))) (471)
15(50(04(42(x1)))) → 11(15(51(10(03(34(42(x1))))))) (472)
15(50(04(43(x1)))) → 11(15(51(10(03(34(43(x1))))))) (473)
15(50(04(45(x1)))) → 11(15(51(10(03(34(45(x1))))))) (474)

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
[25(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1
[04(x1)] = 1 · x1
[40(x1)] = 1 · x1
[21(x1)] = 1 · x1
[15(x1)] = 1 · x1
[51(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[34(x1)] = 1 · x1
[44(x1)] = 1 · x1
[41(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
[45(x1)] = 1 · x1
[35(x1)] = 1 · x1
[31(x1)] = 1 · x1
[55(x1)] = 1 · x1
all of the following rules can be deleted.
25(50(04(40(x1)))) → 21(15(51(10(03(34(40(x1))))))) (475)
25(50(04(44(x1)))) → 21(15(51(10(03(34(44(x1))))))) (476)
25(50(04(41(x1)))) → 21(15(51(10(03(34(41(x1))))))) (477)
25(50(04(42(x1)))) → 21(15(51(10(03(34(42(x1))))))) (478)
25(50(04(43(x1)))) → 21(15(51(10(03(34(43(x1))))))) (479)
25(50(04(45(x1)))) → 21(15(51(10(03(34(45(x1))))))) (480)

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
[35(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1
[04(x1)] = 1 · x1
[40(x1)] = 1 · x1
[31(x1)] = 1 · x1
[15(x1)] = 1 · x1
[51(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[34(x1)] = 1 · x1
[44(x1)] = 1 · x1
[41(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
[45(x1)] = 1 · x1
[55(x1)] = 1 · x1
all of the following rules can be deleted.
35(50(04(40(x1)))) → 31(15(51(10(03(34(40(x1))))))) (481)
35(50(04(44(x1)))) → 31(15(51(10(03(34(44(x1))))))) (482)
35(50(04(41(x1)))) → 31(15(51(10(03(34(41(x1))))))) (483)
35(50(04(42(x1)))) → 31(15(51(10(03(34(42(x1))))))) (484)
35(50(04(43(x1)))) → 31(15(51(10(03(34(43(x1))))))) (485)
35(50(04(45(x1)))) → 31(15(51(10(03(34(45(x1))))))) (486)

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
[55(x1)] = 1 · x1
[50(x1)] = 1 · x1 + 1
[04(x1)] = 1 · x1
[40(x1)] = 1 · x1
[51(x1)] = 1 · x1
[15(x1)] = 1 · x1
[10(x1)] = 1 · x1
[03(x1)] = 1 · x1
[34(x1)] = 1 · x1
[44(x1)] = 1 · x1
[41(x1)] = 1 · x1
[42(x1)] = 1 · x1
[43(x1)] = 1 · x1
[45(x1)] = 1 · x1
all of the following rules can be deleted.
55(50(04(40(x1)))) → 51(15(51(10(03(34(40(x1))))))) (487)
55(50(04(44(x1)))) → 51(15(51(10(03(34(44(x1))))))) (488)
55(50(04(41(x1)))) → 51(15(51(10(03(34(41(x1))))))) (489)
55(50(04(42(x1)))) → 51(15(51(10(03(34(42(x1))))))) (490)
55(50(04(43(x1)))) → 51(15(51(10(03(34(43(x1))))))) (491)
55(50(04(45(x1)))) → 51(15(51(10(03(34(45(x1))))))) (492)

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.