Files
2023-12-06 21:15:33 +07:00

128 lines
5.9 KiB
Plaintext

((x & 8) >> 4) == Concat(0, Extract(3, 3, x3), 0) >> 4
(((x + 1) & 8) >> 16) == Concat(0, Extract(3, 3, 1 + x3), 0) >> 16
(((x << 2) + 8) & 2) == Concat(0,
Extract(1, 1, 8 + Concat(Extract(29, 0, x3), 0)),
0)
(((x << 4) >> 1) & 6) == Concat(0,
Extract(2, 1, Concat(Extract(27, 0, x3), 0) >> 1),
0)
(((x << 2) & 4) >> 16) == Concat(0, Extract(0, 0, x3), 0) >> 16
(((x << 16) - 13) & 2) == Concat(0,
Extract(1,
1,
4294967283 + Concat(Extract(15, 0, x3), 0)),
0)
(((x >> 1) & 4) >> 16) == Concat(0, Extract(2, 2, x3 >> 1), 0) >> 16
(((x & 2) + 8) >> 16) == Concat(2, Extract(1, 1, x3), 0) >> 16
(((x & 4) << 8) >> 16) == Concat(0, Extract(2, 2, x3), 0) >> 16
(((x & 4) >> 4) + 2) == 2 + (Concat(0, Extract(2, 2, x3), 0) >> 4)
(((x & 4) >> 4) << 4) == Concat(Extract(27, 0, Concat(0, Extract(2, 2, x3), 0) >> 4),
0)
(((x & 4) >> 4) >> 1) == Concat(0, Extract(2, 2, x3), 0) >> 5
(((x & 8) >> 4) & 11) == Concat(0,
Extract(3, 3, Concat(0, Extract(3, 3, x3), 0) >> 4),
0,
Extract(1, 0, Concat(0, Extract(3, 3, x3), 0) >> 4))
rotl((((x & 8) >> 4), 12)) == Concat(Extract(19, 0, Concat(0, Extract(3, 3, x3), 0) >> 4),
Extract(31, 20, Concat(0, Extract(3, 3, x3), 0) >> 4))
rotr((((x & 2) >> 4), 1)) == Concat(Extract(0, 0, Concat(0, Extract(1, 1, x3), 0) >> 4),
Extract(31, 1, Concat(0, Extract(1, 1, x3), 0) >> 4))
(((x & 8) >> 4) ^ 16) == Concat(Extract(31, 5, Concat(0, Extract(3, 3, x3), 0) >> 4),
~Extract(4, 4, Concat(0, Extract(3, 3, x3), 0) >> 4),
Extract(3, 0, Concat(0, Extract(3, 3, x3), 0) >> 4))
(((x & 16) & 16) >> 16) == Concat(0, Extract(4, 4, x3), 0) >> 16
(rotl(((x & 2), 2)) >> 16) == Concat(0, Extract(1, 1, x3), 0) >> 16
(rotr(((x & 8), 3)) >> 7) == Concat(0, Extract(3, 3, x3)) >> 7
(((x & 15) ^ 15) >> 16) == Concat(0, ~Extract(3, 0, x3)) >> 16
((rotl((x, 16)) & 4) >> 16) == Concat(0, Extract(18, 18, x3), 0) >> 16
((rotr((x, 16)) & 4) >> 16) == Concat(0, Extract(18, 18, x3), 0) >> 16
(((x ^ 16) & 1) >> 16) == Concat(0, Extract(0, 0, x3)) >> 16
(((x - 14) & 1) >> 16) == Concat(0, Extract(0, 0, x3)) >> 16
((((x + 1) + 1) & 1) >> 16) == Concat(0, Extract(0, 0, x3)) >> 16
((((x + 4) << 4) >> 1) & 3) == Concat(0,
Extract(1, 0, Concat(4 + Extract(27, 0, x3), 0) >> 1))
(rotl((((x + 1) << 16), 16)) >> 16) == Concat(0, 1 + Extract(15, 0, x3)) >> 16
(rotr((((x + 4) << 16), 16)) >> 16) == Concat(0, 4 + Extract(15, 0, x3)) >> 16
((((x + 16) << 16) - 15) & 11) == Concat(0,
Extract(3,
3,
4294967281 +
Concat(16 + Extract(15, 0, x3), 0)),
1)
((((x + 1) >> 4) & 1) >> 16) == Concat(0, Extract(0, 0, 1 + x3 >> 4)) >> 16
((((x + 5) & 2) + 8) >> 16) == Concat(2, Extract(1, 1, 5 + x3), 0) >> 16
((((x + 1) & 4) << 2) >> 16) == Concat(0, Extract(2, 2, 1 + x3), 0) >> 16
((((x + 1) & 1) >> 16) + 1) == 1 + (Concat(0, 1 + Extract(0, 0, x3)) >> 16)
((((x + 3) & 8) >> 16) << 16) == Concat(Extract(15,
0,
Concat(0, Extract(3, 3, 3 + x3), 0) >> 16),
0)
((((x + 2) & 8) >> 16) >> 8) == Concat(0, Extract(3, 3, 2 + x3), 0) >> 24
((((x + 1) & 2) >> 16) & 2) == Concat(0,
Extract(1,
1,
Concat(0, Extract(1, 1, 1 + x3), 0) >> 16),
0)
rotl(((((x + 2) & 3) >> 16), 3)) == Concat(Extract(28,
0,
Concat(0, 2 + Extract(1, 0, x3)) >> 16),
Extract(31,
29,
Concat(0, 2 + Extract(1, 0, x3)) >> 16))
rotr(((((x + 1) & 2) >> 16), 16)) == Concat(Extract(15,
0,
Concat(0, Extract(1, 1, 1 + x3), 0) >> 16),
Extract(31,
16,
Concat(0, Extract(1, 1, 1 + x3), 0) >> 16))
((((x + 1) & 2) >> 16) ^ 10) == Concat(Extract(31,
4,
Concat(0, Extract(1, 1, 1 + x3), 0) >> 16),
~Extract(3,
3,
Concat(0, Extract(1, 1, 1 + x3), 0) >> 16),
Extract(2,
2,
Concat(0, Extract(1, 1, 1 + x3), 0) >> 16),
~Extract(1,
1,
Concat(0, Extract(1, 1, 1 + x3), 0) >> 16),
Extract(0,
0,
Concat(0, Extract(1, 1, 1 + x3), 0) >> 16))
(rotl((((x + 5) & 16), 1)) >> 16) == Concat(0, Extract(4, 4, 5 + x3), 0) >> 16
(rotr((((x + 13) & 4), 2)) >> 16) == Concat(0, Extract(2, 2, 13 + x3)) >> 16
((((x + 1) & 16) ^ 16) >> 16) == Concat(0, ~Extract(4, 4, 1 + x3), 0) >> 16
((((x + 4) & 12) - 8) & 2) == Concat(0,
Extract(1,
1,
4294967288 +
Concat(0, Extract(3, 2, 4 + x3), 0)),
0)
((rotl(((x + 2), 1)) & 16) >> 16) == Concat(0, Extract(3, 3, 2 + Extract(30, 0, x3)), 0) >> 16
((rotr(((x + 2), 1)) & 2) >> 16) == Concat(0, Extract(2, 2, 2 + x3), 0) >> 16
((((x + 15) ^ 16) & 1) >> 16) == Concat(0, 1 + Extract(0, 0, x3)) >> 16
((((x + 5) - 15) & 1) >> 16) == Concat(0, Extract(0, 0, x3)) >> 16
((((x << 16) + 1) >> 4) & 11) == Concat(0,
Extract(3, 3, Concat(Extract(15, 0, x3), 1) >> 4),
0,
Extract(1, 0, Concat(Extract(15, 0, x3), 1) >> 4))
rotl(((((x << 4) + 16) & 10), 1)) == Concat(0,
Extract(3, 3, 16 + Concat(Extract(27, 0, x3), 0)),
0,
Extract(1, 1, 16 + Concat(Extract(27, 0, x3), 0)),
0)
rotr(((((x << 3) + 16) & 4), 16)) == Concat(0,
Extract(2, 2, 16 + Concat(Extract(28, 0, x3), 0)),
0)
(rotl((((x << 4) + 16), 1)) & 10) == Concat(0,
Extract(2, 2, 16 + Concat(Extract(26, 0, x3), 0)),
0)
(rotr((((x << 16) + 16), 16)) >> 16) == Concat(16, Extract(15, 0, x3)) >> 16
(rotr((((x << 3) + 10), 2)) & 1) == Concat(0, Extract(2, 2, 10 + Concat(Extract(28, 0, x3), 0)))
((((x << 14) << 16) >> 10) << 16) == Concat(Extract(15, 0, Concat(Extract(1, 0, x3), 0) >> 10),
0)
((((x << 14) << 5) >> 16) & 3) == Concat(0,
Extract(1, 0, Concat(Extract(12, 0, x3), 0) >> 16))
(rotl((((x << 3) << 15), 14)) >> 14) == Concat(0, Extract(13, 0, x3)) >> 14