The rewrite relation of the following TRS is considered.
0(0(1(1(2(0(3(0(1(2(0(1(1(x1))))))))))))) | → | 0(0(3(0(0(2(0(2(2(0(0(1(0(0(0(1(0(x1))))))))))))))))) | (1) |
0(1(0(3(1(0(2(2(1(1(0(2(1(x1))))))))))))) | → | 0(0(2(2(3(0(0(0(0(1(0(1(0(3(0(1(2(x1))))))))))))))))) | (2) |
0(1(1(0(0(1(3(1(2(0(3(1(2(x1))))))))))))) | → | 0(2(0(2(0(1(3(0(2(0(0(0(0(1(2(2(0(x1))))))))))))))))) | (3) |
0(1(3(2(1(0(3(0(0(1(1(1(1(x1))))))))))))) | → | 0(3(1(3(1(0(0(3(2(0(3(0(3(0(0(1(0(x1))))))))))))))))) | (4) |
0(2(0(2(0(2(3(2(3(1(1(3(1(x1))))))))))))) | → | 0(0(1(3(0(0(3(0(3(2(3(0(0(2(2(1(0(x1))))))))))))))))) | (5) |
0(2(2(3(2(2(1(2(0(3(2(0(3(x1))))))))))))) | → | 0(3(2(1(0(2(3(0(0(1(0(2(1(0(0(3(0(x1))))))))))))))))) | (6) |
0(2(3(0(2(2(3(2(2(1(1(2(3(x1))))))))))))) | → | 1(0(0(2(3(2(0(2(0(1(3(0(2(0(1(1(2(x1))))))))))))))))) | (7) |
0(2(3(1(1(0(2(0(0(2(1(3(2(x1))))))))))))) | → | 0(2(2(0(0(3(2(2(0(1(2(2(0(0(2(2(0(x1))))))))))))))))) | (8) |
0(2(3(2(2(3(1(0(2(0(3(1(3(x1))))))))))))) | → | 0(0(3(0(2(1(1(0(0(2(2(0(2(0(2(2(3(x1))))))))))))))))) | (9) |
1(0(0(3(2(0(1(0(1(2(2(1(1(x1))))))))))))) | → | 0(0(3(3(1(0(0(0(2(0(2(0(1(0(0(1(2(x1))))))))))))))))) | (10) |
1(0(3(0(2(1(1(0(1(1(1(2(2(x1))))))))))))) | → | 0(3(2(0(0(2(0(0(3(0(0(0(3(3(3(3(3(x1))))))))))))))))) | (11) |
1(1(2(0(2(2(0(0(1(3(2(3(2(x1))))))))))))) | → | 2(0(0(0(0(1(2(3(0(1(0(0(3(2(0(0(1(x1))))))))))))))))) | (12) |
1(2(2(1(2(2(0(0(1(2(2(0(1(x1))))))))))))) | → | 0(0(3(0(0(1(2(2(0(3(2(0(2(0(1(0(3(x1))))))))))))))))) | (13) |
1(2(3(1(0(2(1(0(0(1(1(1(0(x1))))))))))))) | → | 0(3(0(1(0(1(2(0(3(0(0(0(1(0(1(3(0(x1))))))))))))))))) | (14) |
1(3(0(0(3(2(2(2(2(1(0(2(3(x1))))))))))))) | → | 3(0(0(2(2(0(3(2(0(3(0(2(3(1(2(0(0(x1))))))))))))))))) | (15) |
1(3(1(0(1(3(1(2(0(1(3(1(0(x1))))))))))))) | → | 1(2(0(3(1(3(0(0(3(3(1(0(3(0(0(0(0(x1))))))))))))))))) | (16) |
1(3(1(1(3(0(0(1(0(0(2(3(0(x1))))))))))))) | → | 2(1(0(2(0(3(2(0(0(0(0(2(0(1(1(3(0(x1))))))))))))))))) | (17) |
1(3(1(3(1(0(2(0(1(3(0(0(1(x1))))))))))))) | → | 2(2(0(0(0(1(0(0(2(0(0(1(3(3(3(0(1(x1))))))))))))))))) | (18) |
1(3(2(1(0(1(0(3(0(1(3(0(0(x1))))))))))))) | → | 0(3(1(0(0(0(3(0(0(2(3(2(1(0(1(0(0(x1))))))))))))))))) | (19) |
1(3(3(0(2(3(0(3(2(0(0(1(1(x1))))))))))))) | → | 3(2(0(3(0(3(0(0(2(0(0(0(1(0(2(3(1(x1))))))))))))))))) | (20) |
1(3(3(2(2(2(3(2(2(0(2(3(0(x1))))))))))))) | → | 3(0(3(2(2(0(2(2(1(0(2(2(3(1(2(0(0(x1))))))))))))))))) | (21) |
2(0(2(1(2(2(3(2(2(2(2(1(0(x1))))))))))))) | → | 1(0(0(0(0(1(0(0(2(0(3(1(0(0(2(3(0(x1))))))))))))))))) | (22) |
2(0(2(2(1(2(2(3(2(0(1(1(2(x1))))))))))))) | → | 0(2(3(1(3(1(0(0(0(0(0(0(1(2(2(1(0(x1))))))))))))))))) | (23) |
2(0(3(3(1(2(2(0(0(2(1(0(1(x1))))))))))))) | → | 3(2(0(1(0(0(2(0(3(1(0(0(0(2(1(0(2(x1))))))))))))))))) | (24) |
2(1(1(0(3(2(1(2(0(0(3(1(3(x1))))))))))))) | → | 2(2(0(1(0(0(0(0(2(2(0(0(2(2(1(3(3(x1))))))))))))))))) | (25) |
2(2(0(1(0(1(0(3(3(2(1(2(3(x1))))))))))))) | → | 0(3(0(1(2(0(1(2(0(2(2(1(2(1(0(0(0(x1))))))))))))))))) | (26) |
2(3(0(0(0(2(3(3(2(0(3(0(3(x1))))))))))))) | → | 2(2(0(0(0(1(2(0(0(0(3(0(2(0(3(2(0(x1))))))))))))))))) | (27) |
2(3(0(2(2(0(2(0(3(2(3(2(3(x1))))))))))))) | → | 1(0(0(3(2(0(3(3(0(0(3(0(0(2(0(0(2(x1))))))))))))))))) | (28) |
3(0(0(1(3(1(2(0(2(0(3(3(3(x1))))))))))))) | → | 0(0(1(0(1(2(0(0(3(0(2(2(2(0(0(1(3(x1))))))))))))))))) | (29) |
3(2(2(2(0(1(3(0(2(2(3(3(0(x1))))))))))))) | → | 1(1(0(1(0(0(3(0(1(2(1(1(0(0(1(0(0(x1))))))))))))))))) | (30) |
{0(☐), 1(☐), 2(☐), 3(☐)}
We obtain the transformed TRS0(0(1(1(2(0(3(0(1(2(0(1(1(x1))))))))))))) | → | 0(0(3(0(0(2(0(2(2(0(0(1(0(0(0(1(0(x1))))))))))))))))) | (1) |
0(1(0(3(1(0(2(2(1(1(0(2(1(x1))))))))))))) | → | 0(0(2(2(3(0(0(0(0(1(0(1(0(3(0(1(2(x1))))))))))))))))) | (2) |
0(1(1(0(0(1(3(1(2(0(3(1(2(x1))))))))))))) | → | 0(2(0(2(0(1(3(0(2(0(0(0(0(1(2(2(0(x1))))))))))))))))) | (3) |
0(1(3(2(1(0(3(0(0(1(1(1(1(x1))))))))))))) | → | 0(3(1(3(1(0(0(3(2(0(3(0(3(0(0(1(0(x1))))))))))))))))) | (4) |
0(2(0(2(0(2(3(2(3(1(1(3(1(x1))))))))))))) | → | 0(0(1(3(0(0(3(0(3(2(3(0(0(2(2(1(0(x1))))))))))))))))) | (5) |
0(2(2(3(2(2(1(2(0(3(2(0(3(x1))))))))))))) | → | 0(3(2(1(0(2(3(0(0(1(0(2(1(0(0(3(0(x1))))))))))))))))) | (6) |
0(2(3(1(1(0(2(0(0(2(1(3(2(x1))))))))))))) | → | 0(2(2(0(0(3(2(2(0(1(2(2(0(0(2(2(0(x1))))))))))))))))) | (8) |
0(2(3(2(2(3(1(0(2(0(3(1(3(x1))))))))))))) | → | 0(0(3(0(2(1(1(0(0(2(2(0(2(0(2(2(3(x1))))))))))))))))) | (9) |
1(3(1(0(1(3(1(2(0(1(3(1(0(x1))))))))))))) | → | 1(2(0(3(1(3(0(0(3(3(1(0(3(0(0(0(0(x1))))))))))))))))) | (16) |
2(1(1(0(3(2(1(2(0(0(3(1(3(x1))))))))))))) | → | 2(2(0(1(0(0(0(0(2(2(0(0(2(2(1(3(3(x1))))))))))))))))) | (25) |
2(3(0(0(0(2(3(3(2(0(3(0(3(x1))))))))))))) | → | 2(2(0(0(0(1(2(0(0(0(3(0(2(0(3(2(0(x1))))))))))))))))) | (27) |
0(0(2(3(0(2(2(3(2(2(1(1(2(3(x1)))))))))))))) | → | 0(1(0(0(2(3(2(0(2(0(1(3(0(2(0(1(1(2(x1)))))))))))))))))) | (31) |
1(0(2(3(0(2(2(3(2(2(1(1(2(3(x1)))))))))))))) | → | 1(1(0(0(2(3(2(0(2(0(1(3(0(2(0(1(1(2(x1)))))))))))))))))) | (32) |
2(0(2(3(0(2(2(3(2(2(1(1(2(3(x1)))))))))))))) | → | 2(1(0(0(2(3(2(0(2(0(1(3(0(2(0(1(1(2(x1)))))))))))))))))) | (33) |
3(0(2(3(0(2(2(3(2(2(1(1(2(3(x1)))))))))))))) | → | 3(1(0(0(2(3(2(0(2(0(1(3(0(2(0(1(1(2(x1)))))))))))))))))) | (34) |
0(1(0(0(3(2(0(1(0(1(2(2(1(1(x1)))))))))))))) | → | 0(0(0(3(3(1(0(0(0(2(0(2(0(1(0(0(1(2(x1)))))))))))))))))) | (35) |
1(1(0(0(3(2(0(1(0(1(2(2(1(1(x1)))))))))))))) | → | 1(0(0(3(3(1(0(0(0(2(0(2(0(1(0(0(1(2(x1)))))))))))))))))) | (36) |
2(1(0(0(3(2(0(1(0(1(2(2(1(1(x1)))))))))))))) | → | 2(0(0(3(3(1(0(0(0(2(0(2(0(1(0(0(1(2(x1)))))))))))))))))) | (37) |
3(1(0(0(3(2(0(1(0(1(2(2(1(1(x1)))))))))))))) | → | 3(0(0(3(3(1(0(0(0(2(0(2(0(1(0(0(1(2(x1)))))))))))))))))) | (38) |
0(1(0(3(0(2(1(1(0(1(1(1(2(2(x1)))))))))))))) | → | 0(0(3(2(0(0(2(0(0(3(0(0(0(3(3(3(3(3(x1)))))))))))))))))) | (39) |
1(1(0(3(0(2(1(1(0(1(1(1(2(2(x1)))))))))))))) | → | 1(0(3(2(0(0(2(0(0(3(0(0(0(3(3(3(3(3(x1)))))))))))))))))) | (40) |
2(1(0(3(0(2(1(1(0(1(1(1(2(2(x1)))))))))))))) | → | 2(0(3(2(0(0(2(0(0(3(0(0(0(3(3(3(3(3(x1)))))))))))))))))) | (41) |
3(1(0(3(0(2(1(1(0(1(1(1(2(2(x1)))))))))))))) | → | 3(0(3(2(0(0(2(0(0(3(0(0(0(3(3(3(3(3(x1)))))))))))))))))) | (42) |
0(1(1(2(0(2(2(0(0(1(3(2(3(2(x1)))))))))))))) | → | 0(2(0(0(0(0(1(2(3(0(1(0(0(3(2(0(0(1(x1)))))))))))))))))) | (43) |
1(1(1(2(0(2(2(0(0(1(3(2(3(2(x1)))))))))))))) | → | 1(2(0(0(0(0(1(2(3(0(1(0(0(3(2(0(0(1(x1)))))))))))))))))) | (44) |
2(1(1(2(0(2(2(0(0(1(3(2(3(2(x1)))))))))))))) | → | 2(2(0(0(0(0(1(2(3(0(1(0(0(3(2(0(0(1(x1)))))))))))))))))) | (45) |
3(1(1(2(0(2(2(0(0(1(3(2(3(2(x1)))))))))))))) | → | 3(2(0(0(0(0(1(2(3(0(1(0(0(3(2(0(0(1(x1)))))))))))))))))) | (46) |
0(1(2(2(1(2(2(0(0(1(2(2(0(1(x1)))))))))))))) | → | 0(0(0(3(0(0(1(2(2(0(3(2(0(2(0(1(0(3(x1)))))))))))))))))) | (47) |
1(1(2(2(1(2(2(0(0(1(2(2(0(1(x1)))))))))))))) | → | 1(0(0(3(0(0(1(2(2(0(3(2(0(2(0(1(0(3(x1)))))))))))))))))) | (48) |
2(1(2(2(1(2(2(0(0(1(2(2(0(1(x1)))))))))))))) | → | 2(0(0(3(0(0(1(2(2(0(3(2(0(2(0(1(0(3(x1)))))))))))))))))) | (49) |
3(1(2(2(1(2(2(0(0(1(2(2(0(1(x1)))))))))))))) | → | 3(0(0(3(0(0(1(2(2(0(3(2(0(2(0(1(0(3(x1)))))))))))))))))) | (50) |
0(1(2(3(1(0(2(1(0(0(1(1(1(0(x1)))))))))))))) | → | 0(0(3(0(1(0(1(2(0(3(0(0(0(1(0(1(3(0(x1)))))))))))))))))) | (51) |
1(1(2(3(1(0(2(1(0(0(1(1(1(0(x1)))))))))))))) | → | 1(0(3(0(1(0(1(2(0(3(0(0(0(1(0(1(3(0(x1)))))))))))))))))) | (52) |
2(1(2(3(1(0(2(1(0(0(1(1(1(0(x1)))))))))))))) | → | 2(0(3(0(1(0(1(2(0(3(0(0(0(1(0(1(3(0(x1)))))))))))))))))) | (53) |
3(1(2(3(1(0(2(1(0(0(1(1(1(0(x1)))))))))))))) | → | 3(0(3(0(1(0(1(2(0(3(0(0(0(1(0(1(3(0(x1)))))))))))))))))) | (54) |
0(1(3(0(0(3(2(2(2(2(1(0(2(3(x1)))))))))))))) | → | 0(3(0(0(2(2(0(3(2(0(3(0(2(3(1(2(0(0(x1)))))))))))))))))) | (55) |
1(1(3(0(0(3(2(2(2(2(1(0(2(3(x1)))))))))))))) | → | 1(3(0(0(2(2(0(3(2(0(3(0(2(3(1(2(0(0(x1)))))))))))))))))) | (56) |
2(1(3(0(0(3(2(2(2(2(1(0(2(3(x1)))))))))))))) | → | 2(3(0(0(2(2(0(3(2(0(3(0(2(3(1(2(0(0(x1)))))))))))))))))) | (57) |
3(1(3(0(0(3(2(2(2(2(1(0(2(3(x1)))))))))))))) | → | 3(3(0(0(2(2(0(3(2(0(3(0(2(3(1(2(0(0(x1)))))))))))))))))) | (58) |
0(1(3(1(1(3(0(0(1(0(0(2(3(0(x1)))))))))))))) | → | 0(2(1(0(2(0(3(2(0(0(0(0(2(0(1(1(3(0(x1)))))))))))))))))) | (59) |
1(1(3(1(1(3(0(0(1(0(0(2(3(0(x1)))))))))))))) | → | 1(2(1(0(2(0(3(2(0(0(0(0(2(0(1(1(3(0(x1)))))))))))))))))) | (60) |
2(1(3(1(1(3(0(0(1(0(0(2(3(0(x1)))))))))))))) | → | 2(2(1(0(2(0(3(2(0(0(0(0(2(0(1(1(3(0(x1)))))))))))))))))) | (61) |
3(1(3(1(1(3(0(0(1(0(0(2(3(0(x1)))))))))))))) | → | 3(2(1(0(2(0(3(2(0(0(0(0(2(0(1(1(3(0(x1)))))))))))))))))) | (62) |
0(1(3(1(3(1(0(2(0(1(3(0(0(1(x1)))))))))))))) | → | 0(2(2(0(0(0(1(0(0(2(0(0(1(3(3(3(0(1(x1)))))))))))))))))) | (63) |
1(1(3(1(3(1(0(2(0(1(3(0(0(1(x1)))))))))))))) | → | 1(2(2(0(0(0(1(0(0(2(0(0(1(3(3(3(0(1(x1)))))))))))))))))) | (64) |
2(1(3(1(3(1(0(2(0(1(3(0(0(1(x1)))))))))))))) | → | 2(2(2(0(0(0(1(0(0(2(0(0(1(3(3(3(0(1(x1)))))))))))))))))) | (65) |
3(1(3(1(3(1(0(2(0(1(3(0(0(1(x1)))))))))))))) | → | 3(2(2(0(0(0(1(0(0(2(0(0(1(3(3(3(0(1(x1)))))))))))))))))) | (66) |
0(1(3(2(1(0(1(0(3(0(1(3(0(0(x1)))))))))))))) | → | 0(0(3(1(0(0(0(3(0(0(2(3(2(1(0(1(0(0(x1)))))))))))))))))) | (67) |
1(1(3(2(1(0(1(0(3(0(1(3(0(0(x1)))))))))))))) | → | 1(0(3(1(0(0(0(3(0(0(2(3(2(1(0(1(0(0(x1)))))))))))))))))) | (68) |
2(1(3(2(1(0(1(0(3(0(1(3(0(0(x1)))))))))))))) | → | 2(0(3(1(0(0(0(3(0(0(2(3(2(1(0(1(0(0(x1)))))))))))))))))) | (69) |
3(1(3(2(1(0(1(0(3(0(1(3(0(0(x1)))))))))))))) | → | 3(0(3(1(0(0(0(3(0(0(2(3(2(1(0(1(0(0(x1)))))))))))))))))) | (70) |
0(1(3(3(0(2(3(0(3(2(0(0(1(1(x1)))))))))))))) | → | 0(3(2(0(3(0(3(0(0(2(0(0(0(1(0(2(3(1(x1)))))))))))))))))) | (71) |
1(1(3(3(0(2(3(0(3(2(0(0(1(1(x1)))))))))))))) | → | 1(3(2(0(3(0(3(0(0(2(0(0(0(1(0(2(3(1(x1)))))))))))))))))) | (72) |
2(1(3(3(0(2(3(0(3(2(0(0(1(1(x1)))))))))))))) | → | 2(3(2(0(3(0(3(0(0(2(0(0(0(1(0(2(3(1(x1)))))))))))))))))) | (73) |
3(1(3(3(0(2(3(0(3(2(0(0(1(1(x1)))))))))))))) | → | 3(3(2(0(3(0(3(0(0(2(0(0(0(1(0(2(3(1(x1)))))))))))))))))) | (74) |
0(1(3(3(2(2(2(3(2(2(0(2(3(0(x1)))))))))))))) | → | 0(3(0(3(2(2(0(2(2(1(0(2(2(3(1(2(0(0(x1)))))))))))))))))) | (75) |
1(1(3(3(2(2(2(3(2(2(0(2(3(0(x1)))))))))))))) | → | 1(3(0(3(2(2(0(2(2(1(0(2(2(3(1(2(0(0(x1)))))))))))))))))) | (76) |
2(1(3(3(2(2(2(3(2(2(0(2(3(0(x1)))))))))))))) | → | 2(3(0(3(2(2(0(2(2(1(0(2(2(3(1(2(0(0(x1)))))))))))))))))) | (77) |
3(1(3(3(2(2(2(3(2(2(0(2(3(0(x1)))))))))))))) | → | 3(3(0(3(2(2(0(2(2(1(0(2(2(3(1(2(0(0(x1)))))))))))))))))) | (78) |
0(2(0(2(1(2(2(3(2(2(2(2(1(0(x1)))))))))))))) | → | 0(1(0(0(0(0(1(0(0(2(0(3(1(0(0(2(3(0(x1)))))))))))))))))) | (79) |
1(2(0(2(1(2(2(3(2(2(2(2(1(0(x1)))))))))))))) | → | 1(1(0(0(0(0(1(0(0(2(0(3(1(0(0(2(3(0(x1)))))))))))))))))) | (80) |
2(2(0(2(1(2(2(3(2(2(2(2(1(0(x1)))))))))))))) | → | 2(1(0(0(0(0(1(0(0(2(0(3(1(0(0(2(3(0(x1)))))))))))))))))) | (81) |
3(2(0(2(1(2(2(3(2(2(2(2(1(0(x1)))))))))))))) | → | 3(1(0(0(0(0(1(0(0(2(0(3(1(0(0(2(3(0(x1)))))))))))))))))) | (82) |
0(2(0(2(2(1(2(2(3(2(0(1(1(2(x1)))))))))))))) | → | 0(0(2(3(1(3(1(0(0(0(0(0(0(1(2(2(1(0(x1)))))))))))))))))) | (83) |
1(2(0(2(2(1(2(2(3(2(0(1(1(2(x1)))))))))))))) | → | 1(0(2(3(1(3(1(0(0(0(0(0(0(1(2(2(1(0(x1)))))))))))))))))) | (84) |
2(2(0(2(2(1(2(2(3(2(0(1(1(2(x1)))))))))))))) | → | 2(0(2(3(1(3(1(0(0(0(0(0(0(1(2(2(1(0(x1)))))))))))))))))) | (85) |
3(2(0(2(2(1(2(2(3(2(0(1(1(2(x1)))))))))))))) | → | 3(0(2(3(1(3(1(0(0(0(0(0(0(1(2(2(1(0(x1)))))))))))))))))) | (86) |
0(2(0(3(3(1(2(2(0(0(2(1(0(1(x1)))))))))))))) | → | 0(3(2(0(1(0(0(2(0(3(1(0(0(0(2(1(0(2(x1)))))))))))))))))) | (87) |
1(2(0(3(3(1(2(2(0(0(2(1(0(1(x1)))))))))))))) | → | 1(3(2(0(1(0(0(2(0(3(1(0(0(0(2(1(0(2(x1)))))))))))))))))) | (88) |
2(2(0(3(3(1(2(2(0(0(2(1(0(1(x1)))))))))))))) | → | 2(3(2(0(1(0(0(2(0(3(1(0(0(0(2(1(0(2(x1)))))))))))))))))) | (89) |
3(2(0(3(3(1(2(2(0(0(2(1(0(1(x1)))))))))))))) | → | 3(3(2(0(1(0(0(2(0(3(1(0(0(0(2(1(0(2(x1)))))))))))))))))) | (90) |
0(2(2(0(1(0(1(0(3(3(2(1(2(3(x1)))))))))))))) | → | 0(0(3(0(1(2(0(1(2(0(2(2(1(2(1(0(0(0(x1)))))))))))))))))) | (91) |
1(2(2(0(1(0(1(0(3(3(2(1(2(3(x1)))))))))))))) | → | 1(0(3(0(1(2(0(1(2(0(2(2(1(2(1(0(0(0(x1)))))))))))))))))) | (92) |
2(2(2(0(1(0(1(0(3(3(2(1(2(3(x1)))))))))))))) | → | 2(0(3(0(1(2(0(1(2(0(2(2(1(2(1(0(0(0(x1)))))))))))))))))) | (93) |
3(2(2(0(1(0(1(0(3(3(2(1(2(3(x1)))))))))))))) | → | 3(0(3(0(1(2(0(1(2(0(2(2(1(2(1(0(0(0(x1)))))))))))))))))) | (94) |
0(2(3(0(2(2(0(2(0(3(2(3(2(3(x1)))))))))))))) | → | 0(1(0(0(3(2(0(3(3(0(0(3(0(0(2(0(0(2(x1)))))))))))))))))) | (95) |
1(2(3(0(2(2(0(2(0(3(2(3(2(3(x1)))))))))))))) | → | 1(1(0(0(3(2(0(3(3(0(0(3(0(0(2(0(0(2(x1)))))))))))))))))) | (96) |
2(2(3(0(2(2(0(2(0(3(2(3(2(3(x1)))))))))))))) | → | 2(1(0(0(3(2(0(3(3(0(0(3(0(0(2(0(0(2(x1)))))))))))))))))) | (97) |
3(2(3(0(2(2(0(2(0(3(2(3(2(3(x1)))))))))))))) | → | 3(1(0(0(3(2(0(3(3(0(0(3(0(0(2(0(0(2(x1)))))))))))))))))) | (98) |
0(3(0(0(1(3(1(2(0(2(0(3(3(3(x1)))))))))))))) | → | 0(0(0(1(0(1(2(0(0(3(0(2(2(2(0(0(1(3(x1)))))))))))))))))) | (99) |
1(3(0(0(1(3(1(2(0(2(0(3(3(3(x1)))))))))))))) | → | 1(0(0(1(0(1(2(0(0(3(0(2(2(2(0(0(1(3(x1)))))))))))))))))) | (100) |
2(3(0(0(1(3(1(2(0(2(0(3(3(3(x1)))))))))))))) | → | 2(0(0(1(0(1(2(0(0(3(0(2(2(2(0(0(1(3(x1)))))))))))))))))) | (101) |
3(3(0(0(1(3(1(2(0(2(0(3(3(3(x1)))))))))))))) | → | 3(0(0(1(0(1(2(0(0(3(0(2(2(2(0(0(1(3(x1)))))))))))))))))) | (102) |
0(3(2(2(2(0(1(3(0(2(2(3(3(0(x1)))))))))))))) | → | 0(1(1(0(1(0(0(3(0(1(2(1(1(0(0(1(0(0(x1)))))))))))))))))) | (103) |
1(3(2(2(2(0(1(3(0(2(2(3(3(0(x1)))))))))))))) | → | 1(1(1(0(1(0(0(3(0(1(2(1(1(0(0(1(0(0(x1)))))))))))))))))) | (104) |
2(3(2(2(2(0(1(3(0(2(2(3(3(0(x1)))))))))))))) | → | 2(1(1(0(1(0(0(3(0(1(2(1(1(0(0(1(0(0(x1)))))))))))))))))) | (105) |
3(3(2(2(2(0(1(3(0(2(2(3(3(0(x1)))))))))))))) | → | 3(1(1(0(1(0(0(3(0(1(2(1(1(0(0(1(0(0(x1)))))))))))))))))) | (106) |
Root-labeling is applied.
We obtain the labeled TRSThere are 348 ruless (increase limit for explicit display).
[00(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 + 335 |
[11(x1)] | = | 1 · x1 + 600 |
[12(x1)] | = | 1 · x1 + 89 |
[20(x1)] | = | 1 · x1 + 197 |
[03(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 + 357 |
[10(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 + 366 |
[13(x1)] | = | 1 · x1 + 265 |
[31(x1)] | = | 1 · x1 + 691 |
[21(x1)] | = | 1 · x1 + 878 |
[23(x1)] | = | 1 · x1 + 543 |
[32(x1)] | = | 1 · x1 + 356 |
[33(x1)] | = | 1 · x1 + 356 |
There are 304 ruless (increase limit for explicit display).
[02(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 + 13 |
[21(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 + 6 |
[20(x1)] | = | 1 · x1 + 11 |
[03(x1)] | = | 1 · x1 + 3 |
[31(x1)] | = | 1 · x1 + 2 |
[10(x1)] | = | 1 · x1 + 1 |
[30(x1)] | = | 1 · x1 + 1 |
[00(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 + 3 |
[33(x1)] | = | 1 · x1 + 2 |
[13(x1)] | = | 1 · x1 + 8 |
[11(x1)] | = | 1 · x1 + 8 |
02(22(23(32(22(21(12(20(03(32(20(03(31(x1))))))))))))) | → | 03(32(21(10(02(23(30(00(01(10(02(21(10(00(03(30(01(x1))))))))))))))))) | (128) |
02(22(23(32(22(21(12(20(03(32(20(03(32(x1))))))))))))) | → | 03(32(21(10(02(23(30(00(01(10(02(21(10(00(03(30(02(x1))))))))))))))))) | (129) |
02(22(23(32(22(21(12(20(03(32(20(03(33(x1))))))))))))) | → | 03(32(21(10(02(23(30(00(01(10(02(21(10(00(03(30(03(x1))))))))))))))))) | (130) |
22(20(03(33(31(12(22(20(00(02(21(10(01(11(x1)))))))))))))) | → | 23(32(20(01(10(00(02(20(03(31(10(00(00(02(21(10(02(21(x1)))))))))))))))))) | (384) |
22(20(03(33(31(12(22(20(00(02(21(10(01(13(x1)))))))))))))) | → | 23(32(20(01(10(00(02(20(03(31(10(00(00(02(21(10(02(23(x1)))))))))))))))))) | (386) |
32(22(20(01(10(01(10(03(33(32(21(12(23(31(x1)))))))))))))) | → | 30(03(30(01(12(20(01(12(20(02(22(21(12(21(10(00(00(01(x1)))))))))))))))))) | (404) |
32(22(20(01(10(01(10(03(33(32(21(12(23(32(x1)))))))))))))) | → | 30(03(30(01(12(20(01(12(20(02(22(21(12(21(10(00(00(02(x1)))))))))))))))))) | (405) |
32(22(20(01(10(01(10(03(33(32(21(12(23(33(x1)))))))))))))) | → | 30(03(30(01(12(20(01(12(20(02(22(21(12(21(10(00(00(03(x1)))))))))))))))))) | (406) |
[01(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 + 4 |
[33(x1)] | = | 1 · x1 + 1 |
[32(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 + 2 |
[23(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 + 1 |
[12(x1)] | = | 1 · x1 + 3 |
[11(x1)] | = | 1 · x1 + 4 |
01(13(33(32(22(22(23(32(22(20(02(23(30(00(x1)))))))))))))) | → | 03(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(00(x1)))))))))))))))))) | (327) |
01(13(33(32(22(22(23(32(22(20(02(23(30(01(x1)))))))))))))) | → | 03(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(01(x1)))))))))))))))))) | (328) |
01(13(33(32(22(22(23(32(22(20(02(23(30(02(x1)))))))))))))) | → | 03(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(02(x1)))))))))))))))))) | (329) |
01(13(33(32(22(22(23(32(22(20(02(23(30(03(x1)))))))))))))) | → | 03(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(03(x1)))))))))))))))))) | (330) |
11(13(33(32(22(22(23(32(22(20(02(23(30(00(x1)))))))))))))) | → | 13(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(00(x1)))))))))))))))))) | (331) |
11(13(33(32(22(22(23(32(22(20(02(23(30(01(x1)))))))))))))) | → | 13(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(01(x1)))))))))))))))))) | (332) |
11(13(33(32(22(22(23(32(22(20(02(23(30(02(x1)))))))))))))) | → | 13(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(02(x1)))))))))))))))))) | (333) |
11(13(33(32(22(22(23(32(22(20(02(23(30(03(x1)))))))))))))) | → | 13(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(03(x1)))))))))))))))))) | (334) |
21(13(33(32(22(22(23(32(22(20(02(23(30(00(x1)))))))))))))) | → | 23(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(00(x1)))))))))))))))))) | (335) |
21(13(33(32(22(22(23(32(22(20(02(23(30(01(x1)))))))))))))) | → | 23(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(01(x1)))))))))))))))))) | (336) |
21(13(33(32(22(22(23(32(22(20(02(23(30(02(x1)))))))))))))) | → | 23(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(02(x1)))))))))))))))))) | (337) |
21(13(33(32(22(22(23(32(22(20(02(23(30(03(x1)))))))))))))) | → | 23(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(03(x1)))))))))))))))))) | (338) |
31(13(33(32(22(22(23(32(22(20(02(23(30(00(x1)))))))))))))) | → | 33(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(00(x1)))))))))))))))))) | (339) |
31(13(33(32(22(22(23(32(22(20(02(23(30(01(x1)))))))))))))) | → | 33(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(01(x1)))))))))))))))))) | (340) |
31(13(33(32(22(22(23(32(22(20(02(23(30(02(x1)))))))))))))) | → | 33(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(02(x1)))))))))))))))))) | (341) |
31(13(33(32(22(22(23(32(22(20(02(23(30(03(x1)))))))))))))) | → | 33(30(03(32(22(20(02(22(21(10(02(22(23(31(12(20(00(03(x1)))))))))))))))))) | (342) |
[33(x1)] | = | 1 · x1 + 1 |
[30(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 + 1 |
[31(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 + 3 |
[20(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 + 1 |
[10(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 + 1 |
[11(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
33(30(00(01(13(31(12(20(02(20(03(33(33(30(x1)))))))))))))) | → | 30(00(01(10(01(12(20(00(03(30(02(22(22(20(00(01(13(30(x1)))))))))))))))))) | (435) |
33(30(00(01(13(31(12(20(02(20(03(33(33(31(x1)))))))))))))) | → | 30(00(01(10(01(12(20(00(03(30(02(22(22(20(00(01(13(31(x1)))))))))))))))))) | (436) |
33(30(00(01(13(31(12(20(02(20(03(33(33(32(x1)))))))))))))) | → | 30(00(01(10(01(12(20(00(03(30(02(22(22(20(00(01(13(32(x1)))))))))))))))))) | (437) |
33(30(00(01(13(31(12(20(02(20(03(33(33(33(x1)))))))))))))) | → | 30(00(01(10(01(12(20(00(03(30(02(22(22(20(00(01(13(33(x1)))))))))))))))))) | (438) |
[03(x1)] | = | 1 · x1 + 1 |
[32(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 + 1 |
[02(x1)] | = | 1 · x1 |
[23(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
03(32(22(22(20(01(13(30(02(22(23(33(30(00(x1)))))))))))))) | → | 01(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(00(x1)))))))))))))))))) | (439) |
03(32(22(22(20(01(13(30(02(22(23(33(30(01(x1)))))))))))))) | → | 01(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(01(x1)))))))))))))))))) | (440) |
03(32(22(22(20(01(13(30(02(22(23(33(30(02(x1)))))))))))))) | → | 01(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(02(x1)))))))))))))))))) | (441) |
03(32(22(22(20(01(13(30(02(22(23(33(30(03(x1)))))))))))))) | → | 01(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(03(x1)))))))))))))))))) | (442) |
[13(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 + 2 |
[23(x1)] | = | 1 · x1 |
[33(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 + 1 |
[31(x1)] | = | 1 · x1 + 1 |
13(32(22(22(20(01(13(30(02(22(23(33(30(00(x1)))))))))))))) | → | 11(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(00(x1)))))))))))))))))) | (443) |
13(32(22(22(20(01(13(30(02(22(23(33(30(01(x1)))))))))))))) | → | 11(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(01(x1)))))))))))))))))) | (444) |
13(32(22(22(20(01(13(30(02(22(23(33(30(02(x1)))))))))))))) | → | 11(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(02(x1)))))))))))))))))) | (445) |
13(32(22(22(20(01(13(30(02(22(23(33(30(03(x1)))))))))))))) | → | 11(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(03(x1)))))))))))))))))) | (446) |
[23(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 + 1 |
[33(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 + 1 |
23(32(22(22(20(01(13(30(02(22(23(33(30(00(x1)))))))))))))) | → | 21(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(00(x1)))))))))))))))))) | (447) |
23(32(22(22(20(01(13(30(02(22(23(33(30(01(x1)))))))))))))) | → | 21(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(01(x1)))))))))))))))))) | (448) |
23(32(22(22(20(01(13(30(02(22(23(33(30(02(x1)))))))))))))) | → | 21(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(02(x1)))))))))))))))))) | (449) |
23(32(22(22(20(01(13(30(02(22(23(33(30(03(x1)))))))))))))) | → | 21(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(03(x1)))))))))))))))))) | (450) |
[33(x1)] | = | 1 · x1 |
[32(x1)] | = | 1 · x1 |
[22(x1)] | = | 1 · x1 |
[20(x1)] | = | 1 · x1 |
[01(x1)] | = | 1 · x1 |
[13(x1)] | = | 1 · x1 |
[30(x1)] | = | 1 · x1 |
[02(x1)] | = | 1 · x1 + 1 |
[23(x1)] | = | 1 · x1 |
[00(x1)] | = | 1 · x1 |
[31(x1)] | = | 1 · x1 |
[11(x1)] | = | 1 · x1 |
[10(x1)] | = | 1 · x1 |
[03(x1)] | = | 1 · x1 |
[12(x1)] | = | 1 · x1 |
[21(x1)] | = | 1 · x1 |
33(32(22(22(20(01(13(30(02(22(23(33(30(00(x1)))))))))))))) | → | 31(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(00(x1)))))))))))))))))) | (451) |
33(32(22(22(20(01(13(30(02(22(23(33(30(01(x1)))))))))))))) | → | 31(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(01(x1)))))))))))))))))) | (452) |
33(32(22(22(20(01(13(30(02(22(23(33(30(02(x1)))))))))))))) | → | 31(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(02(x1)))))))))))))))))) | (453) |
33(32(22(22(20(01(13(30(02(22(23(33(30(03(x1)))))))))))))) | → | 31(11(10(01(10(00(03(30(01(12(21(11(10(00(01(10(00(03(x1)))))))))))))))))) | (454) |
There are no rules in the TRS. Hence, it is terminating.