Theory blast

⊢ (∀x y c. BCARRY 0 x y c ⇔ c) ∧
  ∀i x y c. BCARRY (SUC i) x y c ⇔ bcarry (x i) (y i) (BCARRY i x y c)

⊢ ∀i x y c. BSUM i x y c ⇔ bsum (x i) (y i) (BCARRY i x y c)

⊢ ∀x y c. bcarry x y c ⇔ x ∧ y ∨ (x ∨ y) ∧ c

⊢ ∀x y c. bsum x y c ⇔ ((x ⇔ ¬y) ⇔ ¬c)

⊢ ∀n c x1 x2 y1 y2.
    (∀i. i < n ⇒ (x1 i ⇔ x2 i) ∧ (y1 i ⇔ y2 i)) ⇒
    (BCARRY n x1 y1 c ⇔ BCARRY n x2 y2 c)

⊢ x ∧ y ∨ (x ∨ y) ∧ F ⇔ x ∧ y

⊢ ∀i x y c.
    0 < i ⇒
    (BCARRY i (λi. BIT i x) (λi. BIT i y) c ⇔
     BIT i (BITS (i − 1) 0 x + BITS (i − 1) 0 y + if c then 1 else 0))

⊢ x ∧ y ∨ (x ∨ y) ∧ T ⇔ x ∨ y

⊢ (∀x y c. BCARRY 0 x y c ⇔ c) ∧
  (∀i x y c.
     BCARRY (NUMERAL (BIT1 i)) x y c ⇔
     bcarry (x (NUMERAL (BIT1 i) − 1)) (y (NUMERAL (BIT1 i) − 1))
       (BCARRY (NUMERAL (BIT1 i) − 1) x y c)) ∧
  ∀i x y c.
    BCARRY (NUMERAL (BIT2 i)) x y c ⇔
    bcarry (x (NUMERAL (BIT1 i))) (y (NUMERAL (BIT1 i)))
      (BCARRY (NUMERAL (BIT1 i)) x y c)

⊢ ∀x y c i n b1 b2 b3.
    i = SUC n ∧ (x n ⇔ b1) ∧ (y n ⇔ b2) ∧ (BCARRY n x y c ⇔ b3) ⇒
    (BCARRY i x y c ⇔ bcarry b1 b2 b3)

⊢ ∀x y. x + y = FCP i. BSUM i ($' x) ($' y) F

⊢ ∀x y. x <₊ y ⇔ ¬BCARRY (dimindex (:α)) ($' x) ($¬ ∘ $' y) T

⊢ ∀w m.
    w * m =
    FOLDL (λa j. a + FCP i. w ' j ∧ j ≤ i ∧ m ' (i − j)) 0w
      (COUNT_LIST (dimindex (:α)))

⊢ ∀x y. x − y = FCP i. BSUM i ($' x) ($¬ ∘ $' y) T

⊢ ∀n c x1 x2 y1 y2.
    (∀i. i ≤ n ⇒ (x1 i ⇔ x2 i) ∧ (y1 i ⇔ y2 i)) ⇒
    (BSUM n x1 y1 c ⇔ BSUM n x2 y2 c)

⊢ ((x ⇔ ¬y) ⇔ ¬F) ⇔ (x ⇔ ¬y)

⊢ ∀i x y c.
    BSUM i (λi. BIT i x) (λi. BIT i y) c ⇔
    BIT i (x + y + if c then 1 else 0)

⊢ ((x ⇔ ¬y) ⇔ ¬T) ⇔ (x ⇔ y)

⊢ ∀x y c i b1 b2 b3.
    (x i ⇔ b1) ∧ (y i ⇔ b2) ∧ (BCARRY i x y c ⇔ b3) ⇒
    (BSUM i x y c ⇔ bsum b1 b2 b3)

⊢ ∀a b. a = b ⇔ EVERY (λi. a ' i ⇔ b ' i) (GENLIST I (dimindex (:α)))

⊢ ∀i a b. i < dimindex (:α) ∧ ((a ' i ⇔ b ' i) ⇔ F) ⇒ (a = b ⇔ F)

⊢ ∀b. (b ⇔ ¬b) ⇔ F

⊢ ∀b. (if b then T else T) ⇔ T

⊢ ∀b x y i. (if b then x else y) ' i ⇔ if b then x ' i else y ' i

⊢ a < b + (c + 1) ⇔ a ≤ b + c

⊢ -1w = $FCP (K T)

⊢ ∀b. (¬b ⇔ b) ⇔ F

⊢ ∀w. sw2sw w =
      FCP i.
        if i < dimindex (:α) ∨ dimindex (:β) < dimindex (:α) then w ' i
        else w ' (dimindex (:α) − 1)

⊢ ∀w. w2w w = FCP i. i < dimindex (:α) ∧ w ' i

⊢ INT_MINw = FCP i. i = dimindex (:α) − 1

⊢ ∀w m.
    w >>~ m =
    if dimindex (:α) = 1 then $FCP (K (w ' 0))
    else
      FCP k.
        FOLDL
          (λa j.
             a ∨ (LOG2 (dimindex (:α) − 1) -- 0) m = n2w j ∧ (w ≫ j) ' k) F
          (COUNT_LIST (dimindex (:α))) ∧
        (dimindex (:α) − 1 -- LOG2 (dimindex (:α) − 1) + 1) m = 0w ∨
        n2w (dimindex (:α) − 1) <₊ m ∧ w ' (dimindex (:α) − 1)

⊢ ∀l h n w.
    l + n < dimindex (:α) ∧ l + n ≤ h ⇒ ((h -- l) w ' n ⇔ w ' (n + l))

⊢ ∀l h n w. n < dimindex (:α) ∧ h < l + n ⇒ ((h -- l) w ' n ⇔ F)

⊢ ∀w m.
    w <<~ m =
    if dimindex (:α) = 1 then $FCP (K (¬m ' 0 ∧ w ' 0))
    else
      FCP k.
        FOLDL
          (λa j.
             a ∨
             (LOG2 (dimindex (:α) − 1) -- 0) m = n2w j ∧ j ≤ k ∧
             w ' (k − j)) F (COUNT_LIST (dimindex (:α))) ∧
        (dimindex (:α) − 1 -- LOG2 (dimindex (:α) − 1) + 1) m = 0w

⊢ ∀w m.
    w >>>~ m =
    if dimindex (:α) = 1 then $FCP (K (¬m ' 0 ∧ w ' 0))
    else
      FCP k.
        FOLDL
          (λa j.
             a ∨
             (LOG2 (dimindex (:α) − 1) -- 0) m = n2w j ∧
             k + j < dimindex (:α) ∧ w ' (k + j)) F
          (COUNT_LIST (dimindex (:α))) ∧
        (dimindex (:α) − 1 -- LOG2 (dimindex (:α) − 1) + 1) m = 0w

⊢ ∀w m.
    w #<<~ m =
    FCP k.
      FOLDL
        (λa j.
           a ∨
           word_mod m (n2w (dimindex (:α))) = n2w j ∧
           w '
           ((k + (dimindex (:α) − j) MOD dimindex (:α)) MOD dimindex (:α)))
        F (COUNT_LIST (dimindex (:α)))

⊢ ∀w m.
    w #>>~ m =
    FCP k.
      FOLDL
        (λa j.
           a ∨
           word_mod m (n2w (dimindex (:α))) = n2w j ∧
           w ' ((j + k) MOD dimindex (:α))) F (COUNT_LIST (dimindex (:α)))

⊢ (a ⇎ b) ⇔ (a ⇔ ¬b)