def commandDeclare_bitwise_uint_theorems__ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UInt8.toNat_shiftRight (a b : UInt8) : (a >>> b).toNat = a.toNat >>> (b.toNat % 8)

@[simp]

theorem UInt8.toBitVec_or (a b : UInt8) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec

@[deprecated UInt8.toNat_and (since := "2024-11-28")]

theorem UInt8.and_toNat (a b : UInt8) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt8.toNat_xor (a b : UInt8) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat

@[simp]

theorem UInt8.toBitVec_and (a b : UInt8) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec

@[simp]

theorem UInt8.toNat_or (a b : UInt8) : (a ||| b).toNat = a.toNat ||| b.toNat

@[simp]

theorem UInt8.toNat_and (a b : UInt8) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt8.toBitVec_not {a : UInt8} : (~~~a).toBitVec = ~~~a.toBitVec

@[simp]

theorem UInt8.toNat_shiftLeft (a b : UInt8) : (a <<< b).toNat = a.toNat <<< (b.toNat % 8) % 2 ^ 8

@[simp]

theorem UInt8.toBitVec_xor (a b : UInt8) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec

@[simp]

theorem UInt8.toBitVec_shiftRight (a b : UInt8) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 8)

@[simp]

theorem UInt8.toBitVec_shiftLeft (a b : UInt8) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 8)

@[simp]

theorem UInt16.toNat_xor (a b : UInt16) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat

@[simp]

theorem UInt16.toNat_shiftRight (a b : UInt16) : (a >>> b).toNat = a.toNat >>> (b.toNat % 16)

@[simp]

theorem UInt16.toNat_or (a b : UInt16) : (a ||| b).toNat = a.toNat ||| b.toNat

@[simp]

theorem UInt16.toBitVec_or (a b : UInt16) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec

@[simp]

theorem UInt16.toBitVec_shiftLeft (a b : UInt16) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 16)

@[simp]

theorem UInt16.toBitVec_and (a b : UInt16) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec

@[simp]

theorem UInt16.toBitVec_shiftRight (a b : UInt16) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 16)

@[simp]

theorem UInt16.toBitVec_not {a : UInt16} : (~~~a).toBitVec = ~~~a.toBitVec

@[deprecated UInt16.toNat_and (since := "2024-11-28")]

theorem UInt16.and_toNat (a b : UInt16) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt16.toBitVec_xor (a b : UInt16) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec

@[simp]

theorem UInt16.toNat_and (a b : UInt16) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt16.toNat_shiftLeft (a b : UInt16) : (a <<< b).toNat = a.toNat <<< (b.toNat % 16) % 2 ^ 16

@[simp]

theorem UInt32.toBitVec_not {a : UInt32} : (~~~a).toBitVec = ~~~a.toBitVec

@[simp]

theorem UInt32.toNat_or (a b : UInt32) : (a ||| b).toNat = a.toNat ||| b.toNat

@[simp]

theorem UInt32.toNat_shiftLeft (a b : UInt32) : (a <<< b).toNat = a.toNat <<< (b.toNat % 32) % 2 ^ 32

@[simp]

theorem UInt32.toNat_xor (a b : UInt32) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat

@[simp]

theorem UInt32.toBitVec_xor (a b : UInt32) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec

@[simp]

theorem UInt32.toBitVec_shiftRight (a b : UInt32) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 32)

@[simp]

theorem UInt32.toBitVec_and (a b : UInt32) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec

@[simp]

theorem UInt32.toBitVec_shiftLeft (a b : UInt32) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 32)

@[simp]

theorem UInt32.toBitVec_or (a b : UInt32) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec

@[simp]

theorem UInt32.toNat_shiftRight (a b : UInt32) : (a >>> b).toNat = a.toNat >>> (b.toNat % 32)

@[deprecated UInt32.toNat_and (since := "2024-11-28")]

theorem UInt32.and_toNat (a b : UInt32) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt32.toNat_and (a b : UInt32) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt64.toBitVec_and (a b : UInt64) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec

@[simp]

theorem UInt64.toNat_xor (a b : UInt64) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat

@[simp]

theorem UInt64.toNat_or (a b : UInt64) : (a ||| b).toNat = a.toNat ||| b.toNat

@[simp]

theorem UInt64.toBitVec_shiftLeft (a b : UInt64) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 64)

@[simp]

theorem UInt64.toNat_and (a b : UInt64) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt64.toBitVec_not {a : UInt64} : (~~~a).toBitVec = ~~~a.toBitVec

@[simp]

theorem UInt64.toBitVec_shiftRight (a b : UInt64) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 64)

@[simp]

theorem UInt64.toBitVec_or (a b : UInt64) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec

@[deprecated UInt64.toNat_and (since := "2024-11-28")]

theorem UInt64.and_toNat (a b : UInt64) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt64.toNat_shiftRight (a b : UInt64) : (a >>> b).toNat = a.toNat >>> (b.toNat % 64)

@[simp]

theorem UInt64.toBitVec_xor (a b : UInt64) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec

@[simp]

theorem UInt64.toNat_shiftLeft (a b : UInt64) : (a <<< b).toNat = a.toNat <<< (b.toNat % 64) % 2 ^ 64

@[simp]

theorem USize.toBitVec_and (a b : USize) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec

@[simp]

theorem USize.toNat_and (a b : USize) : (a &&& b).toNat = a.toNat &&& b.toNat

@[deprecated USize.toNat_and (since := "2024-11-28")]

theorem USize.and_toNat (a b : USize) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem USize.toBitVec_xor (a b : USize) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec

@[simp]

theorem USize.toNat_shiftRight (a b : USize) : (a >>> b).toNat = a.toNat >>> (b.toNat % System.Platform.numBits)

@[simp]

theorem USize.toBitVec_shiftRight (a b : USize) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % ↑System.Platform.numBits)

@[simp]

theorem USize.toNat_or (a b : USize) : (a ||| b).toNat = a.toNat ||| b.toNat

@[simp]

theorem USize.toBitVec_or (a b : USize) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec

@[simp]

theorem USize.toNat_xor (a b : USize) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat

@[simp]

theorem USize.toNat_shiftLeft (a b : USize) : (a <<< b).toNat = a.toNat <<< (b.toNat % System.Platform.numBits) % 2 ^ System.Platform.numBits

@[simp]

theorem USize.toBitVec_not {a : USize} : (~~~a).toBitVec = ~~~a.toBitVec

@[simp]

theorem USize.toBitVec_shiftLeft (a b : USize) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % ↑System.Platform.numBits)

@[simp]

theorem Bool.toBitVec_toUInt8 {b : Bool} : b.toUInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)

@[simp]

theorem Bool.toBitVec_toUInt16 {b : Bool} : b.toUInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)

@[simp]

theorem Bool.toBitVec_toUInt32 {b : Bool} : b.toUInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)

@[simp]

theorem Bool.toBitVec_toUInt64 {b : Bool} : b.toUInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)

@[simp]

theorem Bool.toBitVec_toUSize {b : Bool} : b.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)

@[simp]

theorem UInt8.toFin_and (a b : UInt8) : (a &&& b).toFin = a.toFin &&& b.toFin

@[simp]

theorem UInt16.toFin_and (a b : UInt16) : (a &&& b).toFin = a.toFin &&& b.toFin

@[simp]

theorem UInt32.toFin_and (a b : UInt32) : (a &&& b).toFin = a.toFin &&& b.toFin

@[simp]

theorem UInt64.toFin_and (a b : UInt64) : (a &&& b).toFin = a.toFin &&& b.toFin

@[simp]

theorem USize.toFin_and (a b : USize) : (a &&& b).toFin = a.toFin &&& b.toFin

@[simp]

theorem UInt8.toUInt16_and (a b : UInt8) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16

@[simp]

theorem UInt8.toUInt32_and (a b : UInt8) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32

@[simp]

theorem UInt8.toUInt64_and (a b : UInt8) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64

@[simp]

theorem UInt8.toUSize_and (a b : UInt8) : (a &&& b).toUSize = a.toUSize &&& b.toUSize

@[simp]

theorem UInt16.toUInt8_and (a b : UInt16) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8

@[simp]

theorem UInt16.toUInt32_and (a b : UInt16) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32

@[simp]

theorem UInt16.toUInt64_and (a b : UInt16) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64

@[simp]

theorem UInt16.toUSize_and (a b : UInt16) : (a &&& b).toUSize = a.toUSize &&& b.toUSize

@[simp]

theorem UInt32.toUInt8_and (a b : UInt32) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8

@[simp]

theorem UInt32.toUInt16_and (a b : UInt32) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16

@[simp]

theorem UInt32.toUInt64_and (a b : UInt32) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64

@[simp]

theorem UInt32.toUSize_and (a b : UInt32) : (a &&& b).toUSize = a.toUSize &&& b.toUSize

@[simp]

theorem USize.toUInt8_and (a b : USize) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8

@[simp]

theorem USize.toUInt16_and (a b : USize) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16

@[simp]

theorem USize.toUInt32_and (a b : USize) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32

@[simp]

theorem USize.toUInt64_and (a b : USize) : (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64

@[simp]

theorem UInt64.toUInt8_and (a b : UInt64) : (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8

@[simp]

theorem UInt64.toUInt16_and (a b : UInt64) : (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16

@[simp]

theorem UInt64.toUInt32_and (a b : UInt64) : (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32

@[simp]

theorem UInt64.toUSize_and (a b : UInt64) : (a &&& b).toUSize = a.toUSize &&& b.toUSize

@[simp]

theorem UInt8.toFin_or (a b : UInt8) : (a ||| b).toFin = a.toFin ||| b.toFin

@[simp]

theorem UInt16.toFin_or (a b : UInt16) : (a ||| b).toFin = a.toFin ||| b.toFin

@[simp]

theorem UInt32.toFin_or (a b : UInt32) : (a ||| b).toFin = a.toFin ||| b.toFin

@[simp]

theorem UInt64.toFin_or (a b : UInt64) : (a ||| b).toFin = a.toFin ||| b.toFin

@[simp]

theorem USize.toFin_or (a b : USize) : (a ||| b).toFin = a.toFin ||| b.toFin

@[simp]

theorem UInt8.toUInt16_or (a b : UInt8) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16

@[simp]

theorem UInt8.toUInt32_or (a b : UInt8) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32

@[simp]

theorem UInt8.toUInt64_or (a b : UInt8) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64

@[simp]

theorem UInt8.toUSize_or (a b : UInt8) : (a ||| b).toUSize = a.toUSize ||| b.toUSize

@[simp]

theorem UInt16.toUInt8_or (a b : UInt16) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8

@[simp]

theorem UInt16.toUInt32_or (a b : UInt16) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32

@[simp]

theorem UInt16.toUInt64_or (a b : UInt16) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64

@[simp]

theorem UInt16.toUSize_or (a b : UInt16) : (a ||| b).toUSize = a.toUSize ||| b.toUSize

@[simp]

theorem UInt32.toUInt8_or (a b : UInt32) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8

@[simp]

theorem UInt32.toUInt16_or (a b : UInt32) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16

@[simp]

theorem UInt32.toUInt64_or (a b : UInt32) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64

@[simp]

theorem UInt32.toUSize_or (a b : UInt32) : (a ||| b).toUSize = a.toUSize ||| b.toUSize

@[simp]

theorem USize.toUInt8_or (a b : USize) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8

@[simp]

theorem USize.toUInt16_or (a b : USize) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16

@[simp]

theorem USize.toUInt32_or (a b : USize) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32

@[simp]

theorem USize.toUInt64_or (a b : USize) : (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64

@[simp]

theorem UInt64.toUInt8_or (a b : UInt64) : (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8

@[simp]

theorem UInt64.toUInt16_or (a b : UInt64) : (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16

@[simp]

theorem UInt64.toUInt32_or (a b : UInt64) : (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32

@[simp]

theorem UInt64.toUSize_or (a b : UInt64) : (a ||| b).toUSize = a.toUSize ||| b.toUSize

@[simp]

theorem UInt8.toFin_xor (a b : UInt8) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin

@[simp]

theorem UInt16.toFin_xor (a b : UInt16) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin

@[simp]

theorem UInt32.toFin_xor (a b : UInt32) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin

@[simp]

theorem UInt64.toFin_xor (a b : UInt64) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin

@[simp]

theorem USize.toFin_xor (a b : USize) : (a ^^^ b).toFin = a.toFin ^^^ b.toFin

@[simp]

theorem UInt8.toUInt16_xor (a b : UInt8) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16

@[simp]

theorem UInt8.toUInt32_xor (a b : UInt8) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32

@[simp]

theorem UInt8.toUInt64_xor (a b : UInt8) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64

@[simp]

theorem UInt8.toUSize_xor (a b : UInt8) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize

@[simp]

theorem UInt16.toUInt8_xor (a b : UInt16) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8

@[simp]

theorem UInt16.toUInt32_xor (a b : UInt16) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32

@[simp]

theorem UInt16.toUInt64_xor (a b : UInt16) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64

@[simp]

theorem UInt16.toUSize_xor (a b : UInt16) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize

@[simp]

theorem UInt32.toUInt8_xor (a b : UInt32) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8

@[simp]

theorem UInt32.toUInt16_xor (a b : UInt32) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16

@[simp]

theorem UInt32.toUInt64_xor (a b : UInt32) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64

@[simp]

theorem UInt32.toUSize_xor (a b : UInt32) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize

@[simp]

theorem USize.toUInt8_xor (a b : USize) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8

@[simp]

theorem USize.toUInt16_xor (a b : USize) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16

@[simp]

theorem USize.toUInt32_xor (a b : USize) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32

@[simp]

theorem USize.toUInt64_xor (a b : USize) : (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64

@[simp]

theorem UInt64.toUInt8_xor (a b : UInt64) : (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8

@[simp]

theorem UInt64.toUInt16_xor (a b : UInt64) : (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16

@[simp]

theorem UInt64.toUInt32_xor (a b : UInt64) : (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32

@[simp]

theorem UInt64.toUSize_xor (a b : UInt64) : (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize

@[simp]

theorem UInt8.toNat_not (a : UInt8) : (~~~a).toNat = size - 1 - a.toNat

@[simp]

theorem UInt16.toNat_not (a : UInt16) : (~~~a).toNat = size - 1 - a.toNat

@[simp]

theorem UInt32.toNat_not (a : UInt32) : (~~~a).toNat = size - 1 - a.toNat

@[simp]

theorem UInt64.toNat_not (a : UInt64) : (~~~a).toNat = size - 1 - a.toNat

@[simp]

theorem USize.toNat_not (a : USize) : (~~~a).toNat = size - 1 - a.toNat

@[simp]

theorem UInt8.toFin_not (a : UInt8) : (~~~a).toFin = a.toFin.rev

@[simp]

theorem UInt16.toFin_not (a : UInt16) : (~~~a).toFin = a.toFin.rev

@[simp]

theorem UInt32.toFin_not (a : UInt32) : (~~~a).toFin = a.toFin.rev

@[simp]

theorem UInt64.toFin_not (a : UInt64) : (~~~a).toFin = a.toFin.rev

@[simp]

theorem USize.toFin_not (a : USize) : (~~~a).toFin = a.toFin.rev

@[simp]

theorem UInt16.toUInt8_not (a : UInt16) : (~~~a).toUInt8 = ~~~a.toUInt8

@[simp]

theorem UInt32.toUInt8_not (a : UInt32) : (~~~a).toUInt8 = ~~~a.toUInt8

@[simp]

theorem UInt64.toUInt8_not (a : UInt64) : (~~~a).toUInt8 = ~~~a.toUInt8

@[simp]

theorem USize.toUInt8_not (a : USize) : (~~~a).toUInt8 = ~~~a.toUInt8

@[simp]

theorem UInt32.toUInt16_not (a : UInt32) : (~~~a).toUInt16 = ~~~a.toUInt16

@[simp]

theorem UInt64.toUInt16_not (a : UInt64) : (~~~a).toUInt16 = ~~~a.toUInt16

@[simp]

theorem USize.toUInt16_not (a : USize) : (~~~a).toUInt16 = ~~~a.toUInt16

@[simp]

theorem UInt64.toUInt32_not (a : UInt64) : (~~~a).toUInt32 = ~~~a.toUInt32

@[simp]

theorem USize.toUInt32_not (a : USize) : (~~~a).toUInt32 = ~~~a.toUInt32

@[simp]

theorem UInt64.toUSize_not (a : UInt64) : (~~~a).toUSize = ~~~a.toUSize

@[simp]

theorem UInt8.toUInt16_not (a : UInt8) : (~~~a).toUInt16 = ~~~a.toUInt16 % 256

@[simp]

theorem UInt8.toUInt32_not (a : UInt8) : (~~~a).toUInt32 = ~~~a.toUInt32 % 256

@[simp]

theorem UInt8.toUInt64_not (a : UInt8) : (~~~a).toUInt64 = ~~~a.toUInt64 % 256

@[simp]

theorem UInt8.toUSize_not (a : UInt8) : (~~~a).toUSize = ~~~a.toUSize % 256

@[simp]

theorem UInt16.toUInt32_not (a : UInt16) : (~~~a).toUInt32 = ~~~a.toUInt32 % 65536

@[simp]

theorem UInt16.toUInt64_not (a : UInt16) : (~~~a).toUInt64 = ~~~a.toUInt64 % 65536

@[simp]

theorem UInt16.toUSize_not (a : UInt16) : (~~~a).toUSize = ~~~a.toUSize % 65536

@[simp]

theorem UInt32.toUInt64_not (a : UInt32) : (~~~a).toUInt64 = ~~~a.toUInt64 % 4294967296

@[simp]

theorem UInt32.toUSize_not (a : UInt32) : (~~~a).toUSize = ~~~a.toUSize % 4294967296

@[simp]

theorem USize.toUInt64_not (a : USize) : (~~~a).toUInt64 = ~~~a.toUInt64 % UInt64.ofNat size

@[simp]

theorem UInt8.toFin_shiftLeft (a b : UInt8) (hb : b < 8) : (a <<< b).toFin = a.toFin <<< b.toFin

@[simp]

theorem UInt16.toFin_shiftLeft (a b : UInt16) (hb : b < 16) : (a <<< b).toFin = a.toFin <<< b.toFin

@[simp]

theorem UInt32.toFin_shiftLeft (a b : UInt32) (hb : b < 32) : (a <<< b).toFin = a.toFin <<< b.toFin

@[simp]

theorem UInt64.toFin_shiftLeft (a b : UInt64) (hb : b < 64) : (a <<< b).toFin = a.toFin <<< b.toFin

@[simp]

theorem USize.toFin_shiftLeft (a b : USize) (hb : b.toNat < System.Platform.numBits) : (a <<< b).toFin = a.toFin <<< b.toFin

theorem UInt8.shiftLeft_eq_shiftLeft_mod (a b : UInt8) : a <<< b = a <<< (b % 8)

theorem UInt16.shiftLeft_eq_shiftLeft_mod (a b : UInt16) : a <<< b = a <<< (b % 16)

theorem UInt32.shiftLeft_eq_shiftLeft_mod (a b : UInt32) : a <<< b = a <<< (b % 32)

theorem UInt64.shiftLeft_eq_shiftLeft_mod (a b : UInt64) : a <<< b = a <<< (b % 64)

theorem USize.shiftLeft_eq_shiftLeft_mod (a b : USize) : a <<< b = a <<< (b % ofNat System.Platform.numBits)

theorem UInt8.shiftRight_eq_shiftRight_mod (a b : UInt8) : a >>> b = a >>> (b % 8)

theorem UInt16.shiftRight_eq_shiftRight_mod (a b : UInt16) : a >>> b = a >>> (b % 16)

theorem UInt32.shiftRight_eq_shiftRight_mod (a b : UInt32) : a >>> b = a >>> (b % 32)

theorem UInt64.shiftRight_eq_shiftRight_mod (a b : UInt64) : a >>> b = a >>> (b % 64)

theorem USize.shiftRight_eq_shiftRight_mod (a b : USize) : a >>> b = a >>> (b % ofNat System.Platform.numBits)

@[simp]

theorem UInt16.toUInt8_shiftLeft (a b : UInt16) (hb : b < 8) : (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8

@[simp]

theorem UInt32.toUInt8_shiftLeft (a b : UInt32) (hb : b < 8) : (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8

@[simp]

theorem UInt32.toUInt16_shiftLeft (a b : UInt32) (hb : b < 16) : (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16

@[simp]

theorem USize.toUInt8_shiftLeft (a b : USize) (hb : b < 8) : (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8

@[simp]

theorem USize.toUInt16_shiftLeft (a b : USize) (hb : b < 16) : (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16

@[simp]

theorem USize.toUInt32_shiftLeft (a b : USize) (hb : b < 32) : (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32

@[simp]

theorem UInt64.toUInt8_shiftLeft (a b : UInt64) (hb : b < 8) : (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8

@[simp]

theorem UInt64.toUInt16_shiftLeft (a b : UInt64) (hb : b < 16) : (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16

@[simp]

theorem UInt64.toUInt32_shiftLeft (a b : UInt64) (hb : b < 32) : (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32

@[simp]

theorem UInt64.toUSize_shiftLeft (a b : UInt64) (hb : b.toNat < System.Platform.numBits) : (a <<< b).toUSize = a.toUSize <<< b.toUSize

@[simp]

theorem UInt16.toUInt8_shiftLeft_mod (a b : UInt16) : (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8

@[simp]

theorem UInt32.toUInt8_shiftLeft_mod (a b : UInt32) : (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8

@[simp]

theorem UInt32.toUInt16_shiftLeft_mod (a b : UInt32) : (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16

@[simp]

theorem USize.toUInt8_shiftLeft_mod (a b : USize) : (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8

@[simp]

theorem USize.toUInt16_shiftLeft_mod (a b : USize) : (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16

@[simp]

theorem USize.toUInt32_shiftLeft_mod (a b : USize) : (a <<< (b % 32)).toUInt32 = a.toUInt32 <<< b.toUInt32

@[simp]

theorem UInt64.toUInt8_shiftLeft_mod (a b : UInt64) : (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8

@[simp]

theorem UInt64.toUInt16_shiftLeft_mod (a b : UInt64) : (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16

@[simp]

theorem UInt64.toUInt32_shiftLeft_mod (a b : UInt64) : (a <<< (b % 32)).toUInt32 = a.toUInt32 <<< b.toUInt32

@[simp]

theorem UInt64.toUSize_shiftLeft_mod (a b : UInt64) : (a <<< (b % ofNat System.Platform.numBits)).toUSize = a.toUSize <<< b.toUSize

theorem UInt8.toUInt16_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) : (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16 % 256

theorem UInt8.toUInt32_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) : (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32 % 256

theorem UInt8.toUInt64_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) : (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 256

theorem UInt8.toUSize_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) : (a <<< b).toUSize = a.toUSize <<< b.toUSize % 256

theorem UInt16.toUInt32_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) : (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32 % 65536

theorem UInt16.toUInt64_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) : (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 65536

theorem UInt16.toUSize_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) : (a <<< b).toUSize = a.toUSize <<< b.toUSize % 65536

theorem UInt32.toUInt64_shiftLeft_of_lt (a b : UInt32) (hb : b < 32) : (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 4294967296

theorem UInt32.toUSize_shiftLeft_of_lt (a b : UInt32) (hb : b < 32) : (a <<< b).toUSize = a.toUSize <<< b.toUSize % 4294967296

theorem USize.toUInt64_shiftLeft_of_lt (a b : USize) (hb : b.toNat < System.Platform.numBits) : (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % UInt64.ofNat size

@[simp]

theorem UInt8.toUInt16_shiftLeft (a b : UInt8) : (a <<< b).toUInt16 = a.toUInt16 <<< (b % 8).toUInt16 % 256

@[simp]

theorem UInt8.toUInt32_shiftLeft (a b : UInt8) : (a <<< b).toUInt32 = a.toUInt32 <<< (b % 8).toUInt32 % 256

@[simp]

theorem UInt8.toUInt64_shiftLeft (a b : UInt8) : (a <<< b).toUInt64 = a.toUInt64 <<< (b % 8).toUInt64 % 256

@[simp]

theorem UInt8.toUSize_shiftLeft (a b : UInt8) : (a <<< b).toUSize = a.toUSize <<< (b % 8).toUSize % 256

@[simp]

theorem UInt16.toUInt32_shiftLeft (a b : UInt16) : (a <<< b).toUInt32 = a.toUInt32 <<< (b % 16).toUInt32 % 65536

@[simp]

theorem UInt16.toUInt64_shiftLeft (a b : UInt16) : (a <<< b).toUInt64 = a.toUInt64 <<< (b % 16).toUInt64 % 65536

@[simp]

theorem UInt16.toUSize_shiftLeft (a b : UInt16) : (a <<< b).toUSize = a.toUSize <<< (b % 16).toUSize % 65536

@[simp]

theorem UInt32.toUInt64_shiftLeft (a b : UInt32) : (a <<< b).toUInt64 = a.toUInt64 <<< (b % 32).toUInt64 % 4294967296

@[simp]

theorem UInt32.toUSize_shiftLeft (a b : UInt32) : (a <<< b).toUSize = a.toUSize <<< (b % 32).toUSize % 4294967296

@[simp]

theorem USize.toUInt64_shiftLeft (a b : USize) : (a <<< b).toUInt64 = a.toUInt64 <<< (b % ofNat System.Platform.numBits).toUInt64 % UInt64.ofNat size

@[simp]

theorem UInt8.toFin_shiftRight (a b : UInt8) (hb : b < 8) : (a >>> b).toFin = a.toFin >>> b.toFin

@[simp]

theorem UInt16.toFin_shiftRight (a b : UInt16) (hb : b < 16) : (a >>> b).toFin = a.toFin >>> b.toFin

@[simp]

theorem UInt32.toFin_shiftRight (a b : UInt32) (hb : b < 32) : (a >>> b).toFin = a.toFin >>> b.toFin

@[simp]

theorem UInt64.toFin_shiftRight (a b : UInt64) (hb : b < 64) : (a >>> b).toFin = a.toFin >>> b.toFin

@[simp]

theorem USize.toFin_shiftRight (a b : USize) (hb : b.toNat < System.Platform.numBits) : (a >>> b).toFin = a.toFin >>> b.toFin

@[simp]

theorem UInt8.toUInt16_shiftRight (a b : UInt8) : (a >>> b).toUInt16 = a.toUInt16 >>> (b.toUInt16 % 8)

@[simp]

theorem UInt8.toUInt32_shiftRight (a b : UInt8) : (a >>> b).toUInt32 = a.toUInt32 >>> (b.toUInt32 % 8)

@[simp]

theorem UInt8.toUInt64_shiftRight (a b : UInt8) : (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 8)

@[simp]

theorem UInt8.toUSize_shiftRight (a b : UInt8) : (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 8)

@[simp]

theorem UInt16.toUInt32_shiftRight (a b : UInt16) : (a >>> b).toUInt32 = a.toUInt32 >>> (b.toUInt32 % 16)

@[simp]

theorem UInt16.toUInt64_shiftRight (a b : UInt16) : (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 16)

@[simp]

theorem UInt16.toUSize_shiftRight (a b : UInt16) : (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 16)

@[simp]

theorem UInt32.toUInt64_shiftRight (a b : UInt32) : (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 32)

@[simp]

theorem UInt32.toUSize_shiftRight (a b : UInt32) : (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 32)

@[simp]

theorem USize.toUInt64_shiftRight (a b : USize) : (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % UInt64.ofNat System.Platform.numBits)

There is no reasonable statement forUInt16.toUInt8_shiftRight; in fact for a b : UInt16 the expression (a >>> b).toUInt8 is not a function of a.toUInt8 and b.toUInt8.

@[simp]

theorem UInt8.ofFin_and (a b : Fin size) : ofFin (a &&& b) = ofFin a &&& ofFin b

@[simp]

theorem UInt16.ofFin_and (a b : Fin size) : ofFin (a &&& b) = ofFin a &&& ofFin b

@[simp]

theorem UInt32.ofFin_and (a b : Fin size) : ofFin (a &&& b) = ofFin a &&& ofFin b

@[simp]

theorem UInt64.ofFin_and (a b : Fin size) : ofFin (a &&& b) = ofFin a &&& ofFin b

@[simp]

theorem USize.ofFin_and (a b : Fin size) : ofFin (a &&& b) = ofFin a &&& ofFin b

@[simp]

theorem UInt8.ofBitVec_and (a b : BitVec 8) : { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_and (a b : BitVec 16) : { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_and (a b : BitVec 32) : { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_and (a b : BitVec 64) : { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }

@[simp]

theorem USize.ofBitVec_and (a b : BitVec System.Platform.numBits) : { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }

@[simp]

theorem UInt8.ofNat_and (a b : Nat) : ofNat (a &&& b) = ofNat a &&& ofNat b

@[simp]

theorem UInt16.ofNat_and (a b : Nat) : ofNat (a &&& b) = ofNat a &&& ofNat b

@[simp]

theorem UInt32.ofNat_and (a b : Nat) : ofNat (a &&& b) = ofNat a &&& ofNat b

@[simp]

theorem UInt64.ofNat_and (a b : Nat) : ofNat (a &&& b) = ofNat a &&& ofNat b

@[simp]

theorem USize.ofNat_and (a b : Nat) : ofNat (a &&& b) = ofNat a &&& ofNat b

@[simp]

theorem UInt8.ofNatLT_and (a b : Nat) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) : ofNatLT (a &&& b) ⋯ = ofNatLT a ha &&& ofNatLT b hb

@[simp]

theorem UInt16.ofNatLT_and (a b : Nat) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) : ofNatLT (a &&& b) ⋯ = ofNatLT a ha &&& ofNatLT b hb

@[simp]

theorem UInt32.ofNatLT_and (a b : Nat) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) : ofNatLT (a &&& b) ⋯ = ofNatLT a ha &&& ofNatLT b hb

@[simp]

theorem UInt64.ofNatLT_and (a b : Nat) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : ofNatLT (a &&& b) ⋯ = ofNatLT a ha &&& ofNatLT b hb

@[simp]

theorem UInt8.ofFin_or (a b : Fin size) : ofFin (a ||| b) = ofFin a ||| ofFin b

@[simp]

theorem UInt16.ofFin_or (a b : Fin size) : ofFin (a ||| b) = ofFin a ||| ofFin b

@[simp]

theorem UInt32.ofFin_or (a b : Fin size) : ofFin (a ||| b) = ofFin a ||| ofFin b

@[simp]

theorem UInt64.ofFin_or (a b : Fin size) : ofFin (a ||| b) = ofFin a ||| ofFin b

@[simp]

theorem USize.ofFin_or (a b : Fin size) : ofFin (a ||| b) = ofFin a ||| ofFin b

@[simp]

theorem UInt8.ofBitVec_or (a b : BitVec 8) : { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_or (a b : BitVec 16) : { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_or (a b : BitVec 32) : { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_or (a b : BitVec 64) : { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }

@[simp]

theorem USize.ofBitVec_or (a b : BitVec System.Platform.numBits) : { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }

@[simp]

theorem UInt8.ofNat_or (a b : Nat) : ofNat (a ||| b) = ofNat a ||| ofNat b

@[simp]

theorem UInt16.ofNat_or (a b : Nat) : ofNat (a ||| b) = ofNat a ||| ofNat b

@[simp]

theorem UInt32.ofNat_or (a b : Nat) : ofNat (a ||| b) = ofNat a ||| ofNat b

@[simp]

theorem UInt64.ofNat_or (a b : Nat) : ofNat (a ||| b) = ofNat a ||| ofNat b

@[simp]

theorem USize.ofNat_or (a b : Nat) : ofNat (a ||| b) = ofNat a ||| ofNat b

@[simp]

theorem UInt8.ofNatLT_or (a b : Nat) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) : ofNatLT (a ||| b) ⋯ = ofNatLT a ha ||| ofNatLT b hb

@[simp]

theorem UInt16.ofNatLT_or (a b : Nat) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) : ofNatLT (a ||| b) ⋯ = ofNatLT a ha ||| ofNatLT b hb

@[simp]

theorem UInt32.ofNatLT_or (a b : Nat) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) : ofNatLT (a ||| b) ⋯ = ofNatLT a ha ||| ofNatLT b hb

@[simp]

theorem UInt64.ofNatLT_or (a b : Nat) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : ofNatLT (a ||| b) ⋯ = ofNatLT a ha ||| ofNatLT b hb

@[simp]

theorem UInt8.ofFin_xor (a b : Fin size) : ofFin (a ^^^ b) = ofFin a ^^^ ofFin b

@[simp]

theorem UInt16.ofFin_xor (a b : Fin size) : ofFin (a ^^^ b) = ofFin a ^^^ ofFin b

@[simp]

theorem UInt32.ofFin_xor (a b : Fin size) : ofFin (a ^^^ b) = ofFin a ^^^ ofFin b

@[simp]

theorem UInt64.ofFin_xor (a b : Fin size) : ofFin (a ^^^ b) = ofFin a ^^^ ofFin b

@[simp]

theorem USize.ofFin_xor (a b : Fin size) : ofFin (a ^^^ b) = ofFin a ^^^ ofFin b

@[simp]

theorem UInt8.ofBitVec_xor (a b : BitVec 8) : { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_xor (a b : BitVec 16) : { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_xor (a b : BitVec 32) : { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_xor (a b : BitVec 64) : { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }

@[simp]

theorem USize.ofBitVec_xor (a b : BitVec System.Platform.numBits) : { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }

@[simp]

theorem UInt8.ofNat_xor (a b : Nat) : ofNat (a ^^^ b) = ofNat a ^^^ ofNat b

@[simp]

theorem UInt16.ofNat_xor (a b : Nat) : ofNat (a ^^^ b) = ofNat a ^^^ ofNat b

@[simp]

theorem UInt32.ofNat_xor (a b : Nat) : ofNat (a ^^^ b) = ofNat a ^^^ ofNat b

@[simp]

theorem UInt64.ofNat_xor (a b : Nat) : ofNat (a ^^^ b) = ofNat a ^^^ ofNat b

@[simp]

theorem USize.ofNat_xor (a b : Nat) : ofNat (a ^^^ b) = ofNat a ^^^ ofNat b

@[simp]

theorem UInt8.ofNatLT_xor (a b : Nat) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) : ofNatLT (a ^^^ b) ⋯ = ofNatLT a ha ^^^ ofNatLT b hb

@[simp]

theorem UInt16.ofNatLT_xor (a b : Nat) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) : ofNatLT (a ^^^ b) ⋯ = ofNatLT a ha ^^^ ofNatLT b hb

@[simp]

theorem UInt32.ofNatLT_xor (a b : Nat) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) : ofNatLT (a ^^^ b) ⋯ = ofNatLT a ha ^^^ ofNatLT b hb

@[simp]

theorem UInt64.ofNatLT_xor (a b : Nat) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : ofNatLT (a ^^^ b) ⋯ = ofNatLT a ha ^^^ ofNatLT b hb

@[simp]

theorem UInt8.ofBitVec_not (a : BitVec 8) : { toBitVec := ~~~a } = ~~~{ toBitVec := a }

@[simp]

theorem UInt16.ofBitVec_not (a : BitVec 16) : { toBitVec := ~~~a } = ~~~{ toBitVec := a }

@[simp]

theorem UInt32.ofBitVec_not (a : BitVec 32) : { toBitVec := ~~~a } = ~~~{ toBitVec := a }

@[simp]

theorem UInt64.ofBitVec_not (a : BitVec 64) : { toBitVec := ~~~a } = ~~~{ toBitVec := a }

@[simp]

theorem USize.ofBitVec_not (a : BitVec System.Platform.numBits) : { toBitVec := ~~~a } = ~~~{ toBitVec := a }

@[simp]

theorem UInt8.ofFin_rev (a : Fin size) : ofFin a.rev = ~~~ofFin a

@[simp]

theorem UInt16.ofFin_rev (a : Fin size) : ofFin a.rev = ~~~ofFin a

@[simp]

theorem UInt32.ofFin_rev (a : Fin size) : ofFin a.rev = ~~~ofFin a

@[simp]

theorem UInt64.ofFin_rev (a : Fin size) : ofFin a.rev = ~~~ofFin a

@[simp]

theorem USize.ofFin_rev (a : Fin size) : ofFin a.rev = ~~~ofFin a

@[simp]

theorem UInt8.ofBitVec_shiftLeft (a : BitVec 8) (b : Nat) (hb : b < 8) : { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b

@[simp]

theorem UInt16.ofBitVec_shiftLeft (a : BitVec 16) (b : Nat) (hb : b < 16) : { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b

@[simp]

theorem UInt32.ofBitVec_shiftLeft (a : BitVec 32) (b : Nat) (hb : b < 32) : { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b

@[simp]

theorem UInt64.ofBitVec_shiftLeft (a : BitVec 64) (b : Nat) (hb : b < 64) : { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b

@[simp]

theorem USize.ofBitVec_shiftLeft (a : BitVec System.Platform.numBits) (b : Nat) (hb : b < System.Platform.numBits) : { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b

@[simp]

theorem UInt8.ofBitVec_shiftLeft_mod (a : BitVec 8) (b : Nat) : { toBitVec := a <<< (b % 8) } = { toBitVec := a } <<< ofNat b

@[simp]

theorem UInt16.ofBitVec_shiftLeft_mod (a : BitVec 16) (b : Nat) : { toBitVec := a <<< (b % 16) } = { toBitVec := a } <<< ofNat b

@[simp]

theorem UInt32.ofBitVec_shiftLeft_mod (a : BitVec 32) (b : Nat) : { toBitVec := a <<< (b % 32) } = { toBitVec := a } <<< ofNat b

@[simp]

theorem UInt64.ofBitVec_shiftLeft_mod (a : BitVec 64) (b : Nat) : { toBitVec := a <<< (b % 64) } = { toBitVec := a } <<< ofNat b

@[simp]

theorem USize.ofBitVec_shiftLeft_mod (a : BitVec System.Platform.numBits) (b : Nat) : { toBitVec := a <<< (b % System.Platform.numBits) } = { toBitVec := a } <<< ofNat b

@[simp]

theorem UInt8.ofFin_shiftLeft (a b : Fin size) (hb : b < 8) : ofFin (a <<< b) = ofFin a <<< ofFin b

@[simp]

theorem UInt16.ofFin_shiftLeft (a b : Fin size) (hb : b < 16) : ofFin (a <<< b) = ofFin a <<< ofFin b

@[simp]

theorem UInt32.ofFin_shiftLeft (a b : Fin size) (hb : b < 32) : ofFin (a <<< b) = ofFin a <<< ofFin b

@[simp]

theorem UInt64.ofFin_shiftLeft (a b : Fin size) (hb : b < 64) : ofFin (a <<< b) = ofFin a <<< ofFin b

@[simp]

theorem USize.ofFin_shiftLeft (a b : Fin size) (hb : ↑b < System.Platform.numBits) : ofFin (a <<< b) = ofFin a <<< ofFin b

@[simp]

theorem UInt8.ofFin_shiftLeft_mod (a b : Fin size) : ofFin (a <<< (b % 8)) = ofFin a <<< ofFin b

@[simp]

theorem UInt16.ofFin_shiftLeft_mod (a b : Fin size) : ofFin (a <<< (b % 16)) = ofFin a <<< ofFin b

@[simp]

theorem UInt32.ofFin_shiftLeft_mod (a b : Fin size) : ofFin (a <<< (b % 32)) = ofFin a <<< ofFin b

@[simp]

theorem UInt64.ofFin_shiftLeft_mod (a b : Fin size) : ofFin (a <<< (b % 64)) = ofFin a <<< ofFin b

@[simp]

theorem USize.ofFin_shiftLeft_mod (a b : Fin size) : ofFin (a <<< (b % ⟨System.Platform.numBits, ⋯⟩)) = ofFin a <<< ofFin b

@[simp]

theorem UInt8.ofNat_shiftLeft (a b : Nat) (hb : b < 8) : ofNat (a <<< b) = ofNat a <<< ofNat b

@[simp]

theorem UInt16.ofNat_shiftLeft (a b : Nat) (hb : b < 16) : ofNat (a <<< b) = ofNat a <<< ofNat b

@[simp]

theorem UInt32.ofNat_shiftLeft (a b : Nat) (hb : b < 32) : ofNat (a <<< b) = ofNat a <<< ofNat b

@[simp]

theorem UInt64.ofNat_shiftLeft (a b : Nat) (hb : b < 64) : ofNat (a <<< b) = ofNat a <<< ofNat b

@[simp]

theorem USize.ofNat_shiftLeft (a b : Nat) (hb : b < System.Platform.numBits) : ofNat (a <<< b) = ofNat a <<< ofNat b

@[simp]

theorem UInt8.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < 8) : ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯

@[simp]

theorem UInt16.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < 16) : ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯

@[simp]

theorem UInt32.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < 32) : ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯

@[simp]

theorem UInt64.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < 64) : ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯

@[simp]

theorem USize.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < System.Platform.numBits) : ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯

@[simp]

theorem UInt8.ofBitVec_shiftRight (a : BitVec 8) (b : Nat) (hb : b < 8) : { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b

@[simp]

theorem UInt16.ofBitVec_shiftRight (a : BitVec 16) (b : Nat) (hb : b < 16) : { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b

@[simp]

theorem UInt32.ofBitVec_shiftRight (a : BitVec 32) (b : Nat) (hb : b < 32) : { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b

@[simp]

theorem UInt64.ofBitVec_shiftRight (a : BitVec 64) (b : Nat) (hb : b < 64) : { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b

@[simp]

theorem USize.ofBitVec_shiftRight (a : BitVec System.Platform.numBits) (b : Nat) (hb : b < System.Platform.numBits) : { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b

@[simp]

theorem UInt8.ofBitVec_shiftRight_mod (a : BitVec 8) (b : Nat) : { toBitVec := a >>> (b % 8) } = { toBitVec := a } >>> ofNat b

@[simp]

theorem UInt16.ofBitVec_shiftRight_mod (a : BitVec 16) (b : Nat) : { toBitVec := a >>> (b % 16) } = { toBitVec := a } >>> ofNat b

@[simp]

theorem UInt32.ofBitVec_shiftRight_mod (a : BitVec 32) (b : Nat) : { toBitVec := a >>> (b % 32) } = { toBitVec := a } >>> ofNat b

@[simp]

theorem UInt64.ofBitVec_shiftRight_mod (a : BitVec 64) (b : Nat) : { toBitVec := a >>> (b % 64) } = { toBitVec := a } >>> ofNat b

@[simp]

theorem USize.ofBitVec_shiftRight_mod (a : BitVec System.Platform.numBits) (b : Nat) : { toBitVec := a >>> (b % System.Platform.numBits) } = { toBitVec := a } >>> ofNat b

@[simp]

theorem UInt8.ofFin_shiftRight (a b : Fin size) (hb : b < 8) : ofFin (a >>> b) = ofFin a >>> ofFin b

@[simp]

theorem UInt16.ofFin_shiftRight (a b : Fin size) (hb : b < 16) : ofFin (a >>> b) = ofFin a >>> ofFin b

@[simp]

theorem UInt32.ofFin_shiftRight (a b : Fin size) (hb : b < 32) : ofFin (a >>> b) = ofFin a >>> ofFin b

@[simp]

theorem UInt64.ofFin_shiftRight (a b : Fin size) (hb : b < 64) : ofFin (a >>> b) = ofFin a >>> ofFin b

@[simp]

theorem USize.ofFin_shiftRight (a b : Fin size) (hb : ↑b < System.Platform.numBits) : ofFin (a >>> b) = ofFin a >>> ofFin b

@[simp]

theorem UInt8.ofFin_shiftRight_mod (a b : Fin size) : ofFin (a >>> (b % 8)) = ofFin a >>> ofFin b

@[simp]

theorem UInt16.ofFin_shiftRight_mod (a b : Fin size) : ofFin (a >>> (b % 16)) = ofFin a >>> ofFin b

@[simp]

theorem UInt32.ofFin_shiftRight_mod (a b : Fin size) : ofFin (a >>> (b % 32)) = ofFin a >>> ofFin b

@[simp]

theorem UInt64.ofFin_shiftRight_mod (a b : Fin size) : ofFin (a >>> (b % 64)) = ofFin a >>> ofFin b

@[simp]

theorem USize.ofFin_shiftRight_mod (a b : Fin size) : ofFin (a >>> (b % ⟨System.Platform.numBits, ⋯⟩)) = ofFin a >>> ofFin b

theorem UInt8.neg_eq_not_add (a : UInt8) : -a = ~~~a + 1

theorem UInt16.neg_eq_not_add (a : UInt16) : -a = ~~~a + 1

theorem UInt32.neg_eq_not_add (a : UInt32) : -a = ~~~a + 1

theorem UInt64.neg_eq_not_add (a : UInt64) : -a = ~~~a + 1

theorem USize.neg_eq_not_add (a : USize) : -a = ~~~a + 1

theorem UInt8.not_eq_neg_sub (a : UInt8) : ~~~a = -a - 1

theorem UInt16.not_eq_neg_sub (a : UInt16) : ~~~a = -a - 1

theorem UInt32.not_eq_neg_sub (a : UInt32) : ~~~a = -a - 1

theorem UInt64.not_eq_neg_sub (a : UInt64) : ~~~a = -a - 1

theorem USize.not_eq_neg_sub (a : USize) : ~~~a = -a - 1

theorem UInt8.or_assoc (a b c : UInt8) : a ||| b ||| c = a ||| (b ||| c)

theorem UInt16.or_assoc (a b c : UInt16) : a ||| b ||| c = a ||| (b ||| c)

theorem UInt32.or_assoc (a b c : UInt32) : a ||| b ||| c = a ||| (b ||| c)

theorem UInt64.or_assoc (a b c : UInt64) : a ||| b ||| c = a ||| (b ||| c)

theorem USize.or_assoc (a b c : USize) : a ||| b ||| c = a ||| (b ||| c)

instance instAssociativeUInt8HOr : Std.Associative fun (x1 x2 : UInt8) => x1 ||| x2

instance instAssociativeUInt16HOr : Std.Associative fun (x1 x2 : UInt16) => x1 ||| x2

instance instAssociativeUInt32HOr : Std.Associative fun (x1 x2 : UInt32) => x1 ||| x2

instance instAssociativeUInt64HOr : Std.Associative fun (x1 x2 : UInt64) => x1 ||| x2

instance instAssociativeUSizeHOr : Std.Associative fun (x1 x2 : USize) => x1 ||| x2

theorem UInt8.or_comm (a b : UInt8) : a ||| b = b ||| a

theorem UInt16.or_comm (a b : UInt16) : a ||| b = b ||| a

theorem UInt32.or_comm (a b : UInt32) : a ||| b = b ||| a

theorem UInt64.or_comm (a b : UInt64) : a ||| b = b ||| a

theorem USize.or_comm (a b : USize) : a ||| b = b ||| a

instance instCommutativeUInt8HOr : Std.Commutative fun (x1 x2 : UInt8) => x1 ||| x2

instance instCommutativeUInt16HOr : Std.Commutative fun (x1 x2 : UInt16) => x1 ||| x2

instance instCommutativeUInt32HOr : Std.Commutative fun (x1 x2 : UInt32) => x1 ||| x2

instance instCommutativeUInt64HOr : Std.Commutative fun (x1 x2 : UInt64) => x1 ||| x2

instance instCommutativeUSizeHOr : Std.Commutative fun (x1 x2 : USize) => x1 ||| x2

@[simp]

theorem UInt8.or_self {a : UInt8} : a ||| a = a

@[simp]

theorem UInt16.or_self {a : UInt16} : a ||| a = a

@[simp]

theorem UInt32.or_self {a : UInt32} : a ||| a = a

@[simp]

theorem UInt64.or_self {a : UInt64} : a ||| a = a

@[simp]

theorem USize.or_self {a : USize} : a ||| a = a

instance instIdempotentOpUInt8HOr : Std.IdempotentOp fun (x1 x2 : UInt8) => x1 ||| x2

instance instIdempotentOpUInt16HOr : Std.IdempotentOp fun (x1 x2 : UInt16) => x1 ||| x2

instance instIdempotentOpUInt32HOr : Std.IdempotentOp fun (x1 x2 : UInt32) => x1 ||| x2

instance instIdempotentOpUInt64HOr : Std.IdempotentOp fun (x1 x2 : UInt64) => x1 ||| x2

instance instIdempotentOpUSizeHOr : Std.IdempotentOp fun (x1 x2 : USize) => x1 ||| x2

@[simp]

theorem UInt8.or_zero {a : UInt8} : a ||| 0 = a

@[simp]

theorem UInt16.or_zero {a : UInt16} : a ||| 0 = a

@[simp]

theorem UInt32.or_zero {a : UInt32} : a ||| 0 = a

@[simp]

theorem UInt64.or_zero {a : UInt64} : a ||| 0 = a

@[simp]

theorem USize.or_zero {a : USize} : a ||| 0 = a

@[simp]

theorem UInt8.zero_or {a : UInt8} : 0 ||| a = a

@[simp]

theorem UInt16.zero_or {a : UInt16} : 0 ||| a = a

@[simp]

theorem UInt32.zero_or {a : UInt32} : 0 ||| a = a

@[simp]

theorem UInt64.zero_or {a : UInt64} : 0 ||| a = a

@[simp]

theorem USize.zero_or {a : USize} : 0 ||| a = a

instance instLawfulCommIdentityUInt8HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => x1 ||| x2) 0

instance instLawfulCommIdentityUInt16HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => x1 ||| x2) 0

instance instLawfulCommIdentityUInt32HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => x1 ||| x2) 0

instance instLawfulCommIdentityUInt64HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => x1 ||| x2) 0

instance instLawfulCommIdentityUSizeHOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : USize) => x1 ||| x2) 0

@[simp]

theorem UInt8.neg_one_or {a : UInt8} : -1 ||| a = -1

@[simp]

theorem UInt16.neg_one_or {a : UInt16} : -1 ||| a = -1

@[simp]

theorem UInt32.neg_one_or {a : UInt32} : -1 ||| a = -1

@[simp]

theorem UInt64.neg_one_or {a : UInt64} : -1 ||| a = -1

@[simp]

theorem USize.neg_one_or {a : USize} : -1 ||| a = -1

@[simp]

theorem UInt8.or_neg_one {a : UInt8} : a ||| -1 = -1

@[simp]

theorem UInt16.or_neg_one {a : UInt16} : a ||| -1 = -1

@[simp]

theorem UInt32.or_neg_one {a : UInt32} : a ||| -1 = -1

@[simp]

theorem UInt64.or_neg_one {a : UInt64} : a ||| -1 = -1

@[simp]

theorem USize.or_neg_one {a : USize} : a ||| -1 = -1

@[simp]

theorem UInt8.or_eq_zero_iff {a b : UInt8} : a ||| b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem UInt16.or_eq_zero_iff {a b : UInt16} : a ||| b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem UInt32.or_eq_zero_iff {a b : UInt32} : a ||| b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem UInt64.or_eq_zero_iff {a b : UInt64} : a ||| b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem USize.or_eq_zero_iff {a b : USize} : a ||| b = 0 ↔ a = 0 ∧ b = 0

theorem UInt8.and_assoc (a b c : UInt8) : a &&& b &&& c = a &&& (b &&& c)

theorem UInt16.and_assoc (a b c : UInt16) : a &&& b &&& c = a &&& (b &&& c)

theorem UInt32.and_assoc (a b c : UInt32) : a &&& b &&& c = a &&& (b &&& c)

theorem UInt64.and_assoc (a b c : UInt64) : a &&& b &&& c = a &&& (b &&& c)

theorem USize.and_assoc (a b c : USize) : a &&& b &&& c = a &&& (b &&& c)

instance instAssociativeUInt8HAnd : Std.Associative fun (x1 x2 : UInt8) => x1 &&& x2

instance instAssociativeUInt16HAnd : Std.Associative fun (x1 x2 : UInt16) => x1 &&& x2

instance instAssociativeUInt32HAnd : Std.Associative fun (x1 x2 : UInt32) => x1 &&& x2

instance instAssociativeUInt64HAnd : Std.Associative fun (x1 x2 : UInt64) => x1 &&& x2

instance instAssociativeUSizeHAnd : Std.Associative fun (x1 x2 : USize) => x1 &&& x2

theorem UInt8.and_comm (a b : UInt8) : a &&& b = b &&& a

theorem UInt16.and_comm (a b : UInt16) : a &&& b = b &&& a

theorem UInt32.and_comm (a b : UInt32) : a &&& b = b &&& a

theorem UInt64.and_comm (a b : UInt64) : a &&& b = b &&& a

theorem USize.and_comm (a b : USize) : a &&& b = b &&& a

instance instCommutativeUInt8HAnd : Std.Commutative fun (x1 x2 : UInt8) => x1 &&& x2

instance instCommutativeUInt16HAnd : Std.Commutative fun (x1 x2 : UInt16) => x1 &&& x2

instance instCommutativeUInt32HAnd : Std.Commutative fun (x1 x2 : UInt32) => x1 &&& x2

instance instCommutativeUInt64HAnd : Std.Commutative fun (x1 x2 : UInt64) => x1 &&& x2

instance instCommutativeUSizeHAnd : Std.Commutative fun (x1 x2 : USize) => x1 &&& x2

@[simp]

theorem UInt8.and_self {a : UInt8} : a &&& a = a

@[simp]

theorem UInt16.and_self {a : UInt16} : a &&& a = a

@[simp]

theorem UInt32.and_self {a : UInt32} : a &&& a = a

@[simp]

theorem UInt64.and_self {a : UInt64} : a &&& a = a

@[simp]

theorem USize.and_self {a : USize} : a &&& a = a

instance instIdempotentOpUInt8HAnd : Std.IdempotentOp fun (x1 x2 : UInt8) => x1 &&& x2

instance instIdempotentOpUInt16HAnd : Std.IdempotentOp fun (x1 x2 : UInt16) => x1 &&& x2

instance instIdempotentOpUInt32HAnd : Std.IdempotentOp fun (x1 x2 : UInt32) => x1 &&& x2

instance instIdempotentOpUInt64HAnd : Std.IdempotentOp fun (x1 x2 : UInt64) => x1 &&& x2

instance instIdempotentOpUSizeHAnd : Std.IdempotentOp fun (x1 x2 : USize) => x1 &&& x2

@[simp]

theorem UInt8.and_zero {a : UInt8} : a &&& 0 = 0

@[simp]

theorem UInt16.and_zero {a : UInt16} : a &&& 0 = 0

@[simp]

theorem UInt32.and_zero {a : UInt32} : a &&& 0 = 0

@[simp]

theorem UInt64.and_zero {a : UInt64} : a &&& 0 = 0

@[simp]

theorem USize.and_zero {a : USize} : a &&& 0 = 0

@[simp]

theorem UInt8.zero_and {a : UInt8} : 0 &&& a = 0

@[simp]

theorem UInt16.zero_and {a : UInt16} : 0 &&& a = 0

@[simp]

theorem UInt32.zero_and {a : UInt32} : 0 &&& a = 0

@[simp]

theorem UInt64.zero_and {a : UInt64} : 0 &&& a = 0

@[simp]

theorem USize.zero_and {a : USize} : 0 &&& a = 0

@[simp]

theorem UInt8.neg_one_and {a : UInt8} : -1 &&& a = a

@[simp]

theorem UInt16.neg_one_and {a : UInt16} : -1 &&& a = a

@[simp]

theorem UInt32.neg_one_and {a : UInt32} : -1 &&& a = a

@[simp]

theorem UInt64.neg_one_and {a : UInt64} : -1 &&& a = a

@[simp]

theorem USize.neg_one_and {a : USize} : -1 &&& a = a

@[simp]

theorem UInt8.and_neg_one {a : UInt8} : a &&& -1 = a

@[simp]

theorem UInt16.and_neg_one {a : UInt16} : a &&& -1 = a

@[simp]

theorem UInt32.and_neg_one {a : UInt32} : a &&& -1 = a

@[simp]

theorem UInt64.and_neg_one {a : UInt64} : a &&& -1 = a

@[simp]

theorem USize.and_neg_one {a : USize} : a &&& -1 = a

instance instLawfulCommIdentityUInt8HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => x1 &&& x2) (-1)

instance instLawfulCommIdentityUInt16HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => x1 &&& x2) (-1)

instance instLawfulCommIdentityUInt32HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => x1 &&& x2) (-1)

instance instLawfulCommIdentityUInt64HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => x1 &&& x2) (-1)

instance instLawfulCommIdentityUSizeHAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : USize) => x1 &&& x2) (-1)

@[simp]

theorem UInt8.and_eq_neg_one_iff {a b : UInt8} : a &&& b = -1 ↔ a = -1 ∧ b = -1

@[simp]

theorem UInt16.and_eq_neg_one_iff {a b : UInt16} : a &&& b = -1 ↔ a = -1 ∧ b = -1

@[simp]

theorem UInt32.and_eq_neg_one_iff {a b : UInt32} : a &&& b = -1 ↔ a = -1 ∧ b = -1

@[simp]

theorem UInt64.and_eq_neg_one_iff {a b : UInt64} : a &&& b = -1 ↔ a = -1 ∧ b = -1

@[simp]

theorem USize.and_eq_neg_one_iff {a b : USize} : a &&& b = -1 ↔ a = -1 ∧ b = -1

theorem UInt8.xor_assoc (a b c : UInt8) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

theorem UInt16.xor_assoc (a b c : UInt16) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

theorem UInt32.xor_assoc (a b c : UInt32) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

theorem UInt64.xor_assoc (a b c : UInt64) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

theorem USize.xor_assoc (a b c : USize) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

instance instAssociativeUInt8HXor : Std.Associative fun (x1 x2 : UInt8) => x1 ^^^ x2

instance instAssociativeUInt16HXor : Std.Associative fun (x1 x2 : UInt16) => x1 ^^^ x2

instance instAssociativeUInt32HXor : Std.Associative fun (x1 x2 : UInt32) => x1 ^^^ x2

instance instAssociativeUInt64HXor : Std.Associative fun (x1 x2 : UInt64) => x1 ^^^ x2

instance instAssociativeUSizeHXor : Std.Associative fun (x1 x2 : USize) => x1 ^^^ x2

theorem UInt8.xor_comm (a b : UInt8) : a ^^^ b = b ^^^ a

theorem UInt16.xor_comm (a b : UInt16) : a ^^^ b = b ^^^ a

theorem UInt32.xor_comm (a b : UInt32) : a ^^^ b = b ^^^ a

theorem UInt64.xor_comm (a b : UInt64) : a ^^^ b = b ^^^ a

theorem USize.xor_comm (a b : USize) : a ^^^ b = b ^^^ a

instance instCommutativeUInt8HXor : Std.Commutative fun (x1 x2 : UInt8) => x1 ^^^ x2

instance instCommutativeUInt16HXor : Std.Commutative fun (x1 x2 : UInt16) => x1 ^^^ x2

instance instCommutativeUInt32HXor : Std.Commutative fun (x1 x2 : UInt32) => x1 ^^^ x2

instance instCommutativeUInt64HXor : Std.Commutative fun (x1 x2 : UInt64) => x1 ^^^ x2

instance instCommutativeUSizeHXor : Std.Commutative fun (x1 x2 : USize) => x1 ^^^ x2

@[simp]

theorem UInt8.xor_self {a : UInt8} : a ^^^ a = 0

@[simp]

theorem UInt16.xor_self {a : UInt16} : a ^^^ a = 0

@[simp]

theorem UInt32.xor_self {a : UInt32} : a ^^^ a = 0

@[simp]

theorem UInt64.xor_self {a : UInt64} : a ^^^ a = 0

@[simp]

theorem USize.xor_self {a : USize} : a ^^^ a = 0

@[simp]

theorem UInt8.xor_zero {a : UInt8} : a ^^^ 0 = a

@[simp]

theorem UInt16.xor_zero {a : UInt16} : a ^^^ 0 = a

@[simp]

theorem UInt32.xor_zero {a : UInt32} : a ^^^ 0 = a

@[simp]

theorem UInt64.xor_zero {a : UInt64} : a ^^^ 0 = a

@[simp]

theorem USize.xor_zero {a : USize} : a ^^^ 0 = a

@[simp]

theorem UInt8.zero_xor {a : UInt8} : 0 ^^^ a = a

@[simp]

theorem UInt16.zero_xor {a : UInt16} : 0 ^^^ a = a

@[simp]

theorem UInt32.zero_xor {a : UInt32} : 0 ^^^ a = a

@[simp]

theorem UInt64.zero_xor {a : UInt64} : 0 ^^^ a = a

@[simp]

theorem USize.zero_xor {a : USize} : 0 ^^^ a = a

@[simp]

theorem UInt8.neg_one_xor {a : UInt8} : -1 ^^^ a = ~~~a

@[simp]

theorem UInt16.neg_one_xor {a : UInt16} : -1 ^^^ a = ~~~a

@[simp]

theorem UInt32.neg_one_xor {a : UInt32} : -1 ^^^ a = ~~~a

@[simp]

theorem UInt64.neg_one_xor {a : UInt64} : -1 ^^^ a = ~~~a

@[simp]

theorem USize.neg_one_xor {a : USize} : -1 ^^^ a = ~~~a

@[simp]

theorem UInt8.xor_neg_one {a : UInt8} : a ^^^ -1 = ~~~a

@[simp]

theorem UInt16.xor_neg_one {a : UInt16} : a ^^^ -1 = ~~~a

@[simp]

theorem UInt32.xor_neg_one {a : UInt32} : a ^^^ -1 = ~~~a

@[simp]

theorem UInt64.xor_neg_one {a : UInt64} : a ^^^ -1 = ~~~a

@[simp]

theorem USize.xor_neg_one {a : USize} : a ^^^ -1 = ~~~a

instance instLawfulCommIdentityUInt8HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => x1 ^^^ x2) 0

instance instLawfulCommIdentityUInt16HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => x1 ^^^ x2) 0

instance instLawfulCommIdentityUInt32HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => x1 ^^^ x2) 0

instance instLawfulCommIdentityUInt64HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => x1 ^^^ x2) 0

instance instLawfulCommIdentityUSizeHXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : USize) => x1 ^^^ x2) 0

@[simp]

theorem UInt8.xor_eq_zero_iff {a b : UInt8} : a ^^^ b = 0 ↔ a = b

@[simp]

theorem UInt16.xor_eq_zero_iff {a b : UInt16} : a ^^^ b = 0 ↔ a = b

@[simp]

theorem UInt32.xor_eq_zero_iff {a b : UInt32} : a ^^^ b = 0 ↔ a = b

@[simp]

theorem UInt64.xor_eq_zero_iff {a b : UInt64} : a ^^^ b = 0 ↔ a = b

@[simp]

theorem USize.xor_eq_zero_iff {a b : USize} : a ^^^ b = 0 ↔ a = b

@[simp]

theorem UInt8.xor_left_inj {a b : UInt8} (c : UInt8) : a ^^^ c = b ^^^ c ↔ a = b

@[simp]

theorem UInt16.xor_left_inj {a b : UInt16} (c : UInt16) : a ^^^ c = b ^^^ c ↔ a = b

@[simp]

theorem UInt32.xor_left_inj {a b : UInt32} (c : UInt32) : a ^^^ c = b ^^^ c ↔ a = b

@[simp]

theorem UInt64.xor_left_inj {a b : UInt64} (c : UInt64) : a ^^^ c = b ^^^ c ↔ a = b

@[simp]

theorem USize.xor_left_inj {a b : USize} (c : USize) : a ^^^ c = b ^^^ c ↔ a = b

@[simp]

theorem UInt8.xor_right_inj {a b : UInt8} (c : UInt8) : c ^^^ a = c ^^^ b ↔ a = b

@[simp]

theorem UInt16.xor_right_inj {a b : UInt16} (c : UInt16) : c ^^^ a = c ^^^ b ↔ a = b

@[simp]

theorem UInt32.xor_right_inj {a b : UInt32} (c : UInt32) : c ^^^ a = c ^^^ b ↔ a = b

@[simp]

theorem UInt64.xor_right_inj {a b : UInt64} (c : UInt64) : c ^^^ a = c ^^^ b ↔ a = b

@[simp]

theorem USize.xor_right_inj {a b : USize} (c : USize) : c ^^^ a = c ^^^ b ↔ a = b

@[simp]

theorem UInt8.not_zero : ~~~0 = -1

@[simp]

theorem UInt16.not_zero : ~~~0 = -1

@[simp]

theorem UInt32.not_zero : ~~~0 = -1

@[simp]

theorem UInt64.not_zero : ~~~0 = -1

@[simp]

theorem USize.not_zero : ~~~0 = -1

@[simp]

theorem UInt8.not_neg_one : ~~~(-1) = 0

@[simp]

theorem UInt16.not_neg_one : ~~~(-1) = 0

@[simp]

theorem UInt32.not_neg_one : ~~~(-1) = 0

@[simp]

theorem UInt64.not_neg_one : ~~~(-1) = 0

@[simp]

theorem USize.not_neg_one : ~~~(-1) = 0

@[simp]

theorem UInt8.not_not {a : UInt8} : ~~~~~~a = a

@[simp]

theorem UInt16.not_not {a : UInt16} : ~~~~~~a = a

@[simp]

theorem UInt32.not_not {a : UInt32} : ~~~~~~a = a

@[simp]

theorem UInt64.not_not {a : UInt64} : ~~~~~~a = a

@[simp]

theorem USize.not_not {a : USize} : ~~~~~~a = a

@[simp]

theorem UInt8.not_inj {a b : UInt8} : ~~~a = ~~~b ↔ a = b

@[simp]

theorem UInt16.not_inj {a b : UInt16} : ~~~a = ~~~b ↔ a = b

@[simp]

theorem UInt32.not_inj {a b : UInt32} : ~~~a = ~~~b ↔ a = b

@[simp]

theorem UInt64.not_inj {a b : UInt64} : ~~~a = ~~~b ↔ a = b

@[simp]

theorem USize.not_inj {a b : USize} : ~~~a = ~~~b ↔ a = b

@[simp]

theorem UInt8.and_not_self {a : UInt8} : a &&& ~~~a = 0

@[simp]

theorem UInt16.and_not_self {a : UInt16} : a &&& ~~~a = 0

@[simp]

theorem UInt32.and_not_self {a : UInt32} : a &&& ~~~a = 0

@[simp]

theorem UInt64.and_not_self {a : UInt64} : a &&& ~~~a = 0

@[simp]

theorem USize.and_not_self {a : USize} : a &&& ~~~a = 0

@[simp]

theorem UInt8.not_and_self {a : UInt8} : ~~~a &&& a = 0

@[simp]

theorem UInt16.not_and_self {a : UInt16} : ~~~a &&& a = 0

@[simp]

theorem UInt32.not_and_self {a : UInt32} : ~~~a &&& a = 0

@[simp]

theorem UInt64.not_and_self {a : UInt64} : ~~~a &&& a = 0

@[simp]

theorem USize.not_and_self {a : USize} : ~~~a &&& a = 0

@[simp]

theorem UInt8.or_not_self {a : UInt8} : a ||| ~~~a = -1

@[simp]

theorem UInt16.or_not_self {a : UInt16} : a ||| ~~~a = -1

@[simp]

theorem UInt32.or_not_self {a : UInt32} : a ||| ~~~a = -1

@[simp]

theorem UInt64.or_not_self {a : UInt64} : a ||| ~~~a = -1

@[simp]

theorem USize.or_not_self {a : USize} : a ||| ~~~a = -1

@[simp]

theorem UInt8.not_or_self {a : UInt8} : ~~~a ||| a = -1

@[simp]

theorem UInt16.not_or_self {a : UInt16} : ~~~a ||| a = -1

@[simp]

theorem UInt32.not_or_self {a : UInt32} : ~~~a ||| a = -1

@[simp]

theorem UInt64.not_or_self {a : UInt64} : ~~~a ||| a = -1

@[simp]

theorem USize.not_or_self {a : USize} : ~~~a ||| a = -1

theorem UInt8.not_eq_comm {a b : UInt8} : ~~~a = b ↔ a = ~~~b

theorem UInt16.not_eq_comm {a b : UInt16} : ~~~a = b ↔ a = ~~~b

theorem UInt32.not_eq_comm {a b : UInt32} : ~~~a = b ↔ a = ~~~b

theorem UInt64.not_eq_comm {a b : UInt64} : ~~~a = b ↔ a = ~~~b

theorem USize.not_eq_comm {a b : USize} : ~~~a = b ↔ a = ~~~b

@[simp]

theorem UInt8.ne_not_self {a : UInt8} : a ≠ ~~~a

@[simp]

theorem UInt16.ne_not_self {a : UInt16} : a ≠ ~~~a

@[simp]

theorem UInt32.ne_not_self {a : UInt32} : a ≠ ~~~a

@[simp]

theorem UInt64.ne_not_self {a : UInt64} : a ≠ ~~~a

@[simp]

theorem USize.ne_not_self {a : USize} : a ≠ ~~~a

@[simp]

theorem UInt8.not_ne_self {a : UInt8} : ~~~a ≠ a

@[simp]

theorem UInt16.not_ne_self {a : UInt16} : ~~~a ≠ a

@[simp]

theorem UInt32.not_ne_self {a : UInt32} : ~~~a ≠ a

@[simp]

theorem UInt64.not_ne_self {a : UInt64} : ~~~a ≠ a

@[simp]

theorem USize.not_ne_self {a : USize} : ~~~a ≠ a

theorem UInt8.not_xor {a b : UInt8} : ~~~a ^^^ b = ~~~(a ^^^ b)

theorem UInt16.not_xor {a b : UInt16} : ~~~a ^^^ b = ~~~(a ^^^ b)

theorem UInt32.not_xor {a b : UInt32} : ~~~a ^^^ b = ~~~(a ^^^ b)

theorem UInt64.not_xor {a b : UInt64} : ~~~a ^^^ b = ~~~(a ^^^ b)

theorem USize.not_xor {a b : USize} : ~~~a ^^^ b = ~~~(a ^^^ b)

theorem UInt8.xor_not {a b : UInt8} : a ^^^ ~~~b = ~~~(a ^^^ b)

theorem UInt16.xor_not {a b : UInt16} : a ^^^ ~~~b = ~~~(a ^^^ b)

theorem UInt32.xor_not {a b : UInt32} : a ^^^ ~~~b = ~~~(a ^^^ b)

theorem UInt64.xor_not {a b : UInt64} : a ^^^ ~~~b = ~~~(a ^^^ b)

theorem USize.xor_not {a b : USize} : a ^^^ ~~~b = ~~~(a ^^^ b)

@[simp]

theorem UInt8.shiftLeft_zero {a : UInt8} : a <<< 0 = a

@[simp]

theorem UInt16.shiftLeft_zero {a : UInt16} : a <<< 0 = a

@[simp]

theorem UInt32.shiftLeft_zero {a : UInt32} : a <<< 0 = a

@[simp]

theorem UInt64.shiftLeft_zero {a : UInt64} : a <<< 0 = a

@[simp]

theorem USize.shiftLeft_zero {a : USize} : a <<< 0 = a

@[simp]

theorem UInt8.zero_shiftLeft {a : UInt8} : 0 <<< a = 0

@[simp]

theorem UInt16.zero_shiftLeft {a : UInt16} : 0 <<< a = 0

@[simp]

theorem UInt32.zero_shiftLeft {a : UInt32} : 0 <<< a = 0

@[simp]

theorem UInt64.zero_shiftLeft {a : UInt64} : 0 <<< a = 0

@[simp]

theorem USize.zero_shiftLeft {a : USize} : 0 <<< a = 0

theorem UInt8.shiftLeft_xor {a b c : UInt8} : (a ^^^ b) <<< c = a <<< c ^^^ b <<< c

theorem UInt16.shiftLeft_xor {a b c : UInt16} : (a ^^^ b) <<< c = a <<< c ^^^ b <<< c

theorem UInt32.shiftLeft_xor {a b c : UInt32} : (a ^^^ b) <<< c = a <<< c ^^^ b <<< c

theorem UInt64.shiftLeft_xor {a b c : UInt64} : (a ^^^ b) <<< c = a <<< c ^^^ b <<< c

theorem USize.shiftLeft_xor {a b c : USize} : (a ^^^ b) <<< c = a <<< c ^^^ b <<< c

theorem UInt8.shiftLeft_and {a b c : UInt8} : (a &&& b) <<< c = a <<< c &&& b <<< c

theorem UInt16.shiftLeft_and {a b c : UInt16} : (a &&& b) <<< c = a <<< c &&& b <<< c

theorem UInt32.shiftLeft_and {a b c : UInt32} : (a &&& b) <<< c = a <<< c &&& b <<< c

theorem UInt64.shiftLeft_and {a b c : UInt64} : (a &&& b) <<< c = a <<< c &&& b <<< c

theorem USize.shiftLeft_and {a b c : USize} : (a &&& b) <<< c = a <<< c &&& b <<< c

theorem UInt8.shiftLeft_or {a b c : UInt8} : (a ||| b) <<< c = a <<< c ||| b <<< c

theorem UInt16.shiftLeft_or {a b c : UInt16} : (a ||| b) <<< c = a <<< c ||| b <<< c

theorem UInt32.shiftLeft_or {a b c : UInt32} : (a ||| b) <<< c = a <<< c ||| b <<< c

theorem UInt64.shiftLeft_or {a b c : UInt64} : (a ||| b) <<< c = a <<< c ||| b <<< c

theorem USize.shiftLeft_or {a b c : USize} : (a ||| b) <<< c = a <<< c ||| b <<< c

theorem UInt8.shiftLeft_add_of_toNat_lt {a b c : UInt8} (h : b.toNat + c.toNat < 8) : a <<< (b + c) = a <<< b <<< c

theorem UInt16.shiftLeft_add_of_toNat_lt {a b c : UInt16} (h : b.toNat + c.toNat < 16) : a <<< (b + c) = a <<< b <<< c

theorem UInt32.shiftLeft_add_of_toNat_lt {a b c : UInt32} (h : b.toNat + c.toNat < 32) : a <<< (b + c) = a <<< b <<< c

theorem UInt64.shiftLeft_add_of_toNat_lt {a b c : UInt64} (h : b.toNat + c.toNat < 64) : a <<< (b + c) = a <<< b <<< c

theorem USize.shiftLeft_add_of_toNat_lt {a b c : USize} (h : b.toNat + c.toNat < System.Platform.numBits) : a <<< (b + c) = a <<< b <<< c

theorem UInt8.shiftLeft_add {a b c : UInt8} (hb : b < 8) (hc : c < 8) (hbc : b + c < 8) : a <<< (b + c) = a <<< b <<< c

theorem UInt16.shiftLeft_add {a b c : UInt16} (hb : b < 16) (hc : c < 16) (hbc : b + c < 16) : a <<< (b + c) = a <<< b <<< c

theorem UInt32.shiftLeft_add {a b c : UInt32} (hb : b < 32) (hc : c < 32) (hbc : b + c < 32) : a <<< (b + c) = a <<< b <<< c

theorem UInt64.shiftLeft_add {a b c : UInt64} (hb : b < 64) (hc : c < 64) (hbc : b + c < 64) : a <<< (b + c) = a <<< b <<< c

theorem USize.shiftLeft_add {a b c : USize} (hb : b < ofNat System.Platform.numBits) (hc : c < ofNat System.Platform.numBits) (hbc : b + c < ofNat System.Platform.numBits) : a <<< (b + c) = a <<< b <<< c

@[simp]

theorem UInt8.neg_one_shiftLeft_and_shiftLeft {a b : UInt8} : (-1) <<< b &&& a <<< b = a <<< b

@[simp]

theorem UInt16.neg_one_shiftLeft_and_shiftLeft {a b : UInt16} : (-1) <<< b &&& a <<< b = a <<< b

@[simp]

theorem UInt32.neg_one_shiftLeft_and_shiftLeft {a b : UInt32} : (-1) <<< b &&& a <<< b = a <<< b

@[simp]

theorem UInt64.neg_one_shiftLeft_and_shiftLeft {a b : UInt64} : (-1) <<< b &&& a <<< b = a <<< b

@[simp]

theorem USize.neg_one_shiftLeft_and_shiftLeft {a b : USize} : (-1) <<< b &&& a <<< b = a <<< b

@[simp]

theorem UInt8.neg_one_shiftLeft_or_shiftLeft {a b : UInt8} : (-1) <<< b ||| a <<< b = (-1) <<< b

@[simp]

theorem UInt16.neg_one_shiftLeft_or_shiftLeft {a b : UInt16} : (-1) <<< b ||| a <<< b = (-1) <<< b

@[simp]

theorem UInt32.neg_one_shiftLeft_or_shiftLeft {a b : UInt32} : (-1) <<< b ||| a <<< b = (-1) <<< b

@[simp]

theorem UInt64.neg_one_shiftLeft_or_shiftLeft {a b : UInt8} : (-1) <<< b ||| a <<< b = (-1) <<< b

@[simp]

theorem USize.neg_one_shiftLeft_or_shiftLeft {a b : USize} : (-1) <<< b ||| a <<< b = (-1) <<< b

@[simp]

theorem UInt8.shiftRight_zero {a : UInt8} : a >>> 0 = a

@[simp]

theorem UInt16.shiftRight_zero {a : UInt16} : a >>> 0 = a

@[simp]

theorem UInt32.shiftRight_zero {a : UInt32} : a >>> 0 = a

@[simp]

theorem UInt64.shiftRight_zero {a : UInt64} : a >>> 0 = a

@[simp]

theorem USize.shiftRight_zero {a : USize} : a >>> 0 = a

@[simp]

theorem UInt8.zero_shiftRight {a : UInt8} : 0 >>> a = 0

@[simp]

theorem UInt16.zero_shiftRight {a : UInt16} : 0 >>> a = 0

@[simp]

theorem UInt32.zero_shiftRight {a : UInt32} : 0 >>> a = 0

@[simp]

theorem UInt64.zero_shiftRight {a : UInt64} : 0 >>> a = 0

@[simp]

theorem USize.zero_shiftRight {a : USize} : 0 >>> a = 0

theorem UInt8.shiftRight_xor {a b c : UInt8} : (a ^^^ b) >>> c = a >>> c ^^^ b >>> c

theorem UInt16.shiftRight_xor {a b c : UInt16} : (a ^^^ b) >>> c = a >>> c ^^^ b >>> c

theorem UInt32.shiftRight_xor {a b c : UInt32} : (a ^^^ b) >>> c = a >>> c ^^^ b >>> c

theorem UInt64.shiftRight_xor {a b c : UInt64} : (a ^^^ b) >>> c = a >>> c ^^^ b >>> c

theorem USize.shiftRight_xor {a b c : USize} : (a ^^^ b) >>> c = a >>> c ^^^ b >>> c

theorem UInt8.shiftRight_and {a b c : UInt8} : (a &&& b) >>> c = a >>> c &&& b >>> c

theorem UInt16.shiftRight_and {a b c : UInt16} : (a &&& b) >>> c = a >>> c &&& b >>> c

theorem UInt32.shiftRight_and {a b c : UInt32} : (a &&& b) >>> c = a >>> c &&& b >>> c

theorem UInt64.shiftRight_and {a b c : UInt64} : (a &&& b) >>> c = a >>> c &&& b >>> c

theorem USize.shiftRight_and {a b c : USize} : (a &&& b) >>> c = a >>> c &&& b >>> c

theorem UInt8.shiftRight_or {a b c : UInt8} : (a ||| b) >>> c = a >>> c ||| b >>> c

theorem UInt16.shiftRight_or {a b c : UInt16} : (a ||| b) >>> c = a >>> c ||| b >>> c

theorem UInt32.shiftRight_or {a b c : UInt32} : (a ||| b) >>> c = a >>> c ||| b >>> c

theorem UInt64.shiftRight_or {a b c : UInt64} : (a ||| b) >>> c = a >>> c ||| b >>> c

theorem USize.shiftRight_or {a b c : USize} : (a ||| b) >>> c = a >>> c ||| b >>> c

theorem UInt8.and_le_right {a b : UInt8} : a &&& b ≤ b

theorem UInt16.and_le_right {a b : UInt16} : a &&& b ≤ b

theorem UInt32.and_le_right {a b : UInt32} : a &&& b ≤ b

theorem UInt64.and_le_right {a b : UInt64} : a &&& b ≤ b

theorem USize.and_le_right {a b : USize} : a &&& b ≤ b

theorem UInt8.and_le_left {a b : UInt8} : a &&& b ≤ a

theorem UInt16.and_le_left {a b : UInt16} : a &&& b ≤ a

theorem UInt32.and_le_left {a b : UInt32} : a &&& b ≤ a

theorem UInt64.and_le_left {a b : UInt64} : a &&& b ≤ a

theorem USize.and_le_left {a b : USize} : a &&& b ≤ a

theorem UInt8.left_le_or {a b : UInt8} : a ≤ a ||| b

theorem UInt16.left_le_or {a b : UInt16} : a ≤ a ||| b

theorem UInt32.left_le_or {a b : UInt32} : a ≤ a ||| b

theorem UInt64.left_le_or {a b : UInt64} : a ≤ a ||| b

theorem USize.left_le_or {a b : USize} : a ≤ a ||| b

theorem UInt8.right_le_or {a b : UInt8} : b ≤ a ||| b

theorem UInt16.right_le_or {a b : UInt16} : b ≤ a ||| b

theorem UInt32.right_le_or {a b : UInt32} : b ≤ a ||| b

theorem UInt64.right_le_or {a b : UInt64} : b ≤ a ||| b

theorem USize.right_le_or {a b : USize} : b ≤ a ||| b