The relative rewrite relation R/S is considered where R is the following TRS
0(1(1(2(x1)))) | → | 0(1(3(4(2(2(4(2(2(2(x1)))))))))) | (1) |
4(0(1(4(x1)))) | → | 4(2(3(1(1(3(3(3(2(4(x1)))))))))) | (2) |
3(5(0(4(5(x1))))) | → | 0(3(3(3(1(3(1(1(3(4(x1)))))))))) | (3) |
0(2(0(4(0(3(x1)))))) | → | 0(2(2(3(4(2(2(3(1(1(x1)))))))))) | (4) |
0(4(0(1(1(2(x1)))))) | → | 0(0(4(2(4(2(4(2(3(2(x1)))))))))) | (5) |
0(4(3(2(3(5(x1)))))) | → | 5(5(0(5(2(1(2(2(4(5(x1)))))))))) | (6) |
0(4(4(4(0(4(x1)))))) | → | 0(5(4(5(3(4(1(4(2(4(x1)))))))))) | (7) |
1(1(5(0(1(2(x1)))))) | → | 2(2(2(2(5(0(5(4(5(2(x1)))))))))) | (8) |
1(2(3(2(0(3(x1)))))) | → | 2(4(3(1(3(3(3(1(3(1(x1)))))))))) | (9) |
2(0(3(0(2(3(x1)))))) | → | 2(4(1(0(0(0(5(0(2(3(x1)))))))))) | (10) |
2(1(4(4(3(2(x1)))))) | → | 2(2(3(3(4(1(4(2(3(2(x1)))))))))) | (11) |
3(3(0(3(5(4(x1)))))) | → | 3(3(4(2(2(2(4(1(5(4(x1)))))))))) | (12) |
3(3(5(4(3(1(x1)))))) | → | 3(2(4(2(1(5(1(3(1(3(x1)))))))))) | (13) |
3(5(1(5(1(2(x1)))))) | → | 3(4(2(2(1(1(4(3(2(2(x1)))))))))) | (14) |
3(5(3(1(1(0(x1)))))) | → | 4(1(4(2(1(2(3(1(3(0(x1)))))))))) | (15) |
4(1(0(4(4(2(x1)))))) | → | 4(2(3(2(3(3(1(4(2(2(x1)))))))))) | (16) |
4(3(2(0(3(3(x1)))))) | → | 1(5(3(4(1(3(1(1(3(1(x1)))))))))) | (17) |
4(5(3(2(0(2(x1)))))) | → | 4(2(1(2(1(2(5(1(3(1(x1)))))))))) | (18) |
0(1(1(2(0(3(2(x1))))))) | → | 0(2(2(0(5(2(4(1(3(2(x1)))))))))) | (19) |
0(3(0(2(5(1(3(x1))))))) | → | 5(5(0(5(4(1(1(3(2(3(x1)))))))))) | (20) |
0(3(0(3(0(5(4(x1))))))) | → | 0(2(0(0(5(3(3(3(3(4(x1)))))))))) | (21) |
0(3(5(1(1(3(0(x1))))))) | → | 5(5(0(5(5(1(4(1(1(0(x1)))))))))) | (22) |
0(4(0(1(2(5(3(x1))))))) | → | 0(5(2(1(3(3(3(3(4(1(x1)))))))))) | (23) |
0(5(0(4(3(4(5(x1))))))) | → | 0(5(2(0(5(4(2(2(3(5(x1)))))))))) | (24) |
1(2(0(3(2(5(4(x1))))))) | → | 1(1(5(5(0(0(2(1(2(4(x1)))))))))) | (25) |
1(3(0(0(1(1(5(x1))))))) | → | 1(1(4(2(2(5(5(2(5(5(x1)))))))))) | (26) |
1(3(4(0(4(0(2(x1))))))) | → | 3(4(4(1(4(2(5(2(2(2(x1)))))))))) | (27) |
1(5(1(5(2(3(2(x1))))))) | → | 5(2(0(2(3(3(1(1(1(2(x1)))))))))) | (28) |
1(5(2(3(0(5(0(x1))))))) | → | 1(5(2(4(2(4(2(1(3(0(x1)))))))))) | (29) |
1(5(3(2(5(3(5(x1))))))) | → | 2(4(4(3(5(2(2(0(0(5(x1)))))))))) | (30) |
1(5(4(4(5(3(2(x1))))))) | → | 1(2(0(5(2(2(2(0(5(2(x1)))))))))) | (31) |
2(0(3(0(5(4(4(x1))))))) | → | 2(5(2(2(1(1(0(3(3(1(x1)))))))))) | (32) |
2(0(3(4(4(4(4(x1))))))) | → | 5(2(2(2(3(1(3(4(3(4(x1)))))))))) | (33) |
2(3(0(2(0(3(4(x1))))))) | → | 2(3(5(0(0(0(1(4(2(1(x1)))))))))) | (34) |
2(3(5(1(0(0(5(x1))))))) | → | 1(2(0(0(0(5(0(5(2(2(x1)))))))))) | (35) |
3(0(2(3(0(5(4(x1))))))) | → | 2(2(3(0(0(0(5(2(2(4(x1)))))))))) | (36) |
3(0(3(2(0(1(2(x1))))))) | → | 1(3(5(2(4(3(4(2(1(2(x1)))))))))) | (37) |
3(0(4(4(4(0(2(x1))))))) | → | 3(1(3(3(1(1(2(2(2(2(x1)))))))))) | (38) |
3(2(0(1(3(3(0(x1))))))) | → | 2(2(5(0(2(4(2(1(2(0(x1)))))))))) | (39) |
3(4(3(0(4(4(0(x1))))))) | → | 3(4(2(2(1(2(0(3(4(0(x1)))))))))) | (40) |
3(4(4(4(4(3(5(x1))))))) | → | 3(3(4(5(1(4(2(1(1(5(x1)))))))))) | (41) |
3(5(0(0(3(2(4(x1))))))) | → | 2(1(0(0(0(5(5(5(3(4(x1)))))))))) | (42) |
3(5(4(0(3(3(4(x1))))))) | → | 1(3(1(3(3(2(2(4(2(1(x1)))))))))) | (43) |
4(2(0(1(1(3(0(x1))))))) | → | 4(2(5(2(2(3(1(4(2(0(x1)))))))))) | (44) |
4(4(4(5(3(4(0(x1))))))) | → | 1(5(2(4(2(4(2(4(0(0(x1)))))))))) | (45) |
4(4(5(5(3(2(4(x1))))))) | → | 5(2(1(4(5(4(2(1(2(1(x1)))))))))) | (46) |
4(5(0(3(0(3(0(x1))))))) | → | 4(1(4(1(0(0(0(2(5(1(x1)))))))))) | (47) |
4(5(0(4(3(0(0(x1))))))) | → | 4(2(2(1(1(3(3(0(1(0(x1)))))))))) | (48) |
5(3(1(1(3(5(3(x1))))))) | → | 0(0(5(5(4(2(4(2(4(1(x1)))))))))) | (49) |
5(3(2(2(0(1(3(x1))))))) | → | 0(0(5(5(5(5(3(3(3(1(x1)))))))))) | (50) |
5(4(1(0(4(2(0(x1))))))) | → | 5(1(0(0(0(1(4(2(4(1(x1)))))))))) | (51) |
and S is the following TRS.
0(3(4(4(5(x1))))) | → | 0(2(2(2(1(2(4(2(4(5(x1)))))))))) | (52) |
5(5(3(5(3(4(5(x1))))))) | → | 5(0(1(4(2(4(5(1(4(5(x1)))))))))) | (53) |
5(1(4(1(5(2(x1)))))) | → | 5(2(2(4(2(2(1(0(5(2(x1)))))))))) | (54) |
3(0(5(4(x1)))) | → | 5(2(2(2(5(2(2(0(5(4(x1)))))))))) | (55) |
3(2(3(0(3(x1))))) | → | 3(4(3(3(4(2(1(1(3(1(x1)))))))))) | (56) |
3(2(5(4(4(5(0(x1))))))) | → | 3(2(0(0(0(0(5(3(4(0(x1)))))))))) | (57) |
4(4(1(2(0(4(x1)))))) | → | 5(5(4(3(4(2(3(1(3(1(x1)))))))))) | (58) |
1(1(3(5(4(5(0(x1))))))) | → | 3(2(2(4(2(1(4(1(0(0(x1)))))))))) | (59) |
3(4(5(4(x1)))) | → | 3(4(2(2(3(3(4(2(2(1(x1)))))))))) | (60) |
2(1(1(0(x1)))) | → | 2(2(2(4(2(2(4(3(1(0(x1)))))))))) | (61) |
4(1(0(4(x1)))) | → | 4(2(3(3(3(1(1(3(2(4(x1)))))))))) | (62) |
5(4(0(5(3(x1))))) | → | 4(3(1(1(3(1(3(3(3(0(x1)))))))))) | (63) |
3(0(4(0(2(0(x1)))))) | → | 1(1(3(2(2(4(3(2(2(0(x1)))))))))) | (64) |
2(1(1(0(4(0(x1)))))) | → | 2(3(2(4(2(4(2(4(0(0(x1)))))))))) | (65) |
5(3(2(3(4(0(x1)))))) | → | 5(4(2(2(1(2(5(0(5(5(x1)))))))))) | (66) |
4(0(4(4(4(0(x1)))))) | → | 4(2(4(1(4(3(5(4(5(0(x1)))))))))) | (67) |
2(1(0(5(1(1(x1)))))) | → | 2(5(4(5(0(5(2(2(2(2(x1)))))))))) | (68) |
3(0(2(3(2(1(x1)))))) | → | 1(3(1(3(3(3(1(3(4(2(x1)))))))))) | (69) |
3(2(0(3(0(2(x1)))))) | → | 3(2(0(5(0(0(0(1(4(2(x1)))))))))) | (70) |
2(3(4(4(1(2(x1)))))) | → | 2(3(2(4(1(4(3(3(2(2(x1)))))))))) | (71) |
4(5(3(0(3(3(x1)))))) | → | 4(5(1(4(2(2(2(4(3(3(x1)))))))))) | (72) |
1(3(4(5(3(3(x1)))))) | → | 3(1(3(1(5(1(2(4(2(3(x1)))))))))) | (73) |
2(1(5(1(5(3(x1)))))) | → | 2(2(3(4(1(1(2(2(4(3(x1)))))))))) | (74) |
0(1(1(3(5(3(x1)))))) | → | 0(3(1(3(2(1(2(4(1(4(x1)))))))))) | (75) |
2(4(4(0(1(4(x1)))))) | → | 2(2(4(1(3(3(2(3(2(4(x1)))))))))) | (76) |
3(3(0(2(3(4(x1)))))) | → | 1(3(1(1(3(1(4(3(5(1(x1)))))))))) | (77) |
2(0(2(3(5(4(x1)))))) | → | 1(3(1(5(2(1(2(1(2(4(x1)))))))))) | (78) |
2(3(0(2(1(1(0(x1))))))) | → | 2(3(1(4(2(5(0(2(2(0(x1)))))))))) | (79) |
3(1(5(2(0(3(0(x1))))))) | → | 3(2(3(1(1(4(5(0(5(5(x1)))))))))) | (80) |
4(5(0(3(0(3(0(x1))))))) | → | 4(3(3(3(3(5(0(0(2(0(x1)))))))))) | (81) |
0(3(1(1(5(3(0(x1))))))) | → | 0(1(1(4(1(5(5(0(5(5(x1)))))))))) | (82) |
3(5(2(1(0(4(0(x1))))))) | → | 1(4(3(3(3(3(1(2(5(0(x1)))))))))) | (83) |
5(4(3(4(0(5(0(x1))))))) | → | 5(3(2(2(4(5(0(2(5(0(x1)))))))))) | (84) |
4(5(2(3(0(2(1(x1))))))) | → | 4(2(1(2(0(0(5(5(1(1(x1)))))))))) | (85) |
5(1(1(0(0(3(1(x1))))))) | → | 5(5(2(5(5(2(2(4(1(1(x1)))))))))) | (86) |
2(0(4(0(4(3(1(x1))))))) | → | 2(2(2(5(2(4(1(4(4(3(x1)))))))))) | (87) |
2(3(2(5(1(5(1(x1))))))) | → | 2(1(1(1(3(3(2(0(2(5(x1)))))))))) | (88) |
0(5(0(3(2(5(1(x1))))))) | → | 0(3(1(2(4(2(4(2(5(1(x1)))))))))) | (89) |
5(3(5(2(3(5(1(x1))))))) | → | 5(0(0(2(2(5(3(4(4(2(x1)))))))))) | (90) |
2(3(5(4(4(5(1(x1))))))) | → | 2(5(0(2(2(2(5(0(2(1(x1)))))))))) | (91) |
4(4(5(0(3(0(2(x1))))))) | → | 1(3(3(0(1(1(2(2(5(2(x1)))))))))) | (92) |
4(4(4(4(3(0(2(x1))))))) | → | 4(3(4(3(1(3(2(2(2(5(x1)))))))))) | (93) |
4(3(0(2(0(3(2(x1))))))) | → | 1(2(4(1(0(0(0(5(3(2(x1)))))))))) | (94) |
5(0(0(1(5(3(2(x1))))))) | → | 2(2(5(0(5(0(0(0(2(1(x1)))))))))) | (95) |
4(5(0(3(2(0(3(x1))))))) | → | 4(2(2(5(0(0(0(3(2(2(x1)))))))))) | (96) |
2(1(0(2(3(0(3(x1))))))) | → | 2(1(2(4(3(4(2(5(3(1(x1)))))))))) | (97) |
2(0(4(4(4(0(3(x1))))))) | → | 2(2(2(2(1(1(3(3(1(3(x1)))))))))) | (98) |
0(3(3(1(0(2(3(x1))))))) | → | 0(2(1(2(4(2(0(5(2(2(x1)))))))))) | (99) |
0(4(4(0(3(4(3(x1))))))) | → | 0(4(3(0(2(1(2(2(4(3(x1)))))))))) | (100) |
5(3(4(4(4(4(3(x1))))))) | → | 5(1(1(2(4(1(5(4(3(3(x1)))))))))) | (101) |
4(2(3(0(0(5(3(x1))))))) | → | 4(3(5(5(5(0(0(0(1(2(x1)))))))))) | (102) |
4(3(3(0(4(5(3(x1))))))) | → | 1(2(4(2(2(3(3(1(3(1(x1)))))))))) | (103) |
0(3(1(1(0(2(4(x1))))))) | → | 0(2(4(1(3(2(2(5(2(4(x1)))))))))) | (104) |
0(4(3(5(4(4(4(x1))))))) | → | 0(0(4(2(4(2(4(2(5(1(x1)))))))))) | (105) |
4(2(3(5(5(4(4(x1))))))) | → | 1(2(1(2(4(5(4(1(2(5(x1)))))))))) | (106) |
0(3(0(3(0(5(4(x1))))))) | → | 1(5(2(0(0(0(1(4(1(4(x1)))))))))) | (107) |
0(0(3(4(0(5(4(x1))))))) | → | 0(1(0(3(3(1(1(2(2(4(x1)))))))))) | (108) |
3(5(3(1(1(3(5(x1))))))) | → | 1(4(2(4(2(4(5(5(0(0(x1)))))))))) | (109) |
3(1(0(2(2(3(5(x1))))))) | → | 1(3(3(3(5(5(5(5(0(0(x1)))))))))) | (110) |
0(2(4(0(1(4(5(x1))))))) | → | 1(4(2(4(1(0(0(0(1(5(x1)))))))))) | (111) |
5(4(4(3(0(x1))))) | → | 5(4(2(4(2(1(2(2(2(0(x1)))))))))) | (112) |
5(4(3(5(3(5(5(x1))))))) | → | 5(4(1(5(4(2(4(1(0(5(x1)))))))))) | (113) |
2(5(1(4(1(5(x1)))))) | → | 2(5(0(1(2(2(4(2(2(5(x1)))))))))) | (114) |
4(5(0(3(x1)))) | → | 4(5(0(2(2(5(2(2(2(5(x1)))))))))) | (115) |
3(0(3(2(3(x1))))) | → | 1(3(1(1(2(4(3(3(4(3(x1)))))))))) | (116) |
0(5(4(4(5(2(3(x1))))))) | → | 0(4(3(5(0(0(0(0(2(3(x1)))))))))) | (117) |
4(0(2(1(4(4(x1)))))) | → | 1(3(1(3(2(4(3(4(5(5(x1)))))))))) | (118) |
0(5(4(5(3(1(1(x1))))))) | → | 0(0(1(4(1(2(4(2(2(3(x1)))))))))) | (119) |
4(5(4(3(x1)))) | → | 1(2(2(4(3(3(2(2(4(3(x1)))))))))) | (120) |
{2(☐), 1(☐), 0(☐), 4(☐), 3(☐), 5(☐)}
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).
[21(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[03(x1)] | = | 1 + 1 · x1 |
[05(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[44(x1)] | = | 1 + 1 · x1 |
[45(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 + 1 · x1 |
[34(x1)] | = | 1 + 1 · x1 |
[54(x1)] | = | 1 + 1 · x1 |
[12(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 + 1 · x1 |
[14(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 + 1 · x1 |
[20(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 + 1 · x1 |
There are 799 ruless (increase limit for explicit display).
[21(x1)] | = | 1 + 1 · x1 |
[11(x1)] | = | 1 + 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[02(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 + 1 · x1 |
[51(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 + 1 · x1 |
[25(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 + 1 · x1 |
[50(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 + 1 · x1 |
[15(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 + 1 · x1 |
[55(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 + 1 · x1 |
[53(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[44(x1)] | = | 1 + 1 · x1 |
[41(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
21(11(10(02(x1)))) | → | 22(22(24(42(22(24(43(31(10(02(x1)))))))))) | (235) |
21(11(10(01(x1)))) | → | 22(22(24(42(22(24(43(31(10(01(x1)))))))))) | (236) |
21(11(10(00(x1)))) | → | 22(22(24(42(22(24(43(31(10(00(x1)))))))))) | (237) |
21(11(10(04(x1)))) | → | 22(22(24(42(22(24(43(31(10(04(x1)))))))))) | (238) |
21(11(10(03(x1)))) | → | 22(22(24(42(22(24(43(31(10(03(x1)))))))))) | (239) |
21(11(10(05(x1)))) | → | 22(22(24(42(22(24(43(31(10(05(x1)))))))))) | (240) |
21(10(05(51(11(12(x1)))))) | → | 25(54(45(50(05(52(22(22(22(22(x1)))))))))) | (265) |
21(10(05(51(11(11(x1)))))) | → | 25(54(45(50(05(52(22(22(22(21(x1)))))))))) | (266) |
21(10(05(51(11(10(x1)))))) | → | 25(54(45(50(05(52(22(22(22(20(x1)))))))))) | (267) |
21(10(05(51(11(14(x1)))))) | → | 25(54(45(50(05(52(22(22(22(24(x1)))))))))) | (268) |
21(10(05(51(11(13(x1)))))) | → | 25(54(45(50(05(52(22(22(22(23(x1)))))))))) | (269) |
21(10(05(51(11(15(x1)))))) | → | 25(54(45(50(05(52(22(22(22(25(x1)))))))))) | (270) |
21(10(02(23(30(03(33(x1))))))) | → | 21(12(24(43(34(42(25(53(31(13(x1)))))))))) | (395) |
05(54(40(05(53(33(x1)))))) | → | 04(43(31(11(13(31(13(33(33(30(03(x1))))))))))) | (461) |
23(30(02(23(32(21(12(x1))))))) | → | 21(13(31(13(33(33(31(13(34(42(22(x1))))))))))) | (517) |
23(30(02(23(32(21(11(x1))))))) | → | 21(13(31(13(33(33(31(13(34(42(21(x1))))))))))) | (518) |
23(30(02(23(32(21(10(x1))))))) | → | 21(13(31(13(33(33(31(13(34(42(20(x1))))))))))) | (519) |
23(30(02(23(32(21(14(x1))))))) | → | 21(13(31(13(33(33(31(13(34(42(24(x1))))))))))) | (520) |
23(30(02(23(32(21(13(x1))))))) | → | 21(13(31(13(33(33(31(13(34(42(23(x1))))))))))) | (521) |
23(30(02(23(32(21(15(x1))))))) | → | 21(13(31(13(33(33(31(13(34(42(25(x1))))))))))) | (522) |
13(30(02(23(32(21(12(x1))))))) | → | 11(13(31(13(33(33(31(13(34(42(22(x1))))))))))) | (523) |
13(30(02(23(32(21(11(x1))))))) | → | 11(13(31(13(33(33(31(13(34(42(21(x1))))))))))) | (524) |
13(30(02(23(32(21(10(x1))))))) | → | 11(13(31(13(33(33(31(13(34(42(20(x1))))))))))) | (525) |
13(30(02(23(32(21(14(x1))))))) | → | 11(13(31(13(33(33(31(13(34(42(24(x1))))))))))) | (526) |
13(30(02(23(32(21(15(x1))))))) | → | 11(13(31(13(33(33(31(13(34(42(25(x1))))))))))) | (528) |
43(30(02(23(32(21(12(x1))))))) | → | 41(13(31(13(33(33(31(13(34(42(22(x1))))))))))) | (535) |
43(30(02(23(32(21(11(x1))))))) | → | 41(13(31(13(33(33(31(13(34(42(21(x1))))))))))) | (536) |
43(30(02(23(32(21(10(x1))))))) | → | 41(13(31(13(33(33(31(13(34(42(20(x1))))))))))) | (537) |
43(30(02(23(32(21(14(x1))))))) | → | 41(13(31(13(33(33(31(13(34(42(24(x1))))))))))) | (538) |
43(30(02(23(32(21(13(x1))))))) | → | 41(13(31(13(33(33(31(13(34(42(23(x1))))))))))) | (539) |
43(30(02(23(32(21(15(x1))))))) | → | 41(13(31(13(33(33(31(13(34(42(25(x1))))))))))) | (540) |
33(30(02(23(32(21(12(x1))))))) | → | 31(13(31(13(33(33(31(13(34(42(22(x1))))))))))) | (541) |
33(30(02(23(32(21(11(x1))))))) | → | 31(13(31(13(33(33(31(13(34(42(21(x1))))))))))) | (542) |
33(30(02(23(32(21(10(x1))))))) | → | 31(13(31(13(33(33(31(13(34(42(20(x1))))))))))) | (543) |
33(30(02(23(32(21(14(x1))))))) | → | 31(13(31(13(33(33(31(13(34(42(24(x1))))))))))) | (544) |
33(30(02(23(32(21(13(x1))))))) | → | 31(13(31(13(33(33(31(13(34(42(23(x1))))))))))) | (545) |
33(30(02(23(32(21(15(x1))))))) | → | 31(13(31(13(33(33(31(13(34(42(25(x1))))))))))) | (546) |
53(30(02(23(32(21(12(x1))))))) | → | 51(13(31(13(33(33(31(13(34(42(22(x1))))))))))) | (547) |
53(30(02(23(32(21(11(x1))))))) | → | 51(13(31(13(33(33(31(13(34(42(21(x1))))))))))) | (548) |
53(30(02(23(32(21(10(x1))))))) | → | 51(13(31(13(33(33(31(13(34(42(20(x1))))))))))) | (549) |
53(30(02(23(32(21(14(x1))))))) | → | 51(13(31(13(33(33(31(13(34(42(24(x1))))))))))) | (550) |
53(30(02(23(32(21(13(x1))))))) | → | 51(13(31(13(33(33(31(13(34(42(23(x1))))))))))) | (551) |
53(30(02(23(32(21(15(x1))))))) | → | 51(13(31(13(33(33(31(13(34(42(25(x1))))))))))) | (552) |
23(33(30(02(23(34(42(x1))))))) | → | 21(13(31(11(13(31(14(43(35(51(12(x1))))))))))) | (589) |
23(33(30(02(23(34(41(x1))))))) | → | 21(13(31(11(13(31(14(43(35(51(11(x1))))))))))) | (590) |
23(33(30(02(23(34(43(x1))))))) | → | 21(13(31(11(13(31(14(43(35(51(13(x1))))))))))) | (593) |
23(33(30(02(23(34(45(x1))))))) | → | 21(13(31(11(13(31(14(43(35(51(15(x1))))))))))) | (594) |
13(33(30(02(23(34(43(x1))))))) | → | 11(13(31(11(13(31(14(43(35(51(13(x1))))))))))) | (599) |
13(33(30(02(23(34(45(x1))))))) | → | 11(13(31(11(13(31(14(43(35(51(15(x1))))))))))) | (600) |
43(33(30(02(23(34(42(x1))))))) | → | 41(13(31(11(13(31(14(43(35(51(12(x1))))))))))) | (607) |
43(33(30(02(23(34(41(x1))))))) | → | 41(13(31(11(13(31(14(43(35(51(11(x1))))))))))) | (608) |
43(33(30(02(23(34(43(x1))))))) | → | 41(13(31(11(13(31(14(43(35(51(13(x1))))))))))) | (611) |
43(33(30(02(23(34(45(x1))))))) | → | 41(13(31(11(13(31(14(43(35(51(15(x1))))))))))) | (612) |
33(33(30(02(23(34(42(x1))))))) | → | 31(13(31(11(13(31(14(43(35(51(12(x1))))))))))) | (613) |
33(33(30(02(23(34(41(x1))))))) | → | 31(13(31(11(13(31(14(43(35(51(11(x1))))))))))) | (614) |
33(33(30(02(23(34(43(x1))))))) | → | 31(13(31(11(13(31(14(43(35(51(13(x1))))))))))) | (617) |
33(33(30(02(23(34(45(x1))))))) | → | 31(13(31(11(13(31(14(43(35(51(15(x1))))))))))) | (618) |
53(33(30(02(23(34(42(x1))))))) | → | 51(13(31(11(13(31(14(43(35(51(12(x1))))))))))) | (619) |
53(33(30(02(23(34(41(x1))))))) | → | 51(13(31(11(13(31(14(43(35(51(11(x1))))))))))) | (620) |
53(33(30(02(23(34(43(x1))))))) | → | 51(13(31(11(13(31(14(43(35(51(13(x1))))))))))) | (623) |
53(33(30(02(23(34(45(x1))))))) | → | 51(13(31(11(13(31(14(43(35(51(15(x1))))))))))) | (624) |
23(31(10(02(22(23(35(52(x1)))))))) | → | 21(13(33(33(35(55(55(55(50(00(02(x1))))))))))) | (949) |
23(31(10(02(22(23(35(50(x1)))))))) | → | 21(13(33(33(35(55(55(55(50(00(00(x1))))))))))) | (951) |
23(31(10(02(22(23(35(54(x1)))))))) | → | 21(13(33(33(35(55(55(55(50(00(04(x1))))))))))) | (952) |
23(31(10(02(22(23(35(53(x1)))))))) | → | 21(13(33(33(35(55(55(55(50(00(03(x1))))))))))) | (953) |
23(31(10(02(22(23(35(55(x1)))))))) | → | 21(13(33(33(35(55(55(55(50(00(05(x1))))))))))) | (954) |
13(31(10(02(22(23(35(52(x1)))))))) | → | 11(13(33(33(35(55(55(55(50(00(02(x1))))))))))) | (955) |
13(31(10(02(22(23(35(50(x1)))))))) | → | 11(13(33(33(35(55(55(55(50(00(00(x1))))))))))) | (957) |
13(31(10(02(22(23(35(54(x1)))))))) | → | 11(13(33(33(35(55(55(55(50(00(04(x1))))))))))) | (958) |
13(31(10(02(22(23(35(53(x1)))))))) | → | 11(13(33(33(35(55(55(55(50(00(03(x1))))))))))) | (959) |
43(31(10(02(22(23(35(52(x1)))))))) | → | 41(13(33(33(35(55(55(55(50(00(02(x1))))))))))) | (967) |
43(31(10(02(22(23(35(50(x1)))))))) | → | 41(13(33(33(35(55(55(55(50(00(00(x1))))))))))) | (969) |
43(31(10(02(22(23(35(54(x1)))))))) | → | 41(13(33(33(35(55(55(55(50(00(04(x1))))))))))) | (970) |
43(31(10(02(22(23(35(53(x1)))))))) | → | 41(13(33(33(35(55(55(55(50(00(03(x1))))))))))) | (971) |
43(31(10(02(22(23(35(55(x1)))))))) | → | 41(13(33(33(35(55(55(55(50(00(05(x1))))))))))) | (972) |
33(31(10(02(22(23(35(52(x1)))))))) | → | 31(13(33(33(35(55(55(55(50(00(02(x1))))))))))) | (973) |
33(31(10(02(22(23(35(50(x1)))))))) | → | 31(13(33(33(35(55(55(55(50(00(00(x1))))))))))) | (975) |
33(31(10(02(22(23(35(54(x1)))))))) | → | 31(13(33(33(35(55(55(55(50(00(04(x1))))))))))) | (976) |
33(31(10(02(22(23(35(53(x1)))))))) | → | 31(13(33(33(35(55(55(55(50(00(03(x1))))))))))) | (977) |
33(31(10(02(22(23(35(55(x1)))))))) | → | 31(13(33(33(35(55(55(55(50(00(05(x1))))))))))) | (978) |
53(31(10(02(22(23(35(52(x1)))))))) | → | 51(13(33(33(35(55(55(55(50(00(02(x1))))))))))) | (979) |
53(31(10(02(22(23(35(50(x1)))))))) | → | 51(13(33(33(35(55(55(55(50(00(00(x1))))))))))) | (981) |
53(31(10(02(22(23(35(54(x1)))))))) | → | 51(13(33(33(35(55(55(55(50(00(04(x1))))))))))) | (982) |
53(31(10(02(22(23(35(53(x1)))))))) | → | 51(13(33(33(35(55(55(55(50(00(03(x1))))))))))) | (983) |
53(31(10(02(22(23(35(55(x1)))))))) | → | 51(13(33(33(35(55(55(55(50(00(05(x1))))))))))) | (984) |
50(02(24(40(01(14(45(52(x1)))))))) | → | 51(14(42(24(41(10(00(00(01(15(52(x1))))))))))) | (1015) |
50(02(24(40(01(14(45(51(x1)))))))) | → | 51(14(42(24(41(10(00(00(01(15(51(x1))))))))))) | (1016) |
50(02(24(40(01(14(45(50(x1)))))))) | → | 51(14(42(24(41(10(00(00(01(15(50(x1))))))))))) | (1017) |
50(02(24(40(01(14(45(54(x1)))))))) | → | 51(14(42(24(41(10(00(00(01(15(54(x1))))))))))) | (1018) |
50(02(24(40(01(14(45(53(x1)))))))) | → | 51(14(42(24(41(10(00(00(01(15(53(x1))))))))))) | (1019) |
50(02(24(40(01(14(45(55(x1)))))))) | → | 51(14(42(24(41(10(00(00(01(15(55(x1))))))))))) | (1020) |
05(54(44(45(52(23(32(x1))))))) | → | 04(43(35(50(00(00(00(02(23(32(x1)))))))))) | (1045) |
05(54(44(45(52(23(31(x1))))))) | → | 04(43(35(50(00(00(00(02(23(31(x1)))))))))) | (1046) |
05(54(44(45(52(23(30(x1))))))) | → | 04(43(35(50(00(00(00(02(23(30(x1)))))))))) | (1047) |
05(54(44(45(52(23(34(x1))))))) | → | 04(43(35(50(00(00(00(02(23(34(x1)))))))))) | (1048) |
05(54(44(45(52(23(33(x1))))))) | → | 04(43(35(50(00(00(00(02(23(33(x1)))))))))) | (1049) |
05(54(44(45(52(23(35(x1))))))) | → | 04(43(35(50(00(00(00(02(23(35(x1)))))))))) | (1050) |
54(40(02(21(14(44(41(x1))))))) | → | 51(13(31(13(32(24(43(34(45(55(51(x1))))))))))) | (1124) |
54(40(02(21(14(44(43(x1))))))) | → | 51(13(31(13(32(24(43(34(45(55(53(x1))))))))))) | (1127) |
[45(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[33(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 + 1 · x1 |
[35(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
45(54(40(05(53(33(x1)))))) | → | 44(43(31(11(13(31(13(33(33(30(03(x1))))))))))) | (467) |
55(54(40(05(53(33(x1)))))) | → | 54(43(31(11(13(31(13(33(33(30(03(x1))))))))))) | (479) |
01(13(34(45(53(33(32(x1))))))) | → | 03(31(13(31(15(51(12(24(42(23(32(x1))))))))))) | (565) |
01(13(34(45(53(33(31(x1))))))) | → | 03(31(13(31(15(51(12(24(42(23(31(x1))))))))))) | (566) |
01(13(34(45(53(33(30(x1))))))) | → | 03(31(13(31(15(51(12(24(42(23(30(x1))))))))))) | (567) |
01(13(34(45(53(33(34(x1))))))) | → | 03(31(13(31(15(51(12(24(42(23(34(x1))))))))))) | (568) |
01(13(34(45(53(33(33(x1))))))) | → | 03(31(13(31(15(51(12(24(42(23(33(x1))))))))))) | (569) |
01(13(34(45(53(33(35(x1))))))) | → | 03(31(13(31(15(51(12(24(42(23(35(x1))))))))))) | (570) |
24(40(02(21(14(44(41(x1))))))) | → | 21(13(31(13(32(24(43(34(45(55(51(x1))))))))))) | (1094) |
24(40(02(21(14(44(43(x1))))))) | → | 21(13(31(13(32(24(43(34(45(55(53(x1))))))))))) | (1097) |
14(40(02(21(14(44(41(x1))))))) | → | 11(13(31(13(32(24(43(34(45(55(51(x1))))))))))) | (1100) |
14(40(02(21(14(44(43(x1))))))) | → | 11(13(31(13(32(24(43(34(45(55(53(x1))))))))))) | (1103) |
[45(x1)] | = | 1 + 1 · x1 |
[52(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 + 1 · x1 |
[30(x1)] | = | 1 + 1 · x1 |
[02(x1)] | = | 1 + 1 · x1 |
[21(x1)] | = | 1 + 1 · x1 |
[12(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 + 1 · x1 |
[00(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 + 1 · x1 |
[32(x1)] | = | 1 + 1 · x1 |
[25(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 + 1 · x1 |
[24(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
45(52(23(30(02(21(12(x1))))))) | → | 42(21(12(20(00(05(55(51(11(12(x1)))))))))) | (337) |
45(52(23(30(02(21(11(x1))))))) | → | 42(21(12(20(00(05(55(51(11(11(x1)))))))))) | (338) |
45(52(23(30(02(21(10(x1))))))) | → | 42(21(12(20(00(05(55(51(11(10(x1)))))))))) | (339) |
45(52(23(30(02(21(14(x1))))))) | → | 42(21(12(20(00(05(55(51(11(14(x1)))))))))) | (340) |
45(52(23(30(02(21(13(x1))))))) | → | 42(21(12(20(00(05(55(51(11(13(x1)))))))))) | (341) |
45(52(23(30(02(21(15(x1))))))) | → | 42(21(12(20(00(05(55(51(11(15(x1)))))))))) | (342) |
21(10(02(23(30(03(32(x1))))))) | → | 21(12(24(43(34(42(25(53(31(12(x1)))))))))) | (391) |
21(10(02(23(30(03(31(x1))))))) | → | 21(12(24(43(34(42(25(53(31(11(x1)))))))))) | (392) |
13(30(02(23(32(21(13(x1))))))) | → | 11(13(31(13(33(33(31(13(34(42(23(x1))))))))))) | (527) |
13(33(30(02(23(34(42(x1))))))) | → | 11(13(31(11(13(31(14(43(35(51(12(x1))))))))))) | (595) |
13(33(30(02(23(34(41(x1))))))) | → | 11(13(31(11(13(31(14(43(35(51(11(x1))))))))))) | (596) |
13(31(10(02(22(23(35(55(x1)))))))) | → | 11(13(33(33(35(55(55(55(50(00(05(x1))))))))))) | (960) |
45(50(03(31(x1)))) | → | 45(50(02(22(25(52(22(22(25(51(x1)))))))))) | (1040) |
[05(x1)] | = | 1 + 1 · x1 |
[50(x1)] | = | 1 + 1 · x1 |
[03(x1)] | = | 1 + 1 · x1 |
[32(x1)] | = | 1 + 1 · x1 |
[25(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 + 1 · x1 |
[31(x1)] | = | 1 + 1 · x1 |
[24(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 + 1 · x1 |
[02(x1)] | = | 1 + 1 · x1 |
[22(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 + 1 · x1 |
[53(x1)] | = | 1 · x1 |
05(50(03(32(25(51(12(x1))))))) | → | 03(31(12(24(42(24(42(25(51(12(x1)))))))))) | (361) |
05(50(03(32(25(51(11(x1))))))) | → | 03(31(12(24(42(24(42(25(51(11(x1)))))))))) | (362) |
05(50(03(32(25(51(10(x1))))))) | → | 03(31(12(24(42(24(42(25(51(10(x1)))))))))) | (363) |
05(50(03(32(25(51(14(x1))))))) | → | 03(31(12(24(42(24(42(25(51(14(x1)))))))))) | (364) |
05(50(03(32(25(51(13(x1))))))) | → | 03(31(12(24(42(24(42(25(51(13(x1)))))))))) | (365) |
05(50(03(32(25(51(15(x1))))))) | → | 03(31(12(24(42(24(42(25(51(15(x1)))))))))) | (366) |
There are no rules in the TRS. Hence, it is terminating.