|- ∀v w. v + w = n2w (w2n v + w2n w)

|- ∀v w. v * w = n2w (w2n v * w2n w)

|- ∀v w. v + w = n2w (w2n v + w2n w)

|- ∀v w. v * w = n2w (w2n v * w2n w)

|- ∀v w. v + w = n2w (w2n v + w2n w)

|- ∀v w. v * w = n2w (w2n v * w2n w)

|- (∀op x y. BITWISE 0 op x y = 0) ∧
   ∀n op x y.
     BITWISE (SUC n) op x y =
     BITWISE n op x y + SBIT (op (BIT n x) (BIT n y)) n

|- ∀w v. w ⊕ v = n2w (BITWISE 32 (λx y. x ⇎ y) (w2n w) (w2n v))

|- ∀w v. w ⊕ v = n2w (BITWISE 8 (λx y. x ⇎ y) (w2n w) (w2n v))

|- ∀w v. w ⊕ v = n2w (BITWISE 16 (λx y. x ⇎ y) (w2n w) (w2n v))

|- ∀w v. w ‖ v = n2w (BITWISE 32 (λx y. x ∨ y) (w2n w) (w2n v))

|- ∀w v. w ‖ v = n2w (BITWISE 16 (λx y. x ∨ y) (w2n w) (w2n v))

|- ∀w v. w && v = n2w (BITWISE 32 (λx y. x ∧ y) (w2n w) (w2n v))

|- ∀a n. a ≪ n = n2w (2 ** n) * a

|- ∀a n. a ≪ n = n2w (2 ** n) * a

|- ∀a n. a ≪ n = n2w (2 ** n) * a

|- ∀w n. w ⋙ n = n2w (w2n w DIV 2 ** n)

|- ∀w n. w ⋙ n = n2w (w2n w DIV 2 ** n)

|- ∀w n. w ⋙ n = n2w (w2n w DIV 2 ** n)

|- ∀w. word_msb w ⇔ BIT 31 (w2n w)

|- ∀w. word_msb w ⇔ BIT 15 (w2n w)

|- ∀w. word_msb w ⇔ BIT 7 (w2n w)

|- ∀w. word_lsb w ⇔ w2n w MOD 2 ≠ 0

|- ∀w. word_lsb w ⇔ w2n w MOD 2 ≠ 0

|- ∀w. word_lsb w ⇔ w2n w MOD 2 ≠ 0

|- ∀n w.
     w ≫ n =
     if word_msb w then
       n2w (4294967296 − 2 ** (32 − MIN n 32)) ‖ w ⋙ n
     else
       w ⋙ n

|- ∀n w.
     w ≫ n =
     if word_msb w then
       n2w (65536 − 2 ** (16 − MIN n 16)) ‖ w ⋙ n
     else
       w ⋙ n

|- ∀v w. v − w = v + n2w (4294967296 − w2n w)

|- ∀v w. v − w = v + n2w (65536 − w2n w)

|- ∀v w. v − w = v + n2w (256 − w2n w)

|- (h -- l) w = n2w (BITS (MIN h 31) l (w2n w))

|- ∀w n.
     w ⇄ n =
     (let x = n MOD 32 in (31 -- x) w ‖ (x − 1 -- 0) w ≪ (32 − x))

|- ∀w n. w ⇆ n = w ⇄ (32 − n MOD 32)