The relative rewrite relation R/S is considered where R is the following TRS
0(1(2(3(x1)))) | → | 0(0(2(2(0(1(0(5(5(4(x1)))))))))) | (1) |
0(1(4(0(x1)))) | → | 1(5(4(2(2(4(2(2(4(2(x1)))))))))) | (2) |
1(2(5(2(x1)))) | → | 1(3(4(4(1(4(1(0(1(0(x1)))))))))) | (3) |
2(1(2(0(x1)))) | → | 0(2(0(0(4(2(2(0(4(2(x1)))))))))) | (4) |
3(2(5(3(x1)))) | → | 3(2(3(3(2(0(1(0(0(2(x1)))))))))) | (5) |
3(3(5(0(x1)))) | → | 3(0(1(5(4(3(1(3(0(2(x1)))))))))) | (6) |
4(1(4(2(x1)))) | → | 4(2(2(2(2(2(1(0(3(2(x1)))))))))) | (7) |
0(4(5(1(2(x1))))) | → | 0(4(0(3(0(4(5(1(5(5(x1)))))))))) | (8) |
1(2(3(4(0(x1))))) | → | 1(4(4(0(3(2(0(2(1(0(x1)))))))))) | (9) |
1(2(5(2(5(x1))))) | → | 1(3(2(3(0(0(5(0(3(0(x1)))))))))) | (10) |
2(1(2(5(2(x1))))) | → | 0(2(3(2(2(0(0(5(3(2(x1)))))))))) | (11) |
2(2(5(4(5(x1))))) | → | 2(0(2(0(3(5(5(1(5(5(x1)))))))))) | (12) |
2(5(3(1(2(x1))))) | → | 3(4(4(0(4(4(2(4(3(0(x1)))))))))) | (13) |
2(5(5(5(0(x1))))) | → | 3(2(2(2(5(5(4(1(0(0(x1)))))))))) | (14) |
3(2(1(4(2(x1))))) | → | 0(4(3(1(1(5(5(0(2(2(x1)))))))))) | (15) |
3(3(3(5(0(x1))))) | → | 3(2(4(1(5(0(0(0(0(0(x1)))))))))) | (16) |
4(3(3(1(4(x1))))) | → | 4(1(0(0(2(2(4(3(3(0(x1)))))))))) | (17) |
5(3(1(2(4(x1))))) | → | 5(5(4(1(3(0(0(3(0(4(x1)))))))))) | (18) |
0(1(4(0(1(4(x1)))))) | → | 0(2(0(1(3(4(3(1(5(2(x1)))))))))) | (19) |
0(3(1(2(5(3(x1)))))) | → | 0(1(0(4(5(5(4(1(5(3(x1)))))))))) | (20) |
0(3(2(1(4(2(x1)))))) | → | 0(1(0(0(2(0(3(5(3(2(x1)))))))))) | (21) |
1(2(5(1(4(3(x1)))))) | → | 0(3(3(4(3(0(1(0(3(3(x1)))))))))) | (22) |
2(5(5(3(2(5(x1)))))) | → | 0(0(0(3(0(2(1(4(2(3(x1)))))))))) | (23) |
2(5(5(3(5(3(x1)))))) | → | 3(2(2(1(5(3(0(2(0(3(x1)))))))))) | (24) |
3(2(1(2(1(2(x1)))))) | → | 3(3(5(1(1(3(1(0(2(2(x1)))))))))) | (25) |
3(3(5(0(4(2(x1)))))) | → | 3(0(0(2(0(4(1(4(4(2(x1)))))))))) | (26) |
3(4(0(0(5(1(x1)))))) | → | 3(0(0(4(2(1(0(3(0(1(x1)))))))))) | (27) |
3(5(3(3(1(2(x1)))))) | → | 1(5(4(3(3(5(4(5(2(2(x1)))))))))) | (28) |
4(1(4(3(1(3(x1)))))) | → | 4(0(2(2(2(3(2(4(4(3(x1)))))))))) | (29) |
4(3(5(4(5(2(x1)))))) | → | 5(3(0(3(2(2(3(1(5(2(x1)))))))))) | (30) |
5(1(0(1(2(0(x1)))))) | → | 5(4(2(1(0(2(4(3(1(0(x1)))))))))) | (31) |
5(2(5(5(2(1(x1)))))) | → | 1(5(4(5(3(2(3(2(0(1(x1)))))))))) | (32) |
5(3(1(3(5(2(x1)))))) | → | 5(0(1(0(2(0(0(0(5(2(x1)))))))))) | (33) |
5(3(5(4(5(3(x1)))))) | → | 5(3(0(0(0(4(1(0(4(4(x1)))))))))) | (34) |
5(5(3(0(5(3(x1)))))) | → | 5(4(3(0(4(2(2(4(3(0(x1)))))))))) | (35) |
1(1(4(1(2(1(4(x1))))))) | → | 1(2(5(2(0(0(3(1(5(5(x1)))))))))) | (36) |
1(2(0(5(5(3(4(x1))))))) | → | 0(5(4(4(1(5(0(4(4(4(x1)))))))))) | (37) |
1(3(1(2(5(5(3(x1))))))) | → | 3(3(3(0(4(4(0(0(3(3(x1)))))))))) | (38) |
1(3(3(1(2(1(2(x1))))))) | → | 3(1(3(3(0(1(3(4(5(5(x1)))))))))) | (39) |
1(4(1(2(3(4(5(x1))))))) | → | 1(1(0(4(4(2(5(4(4(5(x1)))))))))) | (40) |
2(0(5(4(5(3(5(x1))))))) | → | 2(0(2(1(4(4(0(0(0(4(x1)))))))))) | (41) |
2(4(5(0(5(2(5(x1))))))) | → | 0(4(3(2(1(1(1(4(2(3(x1)))))))))) | (42) |
2(5(1(2(4(0(5(x1))))))) | → | 0(0(5(5(5(0(0(0(3(3(x1)))))))))) | (43) |
3(1(2(5(3(3(3(x1))))))) | → | 1(0(3(0(5(1(1(5(5(0(x1)))))))))) | (44) |
3(1(4(3(5(3(5(x1))))))) | → | 0(0(0(3(4(2(4(1(2(5(x1)))))))))) | (45) |
3(1(5(2(5(1(0(x1))))))) | → | 3(4(4(2(3(4(0(4(0(2(x1)))))))))) | (46) |
4(1(4(3(3(5(3(x1))))))) | → | 4(2(1(3(0(4(3(2(2(0(x1)))))))))) | (47) |
4(3(4(2(5(5(1(x1))))))) | → | 5(2(0(4(1(3(0(1(1(1(x1)))))))))) | (48) |
4(5(0(4(4(5(3(x1))))))) | → | 4(4(5(1(1(1(5(4(4(0(x1)))))))))) | (49) |
4(5(3(1(1(2(4(x1))))))) | → | 4(4(1(4(4(3(2(1(0(4(x1)))))))))) | (50) |
5(1(1(4(5(0(5(x1))))))) | → | 5(0(3(4(2(1(1(5(5(3(x1)))))))))) | (51) |
5(2(4(1(2(5(0(x1))))))) | → | 5(4(3(0(0(4(4(1(5(0(x1)))))))))) | (52) |
and S is the following TRS.
2(2(5(5(4(5(2(x1))))))) | → | 2(1(0(3(4(1(0(1(4(4(x1)))))))))) | (53) |
1(2(3(3(3(0(x1)))))) | → | 1(5(3(1(3(5(1(5(4(2(x1)))))))))) | (54) |
4(5(3(4(1(2(1(x1))))))) | → | 4(0(5(4(1(5(5(0(0(1(x1)))))))))) | (55) |
2(2(4(5(x1)))) | → | 2(1(0(2(3(5(1(5(5(5(x1)))))))))) | (56) |
4(1(4(3(2(3(x1)))))) | → | 4(5(4(1(1(0(3(2(0(3(x1)))))))))) | (57) |
4(2(x1)) | → | 4(3(1(5(4(2(1(1(5(4(x1)))))))))) | (58) |
2(2(4(5(5(3(5(x1))))))) | → | 2(2(4(2(0(1(0(2(5(5(x1)))))))))) | (59) |
0(1(x1)) | → | 0(0(0(1(0(2(3(2(0(1(x1)))))))))) | (60) |
{0(☐), 1(☐), 2(☐), 3(☐), 5(☐), 4(☐)}
We obtain the transformed TRSThere are 160 ruless (increase limit for explicit display).
Root-labeling is applied.
We obtain the labeled TRSThere are 960 ruless (increase limit for explicit display).
[01(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 + 1 · x1 |
[23(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 + 1 · x1 |
[55(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 + 1 · x1 |
[45(x1)] | = | 1 + 1 · x1 |
[34(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 + 1 · x1 |
[52(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 + 1 · x1 |
[21(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
There are 793 ruless (increase limit for explicit display).
[01(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 + 1 · x1 |
[23(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 + 1 · x1 |
[24(x1)] | = | 1 + 1 · x1 |
[50(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 + 1 · x1 |
[15(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
01(12(23(30(x1)))) | → | 00(02(22(20(01(10(05(55(54(40(x1)))))))))) | (181) |
01(12(23(31(x1)))) | → | 00(02(22(20(01(10(05(55(54(41(x1)))))))))) | (182) |
01(12(23(32(x1)))) | → | 00(02(22(20(01(10(05(55(54(42(x1)))))))))) | (183) |
01(12(23(33(x1)))) | → | 00(02(22(20(01(10(05(55(54(43(x1)))))))))) | (184) |
01(12(23(35(x1)))) | → | 00(02(22(20(01(10(05(55(54(45(x1)))))))))) | (185) |
01(12(23(34(x1)))) | → | 00(02(22(20(01(10(05(55(54(44(x1)))))))))) | (186) |
12(23(34(40(00(x1))))) | → | 14(44(40(03(32(20(02(21(10(00(x1)))))))))) | (217) |
12(23(34(40(01(x1))))) | → | 14(44(40(03(32(20(02(21(10(01(x1)))))))))) | (218) |
12(23(34(40(02(x1))))) | → | 14(44(40(03(32(20(02(21(10(02(x1)))))))))) | (219) |
12(23(34(40(03(x1))))) | → | 14(44(40(03(32(20(02(21(10(03(x1)))))))))) | (220) |
12(23(34(40(05(x1))))) | → | 14(44(40(03(32(20(02(21(10(05(x1)))))))))) | (221) |
12(23(34(40(04(x1))))) | → | 14(44(40(03(32(20(02(21(10(04(x1)))))))))) | (222) |
52(25(55(55(50(00(x1)))))) | → | 53(32(22(22(25(55(54(41(10(00(00(x1))))))))))) | (541) |
52(25(55(55(50(01(x1)))))) | → | 53(32(22(22(25(55(54(41(10(00(01(x1))))))))))) | (542) |
52(25(55(55(50(02(x1)))))) | → | 53(32(22(22(25(55(54(41(10(00(02(x1))))))))))) | (543) |
52(25(55(55(50(03(x1)))))) | → | 53(32(22(22(25(55(54(41(10(00(03(x1))))))))))) | (544) |
52(25(55(55(50(05(x1)))))) | → | 53(32(22(22(25(55(54(41(10(00(05(x1))))))))))) | (545) |
52(25(55(55(50(04(x1)))))) | → | 53(32(22(22(25(55(54(41(10(00(04(x1))))))))))) | (546) |
02(25(55(53(32(25(55(x1))))))) | → | 00(00(00(03(30(02(21(14(42(23(35(x1))))))))))) | (629) |
22(25(55(53(32(25(55(x1))))))) | → | 20(00(00(03(30(02(21(14(42(23(35(x1))))))))))) | (641) |
32(25(55(53(32(25(55(x1))))))) | → | 30(00(00(03(30(02(21(14(42(23(35(x1))))))))))) | (647) |
52(25(55(53(32(25(55(x1))))))) | → | 50(00(00(03(30(02(21(14(42(23(35(x1))))))))))) | (653) |
42(25(55(53(32(25(55(x1))))))) | → | 40(00(00(03(30(02(21(14(42(23(35(x1))))))))))) | (659) |
15(52(25(55(52(21(10(x1))))))) | → | 11(15(54(45(53(32(23(32(20(01(10(x1))))))))))) | (775) |
15(52(25(55(52(21(11(x1))))))) | → | 11(15(54(45(53(32(23(32(20(01(11(x1))))))))))) | (776) |
15(52(25(55(52(21(12(x1))))))) | → | 11(15(54(45(53(32(23(32(20(01(12(x1))))))))))) | (777) |
15(52(25(55(52(21(13(x1))))))) | → | 11(15(54(45(53(32(23(32(20(01(13(x1))))))))))) | (778) |
15(52(25(55(52(21(15(x1))))))) | → | 11(15(54(45(53(32(23(32(20(01(15(x1))))))))))) | (779) |
15(52(25(55(52(21(14(x1))))))) | → | 11(15(54(45(53(32(23(32(20(01(14(x1))))))))))) | (780) |
55(52(25(55(52(21(10(x1))))))) | → | 51(15(54(45(53(32(23(32(20(01(10(x1))))))))))) | (793) |
55(52(25(55(52(21(11(x1))))))) | → | 51(15(54(45(53(32(23(32(20(01(11(x1))))))))))) | (794) |
55(52(25(55(52(21(12(x1))))))) | → | 51(15(54(45(53(32(23(32(20(01(12(x1))))))))))) | (795) |
55(52(25(55(52(21(13(x1))))))) | → | 51(15(54(45(53(32(23(32(20(01(13(x1))))))))))) | (796) |
55(52(25(55(52(21(15(x1))))))) | → | 51(15(54(45(53(32(23(32(20(01(15(x1))))))))))) | (797) |
55(52(25(55(52(21(14(x1))))))) | → | 51(15(54(45(53(32(23(32(20(01(14(x1))))))))))) | (798) |
12(23(33(33(30(00(x1)))))) | → | 15(53(31(13(35(51(15(54(42(20(x1)))))))))) | (1099) |
12(23(33(33(30(01(x1)))))) | → | 15(53(31(13(35(51(15(54(42(21(x1)))))))))) | (1100) |
12(23(33(33(30(02(x1)))))) | → | 15(53(31(13(35(51(15(54(42(22(x1)))))))))) | (1101) |
12(23(33(33(30(03(x1)))))) | → | 15(53(31(13(35(51(15(54(42(23(x1)))))))))) | (1102) |
22(24(45(50(x1)))) | → | 21(10(02(23(35(51(15(55(55(50(x1)))))))))) | (1111) |
22(24(45(51(x1)))) | → | 21(10(02(23(35(51(15(55(55(51(x1)))))))))) | (1112) |
22(24(45(52(x1)))) | → | 21(10(02(23(35(51(15(55(55(52(x1)))))))))) | (1113) |
22(24(45(53(x1)))) | → | 21(10(02(23(35(51(15(55(55(53(x1)))))))))) | (1114) |
22(24(45(55(x1)))) | → | 21(10(02(23(35(51(15(55(55(55(x1)))))))))) | (1115) |
22(24(45(54(x1)))) | → | 21(10(02(23(35(51(15(55(55(54(x1)))))))))) | (1116) |
42(25(x1)) | → | 43(31(15(54(42(21(11(15(54(45(x1)))))))))) | (1127) |
42(24(x1)) | → | 43(31(15(54(42(21(11(15(54(44(x1)))))))))) | (1128) |
[03(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 + 1 · x1 |
[42(x1)] | = | 1 + 1 · x1 |
[20(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 + 1 · x1 |
[53(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 + 1 · x1 |
[23(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 + 1 · x1 |
[04(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 + 1 · x1 |
[41(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 + 1 · x1 |
[54(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 + 1 · x1 |
[15(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
03(32(21(14(42(20(x1)))))) | → | 01(10(00(02(20(03(35(53(32(20(x1)))))))))) | (265) |
03(32(21(14(42(21(x1)))))) | → | 01(10(00(02(20(03(35(53(32(21(x1)))))))))) | (266) |
03(32(21(14(42(22(x1)))))) | → | 01(10(00(02(20(03(35(53(32(22(x1)))))))))) | (267) |
03(32(21(14(42(23(x1)))))) | → | 01(10(00(02(20(03(35(53(32(23(x1)))))))))) | (268) |
03(32(21(14(42(25(x1)))))) | → | 01(10(00(02(20(03(35(53(32(25(x1)))))))))) | (269) |
03(32(21(14(42(24(x1)))))) | → | 01(10(00(02(20(03(35(53(32(24(x1)))))))))) | (270) |
22(25(55(55(50(00(x1)))))) | → | 23(32(22(22(25(55(54(41(10(00(00(x1))))))))))) | (529) |
22(25(55(55(50(01(x1)))))) | → | 23(32(22(22(25(55(54(41(10(00(01(x1))))))))))) | (530) |
22(25(55(55(50(02(x1)))))) | → | 23(32(22(22(25(55(54(41(10(00(02(x1))))))))))) | (531) |
22(25(55(55(50(03(x1)))))) | → | 23(32(22(22(25(55(54(41(10(00(03(x1))))))))))) | (532) |
22(25(55(55(50(05(x1)))))) | → | 23(32(22(22(25(55(54(41(10(00(05(x1))))))))))) | (533) |
22(25(55(55(50(04(x1)))))) | → | 23(32(22(22(25(55(54(41(10(00(04(x1))))))))))) | (534) |
42(25(55(55(50(00(x1)))))) | → | 43(32(22(22(25(55(54(41(10(00(00(x1))))))))))) | (547) |
42(25(55(55(50(01(x1)))))) | → | 43(32(22(22(25(55(54(41(10(00(01(x1))))))))))) | (548) |
42(25(55(55(50(02(x1)))))) | → | 43(32(22(22(25(55(54(41(10(00(02(x1))))))))))) | (549) |
42(25(55(55(50(03(x1)))))) | → | 43(32(22(22(25(55(54(41(10(00(03(x1))))))))))) | (550) |
42(25(55(55(50(05(x1)))))) | → | 43(32(22(22(25(55(54(41(10(00(05(x1))))))))))) | (551) |
42(25(55(55(50(04(x1)))))) | → | 43(32(22(22(25(55(54(41(10(00(04(x1))))))))))) | (552) |
04(43(34(42(25(55(51(10(x1)))))))) | → | 05(52(20(04(41(13(30(01(11(11(10(x1))))))))))) | (1057) |
04(43(34(42(25(55(51(11(x1)))))))) | → | 05(52(20(04(41(13(30(01(11(11(11(x1))))))))))) | (1058) |
04(43(34(42(25(55(51(12(x1)))))))) | → | 05(52(20(04(41(13(30(01(11(11(12(x1))))))))))) | (1059) |
04(43(34(42(25(55(51(13(x1)))))))) | → | 05(52(20(04(41(13(30(01(11(11(13(x1))))))))))) | (1060) |
04(43(34(42(25(55(51(15(x1)))))))) | → | 05(52(20(04(41(13(30(01(11(11(15(x1))))))))))) | (1061) |
04(43(34(42(25(55(51(14(x1)))))))) | → | 05(52(20(04(41(13(30(01(11(11(14(x1))))))))))) | (1062) |
24(43(34(42(25(55(51(10(x1)))))))) | → | 25(52(20(04(41(13(30(01(11(11(10(x1))))))))))) | (1069) |
24(43(34(42(25(55(51(11(x1)))))))) | → | 25(52(20(04(41(13(30(01(11(11(11(x1))))))))))) | (1070) |
24(43(34(42(25(55(51(12(x1)))))))) | → | 25(52(20(04(41(13(30(01(11(11(12(x1))))))))))) | (1071) |
24(43(34(42(25(55(51(13(x1)))))))) | → | 25(52(20(04(41(13(30(01(11(11(13(x1))))))))))) | (1072) |
24(43(34(42(25(55(51(15(x1)))))))) | → | 25(52(20(04(41(13(30(01(11(11(15(x1))))))))))) | (1073) |
24(43(34(42(25(55(51(14(x1)))))))) | → | 25(52(20(04(41(13(30(01(11(11(14(x1))))))))))) | (1074) |
44(43(34(42(25(55(51(10(x1)))))))) | → | 45(52(20(04(41(13(30(01(11(11(10(x1))))))))))) | (1087) |
44(43(34(42(25(55(51(11(x1)))))))) | → | 45(52(20(04(41(13(30(01(11(11(11(x1))))))))))) | (1088) |
44(43(34(42(25(55(51(12(x1)))))))) | → | 45(52(20(04(41(13(30(01(11(11(12(x1))))))))))) | (1089) |
44(43(34(42(25(55(51(13(x1)))))))) | → | 45(52(20(04(41(13(30(01(11(11(13(x1))))))))))) | (1090) |
44(43(34(42(25(55(51(15(x1)))))))) | → | 45(52(20(04(41(13(30(01(11(11(15(x1))))))))))) | (1091) |
44(43(34(42(25(55(51(14(x1)))))))) | → | 45(52(20(04(41(13(30(01(11(11(14(x1))))))))))) | (1092) |
41(14(43(32(23(30(x1)))))) | → | 45(54(41(11(10(03(32(20(03(30(x1)))))))))) | (1117) |
41(14(43(32(23(31(x1)))))) | → | 45(54(41(11(10(03(32(20(03(31(x1)))))))))) | (1118) |
41(14(43(32(23(32(x1)))))) | → | 45(54(41(11(10(03(32(20(03(32(x1)))))))))) | (1119) |
41(14(43(32(23(33(x1)))))) | → | 45(54(41(11(10(03(32(20(03(33(x1)))))))))) | (1120) |
41(14(43(32(23(35(x1)))))) | → | 45(54(41(11(10(03(32(20(03(35(x1)))))))))) | (1121) |
41(14(43(32(23(34(x1)))))) | → | 45(54(41(11(10(03(32(20(03(34(x1)))))))))) | (1122) |
[33(x1)] | = | 1 + 1 · x1 |
[35(x1)] | = | 1 + 1 · x1 |
[50(x1)] | = | 1 + 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[42(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 + 1 · x1 |
[31(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 + 1 · x1 |
[52(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 + 1 · x1 |
[55(x1)] | = | 1 + 1 · x1 |
[03(x1)] | = | 1 + 1 · x1 |
[32(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 + 1 · x1 |
[15(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 + 1 · x1 |
[11(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 + 1 · x1 |
[34(x1)] | = | 1 + 1 · x1 |
[40(x1)] | = | 1 · x1 |
33(35(50(04(42(20(x1)))))) | → | 30(00(02(20(04(41(14(44(42(20(x1)))))))))) | (277) |
33(35(50(04(42(21(x1)))))) | → | 30(00(02(20(04(41(14(44(42(21(x1)))))))))) | (278) |
33(35(50(04(42(22(x1)))))) | → | 30(00(02(20(04(41(14(44(42(22(x1)))))))))) | (279) |
33(35(50(04(42(23(x1)))))) | → | 30(00(02(20(04(41(14(44(42(23(x1)))))))))) | (280) |
33(35(50(04(42(25(x1)))))) | → | 30(00(02(20(04(41(14(44(42(25(x1)))))))))) | (281) |
33(35(50(04(42(24(x1)))))) | → | 30(00(02(20(04(41(14(44(42(24(x1)))))))))) | (282) |
53(31(13(35(52(20(x1)))))) | → | 50(01(10(02(20(00(00(05(52(20(x1)))))))))) | (301) |
53(31(13(35(52(21(x1)))))) | → | 50(01(10(02(20(00(00(05(52(21(x1)))))))))) | (302) |
53(31(13(35(52(22(x1)))))) | → | 50(01(10(02(20(00(00(05(52(22(x1)))))))))) | (303) |
53(31(13(35(52(23(x1)))))) | → | 50(01(10(02(20(00(00(05(52(23(x1)))))))))) | (304) |
53(31(13(35(52(25(x1)))))) | → | 50(01(10(02(20(00(00(05(52(25(x1)))))))))) | (305) |
53(31(13(35(52(24(x1)))))) | → | 50(01(10(02(20(00(00(05(52(24(x1)))))))))) | (306) |
02(25(55(55(50(00(x1)))))) | → | 03(32(22(22(25(55(54(41(10(00(00(x1))))))))))) | (517) |
02(25(55(55(50(01(x1)))))) | → | 03(32(22(22(25(55(54(41(10(00(01(x1))))))))))) | (518) |
02(25(55(55(50(02(x1)))))) | → | 03(32(22(22(25(55(54(41(10(00(02(x1))))))))))) | (519) |
02(25(55(55(50(03(x1)))))) | → | 03(32(22(22(25(55(54(41(10(00(03(x1))))))))))) | (520) |
02(25(55(55(50(05(x1)))))) | → | 03(32(22(22(25(55(54(41(10(00(05(x1))))))))))) | (521) |
02(25(55(55(50(04(x1)))))) | → | 03(32(22(22(25(55(54(41(10(00(04(x1))))))))))) | (522) |
32(25(55(55(50(00(x1)))))) | → | 33(32(22(22(25(55(54(41(10(00(00(x1))))))))))) | (535) |
32(25(55(55(50(01(x1)))))) | → | 33(32(22(22(25(55(54(41(10(00(01(x1))))))))))) | (536) |
32(25(55(55(50(02(x1)))))) | → | 33(32(22(22(25(55(54(41(10(00(02(x1))))))))))) | (537) |
32(25(55(55(50(03(x1)))))) | → | 33(32(22(22(25(55(54(41(10(00(03(x1))))))))))) | (538) |
32(25(55(55(50(05(x1)))))) | → | 33(32(22(22(25(55(54(41(10(00(05(x1))))))))))) | (539) |
32(25(55(55(50(04(x1)))))) | → | 33(32(22(22(25(55(54(41(10(00(04(x1))))))))))) | (540) |
03(35(53(33(31(12(20(x1))))))) | → | 01(15(54(43(33(35(54(45(52(22(20(x1))))))))))) | (697) |
03(35(53(33(31(12(21(x1))))))) | → | 01(15(54(43(33(35(54(45(52(22(21(x1))))))))))) | (698) |
03(35(53(33(31(12(22(x1))))))) | → | 01(15(54(43(33(35(54(45(52(22(22(x1))))))))))) | (699) |
03(35(53(33(31(12(23(x1))))))) | → | 01(15(54(43(33(35(54(45(52(22(23(x1))))))))))) | (700) |
03(35(53(33(31(12(25(x1))))))) | → | 01(15(54(43(33(35(54(45(52(22(25(x1))))))))))) | (701) |
03(35(53(33(31(12(24(x1))))))) | → | 01(15(54(43(33(35(54(45(52(22(24(x1))))))))))) | (702) |
13(35(53(33(31(12(20(x1))))))) | → | 11(15(54(43(33(35(54(45(52(22(20(x1))))))))))) | (703) |
13(35(53(33(31(12(21(x1))))))) | → | 11(15(54(43(33(35(54(45(52(22(21(x1))))))))))) | (704) |
13(35(53(33(31(12(22(x1))))))) | → | 11(15(54(43(33(35(54(45(52(22(22(x1))))))))))) | (705) |
13(35(53(33(31(12(23(x1))))))) | → | 11(15(54(43(33(35(54(45(52(22(23(x1))))))))))) | (706) |
13(35(53(33(31(12(25(x1))))))) | → | 11(15(54(43(33(35(54(45(52(22(25(x1))))))))))) | (707) |
13(35(53(33(31(12(24(x1))))))) | → | 11(15(54(43(33(35(54(45(52(22(24(x1))))))))))) | (708) |
23(35(53(33(31(12(20(x1))))))) | → | 21(15(54(43(33(35(54(45(52(22(20(x1))))))))))) | (709) |
23(35(53(33(31(12(21(x1))))))) | → | 21(15(54(43(33(35(54(45(52(22(21(x1))))))))))) | (710) |
23(35(53(33(31(12(22(x1))))))) | → | 21(15(54(43(33(35(54(45(52(22(22(x1))))))))))) | (711) |
23(35(53(33(31(12(23(x1))))))) | → | 21(15(54(43(33(35(54(45(52(22(23(x1))))))))))) | (712) |
23(35(53(33(31(12(25(x1))))))) | → | 21(15(54(43(33(35(54(45(52(22(25(x1))))))))))) | (713) |
23(35(53(33(31(12(24(x1))))))) | → | 21(15(54(43(33(35(54(45(52(22(24(x1))))))))))) | (714) |
33(35(53(33(31(12(20(x1))))))) | → | 31(15(54(43(33(35(54(45(52(22(20(x1))))))))))) | (715) |
33(35(53(33(31(12(21(x1))))))) | → | 31(15(54(43(33(35(54(45(52(22(21(x1))))))))))) | (716) |
33(35(53(33(31(12(22(x1))))))) | → | 31(15(54(43(33(35(54(45(52(22(22(x1))))))))))) | (717) |
33(35(53(33(31(12(23(x1))))))) | → | 31(15(54(43(33(35(54(45(52(22(23(x1))))))))))) | (718) |
33(35(53(33(31(12(25(x1))))))) | → | 31(15(54(43(33(35(54(45(52(22(25(x1))))))))))) | (719) |
33(35(53(33(31(12(24(x1))))))) | → | 31(15(54(43(33(35(54(45(52(22(24(x1))))))))))) | (720) |
53(35(53(33(31(12(20(x1))))))) | → | 51(15(54(43(33(35(54(45(52(22(20(x1))))))))))) | (721) |
53(35(53(33(31(12(21(x1))))))) | → | 51(15(54(43(33(35(54(45(52(22(21(x1))))))))))) | (722) |
53(35(53(33(31(12(22(x1))))))) | → | 51(15(54(43(33(35(54(45(52(22(22(x1))))))))))) | (723) |
53(35(53(33(31(12(23(x1))))))) | → | 51(15(54(43(33(35(54(45(52(22(23(x1))))))))))) | (724) |
53(35(53(33(31(12(25(x1))))))) | → | 51(15(54(43(33(35(54(45(52(22(25(x1))))))))))) | (725) |
53(35(53(33(31(12(24(x1))))))) | → | 51(15(54(43(33(35(54(45(52(22(24(x1))))))))))) | (726) |
43(35(53(33(31(12(20(x1))))))) | → | 41(15(54(43(33(35(54(45(52(22(20(x1))))))))))) | (727) |
43(35(53(33(31(12(21(x1))))))) | → | 41(15(54(43(33(35(54(45(52(22(21(x1))))))))))) | (728) |
43(35(53(33(31(12(22(x1))))))) | → | 41(15(54(43(33(35(54(45(52(22(22(x1))))))))))) | (729) |
43(35(53(33(31(12(23(x1))))))) | → | 41(15(54(43(33(35(54(45(52(22(23(x1))))))))))) | (730) |
43(35(53(33(31(12(25(x1))))))) | → | 41(15(54(43(33(35(54(45(52(22(25(x1))))))))))) | (731) |
43(35(53(33(31(12(24(x1))))))) | → | 41(15(54(43(33(35(54(45(52(22(24(x1))))))))))) | (732) |
34(43(34(42(25(55(51(10(x1)))))))) | → | 35(52(20(04(41(13(30(01(11(11(10(x1))))))))))) | (1075) |
34(43(34(42(25(55(51(11(x1)))))))) | → | 35(52(20(04(41(13(30(01(11(11(11(x1))))))))))) | (1076) |
34(43(34(42(25(55(51(12(x1)))))))) | → | 35(52(20(04(41(13(30(01(11(11(12(x1))))))))))) | (1077) |
34(43(34(42(25(55(51(13(x1)))))))) | → | 35(52(20(04(41(13(30(01(11(11(13(x1))))))))))) | (1078) |
34(43(34(42(25(55(51(15(x1)))))))) | → | 35(52(20(04(41(13(30(01(11(11(15(x1))))))))))) | (1079) |
34(43(34(42(25(55(51(14(x1)))))))) | → | 35(52(20(04(41(13(30(01(11(11(14(x1))))))))))) | (1080) |
There are no rules in the TRS. Hence, it is terminating.