Theory "words"

Signature

Definitions

word_xor_def

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

word_xnor_def

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

word_to_oct_string_def

⊢ word_to_oct_string = w2s 8 HEX

word_to_oct_list_def

⊢ word_to_oct_list = w2l 8

word_to_hex_string_def

⊢ word_to_hex_string = w2s 16 HEX

word_to_hex_list_def

⊢ word_to_hex_list = w2l 16

word_to_dec_string_def

⊢ word_to_dec_string = w2s 10 HEX

word_to_dec_list_def

⊢ word_to_dec_list = w2l 10

word_to_bin_string_def

⊢ word_to_bin_string = w2s 2 HEX

word_to_bin_list_def

⊢ word_to_bin_list = w2l 2

word_T_def

⊢ UINT_MAXw = n2w (UINT_MAX (:α))

word_sub_def

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

word_smin_def

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

word_smax_def

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

word_slice_def

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

word_signed_bits_def

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

word_sign_extend_def

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

word_rrx_def

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

word_ror_def

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

word_ror_bv_def

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

word_rol_def

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

word_rol_bv_def

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

word_reverse_def

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

word_replicate_def

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

word_rem_def

⊢ ∀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

word_reduce_def

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

word_quot_def

⊢ ∀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

word_or_def

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

word_nor_def

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

word_nand_def

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

word_mul_def

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

word_msb_def

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

word_modify_def

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

word_mod_def

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

word_min_def

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

word_max_def

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

word_lt_def

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

word_lsr_def

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

word_lsr_bv_def

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

word_lsl_def

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

word_lsl_bv_def

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

word_lsb_def

⊢ ∀w. word_lsb w ⇔ w ' 0

word_ls_def

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

word_log2_def

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

word_lo_def

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

word_len_def

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

word_le_def

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

word_L_def

⊢ INT_MINw = n2w (INT_MIN (:α))

word_L2_def

⊢ word_L2 = INT_MINw * INT_MINw

word_join_def

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

word_hs_def

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

word_hi_def

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

word_H_def

⊢ INT_MAXw = n2w (INT_MAX (:α))

word_gt_def

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

word_ge_def

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

word_from_oct_string_def

⊢ word_from_oct_string = s2w 8 UNHEX

word_from_oct_list_def

⊢ word_from_oct_list = l2w 8

word_from_hex_string_def

⊢ word_from_hex_string = s2w 16 UNHEX

word_from_hex_list_def

⊢ word_from_hex_list = l2w 16

word_from_dec_string_def

⊢ word_from_dec_string = s2w 10 UNHEX

word_from_dec_list_def

⊢ word_from_dec_list = l2w 10

word_from_bin_string_def

⊢ word_from_bin_string = s2w 2 UNHEX

word_from_bin_list_def

⊢ word_from_bin_list = l2w 2

word_extract_def

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

word_div_def

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

word_concat_def

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

word_compare_def

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

word_bits_def

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

word_bit_def

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

word_asr_def

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

word_asr_bv_def

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

word_and_def

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

word_add_def

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

word_abs_def

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

word_2comp_def

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

word_1comp_def

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

w2w_def

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

w2s_def

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

w2n_def

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

w2l_def

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

UINT_MAX_def

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

sw2sw_def

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

saturate_w2w_def

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

saturate_sub_def

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

saturate_n2w_def

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

saturate_mul_def

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

saturate_add_def

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

s2w_def

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

reduce_xor_def

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

reduce_xnor_def

⊢ reduce_xnor = word_reduce $<=>

reduce_or_def

⊢ reduce_or = word_reduce $\/

reduce_nor_def

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

reduce_nand_def

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

reduce_and_def

⊢ reduce_and = word_reduce $/\

nzcv_def

⊢ ∀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)))

n2w_itself_primitive_def

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

n2w_def

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

l2w_def

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

INT_MIN_def

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

INT_MAX_def

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

dimword_def

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

concat_word_list_def

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

bit_field_insert_def

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

bit_count_upto_def

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

bit_count_def

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

add_with_carry_def

⊢ ∀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))

Theorems

ZERO_SHIFT

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

ZERO_LT_UINT_MAX

⊢ 0 < UINT_MAX (:α)

ZERO_LT_INT_MIN

⊢ 0 < INT_MIN (:α)

ZERO_LT_INT_MAX

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

ZERO_LT_dimword

⊢ 0 < dimword (:α)

ZERO_LO_INT_MIN

⊢ 0w <₊ INT_MINw

ZERO_LE_INT_MAX

⊢ 0 ≤ INT_MAX (:α)

WORD_ZERO_LE

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

word_xor_n2w

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

WORD_XOR_COMP

⊢ ∀a. a ⊕ ¬a = UINT_MAXw

WORD_XOR_COMM

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

WORD_XOR_CLAUSES

⊢ ∀a.
      (UINT_MAXw ⊕ a = ¬a) ∧ (a ⊕ UINT_MAXw = ¬a) ∧ (0w ⊕ a = a) ∧
      (a ⊕ 0w = a) ∧ (a ⊕ a = 0w)

WORD_XOR_ASSOC

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

WORD_XOR

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

WORD_XNOR_NOT_XOR

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

word_xnor_n2w

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

WORD_w2w_OVER_MUL

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

WORD_w2w_OVER_BITWISE

⊢ (∀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)

WORD_w2w_OVER_ADD

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

WORD_w2w_EXTRACT

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

word_T_not_zero

⊢ -1w ≠ 0w

word_T

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

WORD_SUM_ZERO

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

word_sub_w2n

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

WORD_SUB_TRIANGLE

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

WORD_SUB_SUB3

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

WORD_SUB_SUB2

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

WORD_SUB_SUB

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

WORD_SUB_RZERO

⊢ ∀w. w − 0w = w

WORD_SUB_RNEG

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

WORD_SUB_REFL

⊢ ∀w. w − w = 0w

WORD_SUB_PLUS

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

WORD_SUB_NEG

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

WORD_SUB_LZERO

⊢ ∀w. 0w − w = -w

WORD_SUB_LT

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

WORD_SUB_LNEG

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

WORD_SUB_LE

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

WORD_SUB_INTRO

⊢ (∀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)

WORD_SUB_ADD2

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

WORD_SUB_ADD

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

WORD_SUB

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

WORD_SLICE_ZERO2

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

WORD_SLICE_ZERO

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

WORD_SLICE_THM

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

WORD_SLICE_OVER_BITWISE

⊢ (∀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)

word_slice_n2w

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

WORD_SLICE_COMP_THM

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

WORD_SLICE_BITS_THM

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

word_signed_bits_n2w

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

word_sign_extend_bits

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

word_shift_bv

⊢ (∀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 (:α))

WORD_SET_INDUCT

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

word_rrx_word_T

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

word_rrx_n2w

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

word_rrx_0

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

word_ror_n2w

⊢ ∀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_ror

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

WORD_RIGHT_SUB_DISTRIB

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

WORD_RIGHT_OR_OVER_AND

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

WORD_RIGHT_AND_OVER_XOR

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

WORD_RIGHT_AND_OVER_OR

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

WORD_RIGHT_ADD_DISTRIB

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

word_reverse_word_T

⊢ word_reverse (-1w) = -1w

word_reverse_thm

⊢ ∀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_n2w

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

word_reverse_0

⊢ word_reverse 0w = 0w

word_replicate_concat_word_list

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

word_reduce_n2w

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

WORD_RCANCEL_SUB

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

WORD_PRED_THM

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

word_or_n2w

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

WORD_OR_IDEM

⊢ ∀a. a ‖ a = a

WORD_OR_COMP

⊢ ∀a. a ‖ ¬a = UINT_MAXw

WORD_OR_COMM

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

WORD_OR_CLAUSES

⊢ ∀a.
      (UINT_MAXw ‖ a = UINT_MAXw) ∧ (a ‖ UINT_MAXw = UINT_MAXw) ∧
      (0w ‖ a = a) ∧ (a ‖ 0w = a) ∧ (a ‖ a = a)

WORD_OR_ASSOC

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

WORD_OR_ABSORB

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

word_oct_string

⊢ word_from_oct_string ∘ word_to_oct_string = I

word_oct_list

⊢ word_from_oct_list ∘ word_to_oct_list = I

WORD_NOT_XOR

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

WORD_NOT_T

⊢ ¬UINT_MAXw = 0w

WORD_NOT_NOT

⊢ ∀a. ¬¬a = a

WORD_NOT_LOWER_EQUAL

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

WORD_NOT_LOWER_EQ

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

WORD_NOT_LOWER

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

WORD_NOT_LESS_EQUAL

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

WORD_NOT_LESS_EQ

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

WORD_NOT_LESS

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

WORD_NOT_HIGHER

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

WORD_NOT_GREATER

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

WORD_NOT_0

⊢ ¬0w = UINT_MAXw

WORD_NOT

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

WORD_NOR_NOT_OR

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

word_nor_n2w

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

WORD_NEG_T

⊢ -UINT_MAXw = 1w

WORD_NEG_SUB

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

WORD_NEG_RMUL

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

WORD_NEG_NEG

⊢ ∀w. - -w = w

WORD_NEG_MUL

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

WORD_NEG_LMUL

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

WORD_NEG_L

⊢ -INT_MINw = INT_MINw

WORD_NEG_EQ_0

⊢ (-v = 0w) ⇔ (v = 0w)

WORD_NEG_EQ

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

WORD_NEG_ADD

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

WORD_NEG_1_T

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

WORD_NEG_1

⊢ -1w = UINT_MAXw

WORD_NEG_0

⊢ -0w = 0w

WORD_NEG

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

word_nchotomy

⊢ ∀w. ∃n. w = n2w n

WORD_NAND_NOT_AND

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

word_nand_n2w

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

WORD_MULT_SUC

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

WORD_MULT_COMM

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

WORD_MULT_CLAUSES

⊢ ∀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)

WORD_MULT_ASSOC

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

word_mul_n2w

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

WORD_MUL_LSL

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

word_msb_word_T

⊢ word_msb (-1w)

word_msb_neg

⊢ ∀w. word_msb w ⇔ w < 0w

word_msb_n2w_numeric

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

word_msb_n2w

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

WORD_MSB_INT_MIN_LS

⊢ ∀a. word_msb a ⇔ INT_MINw ≤₊ a

word_msb_add_word_L

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

WORD_MSB_1COMP

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

word_msb

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

word_modify_n2w

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

WORD_MODIFY_BIT

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

WORD_MOD_POW2

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

WORD_MOD_1

⊢ ∀m. word_mod m 1w = 0w

WORD_LT_SUB_UPPER

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

word_lt_n2w

⊢ ∀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_LT_LO

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

WORD_LT_EQ_LO

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

WORD_LT

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

word_lsr_n2w

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

word_lsl_n2w

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

word_lsb_word_T

⊢ word_lsb (-1w)

word_lsb_n2w

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

word_lsb

⊢ word_lsb = word_bit 0

WORD_LS_word_T

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

WORD_LS_word_0

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

WORD_LS_T

⊢ ∀w. w ≤₊ UINT_MAXw

word_ls_n2w

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

WORD_LS

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

WORD_LOWER_TRANS

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

WORD_LOWER_REFL

⊢ ∀a. ¬(a <₊ a)

WORD_LOWER_OR_EQ

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

WORD_LOWER_NOT_EQ

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

WORD_LOWER_LOWER_EQ_TRANS

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

WORD_LOWER_LOWER_CASES

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

WORD_LOWER_IMP_LOWER_OR_EQ

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

WORD_LOWER_EQUAL_ANTISYM

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

WORD_LOWER_EQ_TRANS

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

WORD_LOWER_EQ_REFL

⊢ ∀a. a ≤₊ a

WORD_LOWER_EQ_LOWER_TRANS

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

WORD_LOWER_EQ_CASES

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

WORD_LOWER_EQ_ANTISYM

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

WORD_LOWER_CASES_IMP

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

WORD_LOWER_CASES

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

WORD_LOWER_ANTISYM

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

word_log2_n2w

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

word_log2_1

⊢ word_log2 1w = 0w

WORD_LO_word_T

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

WORD_LO_word_0

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

word_lo_n2w

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

WORD_LO

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

WORD_LITERAL_XOR

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

WORD_LITERAL_OR

⊢ (∀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)

WORD_LITERAL_MULT

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

WORD_LITERAL_AND

⊢ (∀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)

WORD_LITERAL_ADD

⊢ (∀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)

WORD_LESS_TRANS

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

WORD_LESS_REFL

⊢ ∀a. ¬(a < a)

WORD_LESS_OR_EQ

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

WORD_LESS_NOT_EQ

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

WORD_LESS_NEG_RIGHT

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

WORD_LESS_NEG_LEFT

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

WORD_LESS_LESS_EQ_TRANS

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

WORD_LESS_LESS_CASES

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

WORD_LESS_IMP_LESS_OR_EQ

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

WORD_LESS_EQUAL_ANTISYM

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

WORD_LESS_EQ_TRANS

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

WORD_LESS_EQ_REFL

⊢ ∀a. a ≤ a

WORD_LESS_EQ_LESS_TRANS

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

WORD_LESS_EQ_H

⊢ ∀a. a ≤ INT_MAXw

WORD_LESS_EQ_CASES

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

WORD_LESS_EQ_ANTISYM

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

WORD_LESS_CASES_IMP

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

WORD_LESS_CASES

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

WORD_LESS_ANTISYM

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

WORD_LESS_0_word_T

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

WORD_LEFT_SUB_DISTRIB

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

WORD_LEFT_OR_OVER_AND

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

WORD_LEFT_AND_OVER_XOR

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

WORD_LEFT_AND_OVER_OR

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

WORD_LEFT_ADD_DISTRIB

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

word_le_n2w

⊢ ∀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_LE_LS

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

WORD_LE_EQ_LS

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

WORD_LE

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

WORD_LCANCEL_SUB

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

WORD_L_PLUS_H

⊢ INT_MINw + INT_MAXw = UINT_MAXw

WORD_L_NEG

⊢ word_msb INT_MINw

word_L_MULT_NEG

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

word_L_MULT

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

WORD_L_LESS_H

⊢ INT_MINw < INT_MAXw

WORD_L_LESS_EQ

⊢ ∀a. INT_MINw ≤ a

word_L2_MULT

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

word_L2

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

word_L

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

word_join_word_T

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

word_join_index

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

word_join_0

⊢ ∀a. word_join 0w a = w2w a

WORD_INDUCT

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

word_index_n2w

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

word_index

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

word_hs_n2w

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

WORD_HS

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

WORD_HIGHER_OR_EQ

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

WORD_HIGHER_EQ

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

WORD_HIGHER

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

word_hi_n2w

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

WORD_HI

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

word_hex_string

⊢ word_from_hex_string ∘ word_to_hex_string = I

word_hex_list

⊢ word_from_hex_list ∘ word_to_hex_list = I

WORD_H_WORD_L

⊢ INT_MAXw = INT_MINw − 1w

WORD_H_POS

⊢ ¬word_msb INT_MAXw

word_H

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

word_gt_n2w

⊢ ∀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_GT

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

WORD_GREATER_OR_EQ

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

WORD_GREATER_EQ

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

WORD_GREATER

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

word_ge_n2w

⊢ ∀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_GE

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

WORD_FINITE

⊢ ∀s. FINITE s

WORD_EXTRACT_ZERO3

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

WORD_EXTRACT_ZERO2

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

WORD_EXTRACT_ZERO

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

word_extract_w2w_mask

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

word_extract_w2w

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

WORD_EXTRACT_OVER_MUL2

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

WORD_EXTRACT_OVER_MUL

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

WORD_EXTRACT_OVER_BITWISE

⊢ (∀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)

WORD_EXTRACT_OVER_ADD2

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

WORD_EXTRACT_OVER_ADD

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

word_extract_n2w

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

WORD_EXTRACT_MIN_HIGH

⊢ (∀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)

word_extract_mask

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

WORD_EXTRACT_LT

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

WORD_EXTRACT_LSL2

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

WORD_EXTRACT_LSL

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

WORD_EXTRACT_ID

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

word_extract_eq_n2w

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

WORD_EXTRACT_COMP_THM

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

WORD_EXTRACT_BITS_COMP

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

WORD_EQ_SUB_ZERO

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

WORD_EQ_SUB_RADD

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

WORD_EQ_SUB_LADD

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

WORD_EQ_NEG

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

word_eq_n2w

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

WORD_EQ_ADD_RCANCEL

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

WORD_EQ_ADD_LCANCEL

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

word_eq_0

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

WORD_EQ

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

WORD_DIVISION

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

WORD_DIV_LSR

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

word_div_1

⊢ ∀v. v // 1w = v

word_dec_string

⊢ word_from_dec_string ∘ word_to_dec_string = I

word_dec_list

⊢ word_from_dec_list ∘ word_to_dec_list = I

WORD_DE_MORGAN_THM

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

word_concat_word_T

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

word_concat_assoc

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

word_concat_0_eq

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

word_concat_0_0

⊢ 0w @@ 0w = 0w

word_concat_0

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

WORD_BITS_ZERO3

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

WORD_BITS_ZERO2

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

WORD_BITS_ZERO

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

word_bits_w2w

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

WORD_BITS_SLICE_THM

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

WORD_BITS_OVER_BITWISE

⊢ (∀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)

word_bits_n2w

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

WORD_BITS_MIN_HIGH

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

word_bits_mask

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

WORD_BITS_LT

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

WORD_BITS_LSR

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

WORD_BITS_LSL

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

WORD_BITS_EXTRACT

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

WORD_BITS_COMP_THM

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

word_bit_thm

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

word_bit_test

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

word_bit_or

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

word_bit_n2w

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

word_bit_lsl

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

WORD_BIT_BITS

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

word_bit_and

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

word_bit_0_word_T

⊢ word_bit 0 (-1w)

word_bit_0

⊢ ∀h. ¬word_bit h 0w

word_bit

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

word_bin_string

⊢ word_from_bin_string ∘ word_to_bin_string = I

word_bin_list

⊢ word_from_bin_list ∘ word_to_bin_list = I

word_asr_n2w

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

word_asr

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

word_and_n2w

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

WORD_AND_IDEM

⊢ ∀a. a && a = a

WORD_AND_EXP_SUB1

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

WORD_AND_COMP

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

WORD_AND_COMM

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

WORD_AND_CLAUSES

⊢ ∀a.
      (UINT_MAXw && a = a) ∧ (a && UINT_MAXw = a) ∧ (0w && a = 0w) ∧
      (a && 0w = 0w) ∧ (a && a = a)

WORD_AND_ASSOC

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

WORD_AND_ABSORD

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

WORD_ALL_BITS

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

WORD_ADD_XOR

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

WORD_ADD_SUB_SYM

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

WORD_ADD_SUB_ASSOC

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

WORD_ADD_SUB3

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

WORD_ADD_SUB2

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

WORD_ADD_SUB

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

WORD_ADD_RINV

⊢ ∀w. w + -w = 0w

WORD_ADD_RIGHT_LS2

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

WORD_ADD_RIGHT_LS

⊢ ∀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

WORD_ADD_RIGHT_LO2

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

WORD_ADD_RIGHT_LO

⊢ ∀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

WORD_ADD_RID_UNIQ

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

WORD_ADD_OR

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

word_add_n2w

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

WORD_ADD_LSL

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

WORD_ADD_LINV

⊢ ∀w. -w + w = 0w

WORD_ADD_LID_UNIQ

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

WORD_ADD_LEFT_LS2

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

WORD_ADD_LEFT_LS

⊢ ∀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

WORD_ADD_LEFT_LO2

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

WORD_ADD_LEFT_LO

⊢ ∀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

WORD_ADD_INV_0_EQ

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

WORD_ADD_EQ_SUB

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

WORD_ADD_COMM

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

WORD_ADD_BIT0

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

WORD_ADD_BIT

⊢ ∀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)

WORD_ADD_ASSOC

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

WORD_ADD_0

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

word_abs_word_abs

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

word_abs_neg

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

word_abs_diff

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

word_abs

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

word_2comp_n2w

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

WORD_2COMP_LSL

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

word_2comp_dimindex_1

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

word_1comp_n2w

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

word_1_n2w

⊢ w2n 1w = 1

word_1_lsl

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

WORD_0_POS

⊢ ¬word_msb 0w

word_0_n2w

⊢ w2n 0w = 0

WORD_0_LS

⊢ ∀w. 0w ≤₊ w

word_0

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

w2w_w2w

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

w2w_n2w

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

w2w_lt

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

w2w_LSL

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

w2w_id

⊢ ∀w. w2w w = w

w2w_eq_n2w

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

w2w_0

⊢ w2w 0w = 0w

w2w

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

w2s_s2w

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

w2n_w2w_le

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

w2n_w2w

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

w2n_plus1

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

w2n_n2w

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

w2n_minus1

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

w2n_lt

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

w2n_lsr

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

w2n_eq_0

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

w2n_add

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

w2n_11_lift

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

w2n_11

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

w2l_l2w

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

TWO_COMP_POS_NEG

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

TWO_COMP_POS

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

TWO_COMP_NEG

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

sw2sw_word_T

⊢ sw2sw (-1w) = -1w

sw2sw_w2w_add

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

sw2sw_w2w

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

sw2sw_sw2sw

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

sw2sw_id

⊢ ∀w. sw2sw w = w

sw2sw_0

⊢ sw2sw 0w = 0w

sw2sw

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

SUC_WORD_PRED

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

SHIFT_ZERO

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

SHIFT_1_SUB_1

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

saturate_w2w_n2w

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

saturate_w2w

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

saturate_sub

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

saturate_mul

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

saturate_add

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

s2w_w2s

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

ROR_UINT_MAX

⊢ ∀n. UINT_MAXw ⇄ n = UINT_MAXw

ROR_ROL

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

ROR_MOD

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

ROR_CYCLE

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

ROR_BITWISE

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

ROR_ADD

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

ROL_MOD

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

ROL_BITWISE

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

ROL_ADD

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

reduce_or

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

reduce_and

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

ranged_word_nchotomy

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

ONE_LT_dimword

⊢ 1 < dimword (:α)

NUMERAL_LESS_THM

⊢ (∀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)

NOT_UINTMAXw

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

NOT_INT_MIN_ZERO

⊢ INT_MINw ≠ 0w

NOT_FINITE_IMP_dimword_2

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

NOT_0w

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

n2w_w2n

⊢ ∀w. n2w (w2n w) = w

n2w_SUC

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

n2w_sub_eq_0

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

n2w_sub

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

n2w_mod

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

n2w_itself_ind

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

n2w_itself_def

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

n2w_DIV

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

n2w_dimword

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

n2w_BITS

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

n2w_11

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

mod_dimindex

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

MOD_DIMINDEX

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

MOD_COMPLEMENT

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

MOD_2EXP_DIMINDEX

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

LSR_LIMIT

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

LSR_LESS

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

LSR_BITWISE

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

LSR_ADD

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

lsr_1_word_T

⊢ -1w ⋙ 1 = INT_MAXw

LSL_UINT_MAX

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

LSL_ONE

⊢ ∀w. w ≪ 1 = w + w

lsl_lsr

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

LSL_LIMIT

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

LSL_BITWISE

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

LSL_ADD

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

LOG2_w2n_lt

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

LOG2_w2n

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

LEAST_BIT_LT

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

l2w_w2l

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

INT_MIN_SUM

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

INT_MIN_LT_DIMWORD

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

INT_MIN_96

⊢ INT_MIN (:96) = 39614081257132168796771975168

INT_MIN_9

⊢ INT_MIN (:9) = 256

INT_MIN_8

⊢ INT_MIN (:8) = 128

INT_MIN_7

⊢ INT_MIN (:7) = 64

INT_MIN_64

⊢ INT_MIN (:64) = 9223372036854775808

INT_MIN_6

⊢ INT_MIN (:6) = 32

INT_MIN_5

⊢ INT_MIN (:5) = 16

INT_MIN_48

⊢ INT_MIN (:48) = 140737488355328

INT_MIN_4

⊢ INT_MIN (:4) = 8

INT_MIN_32

⊢ INT_MIN (:32) = 2147483648

INT_MIN_30

⊢ INT_MIN (:30) = 536870912

INT_MIN_3

⊢ INT_MIN (:3) = 4

INT_MIN_28

⊢ INT_MIN (:28) = 134217728

INT_MIN_24

⊢ INT_MIN (:24) = 8388608

INT_MIN_20

⊢ INT_MIN (:20) = 524288

INT_MIN_2

⊢ INT_MIN (:2) = 2

INT_MIN_16

⊢ INT_MIN (:16) = 32768

INT_MIN_128

⊢ INT_MIN (:128) = 170141183460469231731687303715884105728

INT_MIN_12

⊢ INT_MIN (:12) = 2048

INT_MIN_11

⊢ INT_MIN (:11) = 1024

INT_MIN_10

⊢ INT_MIN (:10) = 512

INT_MIN_1

⊢ INT_MIN (:unit) = 1

INT_MAX_LT_DIMWORD

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

FST_ADD_WITH_CARRY

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

foldl_reduce_xor

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

foldl_reduce_xnor

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

foldl_reduce_or

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

foldl_reduce_nor

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

foldl_reduce_nand

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

foldl_reduce_and

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

finite_96

⊢ FINITE 𝕌(:96)

finite_9

⊢ FINITE 𝕌(:9)

finite_8

⊢ FINITE 𝕌(:8)

finite_7

⊢ FINITE 𝕌(:7)

finite_64

⊢ FINITE 𝕌(:64)

finite_6

⊢ FINITE 𝕌(:6)

finite_5

⊢ FINITE 𝕌(:5)

finite_48

⊢ FINITE 𝕌(:48)

finite_4

⊢ FINITE 𝕌(:4)

finite_32

⊢ FINITE 𝕌(:32)

finite_30

⊢ FINITE 𝕌(:30)

finite_3

⊢ FINITE 𝕌(:3)

finite_28

⊢ FINITE 𝕌(:28)

finite_24

⊢ FINITE 𝕌(:24)

finite_20

⊢ FINITE 𝕌(:20)

finite_2

⊢ FINITE 𝕌(:2)

finite_16

⊢ FINITE 𝕌(:16)

finite_128

⊢ FINITE 𝕌(:128)

finite_12

⊢ FINITE 𝕌(:12)

finite_11

⊢ FINITE 𝕌(:11)

finite_10

⊢ FINITE 𝕌(:10)

finite_1

⊢ FINITE 𝕌(:unit)

FCP_T_F

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

fcp_n2w

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

EXTRACT_JOIN_LSL

⊢ ∀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)

EXTRACT_JOIN_ADD_LSL

⊢ ∀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)

EXTRACT_JOIN_ADD

⊢ ∀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)

EXTRACT_JOIN

⊢ ∀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)

EXTRACT_CONCAT

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

EXTRACT_ALL_BITS

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

EXTEND_EXTRACT

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

EXISTS_HB

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

dimword_sub_int_min

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

dimword_IS_TWICE_INT_MIN

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

dimword_96

⊢ dimword (:96) = 79228162514264337593543950336

dimword_9

⊢ dimword (:9) = 512

dimword_8

⊢ dimword (:8) = 256

dimword_7

⊢ dimword (:7) = 128

dimword_64

⊢ dimword (:64) = 18446744073709551616

dimword_6

⊢ dimword (:6) = 64

dimword_5

⊢ dimword (:5) = 32

dimword_48

⊢ dimword (:48) = 281474976710656

dimword_4

⊢ dimword (:4) = 16

dimword_32

⊢ dimword (:32) = 4294967296

dimword_30

⊢ dimword (:30) = 1073741824

dimword_3

⊢ dimword (:3) = 8

dimword_28

⊢ dimword (:28) = 268435456

dimword_24

⊢ dimword (:24) = 16777216

dimword_20

⊢ dimword (:20) = 1048576

dimword_2

⊢ dimword (:2) = 4

dimword_16

⊢ dimword (:16) = 65536

dimword_128

⊢ dimword (:128) = 340282366920938463463374607431768211456

dimword_12

⊢ dimword (:12) = 4096

dimword_11

⊢ dimword (:11) = 2048

dimword_10

⊢ dimword (:10) = 1024

dimword_1

⊢ dimword (:unit) = 2

dimindex_uint_max_lt_iso

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

dimindex_uint_max_le_iso

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

dimindex_uint_max_iso

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

dimindex_lt_dimword

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

dimindex_int_min_lt_iso

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

dimindex_int_min_le_iso

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

dimindex_int_min_iso

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

dimindex_int_max_lt_iso

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

dimindex_int_max_le_iso

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

dimindex_int_max_iso

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

DIMINDEX_GT_0

⊢ 0 < dimindex (:α)

dimindex_dimword_lt_iso

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

dimindex_dimword_le_iso

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

dimindex_dimword_iso

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

dimindex_96

⊢ dimindex (:96) = 96

dimindex_9

⊢ dimindex (:9) = 9

dimindex_8

⊢ dimindex (:8) = 8

dimindex_7

⊢ dimindex (:7) = 7

dimindex_64

⊢ dimindex (:64) = 64

dimindex_6

⊢ dimindex (:6) = 6

dimindex_5

⊢ dimindex (:5) = 5

dimindex_48

⊢ dimindex (:48) = 48

dimindex_4

⊢ dimindex (:4) = 4

dimindex_32

⊢ dimindex (:32) = 32

dimindex_30

⊢ dimindex (:30) = 30

dimindex_3

⊢ dimindex (:3) = 3

dimindex_28

⊢ dimindex (:28) = 28

dimindex_24

⊢ dimindex (:24) = 24

dimindex_20

⊢ dimindex (:20) = 20

dimindex_2

⊢ dimindex (:2) = 2

dimindex_1_cases

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

dimindex_16

⊢ dimindex (:16) = 16

dimindex_128

⊢ dimindex (:128) = 128

dimindex_12

⊢ dimindex (:12) = 12

dimindex_11

⊢ dimindex (:11) = 11

dimindex_10

⊢ dimindex (:10) = 10

dimindex_1

⊢ dimindex (:unit) = 1

CONCAT_EXTRACT

⊢ ∀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)

BOUND_ORDER

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

BITS_ZEROL_DIMINDEX

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

BIT_UPDATE

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

BIT_SET_ind

⊢ ∀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

BIT_SET_def

⊢ ∀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)

BIT_SET

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

bit_field_insert

⊢ ∀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))

bit_count_upto_SUC

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

bit_count_upto_is_zero

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

bit_count_upto_0

⊢ ∀w. bit_count_upto 0 w = 0

bit_count_is_zero

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

ASR_UINT_MAX

⊢ ∀n. UINT_MAXw ≫ n = UINT_MAXw

ASR_LIMIT

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

ASR_ADD

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

ADD_WITH_CARRY_SUB

⊢ ∀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))