theorem USize.toBitVec32_eq_toBitVec (a : USize) (h : System.Platform.numBits = 32) : a.toBitVec32 h = BitVec.cast h a.toBitVec

theorem USize.toBitVec64_eq_toBitVec (a : USize) (h : System.Platform.numBits = 64) : a.toBitVec64 h = BitVec.cast h a.toBitVec

numBits = 32

theorem USize.le_iff_toBitVec32_le {a b : USize} (h : System.Platform.numBits = 32) : a ≤ b ↔ a.toBitVec32 h ≤ b.toBitVec32 h

theorem USize.lt_iff_toBitVec32_lt {a b : USize} (h : System.Platform.numBits = 32) : a < b ↔ a.toBitVec32 h < b.toBitVec32 h

theorem USize.eq_iff_toBitVec32_eq {a b : USize} (h : System.Platform.numBits = 32) : a = b ↔ a.toBitVec32 h = b.toBitVec32 h

theorem USize.ne_iff_toBitVec32_ne {a b : USize} (h : System.Platform.numBits = 32) : a ≠ b ↔ a.toBitVec32 h ≠ b.toBitVec32 h

theorem USize.toBitVec32_ofNat (n : Nat) (h : System.Platform.numBits = 32) : (OfNat.ofNat n).toBitVec32 h = BitVec.ofNat 32 n

theorem USize.toBitVec32_add {a b : USize} (h : System.Platform.numBits = 32) : (a + b).toBitVec32 h = a.toBitVec32 h + b.toBitVec32 h

theorem USize.toBitVec32_sub {a b : USize} (h : System.Platform.numBits = 32) : (a - b).toBitVec32 h = a.toBitVec32 h - b.toBitVec32 h

theorem USize.toBitVec32_mul {a b : USize} (h : System.Platform.numBits = 32) : (a * b).toBitVec32 h = a.toBitVec32 h * b.toBitVec32 h

theorem USize.toBitVec32_div {a b : USize} (h : System.Platform.numBits = 32) : (a / b).toBitVec32 h = a.toBitVec32 h / b.toBitVec32 h

theorem USize.toBitVec32_mod {a b : USize} (h : System.Platform.numBits = 32) : (a % b).toBitVec32 h = a.toBitVec32 h % b.toBitVec32 h

theorem USize.toBitVec32_neg {a : USize} (h : System.Platform.numBits = 32) : (-a).toBitVec32 h = -a.toBitVec32 h

theorem USize.toBitVec32_not {a : USize} (h : System.Platform.numBits = 32) : (~~~a).toBitVec32 h = ~~~a.toBitVec32 h

theorem USize.toBitVec32_and (a b : USize) (h : System.Platform.numBits = 32) : (a &&& b).toBitVec32 h = a.toBitVec32 h &&& b.toBitVec32 h

theorem USize.toBitVec32_or (a b : USize) (h : System.Platform.numBits = 32) : (a ||| b).toBitVec32 h = a.toBitVec32 h ||| b.toBitVec32 h

theorem USize.toBitVec32_xor (a b : USize) (h : System.Platform.numBits = 32) : (a ^^^ b).toBitVec32 h = a.toBitVec32 h ^^^ b.toBitVec32 h

theorem USize.toBitVec32_shiftLeft (a b : USize) (h : System.Platform.numBits = 32) : (a <<< b).toBitVec32 h = a.toBitVec32 h <<< (b.toBitVec32 h % 32)

theorem USize.toBitVec32_shiftRight (a b : USize) (h : System.Platform.numBits = 32) : (a >>> b).toBitVec32 h = a.toBitVec32 h >>> (b.toBitVec32 h % 32)

theorem USize.toBitVec32_toUInt8 (n : USize) (h : System.Platform.numBits = 32) : n.toUInt8.toBitVec = BitVec.setWidth 8 (n.toBitVec32 h)

theorem USize.toBitVec32_toUInt16 (n : USize) (h : System.Platform.numBits = 32) : n.toUInt16.toBitVec = BitVec.setWidth 16 (n.toBitVec32 h)

theorem USize.toBitVec32_toUInt32 (n : USize) (h : System.Platform.numBits = 32) : n.toUInt32.toBitVec = BitVec.setWidth 32 (n.toBitVec32 h)

theorem USize.toBitVec32_toUInt64 (n : USize) (h : System.Platform.numBits = 32) : n.toUInt64.toBitVec = BitVec.setWidth 64 (n.toBitVec32 h)

theorem UInt8.toBitVec32_toUSize (n : UInt8) (h : System.Platform.numBits = 32) : n.toUSize.toBitVec32 h = BitVec.setWidth 32 n.toBitVec

theorem UInt16.toBitVec32_toUSize (n : UInt16) (h : System.Platform.numBits = 32) : n.toUSize.toBitVec32 h = BitVec.setWidth 32 n.toBitVec

theorem UInt32.toBitVec32_toUSize (n : UInt32) (h : System.Platform.numBits = 32) : n.toUSize.toBitVec32 h = n.toBitVec

theorem UInt64.toBitVec32_toUSize (n : UInt64) (h : System.Platform.numBits = 32) : n.toUSize.toBitVec32 h = BitVec.setWidth 32 n.toBitVec

theorem USize.toBitVec32_ofNatLT {n : Nat} (hn : n < size) (h : System.Platform.numBits = 32) : (ofNatLT n hn).toBitVec32 h = n#'⋯

theorem USize.toBitVec32_ofFin (n : Fin size) (h : System.Platform.numBits = 32) : (ofFin n).toBitVec32 h = { toFin := h ▸ n }

theorem USize.toBitVec32_ofBitVec (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 32) : { toBitVec := n }.toBitVec32 h = BitVec.cast h n

theorem USize.toBitVec32_pow (a : USize) (n : Nat) (h : System.Platform.numBits = 32) : (a ^ n).toBitVec32 h = a.toBitVec32 h ^ n

theorem Bool.toBitVec32_toUSize {b : Bool} (h : System.Platform.numBits = 32) : b.toUSize.toBitVec32 h = BitVec.setWidth 32 (BitVec.ofBool b)

numBits = 64

theorem USize.le_iff_toBitVec64_le {a b : USize} (h : System.Platform.numBits = 64) : a ≤ b ↔ a.toBitVec64 h ≤ b.toBitVec64 h

theorem USize.lt_iff_toBitVec64_lt {a b : USize} (h : System.Platform.numBits = 64) : a < b ↔ a.toBitVec64 h < b.toBitVec64 h

theorem USize.eq_iff_toBitVec64_eq {a b : USize} (h : System.Platform.numBits = 64) : a = b ↔ a.toBitVec64 h = b.toBitVec64 h

theorem USize.ne_iff_toBitVec64_ne {a b : USize} (h : System.Platform.numBits = 64) : a ≠ b ↔ a.toBitVec64 h ≠ b.toBitVec64 h

theorem USize.toBitVec64_ofNat (n : Nat) (h : System.Platform.numBits = 64) : (OfNat.ofNat n).toBitVec64 h = BitVec.ofNat 64 n

theorem USize.toBitVec64_add {a b : USize} (h : System.Platform.numBits = 64) : (a + b).toBitVec64 h = a.toBitVec64 h + b.toBitVec64 h

theorem USize.toBitVec64_sub {a b : USize} (h : System.Platform.numBits = 64) : (a - b).toBitVec64 h = a.toBitVec64 h - b.toBitVec64 h

theorem USize.toBitVec64_mul {a b : USize} (h : System.Platform.numBits = 64) : (a * b).toBitVec64 h = a.toBitVec64 h * b.toBitVec64 h

theorem USize.toBitVec64_div {a b : USize} (h : System.Platform.numBits = 64) : (a / b).toBitVec64 h = a.toBitVec64 h / b.toBitVec64 h

theorem USize.toBitVec64_mod {a b : USize} (h : System.Platform.numBits = 64) : (a % b).toBitVec64 h = a.toBitVec64 h % b.toBitVec64 h

theorem USize.toBitVec64_neg {a : USize} (h : System.Platform.numBits = 64) : (-a).toBitVec64 h = -a.toBitVec64 h

theorem USize.toBitVec64_not {a : USize} (h : System.Platform.numBits = 64) : (~~~a).toBitVec64 h = ~~~a.toBitVec64 h

theorem USize.toBitVec64_and (a b : USize) (h : System.Platform.numBits = 64) : (a &&& b).toBitVec64 h = a.toBitVec64 h &&& b.toBitVec64 h

theorem USize.toBitVec64_or (a b : USize) (h : System.Platform.numBits = 64) : (a ||| b).toBitVec64 h = a.toBitVec64 h ||| b.toBitVec64 h

theorem USize.toBitVec64_xor (a b : USize) (h : System.Platform.numBits = 64) : (a ^^^ b).toBitVec64 h = a.toBitVec64 h ^^^ b.toBitVec64 h

theorem USize.toBitVec64_shiftLeft (a b : USize) (h : System.Platform.numBits = 64) : (a <<< b).toBitVec64 h = a.toBitVec64 h <<< (b.toBitVec64 h % 64)

theorem USize.toBitVec64_shiftRight (a b : USize) (h : System.Platform.numBits = 64) : (a >>> b).toBitVec64 h = a.toBitVec64 h >>> (b.toBitVec64 h % 64)

theorem USize.toBitVec64_toUInt8 (n : USize) (h : System.Platform.numBits = 64) : n.toUInt8.toBitVec = BitVec.setWidth 8 (n.toBitVec64 h)

theorem USize.toBitVec64_toUInt16 (n : USize) (h : System.Platform.numBits = 64) : n.toUInt16.toBitVec = BitVec.setWidth 16 (n.toBitVec64 h)

theorem USize.toBitVec64_toUInt32 (n : USize) (h : System.Platform.numBits = 64) : n.toUInt32.toBitVec = BitVec.setWidth 32 (n.toBitVec64 h)

theorem USize.toBitVec64_toUInt64 (n : USize) (h : System.Platform.numBits = 64) : n.toUInt64.toBitVec = BitVec.setWidth 64 (n.toBitVec64 h)

theorem UInt8.toBitVec64_toUSize (n : UInt8) (h : System.Platform.numBits = 64) : n.toUSize.toBitVec64 h = BitVec.setWidth 64 n.toBitVec

theorem UInt16.toBitVec64_toUSize (n : UInt16) (h : System.Platform.numBits = 64) : n.toUSize.toBitVec64 h = BitVec.setWidth 64 n.toBitVec

theorem UInt32.toBitVec64_toUSize (n : UInt32) (h : System.Platform.numBits = 64) : n.toUSize.toBitVec64 h = BitVec.setWidth 64 n.toBitVec

theorem UInt64.toBitVec64_toUSize (n : UInt64) (h : System.Platform.numBits = 64) : n.toUSize.toBitVec64 h = n.toBitVec

theorem USize.toBitVec64_ofNatLT {n : Nat} (hn : n < size) (h : System.Platform.numBits = 64) : (ofNatLT n hn).toBitVec64 h = n#'⋯

theorem USize.toBitVec64_ofFin (n : Fin size) (h : System.Platform.numBits = 64) : (ofFin n).toBitVec64 h = { toFin := h ▸ n }

theorem USize.toBitVec64_ofBitVec (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 64) : { toBitVec := n }.toBitVec64 h = BitVec.cast h n

theorem USize.toBitVec64_pow (a : USize) (n : Nat) (h : System.Platform.numBits = 64) : (a ^ n).toBitVec64 h = a.toBitVec64 h ^ n

theorem Bool.toBitVec64_toUSize {b : Bool} (h : System.Platform.numBits = 64) : b.toUSize.toBitVec64 h = BitVec.setWidth 64 (BitVec.ofBool b)