Theory bit

⊢ ∀h l n. BITS h l n = MOD_2EXP (SUC h − l) (DIV_2EXP l n)

⊢ ∀n b. BITV n b = BITS b b n

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

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

⊢ (∀x. BIT_REVERSE 0 x = 0) ∧
  ∀n x. BIT_REVERSE (SUC n) x = BIT_REVERSE n x * 2 + SBIT (BIT n x) 0

⊢ ∀b n. BIT b n ⇔ BITS b b n = 1

⊢ ∀x n. DIVMOD_2EXP x n = (n DIV 2 ** x,n MOD 2 ** x)

⊢ ∀x n. DIV_2EXP x n = n DIV 2 ** x

⊢ LOG2 = LOG 2

⊢ ∀n. LOWEST_SET_BIT n = LEAST i. BIT i n

⊢ ∀n a b. MOD_2EXP_EQ n a b ⇔ MOD_2EXP n a = MOD_2EXP n b

⊢ ∀n a. MOD_2EXP_MAX n a ⇔ MOD_2EXP n a = 2 ** n − 1

⊢ ∀x n. MOD_2EXP x n = n MOD 2 ** x

⊢ ∀b n. SBIT b n = if b then 2 ** n else 0

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

⊢ ∀h l n. SLICE h l n = MOD_2EXP (SUC h) n − MOD_2EXP l n

⊢ ∀x n. TIMES_2EXP x n = n * 2 ** x

⊢ ∀m n. BIT 0 (m + n) ⇔ (BIT 0 m ⇎ BIT 0 n)

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

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

⊢ BIT 0 = ODD

⊢ ∀h l n. BITS h l n < 2 ** (SUC h − l)

⊢ ∀h l n. BITS h l n < 2 ** SUC h

⊢ ∀h1 l1 h2 l2 n.
    h2 + l1 ≤ h1 ⇒ BITS h2 l2 (BITS h1 l1 n) = BITS (h2 + l1) (l2 + l1) n

⊢ ∀h1 l1 h2 l2 n.
    BITS h2 l2 (BITS h1 l1 n) = BITS (MIN h1 (h2 + l1)) (l2 + l1) n

⊢ ∀h l x n. BITS h l x DIV 2 ** n = BITS h (l + n) x

⊢ ∀h l n. BITS h l n ≤ n

⊢ ∀n. 0 < n ⇒ BITS (LOG2 n) 0 n = n

⊢ ∀h l n. n < 2 ** SUC h ⇒ BITS h l n = n DIV 2 ** l

⊢ ∀h l n. n < 2 ** l ⇒ BITS h l n = 0

⊢ ∀h a b. BITS h 0 (BITS h 0 a * BITS h 0 b) = BITS h 0 (a * b)

⊢ ∀h l n. BITS h l (SLICE h l n) = BITS h l n

⊢ ∀h h2 l n. h ≤ h2 ⇒ BITS h2 l (SLICE h l n) = BITS h l n

⊢ ∀h l n.
    l ≤ SUC h ⇒
    SBIT (BIT (SUC h) n) (SUC h − l) + BITS h l n = BITS (SUC h) l n

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

⊢ ∀h l a b. b < 2 ** l ⇒ BITS h l (a * 2 ** l + b) = BITS h l (a * 2 ** l)

⊢ ∀h l a b. BITS h l (a * 2 ** SUC h + b) = BITS h l b

⊢ ∀h a b. BITS h 0 (BITS h 0 a + BITS h 0 b) = BITS h 0 (a + b)

⊢ ∀h l n. BITS h l n = n DIV 2 ** l MOD 2 ** (SUC h − l)

⊢ ∀h l n. BITS h l n = n MOD 2 ** SUC h DIV 2 ** l

⊢ ∀h l n. h < l ⇒ BITS h l n = 0

⊢ ∀h l. BITS h l 0 = 0

⊢ ∀h n. BITS h 0 n = n MOD 2 ** SUC h

⊢ ∀h l a. l ≤ h ⇒ BITS h l (a * 2 ** l) = BITS (h − l) 0 a

⊢ ∀n m. (∀i. i ≤ n ⇒ ¬BIT i m) ⇒ BITS n 0 m = 0

⊢ ∀h a. a < 2 ** SUC h ⇒ BITS h 0 a = a

⊢ ∀b n. BITV n b = SBIT (BIT b n) 0

⊢ BITWISE w $/\ x 0 = 0 ∧ BITWISE w $/\ 0 x = 0

⊢ ∀w x y n. x < 2 ** n ⇒ BITWISE w $/\ x (y * 2 ** n) = 0

⊢ ∀wl op a b.
    BITWISE (SUC wl) op (BITS wl 0 a) (BITS wl 0 b) =
    BITWISE (SUC wl) op a b

⊢ (∀m. m ≤ n ⇒ (op (BIT m x) (BIT m y) ⇔ op (BIT m y) (BIT m x))) ⇒
  BITWISE n op x y = BITWISE n op y x

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

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

⊢ ∀n op a b. BITWISE n op a b < 2 ** n

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

⊢ ∀n a b. BITWISE (SUC n) (λx y. ¬x) a b = 2 ** SUC n − 1 − BITS n 0 a

⊢ ∀x n op a b. x < n ⇒ (BIT x (BITWISE n op a b) ⇔ op (BIT x a) (BIT x b))

⊢ ∀b. BIT b (2 ** b)

⊢ ∀h l a b.
    (∀x. l ≤ x ∧ x ≤ h ⇒ (BIT x a ⇔ BIT x b)) ⇔ BITS h l a = BITS h l b

⊢ ∀a b. a ≠ b ⇒ ¬BIT a (2 ** b)

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

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

⊢ ∀b n. BIT b n ⇔ n DIV 2 ** b MOD 2 = 1

⊢ ∀n i. BIT n (i DIV 2) ⇔ BIT (SUC n) i

⊢ ∀b n. BIT b (2 ** n − 1) ⇔ b < n

⊢ ∀i n. BIT i n ⇒ 2 ** i ≤ n

⊢ ∀n. n ≠ 0 ⇒ BIT (LOG2 n) n

⊢ ∀x n f a. x < n ⇒ (BIT x (BIT_MODIFY n f a) ⇔ f x (BIT x a))

⊢ ∀n h l a. l + n ≤ h ⇒ (BIT n (BITS h l a) ⇔ BIT (l + n) a)

⊢ ∀h l x n. h < l + x ⇒ ¬BIT x (BITS h l n)

⊢ ∀x n a. x < n ⇒ (BIT x (BIT_REVERSE n a) ⇔ BIT (n − 1 − x) a)

⊢ ∀n a s. BIT (n + s) (a * 2 ** s) ⇔ BIT n a

⊢ ∀n a s. s ≤ n ⇒ (BIT n (a * 2 ** s) ⇔ BIT (n − s) a)

⊢ ∀n a s. n < s ⇒ ¬BIT n (a * 2 ** s)

⊢ ∀n i a. BIT i (a DIV 2 ** n) ⇔ BIT (i + n) a

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

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

⊢ ∀n a b. (BIT n a ⇔ BIT n b) ⇔ SLICE n n a = SLICE n n b

⊢ ∀y x n. SBIT (BIT x n) (x + y) = SLICE x x n * 2 ** y

⊢ ∀x n. SBIT (BIT x n) x = SLICE x x n

⊢ ∀b n. BIT b n ⇔ SLICE b b n = 2 ** b

⊢ ∀b n. ¬BIT b n ⇔ SLICE b b n = 0

⊢ ∀b h l n. BIT b (SLICE h l n) ⇔ l ≤ b ∧ b ≤ h ∧ BIT b n

⊢ BIT z (2 * n) ⇔ 0 < z ∧ BIT (z − 1) n

⊢ ∀n z. BIT z (2 * n + 1) ⇔ z = 0 ∨ BIT z (2 * n)

⊢ ∀n m. BIT n (2 ** m) ⇔ m = n

⊢ ∀b. ¬BIT b 0

⊢ ∀x n. DIVMOD_2EXP x n = (DIV_2EXP x n,MOD_2EXP x n)

⊢ ∀a b. b ≤ a ∧ 0 < b ⇒ 0 < a DIV b

⊢ ∀n m a. n < m ∧ a < 2 ** m ⇒ a DIV 2 ** n < 2 ** m

⊢ ∀r n. r < n ⇒ (n + r) DIV n = 1

⊢ ∀x n. n DIV 2 ** x * 2 ** x = n − n MOD 2 ** x

⊢ ∀n. 2 * (n DIV 2) = n − n MOD 2

⊢ ∀a b.
    2 ** b ≤ a ∧ a MOD 2 ** b = 0 ⇒ a DIV 2 ** b − 1 = (a − 1) DIV 2 ** b

⊢ ∀a b n. n ≠ 0 ∧ 2 ** a ≤ n ∧ n < 2 ** b ⇒ ∃i. a ≤ i ∧ i < b ∧ BIT i n

⊢ ∀b n. n ≠ 0 ∧ n < 2 ** b ⇒ ∃i. i < b ∧ BIT i n

⊢ ∀a b. 2 ** (a − b) ≤ 2 ** a

⊢ ∀n P. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ $LEAST P = n

⊢ ∀a b. a ≤ b ⇒ ∃p. 2 ** b = p * 2 ** a

⊢ ∀a b x y. a < x ∧ b < y ⇒ a * b < x * y

⊢ ∀x y. 0 < x ⇒ x ≤ y ⇒ LOG2 x ≤ LOG2 y

⊢ ∀n. LOG2 (2 ** n) = n

⊢ ∀n p. 2 ** p ≤ n ∧ n < 2 ** SUC p ⇒ LOG2 n = p

⊢ ∀x n. x < 2 ** n ⇔ x = 0 ∨ LOG2 x < n

⊢ ∀n k. k MOD 2 ** n < 2 ** n

⊢ ∀n h l. l ≤ h ⇒ n MOD 2 ** l ≤ n MOD 2 ** SUC h

⊢ ∀n. 0 < n ⇒ ∀x. (x + 1) MOD n ≠ 0 ⇒ (x + 1) MOD n = x MOD n + 1

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

⊢ ∀n. 0 < n ⇒ ∀x. (x + 1) MOD n = 0 ⇔ x MOD n + 1 = n

⊢ ∀n j k. (k MOD n + j) MOD n = (k + j) MOD n

⊢ ∀n j k. (j + k MOD n) MOD n = (j + k) MOD n

⊢ ∀n a. a ≠ 0 ∧ a MOD 2 ** n = 0 ⇒ 2 ** n ≤ a

⊢ ∀n a. ¬BIT n a ⇔ BITS n n a = 0

⊢ ∀n a. BITS n n a ≠ 0 ⇔ BITS n n a = 1

⊢ ∀n a. BITS n n a ≠ 1 ⇔ BITS n n a = 0

⊢ ∀i n op a b. n ≤ i ⇒ ¬BIT i (BITWISE n op a b)

⊢ ∀i n. LOG2 n < i ⇒ ¬BIT i n

⊢ ∀i n. n < 2 ** i ⇒ ¬BIT i n

⊢ ∀n. n MOD 2 ≠ 0 ⇔ n MOD 2 = 1

⊢ ∀n. n MOD 2 ≠ 1 ⇔ n MOD 2 = 0

⊢ ∀m. m ≠ 0 ⇒ ∃p. m = SUC p

⊢ ∀n. ODD n ⇔ n MOD 2 = 1

⊢ ODD (x MOD 2) ⇔ ODD x

⊢ ∀n. 1 ≤ 2 ** n

⊢ ∀b m n. n < m ⇒ SBIT b (m − n) = SBIT b m DIV 2 ** n

⊢ ∀b m n. SBIT b n * 2 ** m = SBIT b (n + m)

⊢ ∀h l n. SLICE h l n < 2 ** SUC h

⊢ ∀h m' m l n.
    l ≤ m ∧ m' = m + 1 ∧ m < h ⇒ SLICE h m' n + SLICE m l n = SLICE h l n

⊢ ∀h m l n.
    SUC m ≤ h ∧ l ≤ m ⇒ SLICE h (SUC m) n + SLICE m l n = SLICE h l n

⊢ ∀h l x y n. h ≤ x ∧ y ≤ l ⇒ SLICE h l (SLICE x y n) = SLICE h l n

⊢ ∀n h l. SLICE h l n = BITS h l n * 2 ** l

⊢ ∀h l n. h < l ⇒ SLICE h l n = 0

⊢ ∀l h. SLICE h l 0 = 0

⊢ ∀n h. SLICE h 0 n = BITS h 0 n

⊢ ∀a. SUC a − a = 1

⊢ ∀n k. k = k DIV 2 ** n * 2 ** n + k MOD 2 ** n

⊢ (∀x y. 2 ** x ≤ y ⇒ x ≤ LOG2 y) ∧ ∀y x. 0 < x ⇒ x ≤ 2 ** y ⇒ LOG2 x ≤ y

⊢ ∀a b. a < b ⇒ 2 ** a < 2 ** b

⊢ ∀a b. a ≤ b ⇒ 2 ** a ≤ 2 ** b

⊢ ∀n. 2 ** n ≠ 0

⊢ ∀n. 0 < 2 ** n