The rewrite relation of the following TRS is considered.
0(0(1(2(x1)))) | → | 0(2(0(1(1(x1))))) | (1) |
0(1(2(2(x1)))) | → | 0(2(2(1(0(x1))))) | (2) |
0(1(2(2(x1)))) | → | 1(0(2(2(0(x1))))) | (3) |
0(1(2(3(x1)))) | → | 0(2(0(1(3(x1))))) | (4) |
0(1(2(3(x1)))) | → | 0(2(3(3(1(x1))))) | (5) |
0(2(1(2(x1)))) | → | 0(2(2(0(1(x1))))) | (6) |
0(2(1(2(x1)))) | → | 0(2(2(2(1(x1))))) | (7) |
0(2(1(2(x1)))) | → | 0(2(2(2(1(1(x1)))))) | (8) |
0(3(2(2(x1)))) | → | 3(4(0(2(2(x1))))) | (9) |
0(3(2(2(x1)))) | → | 0(2(2(2(2(3(x1)))))) | (10) |
0(4(1(2(x1)))) | → | 0(2(2(1(4(x1))))) | (11) |
0(4(1(2(x1)))) | → | 4(0(2(0(1(x1))))) | (12) |
0(5(0(1(x1)))) | → | 0(2(0(2(5(1(x1)))))) | (13) |
0(5(0(5(x1)))) | → | 0(2(0(5(5(x1))))) | (14) |
0(5(2(1(x1)))) | → | 0(2(2(5(1(x1))))) | (15) |
0(5(2(5(x1)))) | → | 0(2(2(5(5(x1))))) | (16) |
0(5(4(2(x1)))) | → | 4(0(2(2(0(5(x1)))))) | (17) |
2(1(0(3(x1)))) | → | 4(0(2(2(3(1(x1)))))) | (18) |
2(1(0(4(x1)))) | → | 1(4(0(2(2(2(x1)))))) | (19) |
2(5(4(2(x1)))) | → | 4(0(2(2(5(x1))))) | (20) |
0(0(1(0(4(x1))))) | → | 0(0(2(0(1(4(x1)))))) | (21) |
0(0(5(4(2(x1))))) | → | 0(4(0(0(2(5(x1)))))) | (22) |
0(1(0(1(2(x1))))) | → | 0(2(0(1(4(1(x1)))))) | (23) |
0(1(2(0(3(x1))))) | → | 0(2(0(4(1(3(x1)))))) | (24) |
0(1(2(2(2(x1))))) | → | 0(2(2(2(1(2(x1)))))) | (25) |
0(1(2(3(2(x1))))) | → | 1(3(4(0(2(2(x1)))))) | (26) |
0(1(3(2(3(x1))))) | → | 0(0(2(3(3(1(x1)))))) | (27) |
0(1(3(4(2(x1))))) | → | 0(2(3(4(1(1(x1)))))) | (28) |
0(2(1(0(1(x1))))) | → | 0(0(2(0(1(1(x1)))))) | (29) |
0(2(1(2(2(x1))))) | → | 0(2(0(2(2(1(x1)))))) | (30) |
0(2(3(0(5(x1))))) | → | 0(2(0(0(5(3(x1)))))) | (31) |
0(3(0(1(3(x1))))) | → | 0(0(4(3(1(3(x1)))))) | (32) |
0(3(0(4(1(x1))))) | → | 0(0(1(4(4(3(x1)))))) | (33) |
0(3(2(0(4(x1))))) | → | 4(0(0(2(3(4(x1)))))) | (34) |
0(4(5(2(3(x1))))) | → | 0(2(2(3(4(5(x1)))))) | (35) |
0(5(0(0(3(x1))))) | → | 0(2(0(3(0(5(x1)))))) | (36) |
0(5(0(1(2(x1))))) | → | 0(0(2(0(1(5(x1)))))) | (37) |
0(5(1(4(2(x1))))) | → | 0(2(0(1(4(5(x1)))))) | (38) |
0(5(2(5(1(x1))))) | → | 0(2(0(5(5(1(x1)))))) | (39) |
2(1(0(0(4(x1))))) | → | 1(4(4(0(0(2(x1)))))) | (40) |
2(5(0(0(3(x1))))) | → | 0(2(0(0(5(3(x1)))))) | (41) |
2(5(3(0(1(x1))))) | → | 5(0(2(2(3(1(x1)))))) | (42) |
5(0(1(2(2(x1))))) | → | 5(1(0(2(0(2(x1)))))) | (43) |
5(2(0(1(2(x1))))) | → | 1(5(4(0(2(2(x1)))))) | (44) |
5(2(1(0(1(x1))))) | → | 0(2(3(1(5(1(x1)))))) | (45) |
5(2(3(0(1(x1))))) | → | 1(5(0(2(2(3(x1)))))) | (46) |
5(3(0(4(1(x1))))) | → | 4(5(0(2(3(1(x1)))))) | (47) |
{5(☐), 4(☐), 3(☐), 2(☐), 1(☐), 0(☐)}
We obtain the transformed TRSThere are 282 ruless (increase limit for explicit display).
As carrier we take the set {0,...,5}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 6):
[5(x1)] | = | 6x1 + 0 |
[4(x1)] | = | 6x1 + 1 |
[3(x1)] | = | 6x1 + 2 |
[2(x1)] | = | 6x1 + 3 |
[1(x1)] | = | 6x1 + 4 |
[0(x1)] | = | 6x1 + 5 |
There are 1692 ruless (increase limit for explicit display).
[50(x1)] | = |
x1 +
|
||||
[51(x1)] | = |
x1 +
|
||||
[52(x1)] | = |
x1 +
|
||||
[53(x1)] | = |
x1 +
|
||||
[54(x1)] | = |
x1 +
|
||||
[55(x1)] | = |
x1 +
|
||||
[40(x1)] | = |
x1 +
|
||||
[41(x1)] | = |
x1 +
|
||||
[42(x1)] | = |
x1 +
|
||||
[43(x1)] | = |
x1 +
|
||||
[44(x1)] | = |
x1 +
|
||||
[45(x1)] | = |
x1 +
|
||||
[30(x1)] | = |
x1 +
|
||||
[31(x1)] | = |
x1 +
|
||||
[32(x1)] | = |
x1 +
|
||||
[33(x1)] | = |
x1 +
|
||||
[34(x1)] | = |
x1 +
|
||||
[35(x1)] | = |
x1 +
|
||||
[20(x1)] | = |
x1 +
|
||||
[21(x1)] | = |
x1 +
|
||||
[22(x1)] | = |
x1 +
|
||||
[23(x1)] | = |
x1 +
|
||||
[24(x1)] | = |
x1 +
|
||||
[25(x1)] | = |
x1 +
|
||||
[10(x1)] | = |
x1 +
|
||||
[11(x1)] | = |
x1 +
|
||||
[12(x1)] | = |
x1 +
|
||||
[13(x1)] | = |
x1 +
|
||||
[14(x1)] | = |
x1 +
|
||||
[15(x1)] | = |
x1 +
|
||||
[00(x1)] | = |
x1 +
|
||||
[01(x1)] | = |
x1 +
|
||||
[02(x1)] | = |
x1 +
|
||||
[03(x1)] | = |
x1 +
|
||||
[04(x1)] | = |
x1 +
|
||||
[05(x1)] | = |
x1 +
|
There are 1632 ruless (increase limit for explicit display).
23(13(24(03(05(x1))))) | → | 13(04(25(23(03(05(x1)))))) | (2022) |
23(13(24(03(15(x1))))) | → | 13(04(25(23(03(15(x1)))))) | (2023) |
23(13(24(03(25(x1))))) | → | 13(04(25(23(03(25(x1)))))) | (2024) |
23(13(24(03(35(x1))))) | → | 13(04(25(23(03(35(x1)))))) | (2025) |
23(13(24(03(45(x1))))) | → | 13(04(25(23(03(45(x1)))))) | (2026) |
23(13(24(03(55(x1))))) | → | 13(04(25(23(03(55(x1)))))) | (2027) |
23(13(24(03(05(x1))))) | → | 13(24(23(23(03(05(x1)))))) | (2028) |
23(13(24(03(15(x1))))) | → | 13(24(23(23(03(15(x1)))))) | (2029) |
23(13(24(03(25(x1))))) | → | 13(24(23(23(03(25(x1)))))) | (2030) |
23(13(24(03(35(x1))))) | → | 13(24(23(23(03(35(x1)))))) | (2031) |
23(13(24(03(45(x1))))) | → | 13(24(23(23(03(45(x1)))))) | (2032) |
23(13(24(03(55(x1))))) | → | 13(24(23(23(03(55(x1)))))) | (2033) |
23(13(24(03(05(x1))))) | → | 13(14(24(23(23(03(05(x1))))))) | (2034) |
23(13(24(03(15(x1))))) | → | 13(14(24(23(23(03(15(x1))))))) | (2035) |
23(13(24(03(25(x1))))) | → | 13(14(24(23(23(03(25(x1))))))) | (2036) |
23(13(24(03(35(x1))))) | → | 13(14(24(23(23(03(35(x1))))))) | (2037) |
23(13(24(03(45(x1))))) | → | 13(14(24(23(23(03(45(x1))))))) | (2038) |
23(13(24(03(55(x1))))) | → | 13(14(24(23(23(03(55(x1))))))) | (2039) |
25(23(23(13(04(05(x1)))))) | → | 25(13(24(23(23(03(05(x1))))))) | (2040) |
24(23(23(13(04(05(x1)))))) | → | 24(13(24(23(23(03(05(x1))))))) | (2041) |
23(23(23(13(04(05(x1)))))) | → | 23(13(24(23(23(03(05(x1))))))) | (2042) |
22(23(23(13(04(05(x1)))))) | → | 22(13(24(23(23(03(05(x1))))))) | (2043) |
21(23(23(13(04(05(x1)))))) | → | 21(13(24(23(23(03(05(x1))))))) | (2044) |
20(23(23(13(04(05(x1)))))) | → | 20(13(24(23(23(03(05(x1))))))) | (2045) |
25(23(23(13(04(15(x1)))))) | → | 25(13(24(23(23(03(15(x1))))))) | (2046) |
24(23(23(13(04(15(x1)))))) | → | 24(13(24(23(23(03(15(x1))))))) | (2047) |
23(23(23(13(04(15(x1)))))) | → | 23(13(24(23(23(03(15(x1))))))) | (2048) |
22(23(23(13(04(15(x1)))))) | → | 22(13(24(23(23(03(15(x1))))))) | (2049) |
21(23(23(13(04(15(x1)))))) | → | 21(13(24(23(23(03(15(x1))))))) | (2050) |
20(23(23(13(04(15(x1)))))) | → | 20(13(24(23(23(03(15(x1))))))) | (2051) |
25(23(23(13(04(25(x1)))))) | → | 25(13(24(23(23(03(25(x1))))))) | (2052) |
24(23(23(13(04(25(x1)))))) | → | 24(13(24(23(23(03(25(x1))))))) | (2053) |
23(23(23(13(04(25(x1)))))) | → | 23(13(24(23(23(03(25(x1))))))) | (2054) |
22(23(23(13(04(25(x1)))))) | → | 22(13(24(23(23(03(25(x1))))))) | (2055) |
21(23(23(13(04(25(x1)))))) | → | 21(13(24(23(23(03(25(x1))))))) | (2056) |
20(23(23(13(04(25(x1)))))) | → | 20(13(24(23(23(03(25(x1))))))) | (2057) |
25(23(23(13(04(35(x1)))))) | → | 25(13(24(23(23(03(35(x1))))))) | (2058) |
24(23(23(13(04(35(x1)))))) | → | 24(13(24(23(23(03(35(x1))))))) | (2059) |
23(23(23(13(04(35(x1)))))) | → | 23(13(24(23(23(03(35(x1))))))) | (2060) |
22(23(23(13(04(35(x1)))))) | → | 22(13(24(23(23(03(35(x1))))))) | (2061) |
21(23(23(13(04(35(x1)))))) | → | 21(13(24(23(23(03(35(x1))))))) | (2062) |
20(23(23(13(04(35(x1)))))) | → | 20(13(24(23(23(03(35(x1))))))) | (2063) |
25(23(23(13(04(45(x1)))))) | → | 25(13(24(23(23(03(45(x1))))))) | (2064) |
24(23(23(13(04(45(x1)))))) | → | 24(13(24(23(23(03(45(x1))))))) | (2065) |
23(23(23(13(04(45(x1)))))) | → | 23(13(24(23(23(03(45(x1))))))) | (2066) |
22(23(23(13(04(45(x1)))))) | → | 22(13(24(23(23(03(45(x1))))))) | (2067) |
21(23(23(13(04(45(x1)))))) | → | 21(13(24(23(23(03(45(x1))))))) | (2068) |
20(23(23(13(04(45(x1)))))) | → | 20(13(24(23(23(03(45(x1))))))) | (2069) |
25(23(23(13(04(55(x1)))))) | → | 25(13(24(23(23(03(55(x1))))))) | (2070) |
24(23(23(13(04(55(x1)))))) | → | 24(13(24(23(23(03(55(x1))))))) | (2071) |
23(23(23(13(04(55(x1)))))) | → | 23(13(24(23(23(03(55(x1))))))) | (2072) |
22(23(23(13(04(55(x1)))))) | → | 22(13(24(23(23(03(55(x1))))))) | (2073) |
21(23(23(13(04(55(x1)))))) | → | 21(13(24(23(23(03(55(x1))))))) | (2074) |
20(23(23(13(04(55(x1)))))) | → | 20(13(24(23(23(03(55(x1))))))) | (2075) |
23(23(13(24(03(05(x1)))))) | → | 13(24(23(03(25(03(05(x1))))))) | (2076) |
23(23(13(24(03(15(x1)))))) | → | 13(24(23(03(25(03(15(x1))))))) | (2077) |
23(23(13(24(03(25(x1)))))) | → | 13(24(23(03(25(03(25(x1))))))) | (2078) |
23(23(13(24(03(35(x1)))))) | → | 13(24(23(03(25(03(35(x1))))))) | (2079) |
23(23(13(24(03(45(x1)))))) | → | 13(24(23(03(25(03(45(x1))))))) | (2080) |
23(23(13(24(03(55(x1)))))) | → | 13(24(23(03(25(03(55(x1))))))) | (2081) |
There are 186 ruless (increase limit for explicit display).
[55(x1)] | = |
x1 +
|
||||
[45(x1)] | = |
x1 +
|
||||
[35(x1)] | = |
x1 +
|
||||
[20(x1)] | = |
x1 +
|
||||
[21(x1)] | = |
x1 +
|
||||
[22(x1)] | = |
x1 +
|
||||
[23(x1)] | = |
x1 +
|
||||
[24(x1)] | = |
x1 +
|
||||
[25(x1)] | = |
x1 +
|
||||
[13(x1)] | = |
x1 +
|
||||
[14(x1)] | = |
x1 +
|
||||
[15(x1)] | = |
x1 +
|
||||
[03(x1)] | = |
x1 +
|
||||
[04(x1)] | = |
x1 +
|
||||
[05(x1)] | = |
x1 +
|
||||
[20#(x1)] | = |
x1 +
|
||||
[21#(x1)] | = |
x1 +
|
||||
[22#(x1)] | = |
x1 +
|
||||
[23#(x1)] | = |
x1 +
|
||||
[24#(x1)] | = |
x1 +
|
||||
[25#(x1)] | = |
x1 +
|
23(13(24(03(05(x1))))) | → | 13(04(25(23(03(05(x1)))))) | (2022) |
23(13(24(03(15(x1))))) | → | 13(04(25(23(03(15(x1)))))) | (2023) |
23(13(24(03(25(x1))))) | → | 13(04(25(23(03(25(x1)))))) | (2024) |
23(13(24(03(35(x1))))) | → | 13(04(25(23(03(35(x1)))))) | (2025) |
23(13(24(03(45(x1))))) | → | 13(04(25(23(03(45(x1)))))) | (2026) |
23(13(24(03(55(x1))))) | → | 13(04(25(23(03(55(x1)))))) | (2027) |
23(13(24(03(05(x1))))) | → | 13(24(23(23(03(05(x1)))))) | (2028) |
23(13(24(03(15(x1))))) | → | 13(24(23(23(03(15(x1)))))) | (2029) |
23(13(24(03(25(x1))))) | → | 13(24(23(23(03(25(x1)))))) | (2030) |
23(13(24(03(35(x1))))) | → | 13(24(23(23(03(35(x1)))))) | (2031) |
23(13(24(03(45(x1))))) | → | 13(24(23(23(03(45(x1)))))) | (2032) |
23(13(24(03(55(x1))))) | → | 13(24(23(23(03(55(x1)))))) | (2033) |
23(13(24(03(05(x1))))) | → | 13(14(24(23(23(03(05(x1))))))) | (2034) |
23(13(24(03(15(x1))))) | → | 13(14(24(23(23(03(15(x1))))))) | (2035) |
23(13(24(03(25(x1))))) | → | 13(14(24(23(23(03(25(x1))))))) | (2036) |
23(13(24(03(35(x1))))) | → | 13(14(24(23(23(03(35(x1))))))) | (2037) |
23(13(24(03(45(x1))))) | → | 13(14(24(23(23(03(45(x1))))))) | (2038) |
23(13(24(03(55(x1))))) | → | 13(14(24(23(23(03(55(x1))))))) | (2039) |
25(23(23(13(04(05(x1)))))) | → | 25(13(24(23(23(03(05(x1))))))) | (2040) |
24(23(23(13(04(05(x1)))))) | → | 24(13(24(23(23(03(05(x1))))))) | (2041) |
23(23(23(13(04(05(x1)))))) | → | 23(13(24(23(23(03(05(x1))))))) | (2042) |
22(23(23(13(04(05(x1)))))) | → | 22(13(24(23(23(03(05(x1))))))) | (2043) |
21(23(23(13(04(05(x1)))))) | → | 21(13(24(23(23(03(05(x1))))))) | (2044) |
20(23(23(13(04(05(x1)))))) | → | 20(13(24(23(23(03(05(x1))))))) | (2045) |
25(23(23(13(04(15(x1)))))) | → | 25(13(24(23(23(03(15(x1))))))) | (2046) |
24(23(23(13(04(15(x1)))))) | → | 24(13(24(23(23(03(15(x1))))))) | (2047) |
23(23(23(13(04(15(x1)))))) | → | 23(13(24(23(23(03(15(x1))))))) | (2048) |
22(23(23(13(04(15(x1)))))) | → | 22(13(24(23(23(03(15(x1))))))) | (2049) |
21(23(23(13(04(15(x1)))))) | → | 21(13(24(23(23(03(15(x1))))))) | (2050) |
20(23(23(13(04(15(x1)))))) | → | 20(13(24(23(23(03(15(x1))))))) | (2051) |
25(23(23(13(04(25(x1)))))) | → | 25(13(24(23(23(03(25(x1))))))) | (2052) |
24(23(23(13(04(25(x1)))))) | → | 24(13(24(23(23(03(25(x1))))))) | (2053) |
23(23(23(13(04(25(x1)))))) | → | 23(13(24(23(23(03(25(x1))))))) | (2054) |
22(23(23(13(04(25(x1)))))) | → | 22(13(24(23(23(03(25(x1))))))) | (2055) |
21(23(23(13(04(25(x1)))))) | → | 21(13(24(23(23(03(25(x1))))))) | (2056) |
20(23(23(13(04(25(x1)))))) | → | 20(13(24(23(23(03(25(x1))))))) | (2057) |
25(23(23(13(04(35(x1)))))) | → | 25(13(24(23(23(03(35(x1))))))) | (2058) |
24(23(23(13(04(35(x1)))))) | → | 24(13(24(23(23(03(35(x1))))))) | (2059) |
23(23(23(13(04(35(x1)))))) | → | 23(13(24(23(23(03(35(x1))))))) | (2060) |
22(23(23(13(04(35(x1)))))) | → | 22(13(24(23(23(03(35(x1))))))) | (2061) |
21(23(23(13(04(35(x1)))))) | → | 21(13(24(23(23(03(35(x1))))))) | (2062) |
20(23(23(13(04(35(x1)))))) | → | 20(13(24(23(23(03(35(x1))))))) | (2063) |
25(23(23(13(04(45(x1)))))) | → | 25(13(24(23(23(03(45(x1))))))) | (2064) |
24(23(23(13(04(45(x1)))))) | → | 24(13(24(23(23(03(45(x1))))))) | (2065) |
23(23(23(13(04(45(x1)))))) | → | 23(13(24(23(23(03(45(x1))))))) | (2066) |
22(23(23(13(04(45(x1)))))) | → | 22(13(24(23(23(03(45(x1))))))) | (2067) |
21(23(23(13(04(45(x1)))))) | → | 21(13(24(23(23(03(45(x1))))))) | (2068) |
20(23(23(13(04(45(x1)))))) | → | 20(13(24(23(23(03(45(x1))))))) | (2069) |
25(23(23(13(04(55(x1)))))) | → | 25(13(24(23(23(03(55(x1))))))) | (2070) |
24(23(23(13(04(55(x1)))))) | → | 24(13(24(23(23(03(55(x1))))))) | (2071) |
23(23(23(13(04(55(x1)))))) | → | 23(13(24(23(23(03(55(x1))))))) | (2072) |
22(23(23(13(04(55(x1)))))) | → | 22(13(24(23(23(03(55(x1))))))) | (2073) |
21(23(23(13(04(55(x1)))))) | → | 21(13(24(23(23(03(55(x1))))))) | (2074) |
20(23(23(13(04(55(x1)))))) | → | 20(13(24(23(23(03(55(x1))))))) | (2075) |
23(23(13(24(03(05(x1)))))) | → | 13(24(23(03(25(03(05(x1))))))) | (2076) |
23(23(13(24(03(15(x1)))))) | → | 13(24(23(03(25(03(15(x1))))))) | (2077) |
23(23(13(24(03(25(x1)))))) | → | 13(24(23(03(25(03(25(x1))))))) | (2078) |
23(23(13(24(03(35(x1)))))) | → | 13(24(23(03(25(03(35(x1))))))) | (2079) |
23(23(13(24(03(45(x1)))))) | → | 13(24(23(03(25(03(45(x1))))))) | (2080) |
23(23(13(24(03(55(x1)))))) | → | 13(24(23(03(25(03(55(x1))))))) | (2081) |
There are 150 ruless (increase limit for explicit display).
and no rules could be deleted.The dependency pairs are split into 0 components.