The relative rewrite relation R/S is considered where R is the following TRS
3(0(1(5(x1)))) | → | 0(0(5(2(3(2(2(4(3(5(x1)))))))))) | (1) |
3(4(0(1(x1)))) | → | 2(4(2(2(5(4(2(5(2(3(x1)))))))))) | (2) |
0(3(3(1(1(x1))))) | → | 0(0(0(3(4(5(4(3(5(1(x1)))))))))) | (3) |
1(5(5(5(4(x1))))) | → | 1(0(4(5(3(2(5(0(0(4(x1)))))))))) | (4) |
3(0(3(1(5(x1))))) | → | 0(4(5(3(1(5(3(5(3(5(x1)))))))))) | (5) |
3(4(1(5(5(x1))))) | → | 3(5(1(0(2(4(5(2(5(2(x1)))))))))) | (6) |
3(5(0(3(3(x1))))) | → | 3(5(4(2(5(2(4(5(2(3(x1)))))))))) | (7) |
5(4(0(2(1(x1))))) | → | 0(2(4(3(5(1(2(5(2(5(x1)))))))))) | (8) |
0(0(3(0(1(1(x1)))))) | → | 2(0(4(5(2(2(0(3(1(1(x1)))))))))) | (9) |
0(4(4(0(1(4(x1)))))) | → | 4(3(3(5(5(5(2(4(2(3(x1)))))))))) | (10) |
1(0(1(2(3(1(x1)))))) | → | 1(4(4(5(2(2(0(2(3(5(x1)))))))))) | (11) |
1(0(4(4(0(1(x1)))))) | → | 1(0(0(0(4(5(1(2(0(3(x1)))))))))) | (12) |
1(5(2(4(1(5(x1)))))) | → | 1(3(3(2(5(4(3(5(1(4(x1)))))))))) | (13) |
2(4(4(0(1(0(x1)))))) | → | 3(4(2(0(4(3(5(5(5(0(x1)))))))))) | (14) |
3(0(3(2(0(1(x1)))))) | → | 0(2(0(0(2(3(2(3(5(5(x1)))))))))) | (15) |
3(3(3(0(1(0(x1)))))) | → | 3(2(3(2(0(0(3(3(5(0(x1)))))))))) | (16) |
4(0(4(1(1(1(x1)))))) | → | 4(4(5(4(5(5(4(1(2(2(x1)))))))))) | (17) |
4(3(0(2(1(5(x1)))))) | → | 5(4(1(2(1(1(2(3(5(5(x1)))))))))) | (18) |
4(5(1(0(5(5(x1)))))) | → | 4(4(2(3(5(1(0(4(5(5(x1)))))))))) | (19) |
5(5(1(5(3(0(x1)))))) | → | 5(2(3(2(4(4(3(2(2(0(x1)))))))))) | (20) |
0(1(0(2(0(5(5(x1))))))) | → | 2(0(4(5(1(0(4(2(5(4(x1)))))))))) | (21) |
0(1(1(0(1(0(5(x1))))))) | → | 0(4(2(2(1(2(4(5(1(1(x1)))))))))) | (22) |
1(3(1(0(2(5(3(x1))))))) | → | 1(2(5(2(2(3(5(1(2(4(x1)))))))))) | (23) |
1(4(0(5(0(1(3(x1))))))) | → | 1(1(0(2(4(5(2(1(1(3(x1)))))))))) | (24) |
1(4(3(1(5(0(5(x1))))))) | → | 5(1(2(3(5(0(2(4(5(2(x1)))))))))) | (25) |
1(5(1(3(3(3(0(x1))))))) | → | 4(0(4(5(2(3(5(5(2(0(x1)))))))))) | (26) |
1(5(1(4(4(4(4(x1))))))) | → | 1(1(4(0(4(4(5(2(3(4(x1)))))))))) | (27) |
1(5(3(0(1(4(4(x1))))))) | → | 5(5(0(0(3(3(3(5(4(4(x1)))))))))) | (28) |
2(0(1(5(1(0(5(x1))))))) | → | 2(3(5(3(1(4(1(0(4(1(x1)))))))))) | (29) |
2(1(3(0(3(1(4(x1))))))) | → | 3(3(5(0(0(0(0(2(4(3(x1)))))))))) | (30) |
2(2(5(4(1(4(4(x1))))))) | → | 2(3(5(2(0(2(2(2(5(4(x1)))))))))) | (31) |
2(5(5(4(5(0(5(x1))))))) | → | 5(5(3(4(2(5(2(2(3(5(x1)))))))))) | (32) |
3(0(1(1(1(5(4(x1))))))) | → | 3(0(3(0(0(3(2(5(4(2(x1)))))))))) | (33) |
3(0(1(3(0(2(1(x1))))))) | → | 3(5(4(2(2(2(0(4(3(2(x1)))))))))) | (34) |
3(0(1(5(3(4(1(x1))))))) | → | 3(1(2(3(3(2(4(2(3(1(x1)))))))))) | (35) |
3(0(4(1(0(1(5(x1))))))) | → | 4(5(1(3(3(4(2(2(2(2(x1)))))))))) | (36) |
3(4(1(5(5(5(4(x1))))))) | → | 3(0(4(0(4(3(5(4(3(3(x1)))))))))) | (37) |
3(4(4(0(5(1(0(x1))))))) | → | 2(2(0(5(3(3(5(3(1(0(x1)))))))))) | (38) |
4(0(1(5(0(5(5(x1))))))) | → | 2(4(0(4(5(1(1(3(5(4(x1)))))))))) | (39) |
4(0(3(1(4(0(3(x1))))))) | → | 5(0(2(0(0(4(3(1(0(2(x1)))))))))) | (40) |
4(1(0(3(5(1(5(x1))))))) | → | 2(2(1(5(0(4(5(2(2(2(x1)))))))))) | (41) |
4(1(0(5(1(3(3(x1))))))) | → | 4(1(1(2(2(3(2(3(3(2(x1)))))))))) | (42) |
4(1(5(4(0(2(5(x1))))))) | → | 4(1(3(3(4(1(1(1(1(1(x1)))))))))) | (43) |
4(1(5(5(4(4(0(x1))))))) | → | 4(5(0(2(2(3(4(4(2(0(x1)))))))))) | (44) |
4(3(0(1(4(0(1(x1))))))) | → | 1(4(2(3(3(5(0(4(1(3(x1)))))))))) | (45) |
4(3(0(2(1(2(1(x1))))))) | → | 4(2(4(5(3(0(4(3(3(1(x1)))))))))) | (46) |
4(4(0(1(1(0(1(x1))))))) | → | 0(0(3(1(4(3(3(5(5(5(x1)))))))))) | (47) |
4(4(1(2(4(4(1(x1))))))) | → | 4(4(0(0(5(1(3(2(1(2(x1)))))))))) | (48) |
5(4(1(5(0(1(4(x1))))))) | → | 5(4(4(2(2(5(1(0(0(4(x1)))))))))) | (49) |
5(5(5(1(2(4(0(x1))))))) | → | 5(2(3(4(2(4(5(3(3(0(x1)))))))))) | (50) |
and S is the following TRS.
2(1(1(4(2(0(x1)))))) | → | 2(1(4(5(4(2(3(3(5(0(x1)))))))))) | (51) |
3(5(3(5(4(x1))))) | → | 2(2(3(2(5(2(2(3(5(4(x1)))))))))) | (52) |
3(1(0(3(4(x1))))) | → | 3(1(3(3(2(2(2(5(2(4(x1)))))))))) | (53) |
0(1(x1)) | → | 2(2(2(2(2(2(3(0(4(5(x1)))))))))) | (54) |
5(3(1(5(5(1(5(x1))))))) | → | 5(4(5(5(0(3(0(0(3(5(x1)))))))))) | (55) |
4(1(5(1(5(x1))))) | → | 2(4(2(3(3(3(3(1(5(2(x1)))))))))) | (56) |
1(5(4(4(1(0(1(x1))))))) | → | 5(4(5(0(5(3(2(5(0(1(x1)))))))))) | (57) |
1(1(5(x1))) | → | 1(4(2(2(5(5(3(4(3(5(x1)))))))))) | (58) |
3(0(1(x1))) | → | 4(5(0(3(0(2(0(4(3(5(x1)))))))))) | (59) |
5(4(0(0(4(x1))))) | → | 5(3(4(5(4(3(2(5(5(4(x1)))))))))) | (60) |
{3(☐), 0(☐), 1(☐), 5(☐), 2(☐), 4(☐)}
We obtain the transformed TRSThere are 195 ruless (increase limit for explicit display).
Root-labeling is applied.
We obtain the labeled TRSThere are 1170 ruless (increase limit for explicit display).
[03(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 + 1 · x1 |
[05(x1)] | = | 1 · x1 |
There are 582 ruless (increase limit for explicit display).
[03(x1)] | = | 1 + 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 + 1 · x1 |
[15(x1)] | = | 1 + 1 · x1 |
[12(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 + 1 · x1 |
[44(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 + 1 · x1 |
[24(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 + 1 · x1 |
[01(x1)] | = | 1 · x1 |
There are 427 ruless (increase limit for explicit display).
[03(x1)] | = | 1 + 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[00(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 + 1 · x1 |
[12(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 + 1 · x1 |
[50(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
40(04(41(11(11(10(x1)))))) | → | 44(45(54(45(55(54(41(12(22(20(x1)))))))))) | (271) |
13(31(10(02(25(53(31(x1))))))) | → | 12(25(52(22(23(35(51(12(24(41(x1)))))))))) | (297) |
41(15(54(40(02(25(54(x1))))))) | → | 41(13(33(34(41(11(11(11(11(14(x1)))))))))) | (358) |
35(54(40(02(21(10(x1)))))) | → | 30(02(24(43(35(51(12(25(52(25(50(x1))))))))))) | (499) |
55(54(40(02(21(10(x1)))))) | → | 50(02(24(43(35(51(12(25(52(25(50(x1))))))))))) | (517) |
25(54(40(02(21(10(x1)))))) | → | 20(02(24(43(35(51(12(25(52(25(50(x1))))))))))) | (523) |
45(54(40(02(21(10(x1)))))) | → | 40(02(24(43(35(51(12(25(52(25(50(x1))))))))))) | (529) |
11(15(51(13(33(33(30(00(x1)))))))) | → | 14(40(04(45(52(23(35(55(52(20(00(x1))))))))))) | (799) |
11(15(51(13(33(33(30(03(x1)))))))) | → | 14(40(04(45(52(23(35(55(52(20(03(x1))))))))))) | (800) |
11(15(51(13(33(33(30(01(x1)))))))) | → | 14(40(04(45(52(23(35(55(52(20(01(x1))))))))))) | (801) |
11(15(51(13(33(33(30(04(x1)))))))) | → | 14(40(04(45(52(23(35(55(52(20(04(x1))))))))))) | (802) |
11(15(51(13(33(33(30(05(x1)))))))) | → | 14(40(04(45(52(23(35(55(52(20(05(x1))))))))))) | (803) |
11(15(51(13(33(33(30(02(x1)))))))) | → | 14(40(04(45(52(23(35(55(52(20(02(x1))))))))))) | (804) |
03(34(44(40(05(51(10(00(x1)))))))) | → | 02(22(20(05(53(33(35(53(31(10(00(x1))))))))))) | (973) |
03(34(44(40(05(51(10(03(x1)))))))) | → | 02(22(20(05(53(33(35(53(31(10(03(x1))))))))))) | (974) |
03(34(44(40(05(51(10(01(x1)))))))) | → | 02(22(20(05(53(33(35(53(31(10(01(x1))))))))))) | (975) |
03(34(44(40(05(51(10(04(x1)))))))) | → | 02(22(20(05(53(33(35(53(31(10(04(x1))))))))))) | (976) |
03(34(44(40(05(51(10(05(x1)))))))) | → | 02(22(20(05(53(33(35(53(31(10(05(x1))))))))))) | (977) |
03(34(44(40(05(51(10(02(x1)))))))) | → | 02(22(20(05(53(33(35(53(31(10(02(x1))))))))))) | (978) |
11(15(50(x1))) | → | 14(42(22(25(55(53(34(43(35(50(x1)))))))))) | (1201) |
11(15(53(x1))) | → | 14(42(22(25(55(53(34(43(35(53(x1)))))))))) | (1202) |
11(15(51(x1))) | → | 14(42(22(25(55(53(34(43(35(51(x1)))))))))) | (1203) |
11(15(54(x1))) | → | 14(42(22(25(55(53(34(43(35(54(x1)))))))))) | (1204) |
11(15(55(x1))) | → | 14(42(22(25(55(53(34(43(35(55(x1)))))))))) | (1205) |
11(15(52(x1))) | → | 14(42(22(25(55(53(34(43(35(52(x1)))))))))) | (1206) |
03(35(53(35(54(40(x1)))))) | → | 02(22(23(32(25(52(22(23(35(54(40(x1))))))))))) | (1219) |
03(35(53(35(54(43(x1)))))) | → | 02(22(23(32(25(52(22(23(35(54(43(x1))))))))))) | (1220) |
03(35(53(35(54(41(x1)))))) | → | 02(22(23(32(25(52(22(23(35(54(41(x1))))))))))) | (1221) |
03(35(53(35(54(44(x1)))))) | → | 02(22(23(32(25(52(22(23(35(54(44(x1))))))))))) | (1222) |
03(35(53(35(54(45(x1)))))) | → | 02(22(23(32(25(52(22(23(35(54(45(x1))))))))))) | (1223) |
03(35(53(35(54(42(x1)))))) | → | 02(22(23(32(25(52(22(23(35(54(42(x1))))))))))) | (1224) |
[03(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[00(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 + 1 · x1 |
[14(x1)] | = | 1 + 1 · x1 |
[15(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[41(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 + 1 · x1 |
[55(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[24(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 + 1 · x1 |
[30(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 + 1 · x1 |
[50(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
40(04(41(11(11(13(x1)))))) | → | 44(45(54(45(55(54(41(12(22(23(x1)))))))))) | (272) |
40(04(41(11(11(11(x1)))))) | → | 44(45(54(45(55(54(41(12(22(21(x1)))))))))) | (273) |
40(04(41(11(11(12(x1)))))) | → | 44(45(54(45(55(54(41(12(22(22(x1)))))))))) | (276) |
35(54(40(02(21(13(x1)))))) | → | 30(02(24(43(35(51(12(25(52(25(53(x1))))))))))) | (500) |
35(54(40(02(21(11(x1)))))) | → | 30(02(24(43(35(51(12(25(52(25(51(x1))))))))))) | (501) |
35(54(40(02(21(12(x1)))))) | → | 30(02(24(43(35(51(12(25(52(25(52(x1))))))))))) | (504) |
55(54(40(02(21(13(x1)))))) | → | 50(02(24(43(35(51(12(25(52(25(53(x1))))))))))) | (518) |
55(54(40(02(21(11(x1)))))) | → | 50(02(24(43(35(51(12(25(52(25(51(x1))))))))))) | (519) |
55(54(40(02(21(12(x1)))))) | → | 50(02(24(43(35(51(12(25(52(25(52(x1))))))))))) | (522) |
25(54(40(02(21(13(x1)))))) | → | 20(02(24(43(35(51(12(25(52(25(53(x1))))))))))) | (524) |
25(54(40(02(21(11(x1)))))) | → | 20(02(24(43(35(51(12(25(52(25(51(x1))))))))))) | (525) |
25(54(40(02(21(12(x1)))))) | → | 20(02(24(43(35(51(12(25(52(25(52(x1))))))))))) | (528) |
13(34(44(40(05(51(10(00(x1)))))))) | → | 12(22(20(05(53(33(35(53(31(10(00(x1))))))))))) | (979) |
13(34(44(40(05(51(10(03(x1)))))))) | → | 12(22(20(05(53(33(35(53(31(10(03(x1))))))))))) | (980) |
13(34(44(40(05(51(10(01(x1)))))))) | → | 12(22(20(05(53(33(35(53(31(10(01(x1))))))))))) | (981) |
13(34(44(40(05(51(10(04(x1)))))))) | → | 12(22(20(05(53(33(35(53(31(10(04(x1))))))))))) | (982) |
13(34(44(40(05(51(10(05(x1)))))))) | → | 12(22(20(05(53(33(35(53(31(10(05(x1))))))))))) | (983) |
13(34(44(40(05(51(10(02(x1)))))))) | → | 12(22(20(05(53(33(35(53(31(10(02(x1))))))))))) | (984) |
53(34(44(40(05(51(10(00(x1)))))))) | → | 52(22(20(05(53(33(35(53(31(10(00(x1))))))))))) | (985) |
53(34(44(40(05(51(10(03(x1)))))))) | → | 52(22(20(05(53(33(35(53(31(10(03(x1))))))))))) | (986) |
53(34(44(40(05(51(10(01(x1)))))))) | → | 52(22(20(05(53(33(35(53(31(10(01(x1))))))))))) | (987) |
53(34(44(40(05(51(10(04(x1)))))))) | → | 52(22(20(05(53(33(35(53(31(10(04(x1))))))))))) | (988) |
53(34(44(40(05(51(10(05(x1)))))))) | → | 52(22(20(05(53(33(35(53(31(10(05(x1))))))))))) | (989) |
53(34(44(40(05(51(10(02(x1)))))))) | → | 52(22(20(05(53(33(35(53(31(10(02(x1))))))))))) | (990) |
04(40(03(31(14(40(03(30(x1)))))))) | → | 05(50(02(20(00(04(43(31(10(02(20(x1))))))))))) | (1045) |
04(40(03(31(14(40(03(33(x1)))))))) | → | 05(50(02(20(00(04(43(31(10(02(23(x1))))))))))) | (1046) |
04(40(03(31(14(40(03(31(x1)))))))) | → | 05(50(02(20(00(04(43(31(10(02(21(x1))))))))))) | (1047) |
04(40(03(31(14(40(03(34(x1)))))))) | → | 05(50(02(20(00(04(43(31(10(02(24(x1))))))))))) | (1048) |
04(40(03(31(14(40(03(35(x1)))))))) | → | 05(50(02(20(00(04(43(31(10(02(25(x1))))))))))) | (1049) |
04(40(03(31(14(40(03(32(x1)))))))) | → | 05(50(02(20(00(04(43(31(10(02(22(x1))))))))))) | (1050) |
53(31(15(55(51(15(50(x1))))))) | → | 54(45(55(50(03(30(00(03(35(50(x1)))))))))) | (1195) |
53(31(15(55(51(15(53(x1))))))) | → | 54(45(55(50(03(30(00(03(35(53(x1)))))))))) | (1196) |
53(31(15(55(51(15(51(x1))))))) | → | 54(45(55(50(03(30(00(03(35(51(x1)))))))))) | (1197) |
53(31(15(55(51(15(54(x1))))))) | → | 54(45(55(50(03(30(00(03(35(54(x1)))))))))) | (1198) |
53(31(15(55(51(15(55(x1))))))) | → | 54(45(55(50(03(30(00(03(35(55(x1)))))))))) | (1199) |
53(31(15(55(51(15(52(x1))))))) | → | 54(45(55(50(03(30(00(03(35(52(x1)))))))))) | (1200) |
54(40(00(04(40(x1))))) | → | 53(34(45(54(43(32(25(55(54(40(x1)))))))))) | (1207) |
54(40(00(04(43(x1))))) | → | 53(34(45(54(43(32(25(55(54(43(x1)))))))))) | (1208) |
54(40(00(04(41(x1))))) | → | 53(34(45(54(43(32(25(55(54(41(x1)))))))))) | (1209) |
54(40(00(04(44(x1))))) | → | 53(34(45(54(43(32(25(55(54(44(x1)))))))))) | (1210) |
54(40(00(04(45(x1))))) | → | 53(34(45(54(43(32(25(55(54(45(x1)))))))))) | (1211) |
54(40(00(04(42(x1))))) | → | 53(34(45(54(43(32(25(55(54(42(x1)))))))))) | (1212) |
33(35(53(35(54(40(x1)))))) | → | 32(22(23(32(25(52(22(23(35(54(40(x1))))))))))) | (1213) |
33(35(53(35(54(43(x1)))))) | → | 32(22(23(32(25(52(22(23(35(54(43(x1))))))))))) | (1214) |
33(35(53(35(54(41(x1)))))) | → | 32(22(23(32(25(52(22(23(35(54(41(x1))))))))))) | (1215) |
33(35(53(35(54(44(x1)))))) | → | 32(22(23(32(25(52(22(23(35(54(44(x1))))))))))) | (1216) |
33(35(53(35(54(45(x1)))))) | → | 32(22(23(32(25(52(22(23(35(54(45(x1))))))))))) | (1217) |
33(35(53(35(54(42(x1)))))) | → | 32(22(23(32(25(52(22(23(35(54(42(x1))))))))))) | (1218) |
13(35(53(35(54(40(x1)))))) | → | 12(22(23(32(25(52(22(23(35(54(40(x1))))))))))) | (1225) |
13(35(53(35(54(43(x1)))))) | → | 12(22(23(32(25(52(22(23(35(54(43(x1))))))))))) | (1226) |
13(35(53(35(54(41(x1)))))) | → | 12(22(23(32(25(52(22(23(35(54(41(x1))))))))))) | (1227) |
13(35(53(35(54(44(x1)))))) | → | 12(22(23(32(25(52(22(23(35(54(44(x1))))))))))) | (1228) |
13(35(53(35(54(45(x1)))))) | → | 12(22(23(32(25(52(22(23(35(54(45(x1))))))))))) | (1229) |
13(35(53(35(54(42(x1)))))) | → | 12(22(23(32(25(52(22(23(35(54(42(x1))))))))))) | (1230) |
53(35(53(35(54(40(x1)))))) | → | 52(22(23(32(25(52(22(23(35(54(40(x1))))))))))) | (1231) |
53(35(53(35(54(43(x1)))))) | → | 52(22(23(32(25(52(22(23(35(54(43(x1))))))))))) | (1232) |
53(35(53(35(54(41(x1)))))) | → | 52(22(23(32(25(52(22(23(35(54(41(x1))))))))))) | (1233) |
53(35(53(35(54(44(x1)))))) | → | 52(22(23(32(25(52(22(23(35(54(44(x1))))))))))) | (1234) |
53(35(53(35(54(45(x1)))))) | → | 52(22(23(32(25(52(22(23(35(54(45(x1))))))))))) | (1235) |
53(35(53(35(54(42(x1)))))) | → | 52(22(23(32(25(52(22(23(35(54(42(x1))))))))))) | (1236) |
23(35(53(35(54(40(x1)))))) | → | 22(22(23(32(25(52(22(23(35(54(40(x1))))))))))) | (1237) |
23(35(53(35(54(43(x1)))))) | → | 22(22(23(32(25(52(22(23(35(54(43(x1))))))))))) | (1238) |
23(35(53(35(54(41(x1)))))) | → | 22(22(23(32(25(52(22(23(35(54(41(x1))))))))))) | (1239) |
23(35(53(35(54(44(x1)))))) | → | 22(22(23(32(25(52(22(23(35(54(44(x1))))))))))) | (1240) |
23(35(53(35(54(45(x1)))))) | → | 22(22(23(32(25(52(22(23(35(54(45(x1))))))))))) | (1241) |
23(35(53(35(54(42(x1)))))) | → | 22(22(23(32(25(52(22(23(35(54(42(x1))))))))))) | (1242) |
43(35(53(35(54(40(x1)))))) | → | 42(22(23(32(25(52(22(23(35(54(40(x1))))))))))) | (1243) |
43(35(53(35(54(43(x1)))))) | → | 42(22(23(32(25(52(22(23(35(54(43(x1))))))))))) | (1244) |
43(35(53(35(54(41(x1)))))) | → | 42(22(23(32(25(52(22(23(35(54(41(x1))))))))))) | (1245) |
43(35(53(35(54(44(x1)))))) | → | 42(22(23(32(25(52(22(23(35(54(44(x1))))))))))) | (1246) |
43(35(53(35(54(45(x1)))))) | → | 42(22(23(32(25(52(22(23(35(54(45(x1))))))))))) | (1247) |
43(35(53(35(54(42(x1)))))) | → | 42(22(23(32(25(52(22(23(35(54(42(x1))))))))))) | (1248) |
[03(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 + 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[00(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 + 1 · x1 |
[54(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 + 1 · x1 |
[12(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[02(x1)] | = | 1 + 1 · x1 |
[25(x1)] | = | 1 + 1 · x1 |
[55(x1)] | = | 1 + 1 · x1 |
[24(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 + 1 · x1 |
[05(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 + 1 · x1 |
[50(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 + 1 · x1 |
55(55(51(12(24(40(00(x1))))))) | → | 52(23(34(42(24(45(53(33(30(00(x1)))))))))) | (385) |
55(55(51(12(24(40(03(x1))))))) | → | 52(23(34(42(24(45(53(33(30(03(x1)))))))))) | (386) |
55(55(51(12(24(40(01(x1))))))) | → | 52(23(34(42(24(45(53(33(30(01(x1)))))))))) | (387) |
55(55(51(12(24(40(04(x1))))))) | → | 52(23(34(42(24(45(53(33(30(04(x1)))))))))) | (388) |
55(55(51(12(24(40(05(x1))))))) | → | 52(23(34(42(24(45(53(33(30(05(x1)))))))))) | (389) |
55(55(51(12(24(40(02(x1))))))) | → | 52(23(34(42(24(45(53(33(30(02(x1)))))))))) | (390) |
45(54(40(02(21(11(x1)))))) | → | 40(02(24(43(35(51(12(25(52(25(51(x1))))))))))) | (531) |
04(43(30(02(21(15(50(x1))))))) | → | 05(54(41(12(21(11(12(23(35(55(50(x1))))))))))) | (685) |
04(43(30(02(21(15(53(x1))))))) | → | 05(54(41(12(21(11(12(23(35(55(53(x1))))))))))) | (686) |
04(43(30(02(21(15(51(x1))))))) | → | 05(54(41(12(21(11(12(23(35(55(51(x1))))))))))) | (687) |
04(43(30(02(21(15(54(x1))))))) | → | 05(54(41(12(21(11(12(23(35(55(54(x1))))))))))) | (688) |
04(43(30(02(21(15(55(x1))))))) | → | 05(54(41(12(21(11(12(23(35(55(55(x1))))))))))) | (689) |
04(43(30(02(21(15(52(x1))))))) | → | 05(54(41(12(21(11(12(23(35(55(52(x1))))))))))) | (690) |
21(11(14(42(20(00(x1)))))) | → | 21(14(45(54(42(23(33(35(50(00(x1)))))))))) | (1183) |
21(11(14(42(20(03(x1)))))) | → | 21(14(45(54(42(23(33(35(50(03(x1)))))))))) | (1184) |
21(11(14(42(20(01(x1)))))) | → | 21(14(45(54(42(23(33(35(50(01(x1)))))))))) | (1185) |
21(11(14(42(20(04(x1)))))) | → | 21(14(45(54(42(23(33(35(50(04(x1)))))))))) | (1186) |
21(11(14(42(20(05(x1)))))) | → | 21(14(45(54(42(23(33(35(50(05(x1)))))))))) | (1187) |
21(11(14(42(20(02(x1)))))) | → | 21(14(45(54(42(23(33(35(50(02(x1)))))))))) | (1188) |
[03(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 + 1 · x1 |
[31(x1)] | = | 1 + 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 + 1 · x1 |
[00(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 + 1 · x1 |
[54(x1)] | = | 1 + 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[02(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
[55(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 + 1 · x1 |
[24(x1)] | = | 1 · x1 |
[52(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[50(x1)] | = | 1 · x1 |
[05(x1)] | = | 1 + 1 · x1 |
[42(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[44(x1)] | = | 1 + 1 · x1 |
[32(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
41(15(54(40(02(25(55(x1))))))) | → | 41(13(33(34(41(11(11(11(11(15(x1)))))))))) | (359) |
45(54(40(02(21(13(x1)))))) | → | 40(02(24(43(35(51(12(25(52(25(53(x1))))))))))) | (530) |
45(54(40(02(21(12(x1)))))) | → | 40(02(24(43(35(51(12(25(52(25(52(x1))))))))))) | (534) |
12(25(55(54(45(50(05(50(x1)))))))) | → | 15(55(53(34(42(25(52(22(23(35(50(x1))))))))))) | (907) |
12(25(55(54(45(50(05(53(x1)))))))) | → | 15(55(53(34(42(25(52(22(23(35(53(x1))))))))))) | (908) |
12(25(55(54(45(50(05(51(x1)))))))) | → | 15(55(53(34(42(25(52(22(23(35(51(x1))))))))))) | (909) |
12(25(55(54(45(50(05(54(x1)))))))) | → | 15(55(53(34(42(25(52(22(23(35(54(x1))))))))))) | (910) |
12(25(55(54(45(50(05(55(x1)))))))) | → | 15(55(53(34(42(25(52(22(23(35(55(x1))))))))))) | (911) |
12(25(55(54(45(50(05(52(x1)))))))) | → | 15(55(53(34(42(25(52(22(23(35(52(x1))))))))))) | (912) |
33(34(44(40(05(51(10(00(x1)))))))) | → | 32(22(20(05(53(33(35(53(31(10(00(x1))))))))))) | (967) |
33(34(44(40(05(51(10(03(x1)))))))) | → | 32(22(20(05(53(33(35(53(31(10(03(x1))))))))))) | (968) |
33(34(44(40(05(51(10(01(x1)))))))) | → | 32(22(20(05(53(33(35(53(31(10(01(x1))))))))))) | (969) |
33(34(44(40(05(51(10(04(x1)))))))) | → | 32(22(20(05(53(33(35(53(31(10(04(x1))))))))))) | (970) |
33(34(44(40(05(51(10(05(x1)))))))) | → | 32(22(20(05(53(33(35(53(31(10(05(x1))))))))))) | (971) |
33(34(44(40(05(51(10(02(x1)))))))) | → | 32(22(20(05(53(33(35(53(31(10(02(x1))))))))))) | (972) |
[03(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 + 1 · x1 |
[10(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 + 1 · x1 |
[35(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 + 1 · x1 |
[44(x1)] | = | 1 + 1 · x1 |
[40(x1)] | = | 1 + 1 · x1 |
[05(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[53(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[04(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[42(x1)] | = | 1 · x1 |
[41(x1)] | = | 1 + 1 · x1 |
[50(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[25(x1)] | = | 1 · x1 |
23(34(44(40(05(51(10(00(x1)))))))) | → | 22(22(20(05(53(33(35(53(31(10(00(x1))))))))))) | (991) |
23(34(44(40(05(51(10(03(x1)))))))) | → | 22(22(20(05(53(33(35(53(31(10(03(x1))))))))))) | (992) |
23(34(44(40(05(51(10(01(x1)))))))) | → | 22(22(20(05(53(33(35(53(31(10(01(x1))))))))))) | (993) |
23(34(44(40(05(51(10(04(x1)))))))) | → | 22(22(20(05(53(33(35(53(31(10(04(x1))))))))))) | (994) |
23(34(44(40(05(51(10(05(x1)))))))) | → | 22(22(20(05(53(33(35(53(31(10(05(x1))))))))))) | (995) |
23(34(44(40(05(51(10(02(x1)))))))) | → | 22(22(20(05(53(33(35(53(31(10(02(x1))))))))))) | (996) |
43(34(44(40(05(51(10(00(x1)))))))) | → | 42(22(20(05(53(33(35(53(31(10(00(x1))))))))))) | (997) |
43(34(44(40(05(51(10(03(x1)))))))) | → | 42(22(20(05(53(33(35(53(31(10(03(x1))))))))))) | (998) |
43(34(44(40(05(51(10(01(x1)))))))) | → | 42(22(20(05(53(33(35(53(31(10(01(x1))))))))))) | (999) |
43(34(44(40(05(51(10(04(x1)))))))) | → | 42(22(20(05(53(33(35(53(31(10(04(x1))))))))))) | (1000) |
43(34(44(40(05(51(10(05(x1)))))))) | → | 42(22(20(05(53(33(35(53(31(10(05(x1))))))))))) | (1001) |
43(34(44(40(05(51(10(02(x1)))))))) | → | 42(22(20(05(53(33(35(53(31(10(02(x1))))))))))) | (1002) |
11(15(54(44(41(10(01(10(x1)))))))) | → | 15(54(45(50(05(53(32(25(50(01(10(x1))))))))))) | (1333) |
11(15(54(44(41(10(01(13(x1)))))))) | → | 15(54(45(50(05(53(32(25(50(01(13(x1))))))))))) | (1334) |
11(15(54(44(41(10(01(11(x1)))))))) | → | 15(54(45(50(05(53(32(25(50(01(11(x1))))))))))) | (1335) |
11(15(54(44(41(10(01(14(x1)))))))) | → | 15(54(45(50(05(53(32(25(50(01(14(x1))))))))))) | (1336) |
11(15(54(44(41(10(01(15(x1)))))))) | → | 15(54(45(50(05(53(32(25(50(01(15(x1))))))))))) | (1337) |
11(15(54(44(41(10(01(12(x1)))))))) | → | 15(54(45(50(05(53(32(25(50(01(12(x1))))))))))) | (1338) |
[03(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 + 1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[34(x1)] | = | 1 · x1 |
[45(x1)] | = | 1 · x1 |
[54(x1)] | = | 1 · x1 |
[43(x1)] | = | 1 · x1 |
[35(x1)] | = | 1 · x1 |
[51(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[14(x1)] | = | 1 · x1 |
[15(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
03(33(31(11(10(x1))))) | → | 00(00(03(34(45(54(43(35(51(10(x1)))))))))) | (223) |
03(33(31(11(13(x1))))) | → | 00(00(03(34(45(54(43(35(51(13(x1)))))))))) | (224) |
03(33(31(11(11(x1))))) | → | 00(00(03(34(45(54(43(35(51(11(x1)))))))))) | (225) |
03(33(31(11(14(x1))))) | → | 00(00(03(34(45(54(43(35(51(14(x1)))))))))) | (226) |
03(33(31(11(15(x1))))) | → | 00(00(03(34(45(54(43(35(51(15(x1)))))))))) | (227) |
03(33(31(11(12(x1))))) | → | 00(00(03(34(45(54(43(35(51(12(x1)))))))))) | (228) |
There are no rules in the TRS. Hence, it is terminating.