Structure bitTheory

signature bitTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BITS_def : thm
    val BITV_def : thm
    val BITWISE_def : thm
    val BIT_MODIFY_def : thm
    val BIT_REVERSE_def : thm
    val BIT_def : thm
    val DIVMOD_2EXP_def : thm
    val DIV_2EXP_def : thm
    val LOG2_def : thm
    val LOWEST_SET_BIT_def : thm
    val MOD_2EXP_EQ_def : thm
    val MOD_2EXP_MAX_def : thm
    val MOD_2EXP_def : thm
    val SBIT_def : thm
    val SIGN_EXTEND_def : thm
    val SLICE_def : thm
    val TIMES_2EXP_def : thm
  
  (*  Theorems  *)
    val ADD_BIT0 : thm
    val ADD_BITS_SUC : thm
    val ADD_BIT_SUC : thm
    val BIT0_ODD : thm
    val BITSLT_THM : thm
    val BITSLT_THM2 : thm
    val BITS_COMP_THM : thm
    val BITS_COMP_THM2 : thm
    val BITS_DIV_THM : thm
    val BITS_LEQ : thm
    val BITS_LOG2_ZERO_ID : thm
    val BITS_LT_HIGH : thm
    val BITS_LT_LOW : thm
    val BITS_MUL : thm
    val BITS_SLICE_THM : thm
    val BITS_SLICE_THM2 : thm
    val BITS_SUC : thm
    val BITS_SUC_THM : thm
    val BITS_SUM : thm
    val BITS_SUM2 : thm
    val BITS_SUM3 : thm
    val BITS_THM : thm
    val BITS_THM2 : thm
    val BITS_ZERO : thm
    val BITS_ZERO2 : thm
    val BITS_ZERO3 : thm
    val BITS_ZERO4 : thm
    val BITS_ZERO5 : thm
    val BITS_ZEROL : thm
    val BITV_THM : thm
    val BITWISE_BITS : thm
    val BITWISE_COR : thm
    val BITWISE_EVAL : thm
    val BITWISE_LT_2EXP : thm
    val BITWISE_NOT_COR : thm
    val BITWISE_ONE_COMP_LEM : thm
    val BITWISE_THM : thm
    val BIT_B : thm
    val BIT_BITS_THM : thm
    val BIT_B_NEQ : thm
    val BIT_COMPLEMENT : thm
    val BIT_COMP_THM3 : thm
    val BIT_DIV2 : thm
    val BIT_EXP_SUB1 : thm
    val BIT_IMP_GE_TWOEXP : thm
    val BIT_LOG2 : thm
    val BIT_MODIFY_THM : thm
    val BIT_OF_BITS_THM : thm
    val BIT_OF_BITS_THM2 : thm
    val BIT_REVERSE_THM : thm
    val BIT_SHIFT_THM : thm
    val BIT_SHIFT_THM2 : thm
    val BIT_SHIFT_THM3 : thm
    val BIT_SHIFT_THM4 : thm
    val BIT_SHIFT_THM5 : thm
    val BIT_SIGN_EXTEND : thm
    val BIT_SLICE : thm
    val BIT_SLICE_LEM : thm
    val BIT_SLICE_THM : thm
    val BIT_SLICE_THM2 : thm
    val BIT_SLICE_THM3 : thm
    val BIT_SLICE_THM4 : thm
    val BIT_TIMES2 : thm
    val BIT_TIMES2_1 : thm
    val BIT_TWO_POW : thm
    val BIT_ZERO : thm
    val DIVMOD_2EXP : thm
    val DIV_GT0 : thm
    val DIV_LT : thm
    val DIV_MULT_1 : thm
    val DIV_MULT_THM : thm
    val DIV_MULT_THM2 : thm
    val DIV_SUB1 : thm
    val EXISTS_BIT_IN_RANGE : thm
    val EXISTS_BIT_LT : thm
    val EXP_SUB_LESS_EQ : thm
    val LEAST_THM : thm
    val LESS_EQ_EXP_MULT : thm
    val LESS_MULT_MONO2 : thm
    val LOG2_LE_MONO : thm
    val LOG2_TWOEXP : thm
    val LOG2_UNIQUE : thm
    val LT_TWOEXP : thm
    val MOD_2EXP_LT : thm
    val MOD_2EXP_MONO : thm
    val MOD_ADD_1 : thm
    val MOD_LEQ : thm
    val MOD_PLUS_1 : thm
    val MOD_PLUS_LEFT : thm
    val MOD_PLUS_RIGHT : thm
    val MOD_ZERO_GT : thm
    val NOT_BIT : thm
    val NOT_BITS : thm
    val NOT_BITS2 : thm
    val NOT_BIT_GT_BITWISE : thm
    val NOT_BIT_GT_LOG2 : thm
    val NOT_BIT_GT_TWOEXP : thm
    val NOT_MOD2_LEM : thm
    val NOT_MOD2_LEM2 : thm
    val NOT_ZERO_ADD1 : thm
    val ODD_MOD2_LEM : thm
    val ONE_LE_TWOEXP : thm
    val SBIT_DIV : thm
    val SBIT_MULT : thm
    val SLICELT_THM : thm
    val SLICE_COMP_RWT : thm
    val SLICE_COMP_THM : thm
    val SLICE_COMP_THM2 : thm
    val SLICE_THM : thm
    val SLICE_ZERO : thm
    val SLICE_ZERO2 : thm
    val SLICE_ZERO_THM : thm
    val SUC_SUB : thm
    val TWOEXP_DIVISION : thm
    val TWOEXP_LE_IMP_LE_LOG2 : thm
    val TWOEXP_MONO : thm
    val TWOEXP_MONO2 : thm
    val TWOEXP_NOT_ZERO : thm
    val ZERO_LT_TWOEXP : thm
  
  val bit_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [logroot] Parent theory of "bit"
   
   [BITS_def]  Definition
      
      ⊢ ∀h l n. BITS h l n = MOD_2EXP (SUC h − l) (DIV_2EXP l n)
   
   [BITV_def]  Definition
      
      ⊢ ∀n b. BITV n b = BITS b b n
   
   [BITWISE_def]  Definition
      
      ⊢ (∀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
   
   [BIT_MODIFY_def]  Definition
      
      ⊢ (∀f x. BIT_MODIFY 0 f x = 0) ∧
        ∀n f x.
          BIT_MODIFY (SUC n) f x =
          BIT_MODIFY n f x + SBIT (f n (BIT n x)) n
   
   [BIT_REVERSE_def]  Definition
      
      ⊢ (∀x. BIT_REVERSE 0 x = 0) ∧
        ∀n x.
          BIT_REVERSE (SUC n) x = BIT_REVERSE n x * 2 + SBIT (BIT n x) 0
   
   [BIT_def]  Definition
      
      ⊢ ∀b n. BIT b n ⇔ BITS b b n = 1
   
   [DIVMOD_2EXP_def]  Definition
      
      ⊢ ∀x n. DIVMOD_2EXP x n = (n DIV 2 ** x,n MOD 2 ** x)
   
   [DIV_2EXP_def]  Definition
      
      ⊢ ∀x n. DIV_2EXP x n = n DIV 2 ** x
   
   [LOG2_def]  Definition
      
      ⊢ LOG2 = LOG 2
   
   [LOWEST_SET_BIT_def]  Definition
      
      ⊢ ∀n. LOWEST_SET_BIT n = LEAST i. BIT i n
   
   [MOD_2EXP_EQ_def]  Definition
      
      ⊢ ∀n a b. MOD_2EXP_EQ n a b ⇔ MOD_2EXP n a = MOD_2EXP n b
   
   [MOD_2EXP_MAX_def]  Definition
      
      ⊢ ∀n a. MOD_2EXP_MAX n a ⇔ MOD_2EXP n a = 2 ** n − 1
   
   [MOD_2EXP_def]  Definition
      
      ⊢ ∀x n. MOD_2EXP x n = n MOD 2 ** x
   
   [SBIT_def]  Definition
      
      ⊢ ∀b n. SBIT b n = if b then 2 ** n else 0
   
   [SIGN_EXTEND_def]  Definition
      
      ⊢ ∀l h n.
          SIGN_EXTEND l h n =
          (let
             m = n MOD 2 ** l
           in
             if BIT (l − 1) n then 2 ** h − 2 ** l + m else m)
   
   [SLICE_def]  Definition
      
      ⊢ ∀h l n. SLICE h l n = MOD_2EXP (SUC h) n − MOD_2EXP l n
   
   [TIMES_2EXP_def]  Definition
      
      ⊢ ∀x n. TIMES_2EXP x n = n * 2 ** x
   
   [ADD_BIT0]  Theorem
      
      ⊢ ∀m n. BIT 0 (m + n) ⇔ (BIT 0 m ⇎ BIT 0 n)
   
   [ADD_BITS_SUC]  Theorem
      
      ⊢ ∀n a b.
          BITS (SUC n) (SUC n) (a + b) =
          (BITS (SUC n) (SUC n) a + BITS (SUC n) (SUC n) b +
           BITS (SUC n) (SUC n) (BITS n 0 a + BITS n 0 b)) MOD 2
   
   [ADD_BIT_SUC]  Theorem
      
      ⊢ ∀n a b.
          BIT (SUC n) (a + b) ⇔
          if BIT (SUC n) (BITS n 0 a + BITS n 0 b) then
            BIT (SUC n) a ⇔ BIT (SUC n) b
          else BIT (SUC n) a ⇎ BIT (SUC n) b
   
   [BIT0_ODD]  Theorem
      
      ⊢ BIT 0 = ODD
   
   [BITSLT_THM]  Theorem
      
      ⊢ ∀h l n. BITS h l n < 2 ** (SUC h − l)
   
   [BITSLT_THM2]  Theorem
      
      ⊢ ∀h l n. BITS h l n < 2 ** SUC h
   
   [BITS_COMP_THM]  Theorem
      
      ⊢ ∀h1 l1 h2 l2 n.
          h2 + l1 ≤ h1 ⇒
          BITS h2 l2 (BITS h1 l1 n) = BITS (h2 + l1) (l2 + l1) n
   
   [BITS_COMP_THM2]  Theorem
      
      ⊢ ∀h1 l1 h2 l2 n.
          BITS h2 l2 (BITS h1 l1 n) = BITS (MIN h1 (h2 + l1)) (l2 + l1) n
   
   [BITS_DIV_THM]  Theorem
      
      ⊢ ∀h l x n. BITS h l x DIV 2 ** n = BITS h (l + n) x
   
   [BITS_LEQ]  Theorem
      
      ⊢ ∀h l n. BITS h l n ≤ n
   
   [BITS_LOG2_ZERO_ID]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ BITS (LOG2 n) 0 n = n
   
   [BITS_LT_HIGH]  Theorem
      
      ⊢ ∀h l n. n < 2 ** SUC h ⇒ BITS h l n = n DIV 2 ** l
   
   [BITS_LT_LOW]  Theorem
      
      ⊢ ∀h l n. n < 2 ** l ⇒ BITS h l n = 0
   
   [BITS_MUL]  Theorem
      
      ⊢ ∀h a b. BITS h 0 (BITS h 0 a * BITS h 0 b) = BITS h 0 (a * b)
   
   [BITS_SLICE_THM]  Theorem
      
      ⊢ ∀h l n. BITS h l (SLICE h l n) = BITS h l n
   
   [BITS_SLICE_THM2]  Theorem
      
      ⊢ ∀h h2 l n. h ≤ h2 ⇒ BITS h2 l (SLICE h l n) = BITS h l n
   
   [BITS_SUC]  Theorem
      
      ⊢ ∀h l n.
          l ≤ SUC h ⇒
          SBIT (BIT (SUC h) n) (SUC h − l) + BITS h l n = BITS (SUC h) l n
   
   [BITS_SUC_THM]  Theorem
      
      ⊢ ∀h l n.
          BITS (SUC h) l n =
          if SUC h < l then 0
          else SBIT (BIT (SUC h) n) (SUC h − l) + BITS h l n
   
   [BITS_SUM]  Theorem
      
      ⊢ ∀h l a b.
          b < 2 ** l ⇒ BITS h l (a * 2 ** l + b) = BITS h l (a * 2 ** l)
   
   [BITS_SUM2]  Theorem
      
      ⊢ ∀h l a b. BITS h l (a * 2 ** SUC h + b) = BITS h l b
   
   [BITS_SUM3]  Theorem
      
      ⊢ ∀h a b. BITS h 0 (BITS h 0 a + BITS h 0 b) = BITS h 0 (a + b)
   
   [BITS_THM]  Theorem
      
      ⊢ ∀h l n. BITS h l n = (n DIV 2 ** l) MOD 2 ** (SUC h − l)
   
   [BITS_THM2]  Theorem
      
      ⊢ ∀h l n. BITS h l n = n MOD 2 ** SUC h DIV 2 ** l
   
   [BITS_ZERO]  Theorem
      
      ⊢ ∀h l n. h < l ⇒ BITS h l n = 0
   
   [BITS_ZERO2]  Theorem
      
      ⊢ ∀h l. BITS h l 0 = 0
   
   [BITS_ZERO3]  Theorem
      
      ⊢ ∀h n. BITS h 0 n = n MOD 2 ** SUC h
   
   [BITS_ZERO4]  Theorem
      
      ⊢ ∀h l a. l ≤ h ⇒ BITS h l (a * 2 ** l) = BITS (h − l) 0 a
   
   [BITS_ZERO5]  Theorem
      
      ⊢ ∀n m. (∀i. i ≤ n ⇒ ¬BIT i m) ⇒ BITS n 0 m = 0
   
   [BITS_ZEROL]  Theorem
      
      ⊢ ∀h a. a < 2 ** SUC h ⇒ BITS h 0 a = a
   
   [BITV_THM]  Theorem
      
      ⊢ ∀b n. BITV n b = SBIT (BIT b n) 0
   
   [BITWISE_BITS]  Theorem
      
      ⊢ ∀wl op a b.
          BITWISE (SUC wl) op (BITS wl 0 a) (BITS wl 0 b) =
          BITWISE (SUC wl) op a b
   
   [BITWISE_COR]  Theorem
      
      ⊢ ∀x n op a b.
          x < n ⇒
          op (BIT x a) (BIT x b) ⇒
          (BITWISE n op a b DIV 2 ** x) MOD 2 = 1
   
   [BITWISE_EVAL]  Theorem
      
      ⊢ ∀n op a b.
          BITWISE (SUC n) op a b =
          2 * BITWISE n op (a DIV 2) (b DIV 2) +
          SBIT (op (ODD a) (ODD b)) 0
   
   [BITWISE_LT_2EXP]  Theorem
      
      ⊢ ∀n op a b. BITWISE n op a b < 2 ** n
   
   [BITWISE_NOT_COR]  Theorem
      
      ⊢ ∀x n op a b.
          x < n ⇒
          ¬op (BIT x a) (BIT x b) ⇒
          (BITWISE n op a b DIV 2 ** x) MOD 2 = 0
   
   [BITWISE_ONE_COMP_LEM]  Theorem
      
      ⊢ ∀n a b.
          BITWISE (SUC n) (λx y. ¬x) a b = 2 ** SUC n − 1 − BITS n 0 a
   
   [BITWISE_THM]  Theorem
      
      ⊢ ∀x n op a b.
          x < n ⇒ (BIT x (BITWISE n op a b) ⇔ op (BIT x a) (BIT x b))
   
   [BIT_B]  Theorem
      
      ⊢ ∀b. BIT b (2 ** b)
   
   [BIT_BITS_THM]  Theorem
      
      ⊢ ∀h l a b.
          (∀x. l ≤ x ∧ x ≤ h ⇒ (BIT x a ⇔ BIT x b)) ⇔
          BITS h l a = BITS h l b
   
   [BIT_B_NEQ]  Theorem
      
      ⊢ ∀a b. a ≠ b ⇒ ¬BIT a (2 ** b)
   
   [BIT_COMPLEMENT]  Theorem
      
      ⊢ ∀n i a.
          BIT i (2 ** n − a MOD 2 ** n) ⇔
          a MOD 2 ** n = 0 ∧ i = n ∨
          a MOD 2 ** n ≠ 0 ∧ i < n ∧ ¬BIT i (a MOD 2 ** n − 1)
   
   [BIT_COMP_THM3]  Theorem
      
      ⊢ ∀h m l n.
          SUC m ≤ h ∧ l ≤ m ⇒
          BITS h (SUC m) n * 2 ** (SUC m − l) + BITS m l n = BITS h l n
   
   [BIT_DIV2]  Theorem
      
      ⊢ ∀n i. BIT n (i DIV 2) ⇔ BIT (SUC n) i
   
   [BIT_EXP_SUB1]  Theorem
      
      ⊢ ∀b n. BIT b (2 ** n − 1) ⇔ b < n
   
   [BIT_IMP_GE_TWOEXP]  Theorem
      
      ⊢ ∀i n. BIT i n ⇒ 2 ** i ≤ n
   
   [BIT_LOG2]  Theorem
      
      ⊢ ∀n. n ≠ 0 ⇒ BIT (LOG2 n) n
   
   [BIT_MODIFY_THM]  Theorem
      
      ⊢ ∀x n f a. x < n ⇒ (BIT x (BIT_MODIFY n f a) ⇔ f x (BIT x a))
   
   [BIT_OF_BITS_THM]  Theorem
      
      ⊢ ∀n h l a. l + n ≤ h ⇒ (BIT n (BITS h l a) ⇔ BIT (l + n) a)
   
   [BIT_OF_BITS_THM2]  Theorem
      
      ⊢ ∀h l x n. h < l + x ⇒ ¬BIT x (BITS h l n)
   
   [BIT_REVERSE_THM]  Theorem
      
      ⊢ ∀x n a. x < n ⇒ (BIT x (BIT_REVERSE n a) ⇔ BIT (n − 1 − x) a)
   
   [BIT_SHIFT_THM]  Theorem
      
      ⊢ ∀n a s. BIT (n + s) (a * 2 ** s) ⇔ BIT n a
   
   [BIT_SHIFT_THM2]  Theorem
      
      ⊢ ∀n a s. s ≤ n ⇒ (BIT n (a * 2 ** s) ⇔ BIT (n − s) a)
   
   [BIT_SHIFT_THM3]  Theorem
      
      ⊢ ∀n a s. n < s ⇒ ¬BIT n (a * 2 ** s)
   
   [BIT_SHIFT_THM4]  Theorem
      
      ⊢ ∀n i a. BIT i (a DIV 2 ** n) ⇔ BIT (i + n) a
   
   [BIT_SHIFT_THM5]  Theorem
      
      ⊢ ∀n m i a.
          i + n < m ∧ a < 2 ** m ⇒
          (BIT i
             (2 ** m −
              (a DIV 2 ** n + if a MOD 2 ** n = 0 then 0 else 1) MOD 2 ** m) ⇔
           BIT (i + n) (2 ** m − a MOD 2 ** m))
   
   [BIT_SIGN_EXTEND]  Theorem
      
      ⊢ ∀l h n i.
          l ≠ 0 ⇒
          (BIT i (SIGN_EXTEND l h n) ⇔
           if l ≤ h ⇒ i < l then BIT i (n MOD 2 ** l)
           else i < h ∧ BIT (l − 1) n)
   
   [BIT_SLICE]  Theorem
      
      ⊢ ∀n a b. (BIT n a ⇔ BIT n b) ⇔ SLICE n n a = SLICE n n b
   
   [BIT_SLICE_LEM]  Theorem
      
      ⊢ ∀y x n. SBIT (BIT x n) (x + y) = SLICE x x n * 2 ** y
   
   [BIT_SLICE_THM]  Theorem
      
      ⊢ ∀x n. SBIT (BIT x n) x = SLICE x x n
   
   [BIT_SLICE_THM2]  Theorem
      
      ⊢ ∀b n. BIT b n ⇔ SLICE b b n = 2 ** b
   
   [BIT_SLICE_THM3]  Theorem
      
      ⊢ ∀b n. ¬BIT b n ⇔ SLICE b b n = 0
   
   [BIT_SLICE_THM4]  Theorem
      
      ⊢ ∀b h l n. BIT b (SLICE h l n) ⇔ l ≤ b ∧ b ≤ h ∧ BIT b n
   
   [BIT_TIMES2]  Theorem
      
      ⊢ BIT z (2 * n) ⇔ 0 < z ∧ BIT (z − 1) n
   
   [BIT_TIMES2_1]  Theorem
      
      ⊢ ∀n z. BIT z (2 * n + 1) ⇔ z = 0 ∨ BIT z (2 * n)
   
   [BIT_TWO_POW]  Theorem
      
      ⊢ ∀n m. BIT n (2 ** m) ⇔ m = n
   
   [BIT_ZERO]  Theorem
      
      ⊢ ∀b. ¬BIT b 0
   
   [DIVMOD_2EXP]  Theorem
      
      ⊢ ∀x n. DIVMOD_2EXP x n = (DIV_2EXP x n,MOD_2EXP x n)
   
   [DIV_GT0]  Theorem
      
      ⊢ ∀a b. b ≤ a ∧ 0 < b ⇒ 0 < a DIV b
   
   [DIV_LT]  Theorem
      
      ⊢ ∀n m a. n < m ∧ a < 2 ** m ⇒ a DIV 2 ** n < 2 ** m
   
   [DIV_MULT_1]  Theorem
      
      ⊢ ∀r n. r < n ⇒ (n + r) DIV n = 1
   
   [DIV_MULT_THM]  Theorem
      
      ⊢ ∀x n. n DIV 2 ** x * 2 ** x = n − n MOD 2 ** x
   
   [DIV_MULT_THM2]  Theorem
      
      ⊢ ∀n. 2 * (n DIV 2) = n − n MOD 2
   
   [DIV_SUB1]  Theorem
      
      ⊢ ∀a b.
          2 ** b ≤ a ∧ a MOD 2 ** b = 0 ⇒
          a DIV 2 ** b − 1 = (a − 1) DIV 2 ** b
   
   [EXISTS_BIT_IN_RANGE]  Theorem
      
      ⊢ ∀a b n.
          n ≠ 0 ∧ 2 ** a ≤ n ∧ n < 2 ** b ⇒ ∃i. a ≤ i ∧ i < b ∧ BIT i n
   
   [EXISTS_BIT_LT]  Theorem
      
      ⊢ ∀b n. n ≠ 0 ∧ n < 2 ** b ⇒ ∃i. i < b ∧ BIT i n
   
   [EXP_SUB_LESS_EQ]  Theorem
      
      ⊢ ∀a b. 2 ** (a − b) ≤ 2 ** a
   
   [LEAST_THM]  Theorem
      
      ⊢ ∀n P. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ $LEAST P = n
   
   [LESS_EQ_EXP_MULT]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ ∃p. 2 ** b = p * 2 ** a
   
   [LESS_MULT_MONO2]  Theorem
      
      ⊢ ∀a b x y. a < x ∧ b < y ⇒ a * b < x * y
   
   [LOG2_LE_MONO]  Theorem
      
      ⊢ ∀x y. 0 < x ⇒ x ≤ y ⇒ LOG2 x ≤ LOG2 y
   
   [LOG2_TWOEXP]  Theorem
      
      ⊢ ∀n. LOG2 (2 ** n) = n
   
   [LOG2_UNIQUE]  Theorem
      
      ⊢ ∀n p. 2 ** p ≤ n ∧ n < 2 ** SUC p ⇒ LOG2 n = p
   
   [LT_TWOEXP]  Theorem
      
      ⊢ ∀x n. x < 2 ** n ⇔ x = 0 ∨ LOG2 x < n
   
   [MOD_2EXP_LT]  Theorem
      
      ⊢ ∀n k. k MOD 2 ** n < 2 ** n
   
   [MOD_2EXP_MONO]  Theorem
      
      ⊢ ∀n h l. l ≤ h ⇒ n MOD 2 ** l ≤ n MOD 2 ** SUC h
   
   [MOD_ADD_1]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀x. (x + 1) MOD n ≠ 0 ⇒ (x + 1) MOD n = x MOD n + 1
   
   [MOD_LEQ]  Theorem
      
      ⊢ ∀a b. 0 < b ⇒ a MOD b ≤ a
   
   [MOD_PLUS_1]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀x. (x + 1) MOD n = 0 ⇔ x MOD n + 1 = n
   
   [MOD_PLUS_LEFT]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀j k. (k MOD n + j) MOD n = (k + j) MOD n
   
   [MOD_PLUS_RIGHT]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀j k. (j + k MOD n) MOD n = (j + k) MOD n
   
   [MOD_ZERO_GT]  Theorem
      
      ⊢ ∀n a. a ≠ 0 ∧ a MOD 2 ** n = 0 ⇒ 2 ** n ≤ a
   
   [NOT_BIT]  Theorem
      
      ⊢ ∀n a. ¬BIT n a ⇔ BITS n n a = 0
   
   [NOT_BITS]  Theorem
      
      ⊢ ∀n a. BITS n n a ≠ 0 ⇔ BITS n n a = 1
   
   [NOT_BITS2]  Theorem
      
      ⊢ ∀n a. BITS n n a ≠ 1 ⇔ BITS n n a = 0
   
   [NOT_BIT_GT_BITWISE]  Theorem
      
      ⊢ ∀i n op a b. n ≤ i ⇒ ¬BIT i (BITWISE n op a b)
   
   [NOT_BIT_GT_LOG2]  Theorem
      
      ⊢ ∀i n. LOG2 n < i ⇒ ¬BIT i n
   
   [NOT_BIT_GT_TWOEXP]  Theorem
      
      ⊢ ∀i n. n < 2 ** i ⇒ ¬BIT i n
   
   [NOT_MOD2_LEM]  Theorem
      
      ⊢ ∀n. n MOD 2 ≠ 0 ⇔ n MOD 2 = 1
   
   [NOT_MOD2_LEM2]  Theorem
      
      ⊢ ∀n. n MOD 2 ≠ 1 ⇔ n MOD 2 = 0
   
   [NOT_ZERO_ADD1]  Theorem
      
      ⊢ ∀m. m ≠ 0 ⇒ ∃p. m = SUC p
   
   [ODD_MOD2_LEM]  Theorem
      
      ⊢ ∀n. ODD n ⇔ n MOD 2 = 1
   
   [ONE_LE_TWOEXP]  Theorem
      
      ⊢ ∀n. 1 ≤ 2 ** n
   
   [SBIT_DIV]  Theorem
      
      ⊢ ∀b m n. n < m ⇒ SBIT b (m − n) = SBIT b m DIV 2 ** n
   
   [SBIT_MULT]  Theorem
      
      ⊢ ∀b m n. SBIT b n * 2 ** m = SBIT b (n + m)
   
   [SLICELT_THM]  Theorem
      
      ⊢ ∀h l n. SLICE h l n < 2 ** SUC h
   
   [SLICE_COMP_RWT]  Theorem
      
      ⊢ ∀h m' m l n.
          l ≤ m ∧ m' = m + 1 ∧ m < h ⇒
          SLICE h m' n + SLICE m l n = SLICE h l n
   
   [SLICE_COMP_THM]  Theorem
      
      ⊢ ∀h m l n.
          SUC m ≤ h ∧ l ≤ m ⇒ SLICE h (SUC m) n + SLICE m l n = SLICE h l n
   
   [SLICE_COMP_THM2]  Theorem
      
      ⊢ ∀h l x y n. h ≤ x ∧ y ≤ l ⇒ SLICE h l (SLICE x y n) = SLICE h l n
   
   [SLICE_THM]  Theorem
      
      ⊢ ∀n h l. SLICE h l n = BITS h l n * 2 ** l
   
   [SLICE_ZERO]  Theorem
      
      ⊢ ∀h l n. h < l ⇒ SLICE h l n = 0
   
   [SLICE_ZERO2]  Theorem
      
      ⊢ ∀l h. SLICE h l 0 = 0
   
   [SLICE_ZERO_THM]  Theorem
      
      ⊢ ∀n h. SLICE h 0 n = BITS h 0 n
   
   [SUC_SUB]  Theorem
      
      ⊢ ∀a. SUC a − a = 1
   
   [TWOEXP_DIVISION]  Theorem
      
      ⊢ ∀n k. k = k DIV 2 ** n * 2 ** n + k MOD 2 ** n
   
   [TWOEXP_LE_IMP_LE_LOG2]  Theorem
      
      ⊢ (∀x y. 2 ** x ≤ y ⇒ x ≤ LOG2 y) ∧
        ∀y x. 0 < x ⇒ x ≤ 2 ** y ⇒ LOG2 x ≤ y
   
   [TWOEXP_MONO]  Theorem
      
      ⊢ ∀a b. a < b ⇒ 2 ** a < 2 ** b
   
   [TWOEXP_MONO2]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ 2 ** a ≤ 2 ** b
   
   [TWOEXP_NOT_ZERO]  Theorem
      
      ⊢ ∀n. 2 ** n ≠ 0
   
   [ZERO_LT_TWOEXP]  Theorem
      
      ⊢ ∀n. 0 < 2 ** n
   
   
*)
end

HOL 4, Kananaskis-14