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

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

numBits = 32

theorem ISize.le_iff_toBitVec32_sle {a b : ISize} (h : System.Platform.numBits = 32) : a ≤ b ↔ (a.toBitVec32 h).sle (b.toBitVec32 h) = true

theorem ISize.lt_iff_toBitVec32_slt {a b : ISize} (h : System.Platform.numBits = 32) : a < b ↔ (a.toBitVec32 h).slt (b.toBitVec32 h) = true

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

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

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

theorem ISize.toBitVec32_ofInt (i : Int) (h : System.Platform.numBits = 32) : (ofInt i).toBitVec32 h = BitVec.ofInt 32 i

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

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

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

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

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

theorem ISize.toBitVec32_min {a b : ISize} (h : System.Platform.numBits = 32) : (min a b).toBitVec32 h = if (a.toBitVec32 h).sle (b.toBitVec32 h) = true then a.toBitVec32 h else b.toBitVec32 h

theorem ISize.toBitVec32_max {a b : ISize} (h : System.Platform.numBits = 32) : (max a b).toBitVec32 h = if (a.toBitVec32 h).sle (b.toBitVec32 h) = true then b.toBitVec32 h else a.toBitVec32 h

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

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

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

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

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

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

theorem ISize.toBitVec32_shiftRight (a b : ISize) (h : System.Platform.numBits = 32) : (a >>> b).toBitVec32 h = (a.toBitVec32 h).sshiftRight' ((b.toBitVec32 h).smod 32)

theorem ISize.toBitVec32_abs (a : ISize) (h : System.Platform.numBits = 32) : a.abs.toBitVec32 h = (a.toBitVec32 h).abs

theorem ISize.toBitVec32_toInt8 (n : ISize) (h : System.Platform.numBits = 32) : n.toInt8.toBitVec = BitVec.signExtend 8 (n.toBitVec32 h)

theorem ISize.toBitVec32_toInt16 (n : ISize) (h : System.Platform.numBits = 32) : n.toInt16.toBitVec = BitVec.signExtend 16 (n.toBitVec32 h)

theorem ISize.toBitVec32_toInt32 (n : ISize) (h : System.Platform.numBits = 32) : n.toInt32.toBitVec = BitVec.signExtend 32 (n.toBitVec32 h)

theorem ISize.toBitVec32_toInt64 (n : ISize) (h : System.Platform.numBits = 32) : n.toInt64.toBitVec = BitVec.signExtend 64 (n.toBitVec32 h)

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

theorem USize.toBitVec32_toISize (n : USize) (h : System.Platform.numBits = 32) : n.toISize.toBitVec32 h = n.toBitVec32 h

theorem Int8.toBitVec32_toISize (n : Int8) (h : System.Platform.numBits = 32) : n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec

theorem Int16.toBitVec32_toISize (n : Int16) (h : System.Platform.numBits = 32) : n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec

theorem Int32.toBitVec32_toISize (n : Int32) (h : System.Platform.numBits = 32) : n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec

theorem Int64.toBitVec32_toISize (n : Int64) (h : System.Platform.numBits = 32) : n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec

theorem ISize.toBitVec32_ofBitVec (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 32) : (ofBitVec n).toBitVec32 h = BitVec.cast h n

theorem ISize.toBitVec32_minValue (h : System.Platform.numBits = 32) : minValue.toBitVec32 h = BitVec.intMin 32

theorem ISize.toBitVec32_maxValue (h : System.Platform.numBits = 32) : maxValue.toBitVec32 h = BitVec.intMax 32

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

numBits = 64

theorem ISize.le_iff_toBitVec64_sle {a b : ISize} (h : System.Platform.numBits = 64) : a ≤ b ↔ (a.toBitVec64 h).sle (b.toBitVec64 h) = true

theorem ISize.lt_iff_toBitVec64_slt {a b : ISize} (h : System.Platform.numBits = 64) : a < b ↔ (a.toBitVec64 h).slt (b.toBitVec64 h) = true

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

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

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

theorem ISize.toBitVec64_ofInt (i : Int) (h : System.Platform.numBits = 64) : (ofInt i).toBitVec64 h = BitVec.ofInt 64 i

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

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

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

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

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

theorem ISize.toBitVec64_min {a b : ISize} (h : System.Platform.numBits = 64) : (min a b).toBitVec64 h = if (a.toBitVec64 h).sle (b.toBitVec64 h) = true then a.toBitVec64 h else b.toBitVec64 h

theorem ISize.toBitVec64_max {a b : ISize} (h : System.Platform.numBits = 64) : (max a b).toBitVec64 h = if (a.toBitVec64 h).sle (b.toBitVec64 h) = true then b.toBitVec64 h else a.toBitVec64 h

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

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

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

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

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

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

theorem ISize.toBitVec64_shiftRight (a b : ISize) (h : System.Platform.numBits = 64) : (a >>> b).toBitVec64 h = (a.toBitVec64 h).sshiftRight' ((b.toBitVec64 h).smod 64)

theorem ISize.toBitVec64_abs (a : ISize) (h : System.Platform.numBits = 64) : a.abs.toBitVec64 h = (a.toBitVec64 h).abs

theorem ISize.toBitVec64_toInt8 (n : ISize) (h : System.Platform.numBits = 64) : n.toInt8.toBitVec = BitVec.signExtend 8 (n.toBitVec64 h)

theorem ISize.toBitVec64_toInt16 (n : ISize) (h : System.Platform.numBits = 64) : n.toInt16.toBitVec = BitVec.signExtend 16 (n.toBitVec64 h)

theorem ISize.toBitVec64_toInt32 (n : ISize) (h : System.Platform.numBits = 64) : n.toInt32.toBitVec = BitVec.signExtend 32 (n.toBitVec64 h)

theorem ISize.toBitVec64_toInt64 (n : ISize) (h : System.Platform.numBits = 64) : n.toInt64.toBitVec = BitVec.signExtend 64 (n.toBitVec64 h)

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

theorem USize.toBitVec64_toISize (n : USize) (h : System.Platform.numBits = 64) : n.toISize.toBitVec64 h = n.toBitVec64 h

theorem Int8.toBitVec64_toISize (n : Int8) (h : System.Platform.numBits = 64) : n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec

theorem Int16.toBitVec64_toISize (n : Int16) (h : System.Platform.numBits = 64) : n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec

theorem Int32.toBitVec64_toISize (n : Int32) (h : System.Platform.numBits = 64) : n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec

theorem Int64.toBitVec64_toISize (n : Int64) (h : System.Platform.numBits = 64) : n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec

theorem ISize.toBitVec64_ofBitVec (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 64) : (ofBitVec n).toBitVec64 h = BitVec.cast h n

theorem ISize.toBitVec64_minValue (h : System.Platform.numBits = 64) : minValue.toBitVec64 h = BitVec.intMin 64

theorem ISize.toBitVec64_maxValue (h : System.Platform.numBits = 64) : maxValue.toBitVec64 h = BitVec.intMax 64

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