- BCARRY_def_compute
-
|- (∀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)
- BCARRY_LEM
-
|- ∀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))
- BCARRY_EQ
-
|- ∀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)
- BSUM_EQ
-
|- ∀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)
- BSUM_LEM
-
|- ∀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)
- BITWISE_ADD
-
|- ∀x y. x + y = FCP i. BSUM i ($' x) ($' y) F
- BITWISE_SUB
-
|- ∀x y. x − y = FCP i. BSUM i ($' x) ($~ o $' y) T
- BITWISE_LO
-
|- ∀x y. x <₊ y ⇔ ¬BCARRY (dimindex (:α)) ($' x) ($~ o $' y) T
- BITWISE_MUL
-
|- ∀w m.
w * m =
FOLDL (λa j. a + FCP i. w ' j ∧ j ≤ i ∧ m ' (i − j)) 0w
(COUNT_LIST (dimindex (:α)))
- word_lsl_bv_expand
-
|- ∀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)
- word_lsr_bv_expand
-
|- ∀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)
- word_asr_bv_expand
-
|- ∀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)
- word_ror_bv_expand
-
|- ∀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 (:α)))
- word_rol_bv_expand
-
|- ∀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 (:α)))