Theory words

⊢ INT_MAX (:α) = INT_MIN (:α) − 1

⊢ INT_MIN (:α) = 2 ** (dimindex (:α) − 1)

⊢ UINT_MAX (:α) = dimword (:α) − 1

⊢ ∀x y carry_in.
    add_with_carry (x,y,carry_in) =
    (let
       unsigned_sum = w2n x + w2n y + if carry_in then 1 else 0;
       result = n2w unsigned_sum;
       carry_out = (w2n result ≠ unsigned_sum) and
       overflow =
         ((word_msb x ⇔ word_msb y) ∧ (word_msb x ⇎ word_msb result))
     in
       (result,carry_out,overflow))

⊢ ∀w. bit_count w = bit_count_upto (dimindex (:α)) w

⊢ ∀n w. bit_count_upto n w = SUM n (λi. if w ' i then 1 else 0)

⊢ ∀h l a.
    bit_field_insert h l a =
    word_modify (λi. COND (l ≤ i ∧ i ≤ h) (a ' (i − l)))

⊢ concat_word_list [] = 0w ∧
  ∀h t.
    concat_word_list (h::t) = w2w h ‖ concat_word_list t ≪ dimindex (:α)

⊢ dimword (:α) = 2 ** dimindex (:α)

⊢ ∀b l. l2w b l = n2w (l2n b l)

⊢ ∀n. n2w n = FCP i. BIT i n

⊢ n2w_itself =
  WFREC (@R. WF R) (λn2w_itself a. case a of (v,v1) => I (n2w v))

⊢ ∀a b.
    nzcv a b =
    (let
       q = w2n a + w2n (-b);
       r = n2w q
     in
       (word_msb r,r = 0w,BIT (dimindex (:α)) q ∨ b = 0w,
        (word_msb a ⇎ word_msb b) ∧ (word_msb r ⇎ word_msb a)))

⊢ reduce_and = word_reduce $/\

⊢ reduce_nand = word_reduce (λa b. ¬(a ∧ b))

⊢ reduce_nor = word_reduce (λa b. ¬(a ∨ b))

⊢ reduce_or = word_reduce $\/

⊢ reduce_xnor = word_reduce $<=>

⊢ reduce_xor = word_reduce (λx y. x ⇎ y)

⊢ ∀b f s. s2w b f s = n2w (s2n b f s)

⊢ ∀a b. saturate_add a b = saturate_n2w (w2n a + w2n b)

⊢ ∀a b. saturate_mul a b = saturate_n2w (w2n a * w2n b)

⊢ ∀n. saturate_n2w n = if dimword (:α) ≤ n then Tw else n2w n

⊢ ∀a b. saturate_sub a b = n2w (w2n a − w2n b)

⊢ ∀w. saturate_w2w w = saturate_n2w (w2n w)

⊢ ∀w. sw2sw w = n2w (SIGN_EXTEND (dimindex (:α)) (dimindex (:β)) (w2n w))

⊢ ∀b w. w2l b w = n2l b (w2n w)

⊢ ∀w. w2n w = SUM (dimindex (:α)) (λi. SBIT (w ' i) i)

⊢ ∀b f w. w2s b f w = n2s b f (w2n w)

⊢ ∀w. w2w w = n2w (w2n w)

⊢ ∀w. ¬w = FCP i. ¬w ' i

⊢ ∀w. -w = n2w (dimword (:α) − w2n w)

⊢ INT_MAXw = n2w (INT_MAX (:α))

⊢ word_L2 = INT_MINw * INT_MINw

⊢ INT_MINw = n2w (INT_MIN (:α))

⊢ Tw = n2w (UINT_MAX (:α))

⊢ ∀w. word_abs w = if w < 0w then -w else w

⊢ ∀v w. v + w = n2w (w2n v + w2n w)

⊢ ∀v w. v && w = FCP i. v ' i ∧ w ' i

⊢ ∀w n. w >>~ n = w ≫ w2n n

⊢ ∀w n.
    w ≫ n =
    FCP i. if dimindex (:α) ≤ i + n then word_msb w else w ' (i + n)

⊢ ∀b w. word_bit b w ⇔ b ≤ dimindex (:α) − 1 ∧ w ' b

⊢ ∀h l.
    (h -- l) = (λw. FCP i. i + l ≤ MIN h (dimindex (:α) − 1) ∧ w ' (i + l))

⊢ ∀a b. word_compare a b = if a = b then 1w else 0w

⊢ ∀v w. v @@ w = w2w (word_join v w)

⊢ ∀v w. v // w = n2w (w2n v DIV w2n w)

⊢ ∀v w. v ** w = n2w (w2n v ** w2n w)

⊢ ∀h l. (h >< l) = w2w ∘ (h -- l)

⊢ word_from_bin_list = l2w 2

⊢ word_from_bin_string = s2w 2 UNHEX

⊢ word_from_dec_list = l2w 10

⊢ word_from_dec_string = s2w 10 UNHEX

⊢ word_from_hex_list = l2w 16

⊢ word_from_hex_string = s2w 16 UNHEX

⊢ word_from_oct_list = l2w 8

⊢ word_from_oct_string = s2w 8 UNHEX

⊢ ∀a b. a ≥ b ⇔ (let (n,z,c,v) = nzcv a b in n ⇔ v)

⊢ ∀a b. a > b ⇔ (let (n,z,c,v) = nzcv a b in ¬z ∧ (n ⇔ v))

⊢ ∀a b. a >₊ b ⇔ (let (n,z,c,v) = nzcv a b in c ∧ ¬z)

⊢ ∀a b. a ≥₊ b ⇔ (let (n,z,c,v) = nzcv a b in c)

⊢ ∀v w.
    word_join v w =
    (let cv = w2w v and cw = w2w w in cv ≪ dimindex (:β) ‖ cw)

⊢ ∀a b. a ≤ b ⇔ (let (n,z,c,v) = nzcv a b in z ∨ (n ⇎ v))

⊢ ∀w. word_len w = dimindex (:α)

⊢ ∀a b. a <₊ b ⇔ (let (n,z,c,v) = nzcv a b in ¬c)

⊢ ∀w. word_log2 w = n2w (LOG2 (w2n w))

⊢ ∀a b. a ≤₊ b ⇔ (let (n,z,c,v) = nzcv a b in ¬c ∨ z)

⊢ ∀w. word_lsb w ⇔ w ' 0

⊢ ∀w n. w <<~ n = w ≪ w2n n

⊢ ∀w n. w ≪ n = FCP i. i < dimindex (:α) ∧ n ≤ i ∧ w ' (i − n)

⊢ ∀w n. w >>>~ n = w ⋙ w2n n

⊢ ∀w n. w ⋙ n = FCP i. i + n < dimindex (:α) ∧ w ' (i + n)

⊢ ∀a b. a < b ⇔ (let (n,z,c,v) = nzcv a b in n ⇎ v)

⊢ ∀a b. word_max a b = if a <₊ b then b else a

⊢ ∀a b. word_min a b = if a <₊ b then a else b

⊢ ∀v w. word_mod v w = n2w (w2n v MOD w2n w)

⊢ ∀f w. word_modify f w = FCP i. f i (w ' i)

⊢ ∀w. word_msb w ⇔ w ' (dimindex (:α) − 1)

⊢ ∀v w. v * w = n2w (w2n v * w2n w)

⊢ ∀v w. v ~&& w = FCP i. ¬(v ' i ∧ w ' i)

⊢ ∀v w. v ~|| w = FCP i. ¬(v ' i ∨ w ' i)

⊢ ∀v w. v ‖ w = FCP i. v ' i ∨ w ' i

⊢ ∀a b.
    a / b =
    if word_msb a then if word_msb b then -a // -b else -(-a // b)
    else if word_msb b then -(a // -b)
    else a // b

⊢ ∀f w.
    word_reduce f w =
    $FCP
      (K
         (let
            l = GENLIST (λi. w ' (dimindex (:α) − 1 − i)) (dimindex (:α))
          in
            FOLDL f (HD l) (TL l)))

⊢ ∀a b.
    word_rem a b =
    if word_msb a then
      if word_msb b then -word_mod (-a) (-b) else -word_mod (-a) b
    else if word_msb b then word_mod a (-b)
    else word_mod a b

⊢ ∀n w.
    word_replicate n w =
    FCP i. i < n * dimindex (:α) ∧ w ' (i MOD dimindex (:α))

⊢ ∀w. word_reverse w = FCP i. w ' (dimindex (:α) − 1 − i)

⊢ ∀w n. w #<<~ n = w ⇆ w2n n

⊢ ∀w n. w ⇆ n = w ⇄ (dimindex (:α) − n MOD dimindex (:α))

⊢ ∀w n. w #>>~ n = w ⇄ w2n n

⊢ ∀w n. w ⇄ n = FCP i. w ' ((i + n) MOD dimindex (:α))

⊢ ∀c w.
    word_rrx (c,w) =
    (word_lsb w,FCP i. if i = dimindex (:α) − 1 then c else (w ⋙ 1) ' i)

⊢ ∀n w. word_sign_extend n w = n2w (SIGN_EXTEND n (dimindex (:α)) (w2n w))

⊢ ∀h l.
    (h --- l) =
    (λw.
         FCP i.
           l ≤ MIN h (dimindex (:α) − 1) ∧
           w ' (MIN (i + l) (MIN h (dimindex (:α) − 1))))

⊢ ∀h l.
    (h '' l) = (λw. FCP i. l ≤ i ∧ i ≤ MIN h (dimindex (:α) − 1) ∧ w ' i)

⊢ ∀a b. word_smax a b = if a < b then b else a

⊢ ∀a b. word_smin a b = if a < b then a else b

⊢ ∀v w. v − w = v + -w

⊢ word_to_bin_list = w2l 2

⊢ word_to_bin_string = w2s 2 HEX

⊢ word_to_dec_list = w2l 10

⊢ word_to_dec_string = w2s 10 HEX

⊢ word_to_hex_list = w2l 16

⊢ word_to_hex_string = w2s 16 HEX

⊢ word_to_oct_list = w2l 8

⊢ word_to_oct_string = w2s 8 HEX

⊢ ∀v w. v ~?? w = FCP i. v ' i ⇔ w ' i

⊢ ∀v w. v ⊕ w = FCP i. v ' i ⇎ w ' i

⊢ ∀x y.
    add_with_carry (x,¬y,T) =
    (x − y,y ≤₊ x,
     (word_msb x ⇎ word_msb y) ∧ (word_msb (x − y) ⇎ word_msb x))

⊢ ∀w m n. w ≫ m ≫ n = w ≫ (m + n)

⊢ ∀w n. dimindex (:α) ≤ n ⇒ w ≫ n = if word_msb w then Tw else 0w

⊢ ∀n. Tw ≫ n = Tw

⊢ ∀n. n < dimword (:α) ⇒ BITS (dimindex (:α) − 1) 0 n = n

⊢ ∀i n. BIT i n ⇔ i ∈ BIT_SET 0 n

⊢ ∀n i.
    BIT_SET i n =
    if n = 0 then ∅
    else if ODD n then i INSERT BIT_SET (SUC i) (n DIV 2)
    else BIT_SET (SUC i) (n DIV 2)

⊢ ∀P. (∀i n.
         (n ≠ 0 ∧ ODD n ⇒ P (SUC i) (n DIV 2)) ∧
         (n ≠ 0 ∧ ¬ODD n ⇒ P (SUC i) (n DIV 2)) ⇒
         P i n) ⇒
      ∀v v1. P v v1

⊢ ∀n x. (n :+ x) = word_modify (λi b. if i = n then x else b)

⊢ INT_MAX (:α) < INT_MIN (:α) ∧ INT_MIN (:α) ≤ UINT_MAX (:α) ∧
  UINT_MAX (:α) < dimword (:α)

⊢ FINITE 𝕌(:'N) ⇒ CARD 𝕌(:'N word) = 2 ** dimindex (:'N)

⊢ ∀h m l w.
    h − m = dimindex (:β) ∧ m + 1 − l = dimindex (:γ) ∧
    h + 1 − l = dimindex (:δ) ∧ dimindex (:β + γ) ≠ 1 ⇒
    (h >< m + 1) w @@ (m >< l) w = (h >< l) w

⊢ 0 < dimindex (:α)

⊢ ∃m. dimindex (:α) = SUC m

⊢ ∀h l w. dimindex (:γ) = h + 1 − l ⇒ (h >< l) w = w2w ((h >< l) w)

⊢ ∀h w. dimindex (:α) − 1 ≤ h ⇒ (h >< 0) w = w2w w

⊢ ∀v w.
    FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ∧
    dimindex (:α) + dimindex (:β) ≤ dimindex (:γ) ⇒
    (dimindex (:β) − 1 >< 0) (v @@ w) = w ∧
    (dimindex (:α) + dimindex (:β) − 1 >< dimindex (:β)) (v @@ w) = v

⊢ ∀h m m' l s w.
    l ≤ m ∧ m' ≤ h ∧ m' = m + 1 ∧ s = m' − l ⇒
    (h >< m') w ≪ s ‖ (m >< l) w =
    (MIN h (MIN (dimindex (:β) + l − 1) (dimindex (:α) − 1)) >< l) w

⊢ ∀h m m' l s w.
    l ≤ m ∧ m' ≤ h ∧ m' = m + 1 ∧ s = m' − l ⇒
    (h >< m') w ≪ s + (m >< l) w =
    (MIN h (MIN (dimindex (:β) + l − 1) (dimindex (:α) − 1)) >< l) w

⊢ ∀h m m' l s n w.
    l ≤ m ∧ m' ≤ h ∧ m' = m + 1 ∧ s = m' − l + n ⇒
    (h >< m') w ≪ s + (m >< l) w ≪ n =
    (MIN h (MIN (dimindex (:β) + l − 1) (dimindex (:α) − 1)) >< l) w ≪ n

⊢ ∀h m m' l s n w.
    l ≤ m ∧ m' ≤ h ∧ m' = m + 1 ∧ s = m' − l + n ⇒
    (h >< m') w ≪ s ‖ (m >< l) w ≪ n =
    (MIN h (MIN (dimindex (:β) + l − 1) (dimindex (:α) − 1)) >< l) w ≪ n

⊢ $FCP (K T) = Tw ∧ $FCP (K F) = 0w

⊢ ((∀a b. FST (add_with_carry (a,b,F)) = a + b) ∧
   (∀a b. FST (add_with_carry (a,¬b,T)) = a − b) ∧
   ∀a b. FST (add_with_carry (¬a,b,T)) = b − a) ∧
  (∀n a. FST (add_with_carry (a,n2w n,T)) = a − ¬n2w n) ∧
  ∀n b. FST (add_with_carry (n2w n,b,T)) = b − ¬n2w n

⊢ INT_MAX (:α) < dimword (:α)

⊢ INT_MIN (:unit) = 1

⊢ INT_MIN (:10) = 512

⊢ INT_MIN (:11) = 1024

⊢ INT_MIN (:12) = 2048

⊢ INT_MIN (:128) = 170141183460469231731687303715884105728

⊢ INT_MIN (:16) = 32768

⊢ INT_MIN (:2) = 2

⊢ INT_MIN (:20) = 524288

⊢ INT_MIN (:24) = 8388608

⊢ INT_MIN (:28) = 134217728

⊢ INT_MIN (:3) = 4

⊢ INT_MIN (:30) = 536870912

⊢ INT_MIN (:32) = 2147483648

⊢ INT_MIN (:4) = 8

⊢ INT_MIN (:48) = 140737488355328

⊢ INT_MIN (:5) = 16

⊢ INT_MIN (:56) = 36028797018963968

⊢ INT_MIN (:6) = 32

⊢ INT_MIN (:64) = 9223372036854775808

⊢ INT_MIN (:7) = 64

⊢ INT_MIN (:8) = 128

⊢ INT_MIN (:9) = 256

⊢ INT_MIN (:96) = 39614081257132168796771975168

⊢ INT_MIN (:α) < dimword (:α)

⊢ INT_MIN (:α + β) =
  if FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) then dimword (:α) * INT_MIN (:β)
  else INT_MIN (:α + β)

⊢ ∀w. w ≠ 0w ⇒ (LEAST i. w ' i) < dimindex (:α)

⊢ LENGTH (word_to_bin_list w) ≤ dimindex (:α)

⊢ ∀w. w ≠ 0w ⇒
      LOG2 (w2n w) =
      dimindex (:α) − 1 − LEAST i. w ' (dimindex (:α) − 1 − i)

⊢ ∀w. w ≠ 0w ⇒ LOG2 (w2n w) < dimindex (:α)

⊢ ∀w m n. w ≪ m ≪ n = w ≪ (m + n)

⊢ (∀n v w. w ≪ n && v ≪ n = (w && v) ≪ n) ∧
  (∀n v w. w ≪ n ‖ v ≪ n = (w ‖ v) ≪ n) ∧
  ∀n v w. w ≪ n ⊕ v ≪ n = (w ⊕ v) ≪ n

⊢ ∀w n. dimindex (:α) ≤ n ⇒ w ≪ n = 0w

⊢ ∀w. w ≪ 1 = w + w

⊢ ∀n. Tw ≪ n = n2w (dimword (:α) − 2 ** n)

⊢ ∀w m n. w ⋙ m ⋙ n = w ⋙ (m + n)

⊢ (∀n v w. w ⋙ n && v ⋙ n = (w && v) ⋙ n) ∧
  (∀n v w. w ⋙ n ‖ v ⋙ n = (w ‖ v) ⋙ n) ∧
  ∀n v w. w ⋙ n ⊕ v ⋙ n = (w ⊕ v) ⋙ n

⊢ ∀m y. y ≠ 0w ∧ 0 < m ⇒ w2n (y ⋙ m) < w2n y

⊢ ∀w n. dimindex (:α) ≤ n ⇒ w ⋙ n = 0w

⊢ 1 < b ∧ MEM x (w2l b w) ⇒ x < b

⊢ ∀n. n MOD dimword (:α) = MOD_2EXP (dimindex (:α)) n

⊢ ∀n q a.
    0 < n ∧ 0 < q ∧ a < q * n ⇒ (q * n − a) MOD n = (n − a MOD n) MOD n

⊢ ∀n. n MOD dimword (:α) = BITS (dimindex (:α) − 1) 0 n

⊢ ∀w. w ≠ 0w ⇒ ∃i. i < dimindex (:α) ∧ w ' i

⊢ INFINITE 𝕌(:α) ⇒ dimword (:α) = 2

⊢ INT_MINw ≠ 0w

⊢ ∀w. w ≠ Tw ⇒ ∃i. i < dimindex (:α) ∧ ¬w ' i

⊢ (∀m n.
     m < NUMERAL (BIT1 n) ⇔
     m = NUMERAL (BIT1 n) − 1 ∨ m < NUMERAL (BIT1 n) − 1) ∧
  ∀m n. m < NUMERAL (BIT2 n) ⇔ m = NUMERAL (BIT1 n) ∨ m < NUMERAL (BIT1 n)

⊢ 1 < dimword (:α)

⊢ ∀w m n. w ⇆ m ⇆ n = w ⇆ (m + n)

⊢ (∀n v w. w ⇆ n && v ⇆ n = (w && v) ⇆ n) ∧
  (∀n v w. w ⇆ n ‖ v ⇆ n = (w ‖ v) ⇆ n) ∧
  ∀n v w. w ⇆ n ⊕ v ⇆ n = (w ⊕ v) ⇆ n

⊢ ∀w n. w ⇆ (n MOD dimindex (:α)) = w ⇆ n

⊢ ∀w m n. w ⇄ m ⇄ n = w ⇄ (m + n)

⊢ (∀n v w. w ⇄ n && v ⇄ n = (w && v) ⇄ n) ∧
  (∀n v w. w ⇄ n ‖ v ⇄ n = (w ‖ v) ⇄ n) ∧
  ∀n v w. w ⇄ n ⊕ v ⇄ n = (w ⊕ v) ⇄ n

⊢ ∀w n. w ⇄ (n * dimindex (:α)) = w

⊢ ∀w n. w ⇄ (n MOD dimindex (:α)) = w ⇄ n

⊢ ∀w n. w ⇄ n ⇆ n = w ∧ w ⇆ n ⇄ n = w

⊢ ∀n. Tw ⇄ n = Tw

⊢ ∀i n. i < dimindex (:α) ⇒ ((1w ≪ n − 1w) ' i ⇔ i < n)

⊢ (∀a. a ≪ 0 = a) ∧ (∀a. a ≫ 0 = a) ∧ (∀a. a ⋙ 0 = a) ∧ (∀a. a ⇆ 0 = a) ∧
  ∀a. a ⇄ 0 = a

⊢ ∀x. x ≠ 0w ⇒ SUC (w2n (x − 1w)) = w2n x

⊢ ∀a. word_msb a ⇒
      if dimindex (:α) − 1 = 0 ∨ a = INT_MINw then word_msb (-a)
      else ¬word_msb (-a)

⊢ ∀a. ¬word_msb a ⇒ a = 0w ∨ word_msb (-a)

⊢ ∀a. a ≠ 0w ∧ a ≠ INT_MINw ⇒ (¬word_msb a ⇔ word_msb (-a))

⊢ ∀w. 0w ≤₊ w

⊢ ¬word_msb 0w

⊢ ∀n a. -a ≪ n = -(a ≪ n)

⊢ (∀w. w + 0w = w) ∧ ∀w. 0w + w = w

⊢ ∀v w x. v + (w + x) = v + w + x

⊢ ∀n a b.
    n < dimindex (:α) ⇒
    ((a + b) ' n ⇔
     if n = 0 then a ' 0 ⇎ b ' 0
     else if ((n − 1 -- 0) a + (n − 1 -- 0) b) ' n then a ' n ⇔ b ' n
     else a ' n ⇎ b ' n)

⊢ ∀a b. (a + b) ' 0 ⇔ (a ' 0 ⇎ b ' 0)

⊢ ∀v w. v + w = w + v

⊢ ∀v w x. v + w = x ⇔ v = x − w

⊢ ∀v w. v + w = v ⇔ w = 0w

⊢ ∀b c a.
    a + b <₊ c ⇔
    if b ≤₊ c then
      (let x = n2w (w2n c − w2n b) in a <₊ x ∨ b ≠ 0w ∧ -c + x ≤₊ a)
    else -b ≤₊ a ∧ a <₊ -b + c

⊢ ∀c a. c + a <₊ a ⇔ a ≠ 0w ∧ (c ≠ 0w ∧ -c <₊ a ∨ a = -c)

⊢ ∀b c a.
    a + b ≤₊ c ⇔
    if b ≤₊ c then
      (let x = n2w (w2n c − w2n b) in a ≤₊ x ∨ b ≠ 0w ∧ -c + x ≤₊ a)
    else -b ≤₊ a ∧ a ≤₊ -b + c

⊢ ∀c a. c + a ≤₊ a ⇔ c = 0w ∨ a ≠ 0w ∧ (-c <₊ a ∨ a = -c)

⊢ ∀v w. v + w = w ⇔ v = 0w

⊢ ∀w. -w + w = 0w

⊢ ∀n a b. (a + b) ≪ n = a ≪ n + b ≪ n

⊢ ∀a b. a && b = 0w ⇒ a + b = a ‖ b

⊢ ∀v w. v + w = v ⇔ w = 0w

⊢ ∀c a b.
    a <₊ b + c ⇔
    if c ≤₊ a then
      (let x = n2w (w2n a − w2n c) in x <₊ b ∧ (c = 0w ∨ b <₊ -a + x))
    else b <₊ -c ∨ -c + a <₊ b

⊢ ∀c a. a <₊ c + a ⇔ c ≠ 0w ∧ (a = 0w ∨ a <₊ -c)

⊢ ∀c a b.
    a ≤₊ b + c ⇔
    if c ≤₊ a then
      (let x = n2w (w2n a − w2n c) in x ≤₊ b ∧ (c = 0w ∨ b <₊ -a + x))
    else b <₊ -c ∨ -c + a ≤₊ b

⊢ ∀c a. a ≤₊ c + a ⇔ a = 0w ∨ c = 0w ∨ a <₊ -c

⊢ ∀w. w + -w = 0w

⊢ ∀v w. v + w − w = v

⊢ ∀v w. w + v − w = v

⊢ ∀v x. v − (v + x) = -x

⊢ ∀v w x. v + w − x = v + (w − x)

⊢ ∀v w x. v + w − x = v − x + w

⊢ ∀a b. a && b = 0w ⇒ a + b = a ⊕ b

⊢ ∀w h. dimindex (:α) − 1 ≤ h ⇒ (h -- 0) w = w

⊢ ∀a b. a ‖ a && b = a

⊢ ∀a b c. (a && b) && c = a && b && c

⊢ ∀a. Tw && a = a ∧ a && Tw = a ∧ 0w && a = 0w ∧ a && 0w = 0w ∧ a && a = a

⊢ ∀a b. a && b = b && a

⊢ ∀a. a && ¬a = 0w

⊢ ∀m n. n2w n && n2w (2 ** m − 1) = n2w (n MOD 2 ** m)

⊢ ∀a. a && a = a

⊢ ∀h1 l1 h2 l2 w.
    (h2 -- l2) ((h1 -- l1) w) = (MIN h1 (h2 + l1) -- l2 + l1) w

⊢ ∀h l w. (h -- l) w = (h >< l) w

⊢ ∀h l n w.
    h < dimindex (:α) ⇒
    (h -- l) (w ≪ n) = if n ≤ h then (h − n -- l − n) w ≪ (n − l) else 0w

⊢ ∀h l w n. (h -- l) w ⋙ n = (h -- l + n) w

⊢ ∀h l w. w2n ((h -- l) w) < 2 ** (SUC h − l)

⊢ ∀w h l. dimindex (:α) − 1 < h ⇒ (h -- l) w = (dimindex (:α) − 1 -- l) w

⊢ (∀h l v w. (h -- l) v && (h -- l) w = (h -- l) (v && w)) ∧
  (∀h l v w. (h -- l) v ‖ (h -- l) w = (h -- l) (v ‖ w)) ∧
  ∀h l v w. (h -- l) v ⊕ (h -- l) w = (h -- l) (v ⊕ w)

⊢ ∀h l w. (h -- l) ((h '' l) w) = (h -- l) w

⊢ ∀h l w. h < l ⇒ (h -- l) w = 0w

⊢ ∀h l. (h -- l) 0w = 0w

⊢ ∀h l w. dimindex (:α) ≤ l ⇒ (h -- l) w = 0w

⊢ ∀b w. word_bit b w ⇔ (b -- b) w = 1w

⊢ ∀a b. ¬(a && b) = ¬a ‖ ¬b ∧ ¬(a ‖ b) = ¬a && ¬b

⊢ ∀w. w ≠ 0w ⇒ ∀v. v = v // w * w + word_mod v w ∧ word_mod v w <₊ w

⊢ ∀m n. n < dimindex (:α) ⇒ m ⋙ n = m // n2w (2 ** n)

⊢ ∀v w. (∀x. x < dimindex (:α) ⇒ (word_bit x v ⇔ word_bit x w)) ⇔ v = w

⊢ ∀v w x. v + w = v + x ⇔ w = x

⊢ ∀v w x. v + w = x + w ⇔ v = x

⊢ ∀v w. -v = -w ⇔ v = w

⊢ ∀v w x. v = w − x ⇔ v + x = w

⊢ ∀v w x. v − w = x ⇔ v = x + w

⊢ ∀w v. v − w = 0w ⇔ v = w

⊢ ∀n l k j h. (j >< k) ((h -- l) n) = (MIN h (j + l) >< k + l) n

⊢ ∀w h l m n.
    (h >< l) ((m >< n) w) =
    (MIN m (MIN (h + n) (MIN (dimindex (:γ) − 1) (dimindex (:β) + n − 1))) ><
     l + n) w

⊢ ∀w h. w2n w < 2 ** SUC h ⇒ (h >< 0) w = w

⊢ ∀h l n w.
    h < dimindex (:α) ⇒
    (h >< l) (w ≪ n) = if n ≤ h then (h − n >< l − n) w ≪ (n − l) else 0w

⊢ ∀h l n w.
    dimindex (:β) + l ≤ h + n ⇒
    (h >< l) w ≪ n = (dimindex (:β) + l − (n + 1) >< l) w ≪ n

⊢ ∀h l w. w2n ((h >< l) w) < 2 ** (SUC h − l)

⊢ (∀h l w.
     dimindex (:α) ≤ dimindex (:β) + l ∧ dimindex (:α) ≤ h ⇒
     (h >< l) w = (dimindex (:α) − 1 >< l) w) ∧
  ∀h l w.
    dimindex (:β) + l < dimindex (:α) ∧ dimindex (:β) + l ≤ h ⇒
    (h >< l) w = (dimindex (:β) + l − 1 >< l) w

⊢ ∀a b h.
    dimindex (:β) − 1 ≤ h ∧ dimindex (:β) ≤ dimindex (:α) ⇒
    (h >< 0) (a + b) = (h >< 0) a + (h >< 0) b

⊢ ∀a b h.
    h < dimindex (:α) ⇒
    (h >< 0) ((h >< 0) a + (h >< 0) b) = (h >< 0) (a + b)

⊢ (∀h l v w. (h >< l) v && (h >< l) w = (h >< l) (v && w)) ∧
  (∀h l v w. (h >< l) v ‖ (h >< l) w = (h >< l) (v ‖ w)) ∧
  ∀h l v w. (h >< l) v ⊕ (h >< l) w = (h >< l) (v ⊕ w)

⊢ ∀a b h.
    dimindex (:β) − 1 ≤ h ∧ dimindex (:β) ≤ dimindex (:α) ⇒
    (h >< 0) (a * b) = (h >< 0) a * (h >< 0) b

⊢ ∀a b h.
    h < dimindex (:α) ⇒
    (h >< 0) ((h >< 0) a * (h >< 0) b) = (h >< 0) (a * b)

⊢ ∀h l w. h < l ⇒ (h >< l) w = 0w

⊢ ∀h l. (h >< l) 0w = 0w

⊢ ∀h l w. dimindex (:α) ≤ l ⇒ (h >< l) w = 0w

⊢ ∀s. FINITE s

⊢ ∀a b.
    a ≥ b ⇔
    (word_msb b ⇔ word_msb a) ∧ w2n a ≥ w2n b ∨ word_msb b ∧ ¬word_msb a

⊢ ∀a b. a > b ⇔ b < a

⊢ ∀a b. a ≥ b ⇔ b ≤ a

⊢ ∀a b. a ≥ b ⇔ a > b ∨ a = b

⊢ ∀a b.
    a > b ⇔
    (word_msb b ⇔ word_msb a) ∧ w2n a > w2n b ∨ word_msb b ∧ ¬word_msb a

⊢ ∀a b. a >₊ b ⇔ w2n a > w2n b

⊢ ∀a b. a >₊ b ⇔ b <₊ a

⊢ ∀a b. a ≥₊ b ⇔ b ≤₊ a

⊢ ∀a b. a ≥₊ b ⇔ a >₊ b ∨ a = b

⊢ ∀a b. a ≥₊ b ⇔ w2n a ≥ w2n b

⊢ ¬word_msb INT_MAXw

⊢ INT_MAXw = INT_MINw − 1w

⊢ ∀P. P 0w ∧ (∀n. SUC n < dimword (:α) ⇒ P (n2w n) ⇒ P (n2w (SUC n))) ⇒
      ∀x. P x

⊢ ∀v w x. v − w = x − w ⇔ v = x

⊢ ∀a b.
    a ≤ b ⇔
    (word_msb a ⇔ word_msb b) ∧ w2n a ≤ w2n b ∨ word_msb a ∧ ¬word_msb b

⊢ ∀v w x. v * (w + x) = v * w + v * x

⊢ ∀a b c. a && (b ‖ c) = a && b ‖ a && c

⊢ ∀a b c. a && (b ⊕ c) = a && b ⊕ a && c

⊢ ∀a b c. a ‖ b && c = (a ‖ b) && (a ‖ c)

⊢ ∀v w x. v * (w − x) = v * w − v * x

⊢ ¬(0w < -1w) ∧ ¬(0w ≤ -1w) ∧ -1w < 0w ∧ -1w ≤ 0w

⊢ ∀a b. ¬(a < b ∧ b < a)

⊢ ∀a b. a < b ∨ b ≤ a

⊢ ∀a b. ¬(a < b) ∧ a ≠ b ⇒ b < a

⊢ ∀a b. a ≤ b ∧ b ≤ a ⇒ a = b

⊢ ∀a b. ¬(a < b ∧ b ≤ a)

⊢ ∀a b. a ≤ b ∨ b ≤ a

⊢ ∀a. a ≤ INT_MAXw

⊢ ∀a b c. a ≤ b ∧ b < c ⇒ a < c

⊢ ∀a. a ≤ a

⊢ ∀a b c. a ≤ b ∧ b ≤ c ⇒ a ≤ c

⊢ ∀a b. a < b ⇒ a ≤ b

⊢ ∀a b. a = b ∨ a < b ∨ b < a

⊢ ∀a b c. a < b ∧ b ≤ c ⇒ a < c

⊢ ∀a b. -a <₊ b ⇔ b ≠ 0w ∧ (a = 0w ∨ -b <₊ a)

⊢ ∀a b. a <₊ -b ⇔ b ≠ 0w ∧ (a = 0w ∨ b <₊ -a)

⊢ ∀a b. a < b ⇒ a ≠ b

⊢ ∀a b. a ≤ b ⇔ a < b ∨ a = b

⊢ ∀a. ¬(a < a)

⊢ ∀a b c. a < b ∧ b < c ⇒ a < c

⊢ ∀x y. 0w ≤ x ∧ 0w ≤ y ⇒ (x ≤ y ⇔ x ≤₊ y)

⊢ ∀a b.
    a ≤ b ⇔
    INT_MINw ≤₊ a ∧ (b <₊ INT_MINw ∨ a ≤₊ b) ∨
    a <₊ INT_MINw ∧ b <₊ INT_MINw ∧ a ≤₊ b

⊢ (∀m n. -n2w m + -n2w n = -n2w (m + n)) ∧
  ∀m n. n2w m + -n2w n = if n ≤ m then n2w (m − n) else -n2w (n − m)

⊢ (∀n m.
     n2w n && n2w m = n2w (BITWISE (SUC (MIN (LOG2 n) (LOG2 m))) $/\ n m)) ∧
  (∀n m. n2w n && ¬n2w m = n2w (BITWISE (SUC (LOG2 n)) (λa b. a ∧ ¬b) n m)) ∧
  (∀n m. ¬n2w m && n2w n = n2w (BITWISE (SUC (LOG2 n)) (λa b. a ∧ ¬b) n m)) ∧
  ∀n m.
    ¬n2w n && ¬n2w m = ¬n2w (BITWISE (SUC (MAX (LOG2 n) (LOG2 m))) $\/ n m)

⊢ (∀m n. n2w m * -n2w n = -n2w (m * n)) ∧
  ∀m n. -n2w m * -n2w n = n2w (m * n)

⊢ (∀n m.
     n2w n ‖ n2w m = n2w (BITWISE (SUC (MAX (LOG2 n) (LOG2 m))) $\/ n m)) ∧
  (∀n m. n2w n ‖ ¬n2w m = ¬n2w (BITWISE (SUC (LOG2 m)) (λa b. a ∧ ¬b) m n)) ∧
  (∀n m. ¬n2w m ‖ n2w n = ¬n2w (BITWISE (SUC (LOG2 m)) (λa b. a ∧ ¬b) m n)) ∧
  ∀n m.
    ¬n2w n ‖ ¬n2w m = ¬n2w (BITWISE (SUC (MIN (LOG2 n) (LOG2 m))) $/\ n m)

⊢ ∀n m.
    n2w n ⊕ n2w m =
    n2w (BITWISE (SUC (MAX (LOG2 n) (LOG2 m))) (λx y. x ⇎ y) n m)

⊢ ∀a b. a <₊ b ⇔ w2n a < w2n b

⊢ ∀a b. ¬(a <₊ b ∧ b <₊ a)

⊢ ∀a b. a <₊ b ∨ b ≤₊ a

⊢ ∀a b. ¬(a <₊ b) ∧ a ≠ b ⇒ b <₊ a

⊢ ∀a b. a ≤₊ b ∧ b ≤₊ a ⇒ a = b

⊢ ∀a b. ¬(a <₊ b ∧ b ≤₊ a)

⊢ ∀a b. a ≤₊ b ∨ b ≤₊ a

⊢ ∀a b c. a ≤₊ b ∧ b <₊ c ⇒ a <₊ c

⊢ ∀a. a ≤₊ a

⊢ ∀a b c. a ≤₊ b ∧ b ≤₊ c ⇒ a ≤₊ c

⊢ ∀a b. a <₊ b ⇒ a ≤₊ b

⊢ ∀a b. a = b ∨ a <₊ b ∨ b <₊ a

⊢ ∀a b c. a <₊ b ∧ b ≤₊ c ⇒ a <₊ c

⊢ ∀a b. a <₊ b ⇒ a ≠ b

⊢ ∀a b. a ≤₊ b ⇔ a <₊ b ∨ a = b

⊢ ∀a. ¬(a <₊ a)

⊢ ∀a b c. a <₊ b ∧ b <₊ c ⇒ a <₊ c

⊢ (∀n. 0w <₊ n ⇔ n ≠ 0w) ∧ ∀n. ¬(n <₊ 0w)

⊢ ∀n. ¬(n <₊ 0w)

⊢ (∀n. ¬(-1w <₊ n)) ∧ ∀n. n <₊ -1w ⇔ n ≠ -1w

⊢ ∀n. ¬(-1w <₊ n)

⊢ ∀n. ¬(n <₊ -1w) ⇔ n = -1w

⊢ ∀a b. a ≤₊ b ⇔ w2n a ≤ w2n b

⊢ ∀w. w ≤₊ Tw

⊢ ∀n. n ≤₊ 0w ⇔ n = 0w

⊢ (∀n. -1w ≤₊ n ⇔ n = -1w) ∧ ∀n. n ≤₊ -1w

⊢ ∀a b.
    a < b ⇔
    (word_msb a ⇔ word_msb b) ∧ w2n a < w2n b ∨ word_msb a ∧ ¬word_msb b

⊢ ∀x y. 0w ≤ x ∧ 0w ≤ y ⇒ (x < y ⇔ x <₊ y)

⊢ ∀a b.
    a < b ⇔
    INT_MINw ≤₊ a ∧ (b <₊ INT_MINw ∨ a <₊ b) ∨
    a <₊ INT_MINw ∧ b <₊ INT_MINw ∧ a <₊ b

⊢ ∀x y. 0w < y ∧ y < x ⇒ x − y < x

⊢ ∀a. INT_MINw ≤ a

⊢ INT_MINw < INT_MAXw

⊢ word_msb INT_MINw

⊢ INT_MINw + INT_MAXw = Tw

⊢ ∀f w i. i < dimindex (:α) ⇒ (word_modify f w ' i ⇔ f i (w ' i))

⊢ ∀m. word_mod m 1w = 0w

⊢ ∀m v. v < dimindex (:α) − 1 ⇒ word_mod m (n2w (2 ** SUC v)) = (v -- 0) m

⊢ ∀w. word_msb (¬w) ⇔ ¬word_msb w

⊢ ∀a. word_msb a ⇔ INT_MINw ≤₊ a

⊢ ∀v w x. v * (w * x) = v * w * x

⊢ ∀v w.
    0w * v = 0w ∧ v * 0w = 0w ∧ 1w * v = v ∧ v * 1w = v ∧
    (v + 1w) * w = v * w + w ∧ v * (w + 1w) = v + v * w

⊢ ∀v w. v * w = w * v

⊢ ∀v n. v * n2w (n + 1) = v * n2w n + v

⊢ ∀a n. a ≪ n = n2w (2 ** n) * a

⊢ ∀a b. a ~&& b = ¬(a && b)

⊢ ∀w. -w = ¬w + 1w

⊢ ∀v w. -1w * v = -1w * w ⇔ v = w

⊢ ∀v w. v * -1w = w * -1w ⇔ v = w

⊢ -0w = 0w

⊢ -1w = Tw

⊢ ∀i. i < dimindex (:α) ⇒ (-1w) ' i

⊢ ∀v w. -(v + w) = -v + -w

⊢ ∀w v. -v = w ⇔ v = -w

⊢ -v = 0w ⇔ v = 0w

⊢ -INT_MINw = INT_MINw

⊢ ∀v w. -(v * w) = -v * w

⊢ ∀w. -w = -1w * w

⊢ ∀w. - -w = w

⊢ ∀v w. -(v * w) = v * -w

⊢ ∀w v. -(v − w) = w − v

⊢ -Tw = 1w

⊢ ∀a b. a ~|| b = ¬(a ‖ b)

⊢ ∀w. ¬w = -w − 1w

⊢ ¬0w = Tw

⊢ ∀a b. ¬(a > b) ⇔ a ≤ b

⊢ ∀a b. ¬(a >₊ b) ⇔ a ≤₊ b

⊢ ∀a b. ¬(a < b) ⇔ b ≤ a

⊢ ∀a b. a = b ⇒ ¬(a < b)

⊢ ∀a b. ¬(a ≤ b) ⇔ b < a

⊢ ∀a b. ¬(a <₊ b) ⇔ b ≤₊ a

⊢ ∀a b. a = b ⇒ ¬(a <₊ b)

⊢ ∀a b. ¬(a ≤₊ b) ⇔ b <₊ a

⊢ ∀a. ¬¬a = a

⊢ ¬Tw = 0w

⊢ ∀a b. ¬a ⊕ ¬b = a ⊕ b ∧ a ⊕ ¬b = ¬(a ⊕ b) ∧ ¬a ⊕ b = ¬(a ⊕ b)

⊢ ∀a b. a && (a ‖ b) = a

⊢ ∀a b c. (a ‖ b) ‖ c = a ‖ b ‖ c

⊢ ∀a. Tw ‖ a = Tw ∧ a ‖ Tw = Tw ∧ 0w ‖ a = a ∧ a ‖ 0w = a ∧ a ‖ a = a

⊢ ∀a b. a ‖ b = b ‖ a

⊢ ∀a. a ‖ ¬a = Tw

⊢ ∀a. a ‖ a = a

⊢ ∀m. m ≠ 0w ⇒ w2n (m − 1w) < w2n m

⊢ ∀v w x. v − w = v − x ⇔ w = x

⊢ ∀v w x. (v + w) * x = v * x + w * x

⊢ ∀a b c. (a ‖ b) && c = a && c ‖ b && c

⊢ ∀a b c. (a ⊕ b) && c = a && c ⊕ b && c

⊢ ∀a b c. a && b ‖ c = (a ‖ c) && (b ‖ c)

⊢ ∀v w x. (w − x) * v = w * v − x * v

⊢ ∀P. P ∅ ∧ (∀s. P s ⇒ ∀e. e ∉ s ⇒ P (e INSERT s)) ⇒ ∀s. P s

⊢ ∀h w. (h '' 0) w = (h -- 0) w

⊢ ∀h m' m l w.
    l ≤ m ∧ m' = m + 1 ∧ m < h ⇒ (h '' m') w ‖ (m '' l) w = (h '' l) w

⊢ (∀h l v w. (h '' l) v && (h '' l) w = (h '' l) (v && w)) ∧
  (∀h l v w. (h '' l) v ‖ (h '' l) w = (h '' l) (v ‖ w)) ∧
  ∀h l v w. (h '' l) v ⊕ (h '' l) w = (h '' l) (v ⊕ w)

⊢ ∀h l w. (h '' l) w = (h -- l) w ≪ l

⊢ ∀h l w. h < l ⇒ (h '' l) w = 0w

⊢ ∀l h. (h '' l) 0w = 0w

⊢ ∀v w. -w + v = v − w

⊢ ∀v w. v − w + w = v

⊢ ∀v w. v + (w − v) = w

⊢ (∀x y. -y + x = x − y) ∧ (∀x y. x + -y = x − y) ∧
  (∀x y z. -x * y + z = z − x * y) ∧ (∀x y z. z + -x * y = z − x * y) ∧
  (∀x. -1w * x = -x) ∧ (∀x y z. z − -x * y = z + x * y) ∧
  ∀x y z. -x * y − z = -(x * y + z)

⊢ ∀x y. 0w ≤ y ∧ y ≤ x ⇒ 0w ≤ x − y ∧ x − y ≤ x

⊢ ∀v w. -v − w = -(v + w)

⊢ ∀x y. 0w < y ∧ y < x ⇒ 0w < x − y ∧ x − y < x

⊢ ∀w. 0w − w = -w

⊢ ∀v w. -v − -w = w − v

⊢ ∀v w x. v − (w + x) = v − w − x

⊢ ∀w. w − w = 0w

⊢ ∀v w. v − -w = v + w

⊢ ∀w. w − 0w = w

⊢ ∀v w x. v − (w − x) = v + x − w

⊢ ∀v w. v − (v − w) = w

⊢ ∀w v. v − w − v = -w

⊢ ∀v w x. v − w + (w − x) = v − x

⊢ ∀a b. a + b = 0w ⇔ a = -b

⊢ ∀a b. a ~?? b = ¬(a ⊕ b)

⊢ ∀a b. a ⊕ b = a && ¬b ‖ b && ¬a

⊢ ∀a b c. (a ⊕ b) ⊕ c = a ⊕ b ⊕ c

⊢ ∀a. Tw ⊕ a = ¬a ∧ a ⊕ Tw = ¬a ∧ 0w ⊕ a = a ∧ a ⊕ 0w = a ∧ a ⊕ a = 0w

⊢ ∀a b. a ⊕ b = b ⊕ a

⊢ ∀a. a ⊕ ¬a = Tw

⊢ ∀w. 0w ≤ w ⇔ w2n w < INT_MIN (:α)

⊢ ∀w. w2w w = (dimindex (:α) − 1 >< 0) w

⊢ ∀a b. w2w (a + b) = (dimindex (:α) − 1 -- 0) (w2w a + w2w b)

⊢ (∀v w. w2w v && w2w w = w2w (v && w)) ∧
  (∀v w. w2w v ‖ w2w w = w2w (v ‖ w)) ∧ ∀v w. w2w v ⊕ w2w w = w2w (v ⊕ w)

⊢ ∀a b. w2w (a * b) = (dimindex (:α) − 1 -- 0) (w2w a * w2w b)

⊢ 0 ≤ INT_MAX (:α)

⊢ 0w <₊ INT_MINw

⊢ 1 < dimindex (:α) ⇒ 0 < INT_MAX (:α)

⊢ 0 < INT_MIN (:α)

⊢ 0 < UINT_MAX (:α)

⊢ 0 < dimword (:α)

⊢ (∀n. 0w ≪ n = 0w) ∧ (∀n. 0w ≫ n = 0w) ∧ (∀n. 0w ⋙ n = 0w) ∧
  (∀n. 0w ⇆ n = 0w) ∧ ∀n. 0w ⇄ n = 0w

⊢ ∀w. bit_count w = 0 ⇔ w = 0w

⊢ ∀w. bit_count_upto 0 w = 0

⊢ ∀w n.
    bit_count_upto (SUC n) w =
    (if w ' n then 1 else 0) + bit_count_upto n w

⊢ ∀n w. bit_count_upto n w = 0 ⇔ ∀i. i < n ⇒ ¬w ' i

⊢ ∀h l a b.
    h < l + dimindex (:α) ⇒
    bit_field_insert h l a b =
    (let mask = (h '' l) (-1w) in w2w a ≪ l && mask ‖ b && ¬mask)

⊢ h1 < l2 ∨ h2 < l1 ⇒
  bit_field_insert h1 l1 a1 (bit_field_insert h2 l2 a2 b) =
  bit_field_insert h2 l2 a2 (bit_field_insert h1 l1 a1 b)

⊢ h + 1 − l ≤ dimindex (:α) ∧ h + 1 − l ≤ dimindex (:β) ⇒
  bit_field_insert h l (w2w a) b = bit_field_insert h l a b

⊢ CARD 𝕌(:word1) = 2 ** 1

⊢ CARD 𝕌(:word10) = 2 ** 10

⊢ CARD 𝕌(:word11) = 2 ** 11

⊢ CARD 𝕌(:word12) = 2 ** 12

⊢ CARD 𝕌(:word128) = 2 ** 128

⊢ CARD 𝕌(:word16) = 2 ** 16

⊢ CARD 𝕌(:word2) = 2²

⊢ CARD 𝕌(:word20) = 2 ** 20

⊢ CARD 𝕌(:word24) = 2 ** 24

⊢ CARD 𝕌(:word28) = 2 ** 28

⊢ CARD 𝕌(:word3) = 2³

⊢ CARD 𝕌(:word30) = 2 ** 30

⊢ CARD 𝕌(:word32) = 2 ** 32

⊢ CARD 𝕌(:word4) = 2 ** 4

⊢ CARD 𝕌(:word48) = 2 ** 48

⊢ CARD 𝕌(:word5) = 2 ** 5

⊢ CARD 𝕌(:word56) = 2 ** 56

⊢ CARD 𝕌(:word6) = 2 ** 6

⊢ CARD 𝕌(:word64) = 2 ** 64

⊢ CARD 𝕌(:word7) = 2 ** 7

⊢ CARD 𝕌(:word8) = 2 ** 8

⊢ CARD 𝕌(:word9) = 2 ** 9

⊢ CARD 𝕌(:word96) = 2 ** 96

⊢ dimindex (:unit) = 1

⊢ dimindex (:10) = 10

⊢ dimindex (:11) = 11

⊢ dimindex (:12) = 12

⊢ dimindex (:128) = 128

⊢ dimindex (:16) = 16

⊢ ∀a. dimindex (:α) = 1 ⇒ a = 0w ∨ a = 1w

⊢ dimindex (:2) = 2

⊢ dimindex (:20) = 20

⊢ dimindex (:24) = 24

⊢ dimindex (:28) = 28

⊢ dimindex (:3) = 3

⊢ dimindex (:30) = 30

⊢ dimindex (:32) = 32

⊢ dimindex (:4) = 4

⊢ dimindex (:48) = 48

⊢ dimindex (:5) = 5

⊢ dimindex (:56) = 56

⊢ dimindex (:6) = 6

⊢ dimindex (:64) = 64

⊢ dimindex (:7) = 7

⊢ dimindex (:8) = 8

⊢ dimindex (:9) = 9

⊢ dimindex (:96) = 96

⊢ dimindex (:α) = dimindex (:β) ⇔ dimword (:α) = dimword (:β)

⊢ dimindex (:α) ≤ dimindex (:β) ⇔ dimword (:α) ≤ dimword (:β)

⊢ dimindex (:α) < dimindex (:β) ⇔ dimword (:α) < dimword (:β)

⊢ dimindex (:α) = dimindex (:β) ⇔ INT_MAX (:α) = INT_MAX (:β)

⊢ dimindex (:α) ≤ dimindex (:β) ⇔ INT_MAX (:α) ≤ INT_MAX (:β)

⊢ dimindex (:α) < dimindex (:β) ⇔ INT_MAX (:α) < INT_MAX (:β)

⊢ dimindex (:α) = dimindex (:β) ⇔ INT_MIN (:α) = INT_MIN (:β)

⊢ dimindex (:α) ≤ dimindex (:β) ⇔ INT_MIN (:α) ≤ INT_MIN (:β)

⊢ dimindex (:α) < dimindex (:β) ⇔ INT_MIN (:α) < INT_MIN (:β)

⊢ dimindex (:α) < dimword (:α)

⊢ dimindex (:α) = dimindex (:β) ⇔ UINT_MAX (:α) = UINT_MAX (:β)

⊢ dimindex (:α) ≤ dimindex (:β) ⇔ UINT_MAX (:α) ≤ UINT_MAX (:β)

⊢ dimindex (:α) < dimindex (:β) ⇔ UINT_MAX (:α) < UINT_MAX (:β)

⊢ dimword (:unit) = 2

⊢ dimword (:10) = 1024

⊢ dimword (:11) = 2048

⊢ dimword (:12) = 4096

⊢ dimword (:128) = 340282366920938463463374607431768211456

⊢ dimword (:16) = 65536

⊢ dimword (:2) = 4

⊢ dimword (:20) = 1048576

⊢ dimword (:24) = 16777216

⊢ dimword (:28) = 268435456

⊢ dimword (:3) = 8

⊢ dimword (:30) = 1073741824

⊢ dimword (:32) = 4294967296

⊢ dimword (:4) = 16

⊢ dimword (:48) = 281474976710656

⊢ dimword (:5) = 32

⊢ dimword (:56) = 72057594037927936

⊢ dimword (:6) = 64

⊢ dimword (:64) = 18446744073709551616

⊢ dimword (:7) = 128

⊢ dimword (:8) = 256

⊢ dimword (:9) = 512

⊢ dimword (:96) = 79228162514264337593543950336

⊢ dimword (:α) = 2 * INT_MIN (:α)

⊢ dimword (:α) − INT_MIN (:α) = INT_MIN (:α)

⊢ ∀f. $FCP f = word_modify (λi b. f i) 0w

⊢ FINITE 𝕌(:unit)

⊢ FINITE 𝕌(:10)

⊢ FINITE 𝕌(:11)

⊢ FINITE 𝕌(:12)

⊢ FINITE 𝕌(:128)

⊢ FINITE 𝕌(:16)

⊢ FINITE 𝕌(:2)

⊢ FINITE 𝕌(:20)

⊢ FINITE 𝕌(:24)

⊢ FINITE 𝕌(:28)

⊢ FINITE 𝕌(:3)

⊢ FINITE 𝕌(:30)

⊢ FINITE 𝕌(:32)

⊢ FINITE 𝕌(:4)

⊢ FINITE 𝕌(:48)

⊢ FINITE 𝕌(:5)

⊢ FINITE 𝕌(:56)

⊢ FINITE 𝕌(:6)

⊢ FINITE 𝕌(:64)

⊢ FINITE 𝕌(:7)

⊢ FINITE 𝕌(:8)

⊢ FINITE 𝕌(:9)

⊢ FINITE 𝕌(:96)

⊢ ∀w. reduce_and w =
      (let
         l =
           GENLIST (λi. (let n = dimindex (:α) − 1 − i in (n >< n) w))
             (dimindex (:α))
       in
         FOLDL $&& (HD l) (TL l))

⊢ ∀w. reduce_nand w =
      (let
         l =
           GENLIST (λi. (let n = dimindex (:α) − 1 − i in (n >< n) w))
             (dimindex (:α))
       in
         FOLDL $~&& (HD l) (TL l))

⊢ ∀w. reduce_nor w =
      (let
         l =
           GENLIST (λi. (let n = dimindex (:α) − 1 − i in (n >< n) w))
             (dimindex (:α))
       in
         FOLDL $~|| (HD l) (TL l))

⊢ ∀w. reduce_or w =
      (let
         l =
           GENLIST (λi. (let n = dimindex (:α) − 1 − i in (n >< n) w))
             (dimindex (:α))
       in
         FOLDL $|| (HD l) (TL l))

⊢ ∀w. reduce_xnor w =
      (let
         l =
           GENLIST (λi. (let n = dimindex (:α) − 1 − i in (n >< n) w))
             (dimindex (:α))
       in
         FOLDL $~?? (HD l) (TL l))

⊢ ∀w. reduce_xor w =
      (let
         l =
           GENLIST (λi. (let n = dimindex (:α) − 1 − i in (n >< n) w))
             (dimindex (:α))
       in
         FOLDL $?? (HD l) (TL l))

⊢ 0 < b ⇒ l2w b (PAD_RIGHT 0 h ls) = l2w b ls

⊢ ∀b w. 1 < b ⇒ l2w b (w2l b w) = w

⊢ ∀w n. w2n w * 2 ** n < dimword (:α) ⇒ w ≪ n ⋙ n = w

⊢ -1w ⋙ 1 = INT_MAXw

⊢ ∀n. n MOD dimindex (:α) < dimword (:α)

⊢ ∀m n. n2w m = n2w n ⇔ m MOD dimword (:α) = n MOD dimword (:α)

⊢ ∀h l n. h < dimindex (:α) ⇒ n2w (BITS h l n) = (h -- l) (n2w n)

⊢ ∀a n. a < dimword (:α) ⇒ n2w (a DIV 2 ** n) = n2w a ⋙ n

⊢ ∀n. n2w (SUC n) = n2w n + 1w

⊢ n2w (dimword (:α)) = 0w

⊢ n2w_itself (n,(:α)) = n2w n

⊢ ∀P. (∀n. P (n,(:α))) ⇒ ∀v v1. P (v,v1)

⊢ ∀n. n2w (n MOD dimword (:α)) = n2w n

⊢ ∀a b. b ≤ a ⇒ n2w (a − b) = n2w a − n2w b

⊢ ∀a b. a ≤ b ⇒ n2w (a − b) = 0w

⊢ ∀w. n2w (w2n w) = w

⊢ ∀w. ∃n. w = n2w n ∧ n < dimword (:α)

⊢ ∀w. reduce_and w = if w = Tw then 1w else 0w

⊢ ∀w. reduce_or w = if w = 0w then 0w else 1w

⊢ ∀c2n n2c b w.
    1 < b ∧ (∀x. x < b ⇒ c2n (n2c x) = x) ⇒ s2w b c2n (w2s b n2c w) = w

⊢ ∀a b. saturate_add a b = if Tw − a ≤₊ b then Tw else a + b

⊢ ∀a b.
    saturate_mul a b =
    if FINITE 𝕌(:α) ∧ w2w Tw ≤₊ w2w a * w2w b then Tw else a * b

⊢ ∀a b. saturate_sub a b = if a ≤₊ b then 0w else a − b

⊢ ∀w. saturate_w2w w =
      if dimindex (:β) ≤ dimindex (:α) ∧ w2w Tw ≤₊ w then Tw else w2w w

⊢ ∀n. saturate_w2w (n2w n) =
      (let
         m = n MOD dimword (:α)
       in
         if dimindex (:β) ≤ dimindex (:α) ∧ dimword (:β) ≤ m then Tw
         else n2w m)

⊢ ∀w i.
    i < dimindex (:β) ⇒
    (sw2sw w ' i ⇔
     if i < dimindex (:α) ∨ dimindex (:β) < dimindex (:α) then w ' i
     else word_msb w)

⊢ sw2sw 0w = 0w

⊢ ∀w. sw2sw w = w

⊢ ∀w. sw2sw (sw2sw w) =
      if dimindex (:β) < dimindex (:α) ∧ dimindex (:β) < dimindex (:γ) then
        sw2sw (w2w w)
      else sw2sw w

⊢ ∀w. sw2sw w = (if word_msb w then -1w ≪ dimindex (:α) else 0w) ‖ w2w w

⊢ ∀w. sw2sw w = (if word_msb w then -1w ≪ dimindex (:α) else 0w) + w2w w

⊢ sw2sw (-1w) = -1w

⊢ ∀b l. w2l b (l2w b l) = n2l b (l2n b l MOD dimword (:α))

⊢ ∀v w. w2n v = w2n w ⇔ v = w

⊢ ∀a b.
    dimindex (:α) ≤ dimindex (:γ) ∧ dimindex (:β) ≤ dimindex (:γ) ⇒
    (w2n a = w2n b ⇔ w2w a = w2w b)

⊢ ∀a b. ¬word_msb a ∧ ¬word_msb b ⇒ w2n (a + b) = w2n a + w2n b

⊢ w2n a + w2n b < dimword (:α) ⇒ w2n (a + b) = w2n a + w2n b

⊢ ∀w. w2n w = 0 ⇔ w = 0w

⊢ ∀w m. w2n (w ⋙ m) = w2n w DIV 2 ** m

⊢ ∀w. w2n w < dimword (:α)

⊢ w2n (-1w) = dimword (:α) − 1

⊢ ∀n. w2n (n2w n) = n MOD dimword (:α)

⊢ ∀a. w2n a + 1 = if a = Tw then dimword (:α) else w2n (a + 1w)

⊢ ∀w. w2n (w2w w) =
      if dimindex (:α) ≤ dimindex (:β) then w2n w
      else w2n ((dimindex (:β) − 1 -- 0) w)

⊢ ∀w. w2n (w2w w) ≤ w2n w

⊢ ∀b c2n n2c s.
    w2s b n2c (s2w b c2n s) = n2s b n2c (s2n b c2n s MOD dimword (:α))

⊢ ∀w i. i < dimindex (:β) ⇒ (w2w w ' i ⇔ i < dimindex (:α) ∧ w ' i)

⊢ w2w 0w = 0w

⊢ ∀w n.
    w2w (w ≪ n) =
    if n < dimindex (:α) then w2w ((dimindex (:α) − 1 − n -- 0) w) ≪ n
    else 0w

⊢ ∀x y.
    dimindex (:α) ≤ dimindex (:β) ∧ y < dimword (:α) ⇒
    (w2w x = n2w y ⇔ x = n2w y)

⊢ ∀w. w2w w = w

⊢ ∀w. w2n (w2w w) < dimword (:α)

⊢ ∀n. w2w (n2w n) =
      if dimindex (:β) ≤ dimindex (:α) then n2w n
      else n2w (BITS (dimindex (:α) − 1) 0 n)

⊢ ∀w. w2w (w2w w) = w2w ((dimindex (:β) − 1 -- 0) w)

⊢ ∀i. i < dimindex (:α) ⇒ ¬0w ' i

⊢ w2n 0w = 0

⊢ ∀n. 1w ≪ n = n2w (2 ** n)

⊢ w2n 1w = 1

⊢ ∀n. ¬n2w n = n2w (dimword (:α) − 1 − n MOD dimword (:α))

⊢ ∀w. dimindex (:α) = 1 ⇒ -w = w

⊢ ∀n. -n2w n = n2w (dimword (:α) − n MOD dimword (:α))

⊢ ∀n. n < dimindex (:α) ⇒ (INT_MAXw ' n ⇔ n < dimindex (:α) − 1)

⊢ ∀n. n < dimindex (:α) ⇒ (INT_MINw ' n ⇔ n = dimindex (:α) − 1)

⊢ word_L2 = if 1 < dimindex (:α) then 0w else INT_MINw

⊢ word_L2 * word_L2 = word_L2 ∧ INT_MINw * word_L2 = word_L2 ∧
  (∀n. n2w n * word_L2 = if EVEN n then 0w else word_L2) ∧
  ∀n. -n2w n * word_L2 = if EVEN n then 0w else word_L2

⊢ ∀n. n2w n * INT_MINw = if EVEN n then 0w else INT_MINw

⊢ ∀n. -n2w n * INT_MINw = if EVEN n then 0w else INT_MINw

⊢ ∀i. i < dimindex (:α) ⇒ Tw ' i

⊢ -1w ≠ 0w

⊢ ∀w. word_abs w = FCP i. ¬word_msb w ∧ w ' i ∨ word_msb w ∧ (-w) ' i

⊢ ∀a b. word_abs (a − b) = word_abs (b − a)

⊢ ∀w. word_abs (-w) = word_abs w

⊢ ∀w. word_abs (word_abs w) = word_abs w

⊢ ∀m n. n2w m + n2w n = n2w (m + n)

⊢ w2n w1 < 2 ** n ⇒ w1 && w2 ≪ n = 0w

⊢ ∀n m. n2w n && n2w m = n2w (BITWISE (dimindex (:α)) $/\ n m)

⊢ ∀w n.
    w ≫ n =
    if word_msb w then (dimindex (:α) − 1 '' dimindex (:α) − n) Tw ‖ w ⋙ n
    else w ⋙ n

⊢ ∀n w.
    w ≫ n =
    if word_msb w then
      n2w (dimword (:α) − 2 ** (dimindex (:α) − MIN n (dimindex (:α)))) ‖
      w ⋙ n
    else w ⋙ n

⊢ word_from_bin_list ∘ word_to_bin_list = I

⊢ word_from_bin_string ∘ word_to_bin_string = I

⊢ ∀w b. b < dimindex (:α) ⇒ (w ' b ⇔ word_bit b w)

⊢ ∀h. ¬word_bit h 0w

⊢ word_bit 0 (-1w)

⊢ word_bit n (w1 && w2) ⇔ word_bit n w1 ∧ word_bit n w2

⊢ word_bit n (w ≪ i) ⇔ word_bit (n − i) w ∧ n < dimindex (:α) ∧ i ≤ n

⊢ ∀b n. word_bit b (n2w n) ⇔ b ≤ dimindex (:α) − 1 ∧ BIT b n

⊢ word_bit n (w1 ‖ w2) ⇔ word_bit n w1 ∨ word_bit n w2

⊢ word_bit n w ⇔ w && n2w (2 ** n) ≠ 0w

⊢ ∀n w. word_bit n w ⇔ n < dimindex (:α) ∧ w ' n

⊢ ∀h l a. (h -- l) a = if l ≤ h then a ⋙ l && 2w ≪ (h − l) − 1w else 0w

⊢ ∀h l n. (h -- l) (n2w n) = n2w (BITS (MIN h (dimindex (:α) − 1)) l n)

⊢ ∀w h l. (h -- l) (w2w w) = w2w ((MIN h (dimindex (:β) − 1) -- l) w)

⊢ ∀x. FINITE 𝕌(:α) ∧ x < dimword (:β) ⇒ 0w @@ n2w x = n2w x

⊢ 0w @@ 0w = 0w

⊢ ∀x y.
    FINITE 𝕌(:α) ∧ dimindex (:β) ≤ dimindex (:γ) ∧ y < dimword (:β) ⇒
    (0w @@ x = n2w y ⇔ x = n2w y)

⊢ ∀a b c.
    FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ∧
    dimindex (:δ) = dimindex (:α) + dimindex (:β) ∧
    dimindex (:ε) = dimindex (:β) + dimindex (:γ) ∧
    dimindex (:ζ) = dimindex (:δ) + dimindex (:γ) ⇒
    (a @@ b) @@ c = a @@ b @@ c

⊢ -1w @@ -1w = w2w (-1w)

⊢ word_from_dec_list ∘ word_to_dec_list = I

⊢ word_from_dec_string ∘ word_to_dec_string = I

⊢ ∀v. v // 1w = v

⊢ ∀w. w = 0w ⇔ ∀i. i < dimindex (:α) ⇒ ¬w ' i

⊢ (∀m n. n2w m = n2w n ⇔ MOD_2EXP_EQ (dimindex (:α)) m n) ∧
  (∀n. n2w n = -1w ⇔ MOD_2EXP_MAX (dimindex (:α)) n) ∧
  ∀n. -1w = n2w n ⇔ MOD_2EXP_MAX (dimindex (:α)) n

⊢ b ** e = word_exp_tailrec b e 1w

⊢ ∀e b a.
    word_exp_tailrec b e a =
    if e = 0w then a
    else if word_mod e 2w = 0w then word_exp_tailrec (b * b) (e // 2w) a
    else word_exp_tailrec b (e − 1w) (b * a)

⊢ ∀P. (∀b e a.
         (e ≠ 0w ∧ word_mod e 2w ≠ 0w ⇒ P b (e − 1w) (b * a)) ∧
         (e ≠ 0w ∧ word_mod e 2w = 0w ⇒ P (b * b) (e // 2w) a) ⇒
         P b e a) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀x h y.
    dimindex (:α) ≤ dimindex (:β) ∧ dimindex (:α) − 1 ≤ h ∧
    y < dimword (:α) ⇒
    ((h >< 0) x = n2w y ⇔ x = n2w y)

⊢ ∀h l a. (h >< l) a = if l ≤ h then a ⋙ l && 2w ≪ (h − l) − 1w else 0w

⊢ (h >< l) (n2w n) =
  if dimindex (:β) ≤ dimindex (:α) then
    n2w (BITS (MIN h (dimindex (:α) − 1)) l n)
  else
    n2w
      (BITS (MIN (MIN h (dimindex (:α) − 1)) (dimindex (:α) − 1 + l)) l n)

⊢ ∀w h l. dimindex (:α) ≤ dimindex (:β) ⇒ (h >< l) (w2w w) = (h >< l) w

⊢ ∀h l a.
    (h >< l) a = w2w (if l ≤ h then a ⋙ l && 2w ≪ (h − l) − 1w else 0w)

⊢ LENGTH l1 = dimindex (:α) ∧ LENGTH l2 = dimindex (:α) ⇒
  word_from_bin_list l1 && word_from_bin_list l2 =
  word_from_bin_list (MAP2 (λx y. bool_to_bit (ODD x ∧ ODD y)) l1 l2)

⊢ LENGTH ls = dimindex (:α) ∧ EVERY ($> 2) ls ⇒
  ¬word_from_bin_list ls = word_from_bin_list (MAP (λx. 1 − x) ls)

⊢ x < dimindex (:α) ∧ LENGTH ls = dimindex (:α) ⇒
  word_from_bin_list ls ⇆ x =
  word_from_bin_list (LASTN x ls ⧺ BUTLASTN x ls)

⊢ x < dimindex (:α) ∧ LENGTH ls = dimindex (:α) ⇒
  word_from_bin_list ls ⇄ x = word_from_bin_list (DROP x ls ⧺ TAKE x ls)

⊢ LENGTH b1 = LENGTH b2 ⇒
  word_from_bin_list b1 ⊕ word_from_bin_list b2 =
  word_from_bin_list (MAP (λ(x,y). (x + y) MOD 2) (ZIP (b1,b2)))

⊢ ∀a b.
    n2w a ≥ n2w b ⇔
    (let
       sa = BIT (dimindex (:α) − 1) a and sb = BIT (dimindex (:α) − 1) b
     in
       (sa ⇔ sb) ∧ a MOD dimword (:α) ≥ b MOD dimword (:α) ∨ ¬sa ∧ sb)

⊢ ∀a b.
    n2w a > n2w b ⇔
    (let
       sa = BIT (dimindex (:α) − 1) a and sb = BIT (dimindex (:α) − 1) b
     in
       (sa ⇔ sb) ∧ a MOD dimword (:α) > b MOD dimword (:α) ∨ ¬sa ∧ sb)

⊢ word_from_hex_list ∘ word_to_hex_list = I

⊢ word_from_hex_string ∘ word_to_hex_string = I

⊢ ∀a b. n2w a >₊ n2w b ⇔ a MOD dimword (:α) > b MOD dimword (:α)

⊢ ∀a b. n2w a ≥₊ n2w b ⇔ a MOD dimword (:α) ≥ b MOD dimword (:α)

⊢ ∀n i. i < dimindex (:α) ⇒ (n2w n ' i ⇔ BIT i n)

⊢ ∀n i.
    n2w n ' i ⇔
    if i < dimindex (:α) then BIT i n
    else FAIL $' $var$(index too large) (n2w n) i

⊢ ∀a. word_join 0w a = w2w a

⊢ ∀i a b.
    FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) ∧ i < dimindex (:α + β) ⇒
    (word_join a b ' i ⇔
     if i < dimindex (:β) then b ' i else a ' (i − dimindex (:β)))

⊢ word_join (-1w) (-1w) = -1w

⊢ ∀a b.
    n2w a ≤ n2w b ⇔
    (let
       sa = BIT (dimindex (:α) − 1) a and sb = BIT (dimindex (:α) − 1) b
     in
       (sa ⇔ sb) ∧ a MOD dimword (:α) ≤ b MOD dimword (:α) ∨ sa ∧ ¬sb)

⊢ ∀a b. n2w a <₊ n2w b ⇔ a MOD dimword (:α) < b MOD dimword (:α)

⊢ word_log2 1w = 0w

⊢ ∀n. word_log2 (n2w n) = n2w (LOG2 (n MOD dimword (:α)))

⊢ ∀a b. n2w a ≤₊ n2w b ⇔ a MOD dimword (:α) ≤ b MOD dimword (:α)

⊢ word_lsb = word_bit 0

⊢ ∀n. word_lsb (n2w n) ⇔ ODD n

⊢ word_lsb (-1w)

⊢ ∀n m. n2w m ≪ n = if dimindex (:α) − 1 < n then 0w else n2w (m * 2 ** n)

⊢ ∀w n. w ⋙ n = (dimindex (:α) − 1 -- n) w

⊢ ∀a b.
    n2w a < n2w b ⇔
    (let
       sa = BIT (dimindex (:α) − 1) a and sb = BIT (dimindex (:α) − 1) b
     in
       (sa ⇔ sb) ∧ a MOD dimword (:α) < b MOD dimword (:α) ∨ sa ∧ ¬sb)

⊢ ∀f n. word_modify f (n2w n) = n2w (BIT_MODIFY (dimindex (:α)) f n)

⊢ word_msb = word_bit (dimindex (:α) − 1)

⊢ ∀a. word_msb (a + INT_MINw) ⇔ ¬word_msb a

⊢ ∀n. word_msb (n2w n) ⇔ BIT (dimindex (:α) − 1) n

⊢ word_msb (n2w n) ⇔ INT_MIN (:α) ≤ n MOD dimword (:α)

⊢ ∀w. word_msb w ⇔ w < 0w

⊢ word_msb (-1w)

⊢ ∀m n. n2w m * n2w n = n2w (m * n)

⊢ ∀n m.
    n2w n ~&& n2w m = n2w (BITWISE (dimindex (:α)) (λx y. ¬(x ∧ y)) n m)

⊢ ∀w. ∃n. w = n2w n

⊢ ∀n m.
    n2w n ~|| n2w m = n2w (BITWISE (dimindex (:α)) (λx y. ¬(x ∨ y)) n m)

⊢ word_from_oct_list ∘ word_to_oct_list = I

⊢ word_from_oct_string ∘ word_to_oct_string = I

⊢ ∀n m. n2w n ‖ n2w m = n2w (BITWISE (dimindex (:α)) $\/ n m)

⊢ ∀n f.
    word_reduce f (n2w n) =
    $FCP
      (K (let l = BOOLIFY (dimindex (:α)) n [] in FOLDL f (HD l) (TL l)))

⊢ ∀n w. word_replicate n w = concat_word_list (GENLIST (K w) n)

⊢ word_reverse 0w = 0w

⊢ ∀n. word_reverse (n2w n) = n2w (BIT_REVERSE (dimindex (:α)) n)

⊢ ∀w v n.
    word_reverse (word_reverse w) = w ∧
    word_reverse (w ≪ n) = word_reverse w ⋙ n ∧
    word_reverse (w ⋙ n) = word_reverse w ≪ n ∧
    word_reverse (w ‖ v) = word_reverse w ‖ word_reverse v ∧
    word_reverse (w && v) = word_reverse w && word_reverse v ∧
    word_reverse (w ⊕ v) = word_reverse w ⊕ word_reverse v ∧
    word_reverse (¬w) = ¬word_reverse w ∧ word_reverse 0w = 0w ∧
    word_reverse (-1w) = -1w ∧ (word_reverse w = 0w ⇔ w = 0w) ∧
    (word_reverse w = -1w ⇔ w = -1w)

⊢ word_reverse (-1w) = -1w

⊢ ∀w n.
    w ⇄ n =
    (let
       x = n MOD dimindex (:α)
     in
       (dimindex (:α) − 1 -- x) w ‖ (x − 1 -- 0) w ≪ (dimindex (:α) − x))

⊢ ∀n a.
    n2w a ⇄ n =
    (let
       x = n MOD dimindex (:α)
     in
       n2w
         (BITS (dimindex (:α) − 1) x a +
          BITS (x − 1) 0 a * 2 ** (dimindex (:α) − x)))

⊢ word_rrx (F,0w) = (F,0w) ∧ word_rrx (T,0w) = (F,INT_MINw)

⊢ ∀c a.
    word_rrx (c,n2w a) =
    (ODD a,n2w (BITS (dimindex (:α) − 1) 1 a + SBIT c (dimindex (:α) − 1)))

⊢ word_rrx (F,-1w) = (T,INT_MAXw) ∧ word_rrx (T,-1w) = (T,-1w)

⊢ (∀w n. n < dimword (:α) ⇒ w ≪ n = w <<~ n2w n) ∧
  (∀w n. n < dimword (:α) ⇒ w ≫ n = w >>~ n2w n) ∧
  (∀w n. n < dimword (:α) ⇒ w ⋙ n = w >>>~ n2w n) ∧
  (∀w n. w ⇄ n = w #>>~ n2w (n MOD dimindex (:α))) ∧
  ∀w n. w ⇆ n = w #<<~ n2w (n MOD dimindex (:α))

⊢ ∀h l w.
    (h --- l) w =
    word_sign_extend (MIN (SUC h) (dimindex (:α)) − l) ((h -- l) w)

⊢ ∀h l n.
    (h --- l) (n2w n) =
    n2w
      (SIGN_EXTEND (MIN (SUC h) (dimindex (:α)) − l) (dimindex (:α))
         (BITS (MIN h (dimindex (:α) − 1)) l n))

⊢ ∀h l n. (h '' l) (n2w n) = n2w (SLICE (MIN h (dimindex (:α) − 1)) l n)

⊢ ∀x y. y ≤₊ x ⇒ w2n (x − y) = w2n x − w2n y

⊢ ∀n m. n2w n ~?? n2w m = n2w (BITWISE (dimindex (:α)) $<=> n m)

⊢ ∀n m. n2w n ⊕ n2w m = n2w (BITWISE (dimindex (:α)) (λx y. x ⇎ y) n m)