Theory numeral_bit

⊢ (∀f x b e y. BIT_MODF 0 f x b e y = y) ∧
  ∀n f x b e y.
    BIT_MODF (SUC n) f x b e y =
    BIT_MODF n f (x DIV 2) (b + 1) (2 * e)
      (if f b (ODD x) then e + y else y)

⊢ (∀x y. BIT_REV 0 x y = y) ∧
  ∀n x y.
    BIT_REV (SUC n) x y = BIT_REV n (x DIV 2) (2 * y + SBIT (ODD x) 0)

⊢ (∀f. FDUB f 0 = 0) ∧ ∀f n. FDUB f (SUC n) = f (f (SUC n))

⊢ (∀f x. SFUNPOW f 0 x = x) ∧
  ∀f n x. SFUNPOW f (SUC n) x = if x = 0 then 0 else SFUNPOW f n (f x)

⊢ numeral_bit$iBITWISE = BITWISE

⊢ numeral_bit$iDIV2 = DIV2

⊢ ∀n. numeral_bit$iLOG2 n = LOG2 (n + 1)

⊢ numeral_bit$iMOD_2EXP = MOD_2EXP

⊢ numeral_bit$iSUC = SUC

⊢ ∀m f n. BIT_MODIFY m f n = BIT_MODF m f n 0 1 0

⊢ ∀m n. BIT_REVERSE m n = BIT_REV m n 0

⊢ ∀n x. DIV_2EXP n x = FUNPOW DIV2 n x

⊢ FDUB (FDUB f) ZERO = ZERO ∧
  (∀x. FDUB (FDUB f) (numeral_bit$iSUC x) =
       FDUB f (FDUB f (numeral_bit$iSUC x))) ∧
  (∀x. FDUB (FDUB f) <..num comp'n..> = FDUB f (FDUB f <..num comp'n..> )) ∧
  ∀x. FDUB (FDUB f) <..num comp'n..> = FDUB f (FDUB f <..num comp'n..> )

⊢ ∀x. FDUB numeral_bit$iDIV2 x = numeral_bit$iDIV2 (numeral_bit$iDIV2 x)

⊢ ∀x. FDUB numeral$iDUB x = <..num comp'n..>

⊢ ∀m n.
    LOG m n =
    if m < 2 ∨ n = 0 then FAIL LOG $var$(base < 2 or n = 0) m n
    else if n < m then 0
    else SUC (LOG m (n DIV m))

⊢ ∀n. n ≠ 0 ⇒
      LOWEST_SET_BIT n = if ODD n then 0 else 1 + LOWEST_SET_BIT (DIV2 n)

⊢ (∀n. LOWEST_SET_BIT <..num comp'n..> =
       SUC (LOWEST_SET_BIT <..num comp'n..> )) ∧
  ∀n. LOWEST_SET_BIT <..num comp'n..> = 0

⊢ (∀x. MOD_2EXP x 0 = 0) ∧
  ∀x n. MOD_2EXP x <..num comp'n..> = <..num comp'n..>

⊢ (∀a b. MOD_2EXP_EQ 0 a b ⇔ T) ∧
  (∀n a b.
     MOD_2EXP_EQ (SUC n) a b ⇔
     (ODD a ⇔ ODD b) ∧ MOD_2EXP_EQ n (DIV2 a) (DIV2 b)) ∧
  ∀n a. MOD_2EXP_EQ n a a ⇔ T

⊢ (∀a. MOD_2EXP_MAX 0 a ⇔ T) ∧
  ∀n a. MOD_2EXP_MAX (SUC n) a ⇔ ODD a ∧ MOD_2EXP_MAX n (DIV2 a)

⊢ (∀x f a. BITWISE x f 0 0 = <..num comp'n..> ) ∧
  (∀x f a. BITWISE x f <..num comp'n..> 0 = <..num comp'n..> ) ∧
  (∀x f b. BITWISE x f 0 <..num comp'n..> = <..num comp'n..> ) ∧
  ∀x f a b.
    BITWISE x f <..num comp'n..> <..num comp'n..> = <..num comp'n..>

⊢ (∀f x b e y. BIT_MODF 0 f x b e y = y) ∧
  (∀n f b e y.
     BIT_MODF <..num comp'n..> f 0 b <..num comp'n..> y =
     BIT_MODF (<..num comp'n..> − 1) f 0 (b + 1) <..num comp'n..>
       (if f b F then <..num comp'n..> + y else y)) ∧
  (∀n f b e y.
     BIT_MODF <..num comp'n..> f 0 b <..num comp'n..> y =
     BIT_MODF <..num comp'n..> f 0 (b + 1) <..num comp'n..>
       (if f b F then <..num comp'n..> + y else y)) ∧
  (∀n f x b e y.
     BIT_MODF <..num comp'n..> f <..num comp'n..> b <..num comp'n..> y =
     BIT_MODF (<..num comp'n..> − 1) f (DIV2 <..num comp'n..> ) (b + 1)
       <..num comp'n..> (if f b (ODD x) then <..num comp'n..> + y else y)) ∧
  ∀n f x b e y.
    BIT_MODF <..num comp'n..> f <..num comp'n..> b <..num comp'n..> y =
    BIT_MODF <..num comp'n..> f (DIV2 <..num comp'n..> ) (b + 1)
      <..num comp'n..> (if f b (ODD x) then <..num comp'n..> + y else y)

⊢ (∀m f.
     BIT_MODIFY <..num comp'n..> f 0 = BIT_MODF <..num comp'n..> f 0 0 1 0) ∧
  ∀m f n.
    BIT_MODIFY <..num comp'n..> f <..num comp'n..> =
    BIT_MODF <..num comp'n..> f <..num comp'n..> 0 1 0

⊢ (∀x y. BIT_REV 0 x y = y) ∧
  (∀n y.
     BIT_REV <..num comp'n..> 0 y =
     BIT_REV (<..num comp'n..> − 1) 0 <..num comp'n..> ) ∧
  (∀n y.
     BIT_REV <..num comp'n..> 0 y =
     BIT_REV <..num comp'n..> 0 <..num comp'n..> ) ∧
  (∀n x y.
     BIT_REV <..num comp'n..> <..num comp'n..> y =
     BIT_REV (<..num comp'n..> − 1) (DIV2 <..num comp'n..> )
       (if ODD x then <..num comp'n..> else <..num comp'n..> )) ∧
  ∀n x y.
    BIT_REV <..num comp'n..> <..num comp'n..> y =
    BIT_REV <..num comp'n..> (DIV2 <..num comp'n..> )
      (if ODD x then <..num comp'n..> else <..num comp'n..> )

⊢ (∀m. BIT_REVERSE <..num comp'n..> 0 = <..num comp'n..> ) ∧
  ∀n m. BIT_REVERSE <..num comp'n..> <..num comp'n..> = <..num comp'n..>

⊢ (∀n. DIV_2EXP n 0 = 0) ∧
  ∀n x. DIV_2EXP n <..num comp'n..> = <..num comp'n..>

⊢ ∀f. (∀x. SFUNPOW (FDUB f) 0 x = x) ∧ (∀y. SFUNPOW (FDUB f) y 0 = 0) ∧
      (∀n x.
         SFUNPOW (FDUB f) <..num comp'n..> x =
         SFUNPOW (FDUB (FDUB f)) <..num comp'n..> (FDUB f x)) ∧
      ∀n x.
        SFUNPOW (FDUB f) <..num comp'n..> x =
        SFUNPOW (FDUB (FDUB f)) <..num comp'n..> (FDUB f (FDUB f x))

⊢ (∀x. SFUNPOW numeral_bit$iDIV2 0 x = x) ∧
  (∀y. SFUNPOW numeral_bit$iDIV2 y 0 = 0) ∧
  (∀n x.
     SFUNPOW numeral_bit$iDIV2 <..num comp'n..> x =
     SFUNPOW (FDUB numeral_bit$iDIV2) <..num comp'n..>
       (numeral_bit$iDIV2 x)) ∧
  ∀n x.
    SFUNPOW numeral_bit$iDIV2 <..num comp'n..> x =
    SFUNPOW (FDUB numeral_bit$iDIV2) <..num comp'n..>
      (numeral_bit$iDIV2 (numeral_bit$iDIV2 x))

⊢ (∀x. SFUNPOW numeral$iDUB 0 x = x) ∧ (∀y. SFUNPOW numeral$iDUB y 0 = 0) ∧
  (∀n x.
     SFUNPOW numeral$iDUB <..num comp'n..> x =
     SFUNPOW (FDUB numeral$iDUB) <..num comp'n..> <..num comp'n..> ) ∧
  ∀n x.
    SFUNPOW numeral$iDUB <..num comp'n..> x =
    SFUNPOW (FDUB numeral$iDUB) <..num comp'n..> <..num comp'n..>

⊢ (∀n. TIMES_2EXP n 0 = 0) ∧
  ∀n x. TIMES_2EXP n <..num comp'n..> = <..num comp'n..>

⊢ numeral_bit$iDIV2 ZERO = ZERO ∧
  numeral_bit$iDIV2 (numeral_bit$iSUC ZERO) = ZERO ∧
  numeral_bit$iDIV2 <..num comp'n..> = n ∧
  numeral_bit$iDIV2 (numeral_bit$iSUC <..num comp'n..> ) =
  numeral_bit$iSUC n ∧
  numeral_bit$iDIV2 <..num comp'n..> = numeral_bit$iSUC n ∧
  numeral_bit$iDIV2 (numeral_bit$iSUC <..num comp'n..> ) =
  numeral_bit$iSUC n ∧ <..num comp'n..> = <..num comp'n..>

⊢ (∀opr a b. numeral_bit$iBITWISE 0 opr a b = ZERO) ∧
  (∀x opr a b.
     numeral_bit$iBITWISE <..num comp'n..> opr a b =
     (let
        w =
          numeral_bit$iBITWISE (<..num comp'n..> − 1) opr (DIV2 a) (DIV2 b)
      in
        if opr (ODD a) (ODD b) then <..num comp'n..> else <..num comp'n..> )) ∧
  ∀x opr a b.
    numeral_bit$iBITWISE <..num comp'n..> opr a b =
    (let
       w = numeral_bit$iBITWISE <..num comp'n..> opr (DIV2 a) (DIV2 b)
     in
       if opr (ODD a) (ODD b) then <..num comp'n..> else <..num comp'n..> )

⊢ <..num comp'n..> = <..num comp'n..>

⊢ numeral_bit$iLOG2 ZERO = 0 ∧
  (∀n. numeral_bit$iLOG2 <..num comp'n..> = 1 + numeral_bit$iLOG2 n) ∧
  ∀n. numeral_bit$iLOG2 <..num comp'n..> = 1 + numeral_bit$iLOG2 n

⊢ (∀n. numeral_bit$iMOD_2EXP 0 n = ZERO) ∧
  (∀x n. numeral_bit$iMOD_2EXP x ZERO = ZERO) ∧
  (∀x n.
     numeral_bit$iMOD_2EXP <..num comp'n..> <..num comp'n..> =
     <..num comp'n..> ) ∧
  (∀x n.
     numeral_bit$iMOD_2EXP <..num comp'n..> <..num comp'n..> =
     <..num comp'n..> ) ∧
  (∀x n.
     numeral_bit$iMOD_2EXP <..num comp'n..> <..num comp'n..> =
     <..num comp'n..> ) ∧
  ∀x n.
    numeral_bit$iMOD_2EXP <..num comp'n..> <..num comp'n..> =
    <..num comp'n..>

⊢ (∀n. LOG2 <..num comp'n..> = numeral_bit$iLOG2 <..num comp'n..> ) ∧
  ∀n. LOG2 <..num comp'n..> = numeral_bit$iLOG2 <..num comp'n..>

⊢ 0 MOD 2 = 0 ∧ (∀n. <..num comp'n..> MOD 2 = 1) ∧
  ∀n. <..num comp'n..> MOD 2 = 0