This module contains the BitVec simplifying part of the bv_normalize simp set.

theorem Std.Tactic.BVDecide.Normalize.BitVec.le_ult {w : Nat} (x : BitVec w) (y : BitVec w) : (x ≤ y) = ¬y < x

theorem Std.Tactic.BVDecide.Normalize.BitVec.truncate_eq_zeroExtend {w : Nat} {n : Nat} (x : BitVec w) : BitVec.truncate n x = BitVec.zeroExtend n x

theorem Std.Tactic.BVDecide.Normalize.BitVec.ofNatLt_reduce {w : Nat} (n : Nat) (h : n < 2 ^ w) : n#'h = BitVec.ofNat w n

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_and {w : Nat} (a : BitVec w) : 0#w &&& a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_zero {w : Nat} (a : BitVec w) : a &&& 0#w = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.ones_and {w : Nat} (a : BitVec w) : -1#w &&& a = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_ones {w : Nat} (a : BitVec w) : a &&& -1#w = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_self {w : Nat} (a : BitVec w) : a &&& a = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_contra {w : Nat} (a : BitVec w) : a &&& ~~~a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_contra' {w : Nat} (a : BitVec w) : ~~~a &&& a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_not {w : Nat} (a : BitVec w) : a + ~~~a = -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_add {w : Nat} (a : BitVec w) : ~~~a + a = -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg {w : Nat} (a : BitVec w) : a + (~~~a + 1#w) = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg' {w : Nat} (a : BitVec w) : a + (1#w + ~~~a) = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.neg_add {w : Nat} (a : BitVec w) : ~~~a + 1#w + a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.neg_add' {w : Nat} (a : BitVec w) : 1#w + ~~~a + a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg {w : Nat} (x : BitVec w) : ~~~(~~~x + 1#w) = x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg' {w : Nat} (x : BitVec w) : ~~~(1#w + ~~~x) = x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg'' {w : Nat} (x : BitVec w) : ~~~(x + 1#w) = ~~~x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg''' {w : Nat} (x : BitVec w) : ~~~(1#w + x) = ~~~x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_same {w : Nat} (a : BitVec w) : a + a = a * 2#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_left {w : Nat} (a : BitVec w) (b : BitVec w) (c : BitVec w) : a + (b + c) = a + b + c

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right {w : Nat} (a : BitVec w) (b : BitVec w) (c : BitVec w) : a + (b + c) = a + c + b

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_left' {w : Nat} (a : BitVec w) (b : BitVec w) (c : BitVec w) : a + b + c = a + c + b

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right' {w : Nat} (a : BitVec w) (b : BitVec w) (c : BitVec w) : a + b + c = b + c + a

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_sshiftRight {w : Nat} {a : Nat} : (0#w).sshiftRight a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.sshiftRight_zero : ∀ {w : Nat} {a : BitVec w}, a.sshiftRight 0 = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_zero {w : Nat} (a : BitVec w) : a * 0#w = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_mul {w : Nat} (a : BitVec w) : 0#w * a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_zero {w : Nat} {w' : Nat} (n : BitVec w) : n <<< 0#w' = n

theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_zero' {w : Nat} (n : BitVec w) : n <<< 0 = n

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_shiftLeft {w : Nat} (n : Nat) : 0#w <<< n = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_shiftRight {w : Nat} (n : Nat) : 0#w >>> n = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftRight_zero {w : Nat} {w' : Nat} (n : BitVec w) : n >>> 0#w' = n

theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftRight_zero' {w : Nat} (n : BitVec w) : n >>> 0 = n

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_lt_iff_zero_neq {w : Nat} (a : BitVec w) : 0#w < a ↔ a ≠ 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_ult' {w : Nat} (a : BitVec w) : (0#w).ult a = (a != 0#w)

theorem Std.Tactic.BVDecide.Normalize.BitVec.max_ult {w : Nat} (a : BitVec w) : ¬-1#w < a

theorem Std.Tactic.BVDecide.Normalize.BitVec.max_ult' {w : Nat} (a : BitVec w) : (-1#w).ult a = false

theorem Std.Tactic.BVDecide.Normalize.BitVec.ofBool_getLsbD {w : Nat} (a : BitVec w) (i : Nat) : BitVec.ofBool (a.getLsbD i) = BitVec.extractLsb' i 1 a

theorem Std.Tactic.BVDecide.Normalize.BitVec.getElem_eq_getLsbD {w : Nat} (a : BitVec w) (i : Nat) (h : i < w) : a[i] = a.getLsbD i