The relative rewrite relation R/S is considered where R is the following TRS
0(0(1(2(x1)))) | → | 3(4(5(4(4(5(3(0(0(3(x1)))))))))) | (1) |
3(2(2(2(x1)))) | → | 0(3(2(4(4(4(1(3(5(3(x1)))))))))) | (2) |
0(2(4(5(2(x1))))) | → | 0(3(4(0(0(0(0(3(1(3(x1)))))))))) | (3) |
1(4(0(5(1(x1))))) | → | 5(4(4(4(5(4(3(3(3(0(x1)))))))))) | (4) |
5(4(1(2(0(x1))))) | → | 0(0(4(4(3(0(4(1(3(0(x1)))))))))) | (5) |
0(3(2(5(3(5(x1)))))) | → | 3(1(3(4(4(3(4(3(3(5(x1)))))))))) | (6) |
0(5(1(1(5(0(x1)))))) | → | 0(0(0(3(1(3(3(1(3(0(x1)))))))))) | (7) |
1(2(5(2(2(3(x1)))))) | → | 0(4(2(4(5(4(3(4(3(3(x1)))))))))) | (8) |
2(0(0(1(2(3(x1)))))) | → | 1(3(3(3(1(3(4(4(4(3(x1)))))))))) | (9) |
2(0(1(3(5(1(x1)))))) | → | 0(0(3(4(5(4(5(3(0(1(x1)))))))))) | (10) |
2(5(5(0(0(1(x1)))))) | → | 4(1(0(3(4(3(1(5(3(0(x1)))))))))) | (11) |
3(0(4(0(3(1(x1)))))) | → | 4(4(4(5(3(0(1(0(3(1(x1)))))))))) | (12) |
3(2(1(5(5(0(x1)))))) | → | 4(1(3(3(4(0(4(3(3(0(x1)))))))))) | (13) |
3(2(4(1(2(2(x1)))))) | → | 4(4(4(5(4(2(0(3(4(2(x1)))))))))) | (14) |
3(2(5(2(2(0(x1)))))) | → | 3(4(4(0(2(1(3(5(3(0(x1)))))))))) | (15) |
3(4(1(2(2(3(x1)))))) | → | 3(5(4(1(4(4(4(4(4(5(x1)))))))))) | (16) |
3(5(2(0(3(5(x1)))))) | → | 3(3(4(3(4(3(4(4(2(5(x1)))))))))) | (17) |
4(0(0(0(1(4(x1)))))) | → | 2(3(0(3(3(4(1(3(1(4(x1)))))))))) | (18) |
4(0(1(3(2(4(x1)))))) | → | 4(1(4(1(3(3(1(4(1(4(x1)))))))))) | (19) |
4(3(0(5(4(4(x1)))))) | → | 4(3(4(5(3(1(4(4(2(4(x1)))))))))) | (20) |
5(1(2(3(5(0(x1)))))) | → | 2(2(4(4(2(4(4(3(3(0(x1)))))))))) | (21) |
5(3(0(1(3(3(x1)))))) | → | 2(4(4(1(4(4(3(1(3(3(x1)))))))))) | (22) |
5(4(5(5(5(3(x1)))))) | → | 3(5(4(4(2(4(3(4(0(3(x1)))))))))) | (23) |
5(5(0(1(5(3(x1)))))) | → | 5(4(4(4(1(3(0(5(4(3(x1)))))))))) | (24) |
5(5(5(0(2(2(x1)))))) | → | 2(4(1(4(3(4(3(4(4(3(x1)))))))))) | (25) |
5(5(5(5(2(3(x1)))))) | → | 3(3(0(4(1(4(2(4(4(3(x1)))))))))) | (26) |
0(2(4(5(2(2(3(x1))))))) | → | 0(5(1(4(4(1(3(1(5(3(x1)))))))))) | (27) |
0(3(0(4(1(5(3(x1))))))) | → | 0(0(3(3(4(4(3(0(0(5(x1)))))))))) | (28) |
0(4(3(4(5(2(2(x1))))))) | → | 0(0(4(5(3(4(2(3(3(2(x1)))))))))) | (29) |
1(3(2(0(2(2(3(x1))))))) | → | 1(3(4(3(5(1(1(1(2(3(x1)))))))))) | (30) |
1(4(5(5(2(2(0(x1))))))) | → | 3(2(1(3(4(4(5(0(3(0(x1)))))))))) | (31) |
1(5(0(2(2(2(4(x1))))))) | → | 0(5(1(3(5(4(3(3(1(4(x1)))))))))) | (32) |
1(5(4(0(2(1(3(x1))))))) | → | 0(1(1(5(3(3(4(4(0(3(x1)))))))))) | (33) |
2(0(1(5(2(0(5(x1))))))) | → | 3(4(0(0(3(1(3(0(2(5(x1)))))))))) | (34) |
2(2(0(0(2(2(4(x1))))))) | → | 2(1(1(4(4(5(4(4(4(4(x1)))))))))) | (35) |
2(3(0(5(0(1(3(x1))))))) | → | 2(3(1(0(5(1(0(3(1(3(x1)))))))))) | (36) |
2(4(0(2(2(5(0(x1))))))) | → | 1(3(0(4(5(4(4(0(3(0(x1)))))))))) | (37) |
2(4(5(0(2(5(0(x1))))))) | → | 4(4(3(1(3(4(0(5(1(1(x1)))))))))) | (38) |
2(5(2(2(5(2(4(x1))))))) | → | 4(3(4(1(3(0(4(0(4(4(x1)))))))))) | (39) |
3(2(0(2(2(2(2(x1))))))) | → | 4(5(3(1(3(2(3(5(0(5(x1)))))))))) | (40) |
3(2(5(5(2(4(5(x1))))))) | → | 3(0(0(0(3(2(4(3(4(5(x1)))))))))) | (41) |
3(2(5(5(3(2(3(x1))))))) | → | 3(1(0(5(0(3(2(4(3(3(x1)))))))))) | (42) |
3(3(5(0(2(2(2(x1))))))) | → | 4(4(3(0(4(3(3(5(3(5(x1)))))))))) | (43) |
3(4(5(2(1(1(2(x1))))))) | → | 3(4(5(3(5(4(4(2(0(5(x1)))))))))) | (44) |
4(0(3(3(1(5(4(x1))))))) | → | 1(3(1(0(0(0(3(4(4(4(x1)))))))))) | (45) |
4(1(2(4(1(2(2(x1))))))) | → | 3(4(5(3(1(1(4(4(0(5(x1)))))))))) | (46) |
5(2(5(2(3(3(2(x1))))))) | → | 4(3(1(0(3(1(3(2(5(3(x1)))))))))) | (47) |
5(3(2(2(3(0(2(x1))))))) | → | 4(5(4(3(3(1(0(5(0(2(x1)))))))))) | (48) |
5(3(2(5(2(5(0(x1))))))) | → | 5(4(2(2(4(4(3(0(3(1(x1)))))))))) | (49) |
5(5(2(2(2(2(0(x1))))))) | → | 0(5(3(5(1(3(1(0(3(0(x1)))))))))) | (50) |
5(5(5(2(1(1(0(x1))))))) | → | 4(2(2(4(5(4(2(3(3(1(x1)))))))))) | (51) |
5(5(5(2(2(0(0(x1))))))) | → | 1(4(0(3(3(4(2(3(3(1(x1)))))))))) | (52) |
and S is the following TRS.
1(2(1(3(3(4(x1)))))) | → | 1(4(2(4(1(3(0(3(2(4(x1)))))))))) | (53) |
4(5(0(0(x1)))) | → | 4(1(0(4(5(4(3(3(0(0(x1)))))))))) | (54) |
1(5(5(0(5(3(4(x1))))))) | → | 5(3(3(5(4(2(3(3(1(4(x1)))))))))) | (55) |
4(3(0(5(x1)))) | → | 3(3(4(3(4(1(3(3(0(5(x1)))))))))) | (56) |
1(3(2(1(2(2(x1)))))) | → | 5(4(4(5(4(3(3(0(2(5(x1)))))))))) | (57) |
1(2(5(4(0(0(x1)))))) | → | 1(5(4(4(5(3(0(3(4(0(x1)))))))))) | (58) |
2(3(3(0(5(3(2(x1))))))) | → | 5(3(1(0(4(1(0(0(0(5(x1)))))))))) | (59) |
4(5(0(2(2(1(x1)))))) | → | 4(3(3(3(5(3(3(1(2(1(x1)))))))))) | (60) |
2(1(0(0(x1)))) | → | 3(0(0(3(5(4(4(5(4(3(x1)))))))))) | (61) |
2(2(2(3(x1)))) | → | 3(5(3(1(4(4(4(2(3(0(x1)))))))))) | (62) |
2(5(4(2(0(x1))))) | → | 3(1(3(0(0(0(0(4(3(0(x1)))))))))) | (63) |
1(5(0(4(1(x1))))) | → | 0(3(3(3(4(5(4(4(4(5(x1)))))))))) | (64) |
0(2(1(4(5(x1))))) | → | 0(3(1(4(0(3(4(4(0(0(x1)))))))))) | (65) |
5(3(5(2(3(0(x1)))))) | → | 5(3(3(4(3(4(4(3(1(3(x1)))))))))) | (66) |
0(5(1(1(5(0(x1)))))) | → | 0(3(1(3(3(1(3(0(0(0(x1)))))))))) | (67) |
3(2(2(5(2(1(x1)))))) | → | 3(3(4(3(4(5(4(2(4(0(x1)))))))))) | (68) |
3(2(1(0(0(2(x1)))))) | → | 3(4(4(4(3(1(3(3(3(1(x1)))))))))) | (69) |
1(5(3(1(0(2(x1)))))) | → | 1(0(3(5(4(5(4(3(0(0(x1)))))))))) | (70) |
1(0(0(5(5(2(x1)))))) | → | 0(3(5(1(3(4(3(0(1(4(x1)))))))))) | (71) |
1(3(0(4(0(3(x1)))))) | → | 1(3(0(1(0(3(5(4(4(4(x1)))))))))) | (72) |
0(5(5(1(2(3(x1)))))) | → | 0(3(3(4(0(4(3(3(1(4(x1)))))))))) | (73) |
2(2(1(4(2(3(x1)))))) | → | 2(4(3(0(2(4(5(4(4(4(x1)))))))))) | (74) |
0(2(2(5(2(3(x1)))))) | → | 0(3(5(3(1(2(0(4(4(3(x1)))))))))) | (75) |
3(2(2(1(4(3(x1)))))) | → | 5(4(4(4(4(4(1(4(5(3(x1)))))))))) | (76) |
5(3(0(2(5(3(x1)))))) | → | 5(2(4(4(3(4(3(4(3(3(x1)))))))))) | (77) |
4(1(0(0(0(4(x1)))))) | → | 4(1(3(1(4(3(3(0(3(2(x1)))))))))) | (78) |
4(2(3(1(0(4(x1)))))) | → | 4(1(4(1(3(3(1(4(1(4(x1)))))))))) | (79) |
4(4(5(0(3(4(x1)))))) | → | 4(2(4(4(1(3(5(4(3(4(x1)))))))))) | (80) |
0(5(3(2(1(5(x1)))))) | → | 0(3(3(4(4(2(4(4(2(2(x1)))))))))) | (81) |
3(3(1(0(3(5(x1)))))) | → | 3(3(1(3(4(4(1(4(4(2(x1)))))))))) | (82) |
3(5(5(5(4(5(x1)))))) | → | 3(0(4(3(4(2(4(4(5(3(x1)))))))))) | (83) |
3(5(1(0(5(5(x1)))))) | → | 3(4(5(0(3(1(4(4(4(5(x1)))))))))) | (84) |
2(2(0(5(5(5(x1)))))) | → | 3(4(4(3(4(3(4(1(4(2(x1)))))))))) | (85) |
3(2(5(5(5(5(x1)))))) | → | 3(4(4(2(4(1(4(0(3(3(x1)))))))))) | (86) |
3(2(2(5(4(2(0(x1))))))) | → | 3(5(1(3(1(4(4(1(5(0(x1)))))))))) | (87) |
3(5(1(4(0(3(0(x1))))))) | → | 5(0(0(3(4(4(3(3(0(0(x1)))))))))) | (88) |
2(2(5(4(3(4(0(x1))))))) | → | 2(3(3(2(4(3(5(4(0(0(x1)))))))))) | (89) |
3(2(2(0(2(3(1(x1))))))) | → | 3(2(1(1(1(5(3(4(3(1(x1)))))))))) | (90) |
0(2(2(5(5(4(1(x1))))))) | → | 0(3(0(5(4(4(3(1(2(3(x1)))))))))) | (91) |
4(2(2(2(0(5(1(x1))))))) | → | 4(1(3(3(4(5(3(1(5(0(x1)))))))))) | (92) |
3(1(2(0(4(5(1(x1))))))) | → | 3(0(4(4(3(3(5(1(1(0(x1)))))))))) | (93) |
5(0(2(5(1(0(2(x1))))))) | → | 5(2(0(3(1(3(0(0(4(3(x1)))))))))) | (94) |
4(2(2(0(0(2(2(x1))))))) | → | 4(4(4(4(5(4(4(1(1(2(x1)))))))))) | (95) |
3(1(0(5(0(3(2(x1))))))) | → | 3(1(3(0(1(5(0(1(3(2(x1)))))))))) | (96) |
0(5(2(2(0(4(2(x1))))))) | → | 0(3(0(4(4(5(4(0(3(1(x1)))))))))) | (97) |
0(5(2(0(5(4(2(x1))))))) | → | 1(1(5(0(4(3(1(3(4(4(x1)))))))))) | (98) |
4(2(5(2(2(5(2(x1))))))) | → | 4(4(0(4(0(3(1(4(3(4(x1)))))))))) | (99) |
2(2(2(2(0(2(3(x1))))))) | → | 5(0(5(3(2(3(1(3(5(4(x1)))))))))) | (100) |
5(4(2(5(5(2(3(x1))))))) | → | 5(4(3(4(2(3(0(0(0(3(x1)))))))))) | (101) |
3(2(3(5(5(2(3(x1))))))) | → | 3(3(4(2(3(0(5(0(1(3(x1)))))))))) | (102) |
2(2(2(0(5(3(3(x1))))))) | → | 5(3(5(3(3(4(0(3(4(4(x1)))))))))) | (103) |
2(1(1(2(5(4(3(x1))))))) | → | 5(0(2(4(4(5(3(5(4(3(x1)))))))))) | (104) |
4(5(1(3(3(0(4(x1))))))) | → | 4(4(4(3(0(0(0(1(3(1(x1)))))))))) | (105) |
2(2(1(4(2(1(4(x1))))))) | → | 5(0(4(4(1(1(3(5(4(3(x1)))))))))) | (106) |
2(3(3(2(5(2(5(x1))))))) | → | 3(5(2(3(1(3(0(1(3(4(x1)))))))))) | (107) |
2(0(3(2(2(3(5(x1))))))) | → | 2(0(5(0(1(3(3(4(5(4(x1)))))))))) | (108) |
0(5(2(5(2(3(5(x1))))))) | → | 1(3(0(3(4(4(2(2(4(5(x1)))))))))) | (109) |
0(2(2(2(2(5(5(x1))))))) | → | 0(3(0(1(3(1(5(3(5(0(x1)))))))))) | (110) |
0(1(1(2(5(5(5(x1))))))) | → | 1(3(3(2(4(5(4(2(2(4(x1)))))))))) | (111) |
0(0(2(2(5(5(5(x1))))))) | → | 1(3(3(2(4(3(3(0(4(1(x1)))))))))) | (112) |
4(3(3(1(2(1(x1)))))) | → | 4(2(3(0(3(1(4(2(4(1(x1)))))))))) | (113) |
0(0(5(4(x1)))) | → | 0(0(3(3(4(5(4(0(1(4(x1)))))))))) | (114) |
4(3(5(0(5(5(1(x1))))))) | → | 4(1(3(3(2(4(5(3(3(5(x1)))))))))) | (115) |
5(0(3(4(x1)))) | → | 5(0(3(3(1(4(3(4(3(3(x1)))))))))) | (116) |
2(2(1(2(3(1(x1)))))) | → | 5(2(0(3(3(4(5(4(4(5(x1)))))))))) | (117) |
0(0(4(5(2(1(x1)))))) | → | 0(4(3(0(3(5(4(4(5(1(x1)))))))))) | (118) |
2(3(5(0(3(3(2(x1))))))) | → | 5(0(0(0(1(4(0(1(3(5(x1)))))))))) | (119) |
1(2(2(0(5(4(x1)))))) | → | 1(2(1(3(3(5(3(3(3(4(x1)))))))))) | (120) |
{2(☐), 1(☐), 0(☐), 3(☐), 5(☐), 4(☐)}
We obtain the transformed TRSThere are 155 ruless (increase limit for explicit display).
Root-labeling is applied.
We obtain the labeled TRSThere are 930 ruless (increase limit for explicit display).
[02(x1)] | = | 1 + 1 · x1 |
[21(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 + 1 · x1 |
[51(x1)] | = | 1 + 1 · x1 |
[01(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[55(x1)] | = | 1 + 1 · x1 |
[05(x1)] | = | 1 + 1 · x1 |
[53(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 + 1 · x1 |
[30(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 + 1 · x1 |
[22(x1)] | = | 1 + 1 · x1 |
[25(x1)] | = | 1 + 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[42(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 + 1 · x1 |
[20(x1)] | = | 1 + 1 · x1 |
[41(x1)] | = | 1 · x1 |
There are 808 ruless (increase limit for explicit display).
[02(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 + 1 · x1 |
[14(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 + 1 · x1 |
[54(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[34(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 + 1 · x1 |
[15(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 + 1 · x1 |
[20(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 + 1 · x1 |
[12(x1)] | = | 1 + 1 · x1 |
[51(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 + 1 · x1 |
[55(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
13(30(04(40(03(32(x1)))))) | → | 13(30(01(10(03(35(54(44(44(42(x1)))))))))) | (272) |
13(30(04(40(03(31(x1)))))) | → | 13(30(01(10(03(35(54(44(44(41(x1)))))))))) | (273) |
13(30(04(40(03(34(x1)))))) | → | 13(30(01(10(03(35(54(44(44(44(x1)))))))))) | (274) |
13(30(04(40(03(33(x1)))))) | → | 13(30(01(10(03(35(54(44(44(43(x1)))))))))) | (276) |
44(45(50(03(34(40(x1)))))) | → | 42(24(44(41(13(35(54(43(34(40(x1)))))))))) | (313) |
44(45(50(03(34(42(x1)))))) | → | 42(24(44(41(13(35(54(43(34(42(x1)))))))))) | (314) |
44(45(50(03(34(41(x1)))))) | → | 42(24(44(41(13(35(54(43(34(41(x1)))))))))) | (315) |
44(45(50(03(34(44(x1)))))) | → | 42(24(44(41(13(35(54(43(34(44(x1)))))))))) | (316) |
44(45(50(03(34(45(x1)))))) | → | 42(24(44(41(13(35(54(43(34(45(x1)))))))))) | (317) |
44(45(50(03(34(43(x1)))))) | → | 42(24(44(41(13(35(54(43(34(43(x1)))))))))) | (318) |
05(53(32(21(15(50(x1)))))) | → | 03(33(34(44(42(24(44(42(22(20(x1)))))))))) | (319) |
05(53(32(21(15(53(x1)))))) | → | 03(33(34(44(42(24(44(42(22(23(x1)))))))))) | (324) |
31(12(20(04(45(51(14(x1))))))) | → | 30(04(44(43(33(35(51(11(10(04(x1)))))))))) | (382) |
53(32(22(21(14(43(30(x1))))))) | → | 55(54(44(44(44(44(41(14(45(53(30(x1))))))))))) | (649) |
53(32(22(21(14(43(32(x1))))))) | → | 55(54(44(44(44(44(41(14(45(53(32(x1))))))))))) | (650) |
53(32(22(21(14(43(31(x1))))))) | → | 55(54(44(44(44(44(41(14(45(53(31(x1))))))))))) | (651) |
53(32(22(21(14(43(34(x1))))))) | → | 55(54(44(44(44(44(41(14(45(53(34(x1))))))))))) | (652) |
53(32(22(21(14(43(35(x1))))))) | → | 55(54(44(44(44(44(41(14(45(53(35(x1))))))))))) | (653) |
53(32(22(21(14(43(33(x1))))))) | → | 55(54(44(44(44(44(41(14(45(53(33(x1))))))))))) | (654) |
13(35(51(14(40(03(30(00(x1)))))))) | → | 15(50(00(03(34(44(43(33(30(00(00(x1))))))))))) | (703) |
13(35(51(14(40(03(30(02(x1)))))))) | → | 15(50(00(03(34(44(43(33(30(00(02(x1))))))))))) | (704) |
13(35(51(14(40(03(30(01(x1)))))))) | → | 15(50(00(03(34(44(43(33(30(00(01(x1))))))))))) | (705) |
13(35(51(14(40(03(30(04(x1)))))))) | → | 15(50(00(03(34(44(43(33(30(00(04(x1))))))))))) | (706) |
13(35(51(14(40(03(30(05(x1)))))))) | → | 15(50(00(03(34(44(43(33(30(00(05(x1))))))))))) | (707) |
13(35(51(14(40(03(30(03(x1)))))))) | → | 15(50(00(03(34(44(43(33(30(00(03(x1))))))))))) | (708) |
03(35(51(14(40(03(30(00(x1)))))))) | → | 05(50(00(03(34(44(43(33(30(00(00(x1))))))))))) | (709) |
03(35(51(14(40(03(30(02(x1)))))))) | → | 05(50(00(03(34(44(43(33(30(00(02(x1))))))))))) | (710) |
03(35(51(14(40(03(30(01(x1)))))))) | → | 05(50(00(03(34(44(43(33(30(00(01(x1))))))))))) | (711) |
03(35(51(14(40(03(30(04(x1)))))))) | → | 05(50(00(03(34(44(43(33(30(00(04(x1))))))))))) | (712) |
03(35(51(14(40(03(30(05(x1)))))))) | → | 05(50(00(03(34(44(43(33(30(00(05(x1))))))))))) | (713) |
03(35(51(14(40(03(30(03(x1)))))))) | → | 05(50(00(03(34(44(43(33(30(00(03(x1))))))))))) | (714) |
53(35(51(14(40(03(30(00(x1)))))))) | → | 55(50(00(03(34(44(43(33(30(00(00(x1))))))))))) | (721) |
53(35(51(14(40(03(30(02(x1)))))))) | → | 55(50(00(03(34(44(43(33(30(00(02(x1))))))))))) | (722) |
53(35(51(14(40(03(30(01(x1)))))))) | → | 55(50(00(03(34(44(43(33(30(00(01(x1))))))))))) | (723) |
53(35(51(14(40(03(30(04(x1)))))))) | → | 55(50(00(03(34(44(43(33(30(00(04(x1))))))))))) | (724) |
53(35(51(14(40(03(30(05(x1)))))))) | → | 55(50(00(03(34(44(43(33(30(00(05(x1))))))))))) | (725) |
53(35(51(14(40(03(30(03(x1)))))))) | → | 55(50(00(03(34(44(43(33(30(00(03(x1))))))))))) | (726) |
22(22(21(14(42(21(14(40(x1)))))))) | → | 25(50(04(44(41(11(13(35(54(43(30(x1))))))))))) | (877) |
22(22(21(14(42(21(14(42(x1)))))))) | → | 25(50(04(44(41(11(13(35(54(43(32(x1))))))))))) | (878) |
22(22(21(14(42(21(14(41(x1)))))))) | → | 25(50(04(44(41(11(13(35(54(43(31(x1))))))))))) | (879) |
22(22(21(14(42(21(14(44(x1)))))))) | → | 25(50(04(44(41(11(13(35(54(43(34(x1))))))))))) | (880) |
22(22(21(14(42(21(14(45(x1)))))))) | → | 25(50(04(44(41(11(13(35(54(43(35(x1))))))))))) | (881) |
22(22(21(14(42(21(14(43(x1)))))))) | → | 25(50(04(44(41(11(13(35(54(43(33(x1))))))))))) | (882) |
12(22(21(14(42(21(14(40(x1)))))))) | → | 15(50(04(44(41(11(13(35(54(43(30(x1))))))))))) | (883) |
12(22(21(14(42(21(14(42(x1)))))))) | → | 15(50(04(44(41(11(13(35(54(43(32(x1))))))))))) | (884) |
12(22(21(14(42(21(14(41(x1)))))))) | → | 15(50(04(44(41(11(13(35(54(43(31(x1))))))))))) | (885) |
12(22(21(14(42(21(14(44(x1)))))))) | → | 15(50(04(44(41(11(13(35(54(43(34(x1))))))))))) | (886) |
12(22(21(14(42(21(14(45(x1)))))))) | → | 15(50(04(44(41(11(13(35(54(43(35(x1))))))))))) | (887) |
12(22(21(14(42(21(14(43(x1)))))))) | → | 15(50(04(44(41(11(13(35(54(43(33(x1))))))))))) | (888) |
02(22(21(14(42(21(14(40(x1)))))))) | → | 05(50(04(44(41(11(13(35(54(43(30(x1))))))))))) | (889) |
02(22(21(14(42(21(14(42(x1)))))))) | → | 05(50(04(44(41(11(13(35(54(43(32(x1))))))))))) | (890) |
02(22(21(14(42(21(14(41(x1)))))))) | → | 05(50(04(44(41(11(13(35(54(43(31(x1))))))))))) | (891) |
02(22(21(14(42(21(14(44(x1)))))))) | → | 05(50(04(44(41(11(13(35(54(43(34(x1))))))))))) | (892) |
02(22(21(14(42(21(14(45(x1)))))))) | → | 05(50(04(44(41(11(13(35(54(43(35(x1))))))))))) | (893) |
02(22(21(14(42(21(14(43(x1)))))))) | → | 05(50(04(44(41(11(13(35(54(43(33(x1))))))))))) | (894) |
32(22(21(14(42(21(14(40(x1)))))))) | → | 35(50(04(44(41(11(13(35(54(43(30(x1))))))))))) | (895) |
32(22(21(14(42(21(14(42(x1)))))))) | → | 35(50(04(44(41(11(13(35(54(43(32(x1))))))))))) | (896) |
32(22(21(14(42(21(14(41(x1)))))))) | → | 35(50(04(44(41(11(13(35(54(43(31(x1))))))))))) | (897) |
32(22(21(14(42(21(14(44(x1)))))))) | → | 35(50(04(44(41(11(13(35(54(43(34(x1))))))))))) | (898) |
32(22(21(14(42(21(14(45(x1)))))))) | → | 35(50(04(44(41(11(13(35(54(43(35(x1))))))))))) | (899) |
32(22(21(14(42(21(14(43(x1)))))))) | → | 35(50(04(44(41(11(13(35(54(43(33(x1))))))))))) | (900) |
52(22(21(14(42(21(14(40(x1)))))))) | → | 55(50(04(44(41(11(13(35(54(43(30(x1))))))))))) | (901) |
52(22(21(14(42(21(14(42(x1)))))))) | → | 55(50(04(44(41(11(13(35(54(43(32(x1))))))))))) | (902) |
52(22(21(14(42(21(14(41(x1)))))))) | → | 55(50(04(44(41(11(13(35(54(43(31(x1))))))))))) | (903) |
52(22(21(14(42(21(14(44(x1)))))))) | → | 55(50(04(44(41(11(13(35(54(43(34(x1))))))))))) | (904) |
52(22(21(14(42(21(14(45(x1)))))))) | → | 55(50(04(44(41(11(13(35(54(43(35(x1))))))))))) | (905) |
52(22(21(14(42(21(14(43(x1)))))))) | → | 55(50(04(44(41(11(13(35(54(43(33(x1))))))))))) | (906) |
42(22(21(14(42(21(14(40(x1)))))))) | → | 45(50(04(44(41(11(13(35(54(43(30(x1))))))))))) | (907) |
42(22(21(14(42(21(14(42(x1)))))))) | → | 45(50(04(44(41(11(13(35(54(43(32(x1))))))))))) | (908) |
42(22(21(14(42(21(14(41(x1)))))))) | → | 45(50(04(44(41(11(13(35(54(43(31(x1))))))))))) | (909) |
42(22(21(14(42(21(14(44(x1)))))))) | → | 45(50(04(44(41(11(13(35(54(43(34(x1))))))))))) | (910) |
42(22(21(14(42(21(14(45(x1)))))))) | → | 45(50(04(44(41(11(13(35(54(43(35(x1))))))))))) | (911) |
42(22(21(14(42(21(14(43(x1)))))))) | → | 45(50(04(44(41(11(13(35(54(43(33(x1))))))))))) | (912) |
43(33(31(12(21(10(x1)))))) | → | 42(23(30(03(31(14(42(24(41(10(x1)))))))))) | (1057) |
43(33(31(12(21(12(x1)))))) | → | 42(23(30(03(31(14(42(24(41(12(x1)))))))))) | (1058) |
43(33(31(12(21(11(x1)))))) | → | 42(23(30(03(31(14(42(24(41(11(x1)))))))))) | (1059) |
43(33(31(12(21(14(x1)))))) | → | 42(23(30(03(31(14(42(24(41(14(x1)))))))))) | (1060) |
43(33(31(12(21(15(x1)))))) | → | 42(23(30(03(31(14(42(24(41(15(x1)))))))))) | (1061) |
43(33(31(12(21(13(x1)))))) | → | 42(23(30(03(31(14(42(24(41(13(x1)))))))))) | (1062) |
50(03(34(40(x1)))) | → | 50(03(33(31(14(43(34(43(33(30(x1)))))))))) | (1075) |
50(03(34(45(x1)))) | → | 50(03(33(31(14(43(34(43(33(35(x1)))))))))) | (1079) |
00(04(45(52(21(10(x1)))))) | → | 04(43(30(03(35(54(44(45(51(10(x1)))))))))) | (1081) |
00(04(45(52(21(12(x1)))))) | → | 04(43(30(03(35(54(44(45(51(12(x1)))))))))) | (1082) |
00(04(45(52(21(11(x1)))))) | → | 04(43(30(03(35(54(44(45(51(11(x1)))))))))) | (1083) |
00(04(45(52(21(14(x1)))))) | → | 04(43(30(03(35(54(44(45(51(14(x1)))))))))) | (1084) |
00(04(45(52(21(15(x1)))))) | → | 04(43(30(03(35(54(44(45(51(15(x1)))))))))) | (1085) |
00(04(45(52(21(13(x1)))))) | → | 04(43(30(03(35(54(44(45(51(13(x1)))))))))) | (1086) |
22(22(21(12(23(31(11(x1))))))) | → | 25(52(20(03(33(34(45(54(44(45(51(x1))))))))))) | (1095) |
12(22(21(12(23(31(11(x1))))))) | → | 15(52(20(03(33(34(45(54(44(45(51(x1))))))))))) | (1101) |
02(22(21(12(23(31(11(x1))))))) | → | 05(52(20(03(33(34(45(54(44(45(51(x1))))))))))) | (1107) |
32(22(21(12(23(31(11(x1))))))) | → | 35(52(20(03(33(34(45(54(44(45(51(x1))))))))))) | (1113) |
52(22(21(12(23(31(11(x1))))))) | → | 55(52(20(03(33(34(45(54(44(45(51(x1))))))))))) | (1119) |
42(22(21(12(23(31(11(x1))))))) | → | 45(52(20(03(33(34(45(54(44(45(51(x1))))))))))) | (1125) |
22(23(35(50(03(33(32(21(x1)))))))) | → | 25(50(00(00(01(14(40(01(13(35(51(x1))))))))))) | (1131) |
12(23(35(50(03(33(32(21(x1)))))))) | → | 15(50(00(00(01(14(40(01(13(35(51(x1))))))))))) | (1137) |
02(23(35(50(03(33(32(21(x1)))))))) | → | 05(50(00(00(01(14(40(01(13(35(51(x1))))))))))) | (1143) |
32(23(35(50(03(33(32(21(x1)))))))) | → | 35(50(00(00(01(14(40(01(13(35(51(x1))))))))))) | (1149) |
52(23(35(50(03(33(32(21(x1)))))))) | → | 55(50(00(00(01(14(40(01(13(35(51(x1))))))))))) | (1155) |
[02(x1)] | = | 1 + 1 · x1 |
[21(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 + 1 · x1 |
[01(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[35(x1)] | = | 1 + 1 · x1 |
[33(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 + 1 · x1 |
[42(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 + 1 · x1 |
[15(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 + 1 · x1 |
[51(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 + 1 · x1 |
[43(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 · x1 |
33(31(10(03(35(50(x1)))))) | → | 33(31(13(34(44(41(14(44(42(20(x1)))))))))) | (325) |
21(15(50(04(41(11(x1)))))) | → | 20(03(33(33(34(45(54(44(44(45(51(x1))))))))))) | (555) |
11(15(50(04(41(11(x1)))))) | → | 10(03(33(33(34(45(54(44(44(45(51(x1))))))))))) | (561) |
50(03(34(41(x1)))) | → | 50(03(33(31(14(43(34(43(33(31(x1)))))))))) | (1077) |
42(23(35(50(03(33(32(21(x1)))))))) | → | 45(50(00(00(01(14(40(01(13(35(51(x1))))))))))) | (1161) |
[02(x1)] | = | 1 + 1 · x1 |
[21(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 + 1 · x1 |
[01(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[35(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 + 1 · x1 |
[43(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
13(30(04(40(03(30(x1)))))) | → | 13(30(01(10(03(35(54(44(44(40(x1)))))))))) | (271) |
33(31(10(03(35(53(x1)))))) | → | 33(31(13(34(44(41(14(44(42(23(x1)))))))))) | (330) |
13(32(22(21(14(43(30(x1))))))) | → | 15(54(44(44(44(44(41(14(45(53(30(x1))))))))))) | (631) |
13(32(22(21(14(43(32(x1))))))) | → | 15(54(44(44(44(44(41(14(45(53(32(x1))))))))))) | (632) |
13(32(22(21(14(43(31(x1))))))) | → | 15(54(44(44(44(44(41(14(45(53(31(x1))))))))))) | (633) |
13(32(22(21(14(43(34(x1))))))) | → | 15(54(44(44(44(44(41(14(45(53(34(x1))))))))))) | (634) |
13(32(22(21(14(43(35(x1))))))) | → | 15(54(44(44(44(44(41(14(45(53(35(x1))))))))))) | (635) |
13(32(22(21(14(43(33(x1))))))) | → | 15(54(44(44(44(44(41(14(45(53(33(x1))))))))))) | (636) |
03(32(22(21(14(43(30(x1))))))) | → | 05(54(44(44(44(44(41(14(45(53(30(x1))))))))))) | (637) |
03(32(22(21(14(43(32(x1))))))) | → | 05(54(44(44(44(44(41(14(45(53(32(x1))))))))))) | (638) |
03(32(22(21(14(43(31(x1))))))) | → | 05(54(44(44(44(44(41(14(45(53(31(x1))))))))))) | (639) |
03(32(22(21(14(43(34(x1))))))) | → | 05(54(44(44(44(44(41(14(45(53(34(x1))))))))))) | (640) |
03(32(22(21(14(43(35(x1))))))) | → | 05(54(44(44(44(44(41(14(45(53(35(x1))))))))))) | (641) |
03(32(22(21(14(43(33(x1))))))) | → | 05(54(44(44(44(44(41(14(45(53(33(x1))))))))))) | (642) |
[02(x1)] | = | 1 + 1 · x1 |
[21(x1)] | = | 1 + 1 · x1 |
[14(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 + 1 · x1 |
[33(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 + 1 · x1 |
02(21(14(45(54(x1))))) | → | 03(31(14(40(03(34(44(40(00(04(x1)))))))))) | (238) |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[03(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 + 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[54(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 + 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
50(03(34(42(x1)))) | → | 50(03(33(31(14(43(34(43(33(32(x1)))))))))) | (1076) |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[03(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
13(30(04(40(03(35(x1)))))) | → | 13(30(01(10(03(35(54(44(44(45(x1)))))))))) | (275) |
There are no rules in the TRS. Hence, it is terminating.