theorem Nat.eq_one_mod_two_of_ne_zero (n : ℕ) (h : (n % 2 != 0) = true) : n % 2 = 1

theorem Nat.sub_mod_of_lt (n : ℕ) (x : ℕ) (hxgt0 : x > 0) (hxltn : x < n) : (n - x) % n = n - x

theorem Nat.two_pow_pred_sub_two_pow {w : ℕ} (h : 0 < w) : 2 ^ (w - 1) - 2 ^ w = -2 ^ (w - 1)

@[simp]

theorem Nat.one_mod_two_pow_eq {n : ℕ} (hn : n ≠ 0) : 1 % 2 ^ n = 1

theorem Nat.cases_of_lt_mod_add {a : ℕ} {b : ℕ} {m : ℕ} {k : ℕ} (hsum : (a + b) % m < k) (ha : a < m) (hb : b < m) : a + b < m ∧ a + b < k ∨ a + b ≥ m ∧ a + b < m + k

theorem Nat.mod_eq_if {a : ℕ} {b : ℕ} : a % b = if 0 ≤ a ∧ a < b then a else if b ≤ a ∧ a < 2 * b then a - b else a % b

@[simp]

theorem Nat.mod_two_pow_mod_two (x : ℕ) (w : ℕ) : 0 < w → x % 2 ^ w % 2 = x % 2

theorem Nat.two_le_add_iff_odd_and_odd (n : ℕ) (m : ℕ) : 2 ≤ n % 2 + m % 2 ↔ n % 2 = 1 ∧ m % 2 = 1

theorem Nat.add_odd_iff_neq (n : ℕ) (m : ℕ) : (n + m) % 2 = 1 ↔ (n % 2 = 1) ≠ (m % 2 = 1)

theorem Nat.mod_eq_of_eq {a : ℕ} {b : ℕ} {c : ℕ} (h : a = b) : a % c = b % c

@[simp]

theorem BitVec.replicate_one {w : ℕ} : BitVec.replicate w 1#1 = BitVec.cast ⋯ (BitVec.allOnes w)

@[simp]

theorem BitVec.replicate_zero {w : ℕ} : BitVec.replicate w 0#1 = BitVec.cast ⋯ 0#w

theorem BitVec.abs_eq_add_xor {w : ℕ} {x : BitVec w} : let_fun y := BitVec.cast ⋯ (BitVec.replicate w (BitVec.ofBool x.msb)); x.abs = x + y ^^^ y

theorem BitVec.abs_eq_if {w : ℕ} {x : BitVec w} : x.abs = if x.msb = true then -x else x

@[simp]

theorem BitVec.toNat_shiftLeft' {w : ℕ} (A : BitVec w) (B : BitVec w) : (A <<< B).toNat = A.toNat * 2 ^ B.toNat % 2 ^ w

theorem BitVec.one_shiftLeft_mul_eq_shiftLeft {w : ℕ} {A : BitVec w} {B : BitVec w} : 1 <<< B * A = A <<< B

@[simp]

def BitVec.msb_one {w : ℕ} (h : 1 < w) : (1#w).msb = false

Equations

• ⋯ = ⋯

@[simp]

theorem BitVec.msb_one_of_width_one : (1#1).msb = true

def BitVec.msb_allOnes {w : ℕ} (h : 0 < w) : (BitVec.allOnes w).msb = true

Equations

• ⋯ = ⋯

def BitVec.neg_allOnes {w : ℕ} : -BitVec.allOnes w = 1#w

Equations

• ⋯ = ⋯

theorem BitVec.udiv_one_eq_self (w : ℕ) (x : BitVec w) : x.udiv 1#w = x

theorem BitVec.udiv_eq_zero_iff {w : ℕ} {x : BitVec w} {y : BitVec w} (h : 0#w < y) : x.udiv y = 0#w ↔ x < y

@[simp]

theorem BitVec.udiv_eq_zero {w : ℕ} {x : BitVec w} {y : BitVec w} (h : x < y) : x.udiv y = 0#w

def BitVec.sdiv_one_allOnes {w : ℕ} (h : 1 < w) : (1#w).sdiv (BitVec.allOnes w) = BitVec.allOnes w

Equations

• ⋯ = ⋯

theorem BitVec.width_one_cases (a : BitVec 1) : a = 0#1 ∨ a = 1#1

theorem BitVec.sub_eq_add_neg {w : ℕ} {x : BitVec w} {y : BitVec w} : x - y = x + -y

theorem BitVec.toNat_neq_of_neq_ofNat {w : ℕ} {a : BitVec w} {n : ℕ} (h : a ≠ BitVec.ofNat w n) : a.toNat ≠ n

theorem BitVec.gt_one_of_neq_0_neq_1 {w : ℕ} (a : BitVec w) (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a > 1

def BitVec.one_sdiv {w : ℕ} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1) (hao : a ≠ BitVec.allOnes w) : (1#w).sdiv a = 0#w

Equations

• ⋯ = ⋯

def BitVec.sdiv_one_one {w : ℕ} : (1#w).sdiv 1#w = 1#w

Equations

• ⋯ = ⋯

theorem BitVec.toNat_neq_zero_of_neq_zero {w : ℕ} {x : BitVec w} (hx : x ≠ 0) : x.toNat ≠ 0

theorem BitVec.eq_zero_of_toNat_mod_eq_zero {w : ℕ} {x : BitVec w} (hx : x.toNat % 2 ^ w = 0) : x = 0

theorem BitVec.toNat_one {w : ℕ} (hw : autoParam (w ≠ 0) _auto✝) : BitVec.toNat 1 = 1

theorem BitVec.intMin_eq_one {w : ℕ} (hw : w ≤ 1) : BitVec.intMin w = 1

theorem BitVec.intMin_neq_one {w : ℕ} (h : w > 1) : BitVec.intMin w ≠ 1

theorem BitVec.width_one_cases' (x : BitVec 1) : x = 0 ∨ x = 1

theorem BitVec.ult_toNat {n : ℕ} (x : BitVec n) (y : BitVec n) : (y >ᵤ x) = decide (x.toNat < y.toNat)

theorem BitVec.getLsb_geX {w : ℕ} {i : ℕ} (x : BitVec w) (hi : i ≥ w) : x.getLsbD i = false

theorem BitVec.intMin_slt_zero {w : ℕ} (h : 0 < w) : (0 >ₛ BitVec.intMin w) = true

theorem BitVec.neg_sgt_eq_slt_neg {w : ℕ} {A : BitVec w} {B : BitVec w} (h : A ≠ BitVec.intMin w) (h2 : B ≠ BitVec.intMin w) : (-A >ₛ B) = (-B >ₛ A)

theorem BitVec.sgt_zero_eq_not_neg_sgt_zero {w : ℕ} (A : BitVec w) (h_ne_intMin : A ≠ BitVec.intMin w) (h_ne_zero : A ≠ 0) : (A >ₛ 0#w) = true ↔ ¬(-A >ₛ 0#w) = true

theorem BitVec.sgt_same {w : ℕ} (A : BitVec w) : ¬(A >ₛ A) = true

theorem BitVec.intMin_not_gt_zero {w : ℕ} : ¬(BitVec.intMin w >ₛ 0#w) = true

theorem BitVec.zero_sub_eq_neg {w : ℕ} {A : BitVec w} : BitVec.ofInt w 0 - A = -A

theorem BitVec.width_zero_eq_zero (x : BitVec 0) : x = 0#0

@[simp]

theorem BitVec.toInt_width_zero (x : BitVec 0) : x.toInt = 0

@[simp]

theorem BitVec.neg_of_ofNat_0_minus_self {w : ℕ} (x : BitVec w) : 0#w - x = -x

@[simp]

theorem BitVec.carry_and_xor_false {i : ℕ} : ∀ {w : ℕ} {a b : BitVec w}, BitVec.carry i (a &&& b) (a ^^^ b) false = false

@[simp]

theorem BitVec.and_add_xor_eq_or {w : ℕ} {a : BitVec w} {b : BitVec w} : (a &&& b) + (a ^^^ b) = a ||| b

@[simp]

theorem BitVec.ofBool_eq' {a : Bool} {b : Bool} : BitVec.ofBool a = BitVec.ofBool b ↔ a = b

theorem BitVec.allOnes_xor_eq_not {w : ℕ} (x : BitVec w) : BitVec.allOnes w ^^^ x = ~~~x

theorem BitVec.allOnes_sub_eq_xor {w : ℕ} (x : BitVec w) : BitVec.allOnes w - x = x ^^^ BitVec.allOnes w

@[simp]

theorem BitVec.and_add_or {w : ℕ} {A : BitVec w} {B : BitVec w} : (B &&& A) + (B ||| A) = B + A

@[simp]

theorem BitVec.msb_signExtend_of_ge {w : ℕ} {i : ℕ} (h : i ≥ w) (x : BitVec w) : (BitVec.signExtend i x).msb = x.msb

theorem BitVec.signExtend_succ {w : ℕ} (i : ℕ) (x : BitVec w) : BitVec.signExtend (i + 1) x = BitVec.cons (if i < w then x.getLsbD i else x.msb) (BitVec.signExtend i x)

@[simp]

theorem BitVec.one_shiftLeft_mul {w : ℕ} {x : BitVec w} {y : BitVec w} : 1#w <<< x.toNat * y = y <<< x.toNat

@[simp]

theorem BitVec.mul_allOnes {w : ℕ} {x : BitVec w} : x * BitVec.allOnes w = -x

@[simp]

theorem BitVec.allOnes_sshiftRight {w : ℕ} {n : ℕ} : (BitVec.allOnes w).sshiftRight n = BitVec.allOnes w

@[simp]

theorem BitVec.zero_sshiftRight {w : ℕ} {n : ℕ} : (0#w).sshiftRight n = 0#w

@[simp]

theorem BitVec.zero_ushiftRight {w : ℕ} {n : ℕ} : 0#w >>> n = 0#w

theorem BitVec.ofInt_neg_one {w : ℕ} : BitVec.ofInt w (-1) = -1#w

@[simp]

theorem BitVec.shiftLeft_and_distrib' {w : ℕ} {x : BitVec w} {y : BitVec w} {n : ℕ} {m : ℕ} : x <<< n &&& y <<< (m + n) = (x &&& y <<< m) <<< n

@[simp]

theorem BitVec.zero_sub {w : ℕ} {x : BitVec w} : 0#w - x = -x

theorem BitVec.getLsbD_sub {w : ℕ} {i : ℕ} {i_lt : i < w} {x : BitVec w} {y : BitVec w} : (x - y).getLsbD i = (x.getLsbD i ^^ ((~~~y + 1).getLsbD i ^^ BitVec.carry i x (~~~y + 1) false))

theorem BitVec.getMsbD_add {w : ℕ} {i : ℕ} {i_lt : i < w} {x : BitVec w} {y : BitVec w} : (x + y).getMsbD i = (x.getMsbD i ^^ (y.getMsbD i ^^ BitVec.carry (w - 1 - i) x y false))

theorem BitVec.getMsbD_sub {w : ℕ} {i : ℕ} {i_lt : i < w} {x : BitVec w} {y : BitVec w} : (x - y).getMsbD i = (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ BitVec.carry (w - 1 - i) x (~~~y + 1) false))

theorem BitVec.msb_add {w : ℕ} {x : BitVec w} {y : BitVec w} : (x + y).msb = (x.getMsbD 0 ^^ (y.getMsbD 0 ^^ BitVec.carry (w - 1) x y false))

theorem BitVec.msb_sub {w : ℕ} {x : BitVec w} {y : BitVec w} : (x - y).msb = (x.getMsbD 0 ^^ ((~~~y + 1#w).getMsbD 0 ^^ BitVec.carry (w - 1 - 0) x (~~~y + 1#w) false))

theorem BitVec.msb_neg {w : ℕ} {x : BitVec w} : (-x).msb = (~~~x + 1#w).msb

theorem BitVec.getLsbD_neg {w : ℕ} {i : ℕ} {x : BitVec w} : (-x).getLsbD i = (~~~x + 1#w).getLsbD i

theorem BitVec.getMsbD_neg {w : ℕ} {i : ℕ} {x : BitVec w} : (-x).getMsbD i = (~~~x + 1#w).getMsbD i

theorem BitVec.getLsbD_abs {w : ℕ} {i : ℕ} {x : BitVec w} : x.abs.getLsbD i = (if x.msb = true then -x else x).getLsbD i

theorem BitVec.getMsbD_abs {w : ℕ} {i : ℕ} {x : BitVec w} : x.abs.getMsbD i = (if x.msb = true then -x else x).getMsbD i

theorem BitVec.msb_abs {w : ℕ} {x : BitVec w} : x.abs.msb = (if x.msb = true then -x else x).msb

theorem Bool.xor_decide (p : Prop) (q : Prop) [dp : Decidable p] [Decidable q] : (decide p ^^ decide q) = decide (p ≠ q)

@[simp]

theorem Bool.xor_not_xor {a : Bool} {b : Bool} : (!(a ^^ b) ^^ b) = !a

@[simp]

theorem Bool.not_xor_and_self {a : Bool} {b : Bool} : (!(a ^^ b) && b) = (a && b)

theorem Bool.xor_inv_left {a : Bool} {b : Bool} {c : Bool} : (a ^^ b) = c ↔ b = (a ^^ c)

@[simp]

theorem Bool.xor_ne_self {a : Bool} {b : Bool} : (a ^^ (!a) != b) = !b

@[simp]

theorem Bool.not_eq_and {a : Bool} {b : Bool} : ((!b) == (a && b)) = (!a && b)

@[simp]

theorem Bool.not_bne' {a : Bool} {b : Bool} : (!a != b) = (a == b)