The rewrite relation of the following TRS is considered.
0(0(0(1(1(0(0(0(0(1(2(0(1(x1))))))))))))) | → | 1(1(1(1(0(0(0(1(0(0(1(1(0(1(1(0(0(x1))))))))))))))))) | (1) |
0(0(0(1(1(2(2(1(1(0(0(1(1(x1))))))))))))) | → | 0(1(1(0(2(0(0(0(1(0(1(1(0(0(0(1(0(x1))))))))))))))))) | (2) |
0(1(0(0(2(1(0(0(1(0(0(1(0(x1))))))))))))) | → | 0(1(1(0(0(0(1(1(0(1(0(0(1(1(1(0(0(x1))))))))))))))))) | (3) |
0(1(0(1(1(0(0(0(0(2(0(1(2(x1))))))))))))) | → | 1(1(1(0(0(0(1(0(1(1(0(1(1(1(0(0(2(x1))))))))))))))))) | (4) |
0(1(0(1(1(0(2(1(0(1(0(0(0(x1))))))))))))) | → | 0(1(1(0(1(1(0(0(1(0(0(1(0(1(1(1(0(x1))))))))))))))))) | (5) |
0(1(1(0(0(1(0(2(0(0(0(2(1(x1))))))))))))) | → | 0(0(1(1(0(1(0(1(1(0(0(1(1(2(1(1(1(x1))))))))))))))))) | (6) |
0(1(2(1(0(0(0(0(0(2(1(1(1(x1))))))))))))) | → | 0(1(0(1(1(2(0(1(0(0(0(1(1(0(0(0(1(x1))))))))))))))))) | (7) |
0(2(0(0(2(1(0(0(0(0(0(0(1(x1))))))))))))) | → | 1(0(0(1(0(1(1(1(0(0(0(1(0(0(0(0(1(x1))))))))))))))))) | (8) |
0(2(1(0(1(2(1(2(2(0(1(1(1(x1))))))))))))) | → | 0(2(1(1(0(0(2(1(1(0(0(1(2(1(1(1(1(x1))))))))))))))))) | (9) |
0(2(1(0(2(1(0(1(2(0(0(0(1(x1))))))))))))) | → | 0(0(2(1(1(1(1(0(0(1(0(2(0(0(0(1(0(x1))))))))))))))))) | (10) |
0(2(1(1(0(0(0(0(2(1(0(1(1(x1))))))))))))) | → | 0(0(1(0(1(0(1(0(2(1(1(1(0(0(0(0(0(x1))))))))))))))))) | (11) |
0(2(2(0(0(1(1(0(1(0(1(0(1(x1))))))))))))) | → | 0(0(2(1(0(0(0(1(1(0(1(1(0(1(1(0(0(x1))))))))))))))))) | (12) |
1(0(0(0(0(1(1(1(0(0(2(1(1(x1))))))))))))) | → | 1(1(1(1(1(1(1(1(1(1(0(1(1(0(1(0(0(x1))))))))))))))))) | (13) |
1(0(0(0(1(1(1(2(0(0(1(0(2(x1))))))))))))) | → | 0(1(1(0(1(0(0(1(0(0(0(0(0(2(0(1(2(x1))))))))))))))))) | (14) |
1(0(0(0(1(2(0(1(0(0(0(1(0(x1))))))))))))) | → | 1(1(1(0(0(0(1(1(0(1(1(0(1(1(1(0(1(x1))))))))))))))))) | (15) |
1(0(0(0(2(1(0(0(2(0(1(0(1(x1))))))))))))) | → | 2(1(0(0(1(1(0(1(0(0(0(0(0(1(0(0(0(x1))))))))))))))))) | (16) |
1(0(0(1(0(1(2(1(0(2(1(1(0(x1))))))))))))) | → | 0(1(1(1(0(0(0(0(0(2(1(1(1(1(1(1(0(x1))))))))))))))))) | (17) |
1(0(0(1(0(2(1(1(0(1(1(0(1(x1))))))))))))) | → | 1(1(1(1(0(0(1(0(1(0(1(1(1(0(0(1(1(x1))))))))))))))))) | (18) |
1(0(0(1(2(0(0(0(2(2(1(1(2(x1))))))))))))) | → | 1(0(0(0(1(0(2(2(0(1(1(1(0(1(2(1(2(x1))))))))))))))))) | (19) |
1(0(0(1(2(1(1(1(0(2(0(2(1(x1))))))))))))) | → | 1(0(0(1(0(0(1(2(0(1(0(1(2(2(1(0(0(x1))))))))))))))))) | (20) |
1(0(0(2(0(1(0(1(0(2(1(0(2(x1))))))))))))) | → | 0(1(0(0(0(2(0(1(1(0(1(0(1(1(0(0(2(x1))))))))))))))))) | (21) |
1(0(1(0(1(2(1(1(2(1(0(0(1(x1))))))))))))) | → | 1(1(0(0(1(0(0(2(2(0(0(0(0(1(1(0(0(x1))))))))))))))))) | (22) |
1(0(1(2(0(1(2(1(0(0(1(0(0(x1))))))))))))) | → | 0(0(0(0(0(1(1(0(1(1(1(1(0(2(1(0(1(x1))))))))))))))))) | (23) |
1(0(2(2(1(0(1(0(1(0(1(0(2(x1))))))))))))) | → | 1(1(1(0(0(0(0(0(0(1(1(0(0(0(2(1(2(x1))))))))))))))))) | (24) |
1(1(0(1(0(2(2(2(1(0(0(0(0(x1))))))))))))) | → | 1(1(0(1(1(0(1(0(1(0(1(0(0(2(0(0(1(x1))))))))))))))))) | (25) |
1(1(0(2(2(0(0(1(2(1(2(1(2(x1))))))))))))) | → | 1(1(2(0(0(0(1(1(0(2(2(1(1(0(1(0(2(x1))))))))))))))))) | (26) |
1(1(1(1(0(1(0(2(1(1(0(0(2(x1))))))))))))) | → | 1(1(1(0(0(1(0(1(1(0(1(0(0(2(1(0(2(x1))))))))))))))))) | (27) |
1(1(1(2(1(1(0(2(0(2(0(1(0(x1))))))))))))) | → | 1(1(1(0(0(1(0(2(2(0(0(1(2(1(0(1(0(x1))))))))))))))))) | (28) |
1(1(2(1(1(0(1(1(0(1(1(0(2(x1))))))))))))) | → | 1(1(2(0(1(0(1(0(0(0(0(0(1(0(0(1(2(x1))))))))))))))))) | (29) |
1(1(2(2(1(1(1(1(0(1(1(0(0(x1))))))))))))) | → | 1(0(1(1(1(2(1(1(0(1(0(1(1(1(0(0(0(x1))))))))))))))))) | (30) |
1(1(2(2(2(1(0(0(1(1(0(0(0(x1))))))))))))) | → | 0(1(0(1(1(1(1(1(0(2(1(0(1(1(0(0(0(x1))))))))))))))))) | (31) |
1(2(0(1(0(1(1(1(0(1(1(1(1(x1))))))))))))) | → | 1(0(0(1(1(1(0(1(0(0(1(1(0(1(1(0(1(x1))))))))))))))))) | (32) |
1(2(1(0(0(0(0(1(0(1(1(2(1(x1))))))))))))) | → | 0(1(0(0(1(0(0(0(1(1(0(0(2(1(0(0(0(x1))))))))))))))))) | (33) |
1(2(1(0(1(0(0(1(0(2(0(1(1(x1))))))))))))) | → | 1(0(0(1(0(0(0(2(2(0(0(1(0(0(1(1(0(x1))))))))))))))))) | (34) |
1(2(2(0(1(1(1(1(1(1(0(1(0(x1))))))))))))) | → | 1(0(0(2(2(0(0(1(0(0(1(0(0(0(1(1(0(x1))))))))))))))))) | (35) |
2(1(0(0(1(1(0(1(2(1(0(1(1(x1))))))))))))) | → | 1(0(0(0(1(0(0(0(0(2(1(0(0(1(1(0(1(x1))))))))))))))))) | (36) |
2(1(0(1(2(0(0(2(0(1(0(1(2(x1))))))))))))) | → | 2(1(0(0(1(0(0(0(0(1(0(2(2(2(0(1(2(x1))))))))))))))))) | (37) |
2(1(0(2(2(2(2(1(0(0(0(0(1(x1))))))))))))) | → | 1(1(1(0(0(0(1(1(2(1(0(0(1(2(0(1(0(x1))))))))))))))))) | (38) |
2(1(1(0(1(0(1(1(1(2(1(1(0(x1))))))))))))) | → | 1(1(2(1(1(0(0(1(1(0(0(1(1(0(1(0(0(x1))))))))))))))))) | (39) |
2(1(1(0(2(1(0(2(1(0(0(0(1(x1))))))))))))) | → | 0(1(0(1(1(1(1(2(0(1(0(0(1(0(0(1(0(x1))))))))))))))))) | (40) |
2(1(1(1(1(1(1(1(0(0(2(0(1(x1))))))))))))) | → | 1(1(1(0(1(1(1(0(1(0(0(1(0(2(0(1(0(x1))))))))))))))))) | (41) |
2(2(1(0(0(2(1(1(1(1(1(0(1(x1))))))))))))) | → | 2(2(2(0(0(0(1(0(1(0(1(1(0(1(1(1(0(x1))))))))))))))))) | (42) |
2(2(1(0(0(2(1(2(0(0(1(0(2(x1))))))))))))) | → | 2(1(0(0(0(2(1(0(0(1(2(0(0(1(1(1(2(x1))))))))))))))))) | (43) |
2(2(2(0(0(0(1(0(0(0(0(1(0(x1))))))))))))) | → | 0(2(0(0(1(1(1(0(1(1(0(0(0(1(0(1(0(x1))))))))))))))))) | (44) |
{2(☐), 1(☐), 0(☐)}
We obtain the transformed TRSThere are 132 ruless (increase limit for explicit display).
As carrier we take the set {0,1,2}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 3):
[2(x1)] | = | 3x1 + 0 |
[1(x1)] | = | 3x1 + 1 |
[0(x1)] | = | 3x1 + 2 |
There are 396 ruless (increase limit for explicit display).
[20(x1)] | = |
x1 +
|
||||
[21(x1)] | = |
x1 +
|
||||
[22(x1)] | = |
x1 +
|
||||
[10(x1)] | = |
x1 +
|
||||
[11(x1)] | = |
x1 +
|
||||
[12(x1)] | = |
x1 +
|
||||
[00(x1)] | = |
x1 +
|
||||
[01(x1)] | = |
x1 +
|
||||
[02(x1)] | = |
x1 +
|
There are 372 ruless (increase limit for explicit display).
22(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (573) |
21(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 21(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (574) |
20(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 20(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (575) |
22(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (576) |
21(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 21(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (577) |
20(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 20(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (578) |
22(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (579) |
21(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (580) |
20(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (581) |
22(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (582) |
21(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (583) |
20(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (584) |
22(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (585) |
21(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (586) |
20(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (587) |
22(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 22(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (588) |
21(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (589) |
20(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 20(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (590) |
22(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 22(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (591) |
21(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (592) |
20(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 20(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (593) |
22(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 22(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (594) |
21(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (595) |
20(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 20(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (596) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (597) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(21(x1)))))))) | (598) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))) | (599) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(21(x1))))))))) | (600) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (601) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(11(x1)))))))) | (602) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))) | (603) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(11(x1))))))))) | (604) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (605) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(01(x1)))))))) | (606) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))) | (607) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(01(x1))))))))) | (608) |
20#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 20#(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (609) |
20#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1))))))))))))))) | (610) |
20#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 20#(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (611) |
20#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1))))))))))))))) | (612) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 20#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (613) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1))))))))))))))) | (614) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 20#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (615) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1))))))))))))))) | (616) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 20#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (617) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1))))))))))))))) | (618) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(21(x1)))))))) | (619) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (620) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))) | (621) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(21(x1))))))))) | (622) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(11(x1)))))))) | (623) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (624) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))) | (625) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(11(x1))))))))) | (626) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(01(x1)))))))) | (627) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (628) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))) | (629) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(01(x1))))))))) | (630) |
21#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 21#(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (631) |
21#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1))))))))))))))) | (632) |
21#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 21#(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (633) |
21#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1))))))))))))))) | (634) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (635) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1))))))))))))))) | (636) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (637) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1))))))))))))))) | (638) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (639) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1))))))))))))))) | (640) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(21(x1)))))))) | (641) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))) | (642) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(21(x1))))))))) | (643) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (644) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(11(x1)))))))) | (645) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))) | (646) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(11(x1))))))))) | (647) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (648) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(01(x1)))))))) | (649) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))) | (650) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(01(x1))))))))) | (651) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22#(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (652) |
22#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22#(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (653) |
22#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1))))))))))))))) | (654) |
22#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22#(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (655) |
22#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1))))))))))))))) | (656) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1))))))))))))))) | (657) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 22#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (658) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1))))))))))))))) | (659) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 22#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (660) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1))))))))))))))) | (661) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 22#(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (662) |
[20(x1)] | = |
x1 +
|
||||
[21(x1)] | = |
x1 +
|
||||
[22(x1)] | = |
x1 +
|
||||
[10(x1)] | = |
x1 +
|
||||
[11(x1)] | = |
x1 +
|
||||
[12(x1)] | = |
x1 +
|
||||
[00(x1)] | = |
x1 +
|
||||
[01(x1)] | = |
x1 +
|
||||
[02(x1)] | = |
x1 +
|
||||
[20#(x1)] | = |
x1 +
|
||||
[21#(x1)] | = |
x1 +
|
||||
[22#(x1)] | = |
x1 +
|
22(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (573) |
21(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 21(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (574) |
20(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 20(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1)))))))))))))))))) | (575) |
22(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (576) |
21(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 21(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (577) |
20(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 20(10(01(22(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1)))))))))))))))))) | (578) |
22(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (579) |
21(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (580) |
20(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))))) | (581) |
22(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (582) |
21(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (583) |
20(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))))) | (584) |
22(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (585) |
21(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (586) |
20(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20(10(21(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))))) | (587) |
22(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 22(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (588) |
21(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (589) |
20(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 20(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1)))))))))))))))))) | (590) |
22(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 22(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (591) |
21(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (592) |
20(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 20(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1)))))))))))))))))) | (593) |
22(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 22(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (594) |
21(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (595) |
20(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 20(00(12(21(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1)))))))))))))))))) | (596) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(21(x1)))))))) | (598) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))) | (599) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(21(x1))))))))) | (600) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(11(x1)))))))) | (602) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))) | (603) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(11(x1))))))))) | (604) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(01(x1)))))))) | (606) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))) | (607) |
20#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(01(x1))))))))) | (608) |
20#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1))))))))))))))) | (610) |
20#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1))))))))))))))) | (612) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1))))))))))))))) | (614) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1))))))))))))))) | (616) |
20#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1))))))))))))))) | (618) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(21(x1)))))))) | (619) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))) | (621) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(21(x1))))))))) | (622) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(11(x1)))))))) | (623) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))) | (625) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(11(x1))))))))) | (626) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(01(x1)))))))) | (627) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))) | (629) |
21#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(01(x1))))))))) | (630) |
21#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1))))))))))))))) | (632) |
21#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1))))))))))))))) | (634) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1))))))))))))))) | (636) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1))))))))))))))) | (638) |
21#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1))))))))))))))) | (640) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(21(x1)))))))) | (641) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(21(x1)))))))))))))))) | (642) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(21(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(21(x1))))))))) | (643) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(11(x1)))))))) | (645) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(11(x1)))))))))))))))) | (646) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(11(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(11(x1))))))))) | (647) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 20#(00(12(01(02(02(12(01(x1)))))))) | (649) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 21#(10(01(12(11(11(01(22(20(00(12(01(02(02(12(01(x1)))))))))))))))) | (650) |
22#(10(11(21(20(00(02(02(22(10(01(02(12(01(x1)))))))))))))) | → | 22#(20(00(12(01(02(02(12(01(x1))))))))) | (651) |
22#(00(12(01(02(22(10(11(11(01(02(02(12(11(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(12(x1))))))))))))))) | (654) |
22#(00(12(01(02(22(10(11(11(01(02(02(12(01(x1)))))))))))))) | → | 22#(00(02(02(02(02(12(01(02(12(01(12(11(01(02(x1))))))))))))))) | (656) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(21(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(21(x1))))))))))))))) | (657) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(11(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(11(x1))))))))))))))) | (659) |
22#(00(02(12(11(21(00(12(01(12(11(11(11(01(x1)))))))))))))) | → | 21#(00(02(12(01(12(11(01(12(01(02(12(11(11(01(x1))))))))))))))) | (661) |
The dependency pairs are split into 0 components.