((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