Documentation

Init.Data.UInt.Bitwise

source
def commandDeclare_bitwise_uint_theorems__ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem UInt8.toBitVec_not {a : UInt8} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem UInt8.toBitVec_or (a b : UInt8) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt8.toNat_xor (a b : UInt8) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt8.toBitVec_and (a b : UInt8) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt8.toNat_or (a b : UInt8) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt8.toNat_shiftRight (a b : UInt8) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 8)
    source
    @[simp]
    theorem UInt8.toBitVec_shiftRight (a b : UInt8) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 8)
    source
    @[simp]
    theorem UInt8.toNat_shiftLeft (a b : UInt8) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 8) % 2 ^ 8
    source
    @[simp]
    theorem UInt8.toNat_and (a b : UInt8) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt8.toBitVec_xor (a b : UInt8) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt8.toBitVec_shiftLeft (a b : UInt8) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 8)
    source
    @[simp]
    theorem UInt16.toBitVec_shiftLeft (a b : UInt16) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 16)
    source
    @[simp]
    theorem UInt16.toNat_shiftRight (a b : UInt16) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 16)
    source
    @[simp]
    theorem UInt16.toNat_or (a b : UInt16) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt16.toBitVec_or (a b : UInt16) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt16.toNat_xor (a b : UInt16) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt16.toBitVec_and (a b : UInt16) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt16.toBitVec_shiftRight (a b : UInt16) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 16)
    source
    @[simp]
    theorem UInt16.toBitVec_not {a : UInt16} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem UInt16.toBitVec_xor (a b : UInt16) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt16.toNat_and (a b : UInt16) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt16.toNat_shiftLeft (a b : UInt16) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 16) % 2 ^ 16
    source
    @[simp]
    theorem UInt32.toBitVec_shiftRight (a b : UInt32) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 32)
    source
    @[simp]
    theorem UInt32.toNat_shiftRight (a b : UInt32) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 32)
    source
    @[simp]
    theorem UInt32.toNat_or (a b : UInt32) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt32.toBitVec_xor (a b : UInt32) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt32.toBitVec_not {a : UInt32} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_shiftLeft (a b : UInt32) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 32) % 2 ^ 32
    source
    @[simp]
    theorem UInt32.toBitVec_or (a b : UInt32) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_and (a b : UInt32) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt32.toBitVec_shiftLeft (a b : UInt32) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 32)
    source
    @[simp]
    theorem UInt32.toBitVec_and (a b : UInt32) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_xor (a b : UInt32) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_not {a : UInt64} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem UInt64.toBitVec_or (a b : UInt64) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt64.toNat_or (a b : UInt64) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_and (a b : UInt64) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt64.toNat_and (a b : UInt64) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt64.toNat_xor (a b : UInt64) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_shiftLeft (a b : UInt64) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 64)
    source
    @[simp]
    theorem UInt64.toNat_shiftRight (a b : UInt64) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 64)
    source
    @[simp]
    theorem UInt64.toBitVec_xor (a b : UInt64) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt64.toBitVec_shiftRight (a b : UInt64) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 64)
    source
    @[simp]
    theorem UInt64.toNat_shiftLeft (a b : UInt64) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 64) % 2 ^ 64
    source
    @[simp]
    theorem USize.toBitVec_shiftLeft (a b : USize) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % ↑System.Platform.numBits)
    source
    @[simp]
    theorem USize.toBitVec_or (a b : USize) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem USize.toNat_shiftLeft (a b : USize) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % System.Platform.numBits) % 2 ^ System.Platform.numBits
    source
    @[simp]
    theorem USize.toBitVec_xor (a b : USize) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem USize.toNat_shiftRight (a b : USize) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % System.Platform.numBits)
    source
    @[simp]
    theorem USize.toBitVec_shiftRight (a b : USize) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % ↑System.Platform.numBits)
    source
    @[simp]
    theorem USize.toNat_xor (a b : USize) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem USize.toNat_or (a b : USize) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem USize.toNat_and (a b : USize) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem USize.toBitVec_not {a : USize} :
    (~~~a).toBitVec = ~~~a.toBitVec
    source
    @[simp]
    theorem USize.toBitVec_and (a b : USize) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem Bool.toBitVec_toUInt8 {b : Bool} :
    b.toUInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toUInt16 {b : Bool} :
    b.toUInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toUInt32 {b : Bool} :
    b.toUInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toUInt64 {b : Bool} :
    b.toUInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)
    source
    @[simp]
    theorem Bool.toBitVec_toUSize {b : Bool} :
    b.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)
    source
    @[simp]
    theorem UInt8.toFin_and (a b : UInt8) :
    (a &&& b).toFin = a.toFin &&& b.toFin
    source
    @[simp]
    theorem UInt16.toFin_and (a b : UInt16) :
    (a &&& b).toFin = a.toFin &&& b.toFin
    source
    @[simp]
    theorem UInt32.toFin_and (a b : UInt32) :
    (a &&& b).toFin = a.toFin &&& b.toFin
    source
    @[simp]
    theorem UInt64.toFin_and (a b : UInt64) :
    (a &&& b).toFin = a.toFin &&& b.toFin
    source
    @[simp]
    theorem USize.toFin_and (a b : USize) :
    (a &&& b).toFin = a.toFin &&& b.toFin
    source
    @[simp]
    theorem UInt8.toUInt16_and (a b : UInt8) :
    (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
    source
    @[simp]
    theorem UInt8.toUInt32_and (a b : UInt8) :
    (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
    source
    @[simp]
    theorem UInt8.toUInt64_and (a b : UInt8) :
    (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
    source
    @[simp]
    theorem UInt8.toUSize_and (a b : UInt8) :
    (a &&& b).toUSize = a.toUSize &&& b.toUSize
    source
    @[simp]
    theorem UInt16.toUInt8_and (a b : UInt16) :
    (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
    source
    @[simp]
    theorem UInt16.toUInt32_and (a b : UInt16) :
    (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
    source
    @[simp]
    theorem UInt16.toUInt64_and (a b : UInt16) :
    (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
    source
    @[simp]
    theorem UInt16.toUSize_and (a b : UInt16) :
    (a &&& b).toUSize = a.toUSize &&& b.toUSize
    source
    @[simp]
    theorem UInt32.toUInt8_and (a b : UInt32) :
    (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt16_and (a b : UInt32) :
    (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
    source
    @[simp]
    theorem UInt32.toUInt64_and (a b : UInt32) :
    (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
    source
    @[simp]
    theorem UInt32.toUSize_and (a b : UInt32) :
    (a &&& b).toUSize = a.toUSize &&& b.toUSize
    source
    @[simp]
    theorem USize.toUInt8_and (a b : USize) :
    (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
    source
    @[simp]
    theorem USize.toUInt16_and (a b : USize) :
    (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
    source
    @[simp]
    theorem USize.toUInt32_and (a b : USize) :
    (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
    source
    @[simp]
    theorem USize.toUInt64_and (a b : USize) :
    (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
    source
    @[simp]
    theorem UInt64.toUInt8_and (a b : UInt64) :
    (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
    source
    @[simp]
    theorem UInt64.toUInt16_and (a b : UInt64) :
    (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
    source
    @[simp]
    theorem UInt64.toUInt32_and (a b : UInt64) :
    (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
    source
    @[simp]
    theorem UInt64.toUSize_and (a b : UInt64) :
    (a &&& b).toUSize = a.toUSize &&& b.toUSize
    source
    @[simp]
    theorem UInt8.toFin_or (a b : UInt8) :
    (a ||| b).toFin = a.toFin ||| b.toFin
    source
    @[simp]
    theorem UInt16.toFin_or (a b : UInt16) :
    (a ||| b).toFin = a.toFin ||| b.toFin
    source
    @[simp]
    theorem UInt32.toFin_or (a b : UInt32) :
    (a ||| b).toFin = a.toFin ||| b.toFin
    source
    @[simp]
    theorem UInt64.toFin_or (a b : UInt64) :
    (a ||| b).toFin = a.toFin ||| b.toFin
    source
    @[simp]
    theorem USize.toFin_or (a b : USize) :
    (a ||| b).toFin = a.toFin ||| b.toFin
    source
    @[simp]
    theorem UInt8.toUInt16_or (a b : UInt8) :
    (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
    source
    @[simp]
    theorem UInt8.toUInt32_or (a b : UInt8) :
    (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
    source
    @[simp]
    theorem UInt8.toUInt64_or (a b : UInt8) :
    (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
    source
    @[simp]
    theorem UInt8.toUSize_or (a b : UInt8) :
    (a ||| b).toUSize = a.toUSize ||| b.toUSize
    source
    @[simp]
    theorem UInt16.toUInt8_or (a b : UInt16) :
    (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
    source
    @[simp]
    theorem UInt16.toUInt32_or (a b : UInt16) :
    (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
    source
    @[simp]
    theorem UInt16.toUInt64_or (a b : UInt16) :
    (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
    source
    @[simp]
    theorem UInt16.toUSize_or (a b : UInt16) :
    (a ||| b).toUSize = a.toUSize ||| b.toUSize
    source
    @[simp]
    theorem UInt32.toUInt8_or (a b : UInt32) :
    (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt16_or (a b : UInt32) :
    (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
    source
    @[simp]
    theorem UInt32.toUInt64_or (a b : UInt32) :
    (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
    source
    @[simp]
    theorem UInt32.toUSize_or (a b : UInt32) :
    (a ||| b).toUSize = a.toUSize ||| b.toUSize
    source
    @[simp]
    theorem USize.toUInt8_or (a b : USize) :
    (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
    source
    @[simp]
    theorem USize.toUInt16_or (a b : USize) :
    (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
    source
    @[simp]
    theorem USize.toUInt32_or (a b : USize) :
    (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
    source
    @[simp]
    theorem USize.toUInt64_or (a b : USize) :
    (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
    source
    @[simp]
    theorem UInt64.toUInt8_or (a b : UInt64) :
    (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
    source
    @[simp]
    theorem UInt64.toUInt16_or (a b : UInt64) :
    (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
    source
    @[simp]
    theorem UInt64.toUInt32_or (a b : UInt64) :
    (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
    source
    @[simp]
    theorem UInt64.toUSize_or (a b : UInt64) :
    (a ||| b).toUSize = a.toUSize ||| b.toUSize
    source
    @[simp]
    theorem UInt8.toFin_xor (a b : UInt8) :
    (a ^^^ b).toFin = a.toFin ^^^ b.toFin
    source
    @[simp]
    theorem UInt16.toFin_xor (a b : UInt16) :
    (a ^^^ b).toFin = a.toFin ^^^ b.toFin
    source
    @[simp]
    theorem UInt32.toFin_xor (a b : UInt32) :
    (a ^^^ b).toFin = a.toFin ^^^ b.toFin
    source
    @[simp]
    theorem UInt64.toFin_xor (a b : UInt64) :
    (a ^^^ b).toFin = a.toFin ^^^ b.toFin
    source
    @[simp]
    theorem USize.toFin_xor (a b : USize) :
    (a ^^^ b).toFin = a.toFin ^^^ b.toFin
    source
    @[simp]
    theorem UInt8.toUInt16_xor (a b : UInt8) :
    (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
    source
    @[simp]
    theorem UInt8.toUInt32_xor (a b : UInt8) :
    (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
    source
    @[simp]
    theorem UInt8.toUInt64_xor (a b : UInt8) :
    (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
    source
    @[simp]
    theorem UInt8.toUSize_xor (a b : UInt8) :
    (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
    source
    @[simp]
    theorem UInt16.toUInt8_xor (a b : UInt16) :
    (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
    source
    @[simp]
    theorem UInt16.toUInt32_xor (a b : UInt16) :
    (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
    source
    @[simp]
    theorem UInt16.toUInt64_xor (a b : UInt16) :
    (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
    source
    @[simp]
    theorem UInt16.toUSize_xor (a b : UInt16) :
    (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
    source
    @[simp]
    theorem UInt32.toUInt8_xor (a b : UInt32) :
    (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt16_xor (a b : UInt32) :
    (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
    source
    @[simp]
    theorem UInt32.toUInt64_xor (a b : UInt32) :
    (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
    source
    @[simp]
    theorem UInt32.toUSize_xor (a b : UInt32) :
    (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
    source
    @[simp]
    theorem USize.toUInt8_xor (a b : USize) :
    (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
    source
    @[simp]
    theorem USize.toUInt16_xor (a b : USize) :
    (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
    source
    @[simp]
    theorem USize.toUInt32_xor (a b : USize) :
    (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
    source
    @[simp]
    theorem USize.toUInt64_xor (a b : USize) :
    (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
    source
    @[simp]
    theorem UInt64.toUInt8_xor (a b : UInt64) :
    (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
    source
    @[simp]
    theorem UInt64.toUInt16_xor (a b : UInt64) :
    (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
    source
    @[simp]
    theorem UInt64.toUInt32_xor (a b : UInt64) :
    (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
    source
    @[simp]
    theorem UInt64.toUSize_xor (a b : UInt64) :
    (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
    source
    @[simp]
    theorem UInt8.toNat_not (a : UInt8) :
    (~~~a).toNat = size - 1 - a.toNat
    source
    @[simp]
    theorem UInt16.toNat_not (a : UInt16) :
    (~~~a).toNat = size - 1 - a.toNat
    source
    @[simp]
    theorem UInt32.toNat_not (a : UInt32) :
    (~~~a).toNat = size - 1 - a.toNat
    source
    @[simp]
    theorem UInt64.toNat_not (a : UInt64) :
    (~~~a).toNat = size - 1 - a.toNat
    source
    @[simp]
    theorem USize.toNat_not (a : USize) :
    (~~~a).toNat = size - 1 - a.toNat
    source
    @[simp]
    theorem UInt8.toFin_not (a : UInt8) :
    (~~~a).toFin = a.toFin.rev
    source
    @[simp]
    theorem UInt16.toFin_not (a : UInt16) :
    (~~~a).toFin = a.toFin.rev
    source
    @[simp]
    theorem UInt32.toFin_not (a : UInt32) :
    (~~~a).toFin = a.toFin.rev
    source
    @[simp]
    theorem UInt64.toFin_not (a : UInt64) :
    (~~~a).toFin = a.toFin.rev
    source
    @[simp]
    theorem USize.toFin_not (a : USize) :
    (~~~a).toFin = a.toFin.rev
    source
    @[simp]
    theorem UInt16.toUInt8_not (a : UInt16) :
    (~~~a).toUInt8 = ~~~a.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt8_not (a : UInt32) :
    (~~~a).toUInt8 = ~~~a.toUInt8
    source
    @[simp]
    theorem UInt64.toUInt8_not (a : UInt64) :
    (~~~a).toUInt8 = ~~~a.toUInt8
    source
    @[simp]
    theorem USize.toUInt8_not (a : USize) :
    (~~~a).toUInt8 = ~~~a.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt16_not (a : UInt32) :
    (~~~a).toUInt16 = ~~~a.toUInt16
    source
    @[simp]
    theorem UInt64.toUInt16_not (a : UInt64) :
    (~~~a).toUInt16 = ~~~a.toUInt16
    source
    @[simp]
    theorem USize.toUInt16_not (a : USize) :
    (~~~a).toUInt16 = ~~~a.toUInt16
    source
    @[simp]
    theorem UInt64.toUInt32_not (a : UInt64) :
    (~~~a).toUInt32 = ~~~a.toUInt32
    source
    @[simp]
    theorem USize.toUInt32_not (a : USize) :
    (~~~a).toUInt32 = ~~~a.toUInt32
    source
    @[simp]
    theorem UInt64.toUSize_not (a : UInt64) :
    (~~~a).toUSize = ~~~a.toUSize
    source
    @[simp]
    theorem UInt8.toUInt16_not (a : UInt8) :
    (~~~a).toUInt16 = ~~~a.toUInt16 % 256
    source
    @[simp]
    theorem UInt8.toUInt32_not (a : UInt8) :
    (~~~a).toUInt32 = ~~~a.toUInt32 % 256
    source
    @[simp]
    theorem UInt8.toUInt64_not (a : UInt8) :
    (~~~a).toUInt64 = ~~~a.toUInt64 % 256
    source
    @[simp]
    theorem UInt8.toUSize_not (a : UInt8) :
    (~~~a).toUSize = ~~~a.toUSize % 256
    source
    @[simp]
    theorem UInt16.toUInt32_not (a : UInt16) :
    (~~~a).toUInt32 = ~~~a.toUInt32 % 65536
    source
    @[simp]
    theorem UInt16.toUInt64_not (a : UInt16) :
    (~~~a).toUInt64 = ~~~a.toUInt64 % 65536
    source
    @[simp]
    theorem UInt16.toUSize_not (a : UInt16) :
    (~~~a).toUSize = ~~~a.toUSize % 65536
    source
    @[simp]
    theorem UInt32.toUInt64_not (a : UInt32) :
    (~~~a).toUInt64 = ~~~a.toUInt64 % 4294967296
    source
    @[simp]
    theorem UInt32.toUSize_not (a : UInt32) :
    (~~~a).toUSize = ~~~a.toUSize % 4294967296
    source
    @[simp]
    theorem USize.toUInt64_not (a : USize) :
    (~~~a).toUInt64 = ~~~a.toUInt64 % UInt64.ofNat size
    source
    @[simp]
    theorem UInt8.toFin_shiftLeft (a b : UInt8) (hb : b < 8) :
    (a <<< b).toFin = a.toFin <<< b.toFin
    source
    @[simp]
    theorem UInt16.toFin_shiftLeft (a b : UInt16) (hb : b < 16) :
    (a <<< b).toFin = a.toFin <<< b.toFin
    source
    @[simp]
    theorem UInt32.toFin_shiftLeft (a b : UInt32) (hb : b < 32) :
    (a <<< b).toFin = a.toFin <<< b.toFin
    source
    @[simp]
    theorem UInt64.toFin_shiftLeft (a b : UInt64) (hb : b < 64) :
    (a <<< b).toFin = a.toFin <<< b.toFin
    source
    @[simp]
    theorem USize.toFin_shiftLeft (a b : USize) (hb : b.toNat < System.Platform.numBits) :
    (a <<< b).toFin = a.toFin <<< b.toFin
    source
    theorem UInt8.shiftLeft_eq_shiftLeft_mod (a b : UInt8) :
    a <<< b = a <<< (b % 8)
    source
    theorem UInt16.shiftLeft_eq_shiftLeft_mod (a b : UInt16) :
    a <<< b = a <<< (b % 16)
    source
    theorem UInt32.shiftLeft_eq_shiftLeft_mod (a b : UInt32) :
    a <<< b = a <<< (b % 32)
    source
    theorem UInt64.shiftLeft_eq_shiftLeft_mod (a b : UInt64) :
    a <<< b = a <<< (b % 64)
    source
    theorem USize.shiftLeft_eq_shiftLeft_mod (a b : USize) :
    a <<< b = a <<< (b % ofNat System.Platform.numBits)
    source
    theorem UInt8.shiftRight_eq_shiftRight_mod (a b : UInt8) :
    a >>> b = a >>> (b % 8)
    source
    theorem UInt16.shiftRight_eq_shiftRight_mod (a b : UInt16) :
    a >>> b = a >>> (b % 16)
    source
    theorem UInt32.shiftRight_eq_shiftRight_mod (a b : UInt32) :
    a >>> b = a >>> (b % 32)
    source
    theorem UInt64.shiftRight_eq_shiftRight_mod (a b : UInt64) :
    a >>> b = a >>> (b % 64)
    source
    theorem USize.shiftRight_eq_shiftRight_mod (a b : USize) :
    a >>> b = a >>> (b % ofNat System.Platform.numBits)
    source
    @[simp]
    theorem UInt16.toUInt8_shiftLeft (a b : UInt16) (hb : b < 8) :
    (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt8_shiftLeft (a b : UInt32) (hb : b < 8) :
    (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt16_shiftLeft (a b : UInt32) (hb : b < 16) :
    (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16
    source
    @[simp]
    theorem USize.toUInt8_shiftLeft (a b : USize) (hb : b < 8) :
    (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8
    source
    @[simp]
    theorem USize.toUInt16_shiftLeft (a b : USize) (hb : b < 16) :
    (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16
    source
    @[simp]
    theorem USize.toUInt32_shiftLeft (a b : USize) (hb : b < 32) :
    (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32
    source
    @[simp]
    theorem UInt64.toUInt8_shiftLeft (a b : UInt64) (hb : b < 8) :
    (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8
    source
    @[simp]
    theorem UInt64.toUInt16_shiftLeft (a b : UInt64) (hb : b < 16) :
    (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16
    source
    @[simp]
    theorem UInt64.toUInt32_shiftLeft (a b : UInt64) (hb : b < 32) :
    (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32
    source
    @[simp]
    theorem UInt64.toUSize_shiftLeft (a b : UInt64) (hb : b.toNat < System.Platform.numBits) :
    (a <<< b).toUSize = a.toUSize <<< b.toUSize
    source
    @[simp]
    theorem UInt16.toUInt8_shiftLeft_mod (a b : UInt16) :
    (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt8_shiftLeft_mod (a b : UInt32) :
    (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8
    source
    @[simp]
    theorem UInt32.toUInt16_shiftLeft_mod (a b : UInt32) :
    (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16
    source
    @[simp]
    theorem USize.toUInt8_shiftLeft_mod (a b : USize) :
    (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8
    source
    @[simp]
    theorem USize.toUInt16_shiftLeft_mod (a b : USize) :
    (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16
    source
    @[simp]
    theorem USize.toUInt32_shiftLeft_mod (a b : USize) :
    (a <<< (b % 32)).toUInt32 = a.toUInt32 <<< b.toUInt32
    source
    @[simp]
    theorem UInt64.toUInt8_shiftLeft_mod (a b : UInt64) :
    (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8
    source
    @[simp]
    theorem UInt64.toUInt16_shiftLeft_mod (a b : UInt64) :
    (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16
    source
    @[simp]
    theorem UInt64.toUInt32_shiftLeft_mod (a b : UInt64) :
    (a <<< (b % 32)).toUInt32 = a.toUInt32 <<< b.toUInt32
    source
    @[simp]
    theorem UInt64.toUSize_shiftLeft_mod (a b : UInt64) :
    (a <<< (b % ofNat System.Platform.numBits)).toUSize = a.toUSize <<< b.toUSize
    source
    theorem UInt8.toUInt16_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) :
    (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16 % 256
    source
    theorem UInt8.toUInt32_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) :
    (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32 % 256
    source
    theorem UInt8.toUInt64_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) :
    (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 256
    source
    theorem UInt8.toUSize_shiftLeft_of_lt (a b : UInt8) (hb : b < 8) :
    (a <<< b).toUSize = a.toUSize <<< b.toUSize % 256
    source
    theorem UInt16.toUInt32_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) :
    (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32 % 65536
    source
    theorem UInt16.toUInt64_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) :
    (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 65536
    source
    theorem UInt16.toUSize_shiftLeft_of_lt (a b : UInt16) (hb : b < 16) :
    (a <<< b).toUSize = a.toUSize <<< b.toUSize % 65536
    source
    theorem UInt32.toUInt64_shiftLeft_of_lt (a b : UInt32) (hb : b < 32) :
    (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 4294967296
    source
    theorem UInt32.toUSize_shiftLeft_of_lt (a b : UInt32) (hb : b < 32) :
    (a <<< b).toUSize = a.toUSize <<< b.toUSize % 4294967296
    source
    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
    source
    @[simp]
    theorem UInt8.toUInt16_shiftLeft (a b : UInt8) :
    (a <<< b).toUInt16 = a.toUInt16 <<< (b % 8).toUInt16 % 256
    source
    @[simp]
    theorem UInt8.toUInt32_shiftLeft (a b : UInt8) :
    (a <<< b).toUInt32 = a.toUInt32 <<< (b % 8).toUInt32 % 256
    source
    @[simp]
    theorem UInt8.toUInt64_shiftLeft (a b : UInt8) :
    (a <<< b).toUInt64 = a.toUInt64 <<< (b % 8).toUInt64 % 256
    source
    @[simp]
    theorem UInt8.toUSize_shiftLeft (a b : UInt8) :
    (a <<< b).toUSize = a.toUSize <<< (b % 8).toUSize % 256
    source
    @[simp]
    theorem UInt16.toUInt32_shiftLeft (a b : UInt16) :
    (a <<< b).toUInt32 = a.toUInt32 <<< (b % 16).toUInt32 % 65536
    source
    @[simp]
    theorem UInt16.toUInt64_shiftLeft (a b : UInt16) :
    (a <<< b).toUInt64 = a.toUInt64 <<< (b % 16).toUInt64 % 65536
    source
    @[simp]
    theorem UInt16.toUSize_shiftLeft (a b : UInt16) :
    (a <<< b).toUSize = a.toUSize <<< (b % 16).toUSize % 65536
    source
    @[simp]
    theorem UInt32.toUInt64_shiftLeft (a b : UInt32) :
    (a <<< b).toUInt64 = a.toUInt64 <<< (b % 32).toUInt64 % 4294967296
    source
    @[simp]
    theorem UInt32.toUSize_shiftLeft (a b : UInt32) :
    (a <<< b).toUSize = a.toUSize <<< (b % 32).toUSize % 4294967296
    source
    @[simp]
    theorem USize.toUInt64_shiftLeft (a b : USize) :
    (a <<< b).toUInt64 = a.toUInt64 <<< (b % ofNat System.Platform.numBits).toUInt64 % UInt64.ofNat size
    source
    @[simp]
    theorem UInt8.toFin_shiftRight (a b : UInt8) (hb : b < 8) :
    (a >>> b).toFin = a.toFin >>> b.toFin
    source
    @[simp]
    theorem UInt16.toFin_shiftRight (a b : UInt16) (hb : b < 16) :
    (a >>> b).toFin = a.toFin >>> b.toFin
    source
    @[simp]
    theorem UInt32.toFin_shiftRight (a b : UInt32) (hb : b < 32) :
    (a >>> b).toFin = a.toFin >>> b.toFin
    source
    @[simp]
    theorem UInt64.toFin_shiftRight (a b : UInt64) (hb : b < 64) :
    (a >>> b).toFin = a.toFin >>> b.toFin
    source
    @[simp]
    theorem USize.toFin_shiftRight (a b : USize) (hb : b.toNat < System.Platform.numBits) :
    (a >>> b).toFin = a.toFin >>> b.toFin
    source
    @[simp]
    theorem UInt8.toUInt16_shiftRight (a b : UInt8) :
    (a >>> b).toUInt16 = a.toUInt16 >>> (b.toUInt16 % 8)
    source
    @[simp]
    theorem UInt8.toUInt32_shiftRight (a b : UInt8) :
    (a >>> b).toUInt32 = a.toUInt32 >>> (b.toUInt32 % 8)
    source
    @[simp]
    theorem UInt8.toUInt64_shiftRight (a b : UInt8) :
    (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 8)
    source
    @[simp]
    theorem UInt8.toUSize_shiftRight (a b : UInt8) :
    (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 8)
    source
    @[simp]
    theorem UInt16.toUInt32_shiftRight (a b : UInt16) :
    (a >>> b).toUInt32 = a.toUInt32 >>> (b.toUInt32 % 16)
    source
    @[simp]
    theorem UInt16.toUInt64_shiftRight (a b : UInt16) :
    (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 16)
    source
    @[simp]
    theorem UInt16.toUSize_shiftRight (a b : UInt16) :
    (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 16)
    source
    @[simp]
    theorem UInt32.toUInt64_shiftRight (a b : UInt32) :
    (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 32)
    source
    @[simp]
    theorem UInt32.toUSize_shiftRight (a b : UInt32) :
    (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 32)
    source
    @[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.

    source
    @[simp]
    theorem UInt8.ofFin_and (a b : Fin size) :
    ofFin (a &&& b) = ofFin a &&& ofFin b
    source
    @[simp]
    theorem UInt16.ofFin_and (a b : Fin size) :
    ofFin (a &&& b) = ofFin a &&& ofFin b
    source
    @[simp]
    theorem UInt32.ofFin_and (a b : Fin size) :
    ofFin (a &&& b) = ofFin a &&& ofFin b
    source
    @[simp]
    theorem UInt64.ofFin_and (a b : Fin size) :
    ofFin (a &&& b) = ofFin a &&& ofFin b
    source
    @[simp]
    theorem USize.ofFin_and (a b : Fin size) :
    ofFin (a &&& b) = ofFin a &&& ofFin b
    source
    @[simp]
    theorem UInt8.ofBitVec_and (a b : BitVec 8) :
    { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
    source
    @[simp]
    theorem UInt16.ofBitVec_and (a b : BitVec 16) :
    { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
    source
    @[simp]
    theorem UInt32.ofBitVec_and (a b : BitVec 32) :
    { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
    source
    @[simp]
    theorem UInt64.ofBitVec_and (a b : BitVec 64) :
    { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
    source
    @[simp]
    theorem USize.ofBitVec_and (a b : BitVec System.Platform.numBits) :
    { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
    source
    @[simp]
    theorem UInt8.ofNat_and (a b : Nat) :
    ofNat (a &&& b) = ofNat a &&& ofNat b
    source
    @[simp]
    theorem UInt16.ofNat_and (a b : Nat) :
    ofNat (a &&& b) = ofNat a &&& ofNat b
    source
    @[simp]
    theorem UInt32.ofNat_and (a b : Nat) :
    ofNat (a &&& b) = ofNat a &&& ofNat b
    source
    @[simp]
    theorem UInt64.ofNat_and (a b : Nat) :
    ofNat (a &&& b) = ofNat a &&& ofNat b
    source
    @[simp]
    theorem USize.ofNat_and (a b : Nat) :
    ofNat (a &&& b) = ofNat a &&& ofNat b
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem UInt8.ofFin_or (a b : Fin size) :
    ofFin (a ||| b) = ofFin a ||| ofFin b
    source
    @[simp]
    theorem UInt16.ofFin_or (a b : Fin size) :
    ofFin (a ||| b) = ofFin a ||| ofFin b
    source
    @[simp]
    theorem UInt32.ofFin_or (a b : Fin size) :
    ofFin (a ||| b) = ofFin a ||| ofFin b
    source
    @[simp]
    theorem UInt64.ofFin_or (a b : Fin size) :
    ofFin (a ||| b) = ofFin a ||| ofFin b
    source
    @[simp]
    theorem USize.ofFin_or (a b : Fin size) :
    ofFin (a ||| b) = ofFin a ||| ofFin b
    source
    @[simp]
    theorem UInt8.ofBitVec_or (a b : BitVec 8) :
    { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
    source
    @[simp]
    theorem UInt16.ofBitVec_or (a b : BitVec 16) :
    { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
    source
    @[simp]
    theorem UInt32.ofBitVec_or (a b : BitVec 32) :
    { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
    source
    @[simp]
    theorem UInt64.ofBitVec_or (a b : BitVec 64) :
    { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
    source
    @[simp]
    theorem USize.ofBitVec_or (a b : BitVec System.Platform.numBits) :
    { toBitVec := a ||| b } = { toBitVec := a } ||| { toBitVec := b }
    source
    @[simp]
    theorem UInt8.ofNat_or (a b : Nat) :
    ofNat (a ||| b) = ofNat a ||| ofNat b
    source
    @[simp]
    theorem UInt16.ofNat_or (a b : Nat) :
    ofNat (a ||| b) = ofNat a ||| ofNat b
    source
    @[simp]
    theorem UInt32.ofNat_or (a b : Nat) :
    ofNat (a ||| b) = ofNat a ||| ofNat b
    source
    @[simp]
    theorem UInt64.ofNat_or (a b : Nat) :
    ofNat (a ||| b) = ofNat a ||| ofNat b
    source
    @[simp]
    theorem USize.ofNat_or (a b : Nat) :
    ofNat (a ||| b) = ofNat a ||| ofNat b
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem UInt8.ofFin_xor (a b : Fin size) :
    ofFin (a ^^^ b) = ofFin a ^^^ ofFin b
    source
    @[simp]
    theorem UInt16.ofFin_xor (a b : Fin size) :
    ofFin (a ^^^ b) = ofFin a ^^^ ofFin b
    source
    @[simp]
    theorem UInt32.ofFin_xor (a b : Fin size) :
    ofFin (a ^^^ b) = ofFin a ^^^ ofFin b
    source
    @[simp]
    theorem UInt64.ofFin_xor (a b : Fin size) :
    ofFin (a ^^^ b) = ofFin a ^^^ ofFin b
    source
    @[simp]
    theorem USize.ofFin_xor (a b : Fin size) :
    ofFin (a ^^^ b) = ofFin a ^^^ ofFin b
    source
    @[simp]
    theorem UInt8.ofBitVec_xor (a b : BitVec 8) :
    { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
    source
    @[simp]
    theorem UInt16.ofBitVec_xor (a b : BitVec 16) :
    { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
    source
    @[simp]
    theorem UInt32.ofBitVec_xor (a b : BitVec 32) :
    { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
    source
    @[simp]
    theorem UInt64.ofBitVec_xor (a b : BitVec 64) :
    { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
    source
    @[simp]
    theorem USize.ofBitVec_xor (a b : BitVec System.Platform.numBits) :
    { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
    source
    @[simp]
    theorem UInt8.ofNat_xor (a b : Nat) :
    ofNat (a ^^^ b) = ofNat a ^^^ ofNat b
    source
    @[simp]
    theorem UInt16.ofNat_xor (a b : Nat) :
    ofNat (a ^^^ b) = ofNat a ^^^ ofNat b
    source
    @[simp]
    theorem UInt32.ofNat_xor (a b : Nat) :
    ofNat (a ^^^ b) = ofNat a ^^^ ofNat b
    source
    @[simp]
    theorem UInt64.ofNat_xor (a b : Nat) :
    ofNat (a ^^^ b) = ofNat a ^^^ ofNat b
    source
    @[simp]
    theorem USize.ofNat_xor (a b : Nat) :
    ofNat (a ^^^ b) = ofNat a ^^^ ofNat b
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem UInt8.ofBitVec_not (a : BitVec 8) :
    { toBitVec := ~~~a } = ~~~{ toBitVec := a }
    source
    @[simp]
    theorem UInt16.ofBitVec_not (a : BitVec 16) :
    { toBitVec := ~~~a } = ~~~{ toBitVec := a }
    source
    @[simp]
    theorem UInt32.ofBitVec_not (a : BitVec 32) :
    { toBitVec := ~~~a } = ~~~{ toBitVec := a }
    source
    @[simp]
    theorem UInt64.ofBitVec_not (a : BitVec 64) :
    { toBitVec := ~~~a } = ~~~{ toBitVec := a }
    source
    @[simp]
    theorem USize.ofBitVec_not (a : BitVec System.Platform.numBits) :
    { toBitVec := ~~~a } = ~~~{ toBitVec := a }
    source
    @[simp]
    theorem UInt8.ofFin_rev (a : Fin size) :
    ofFin a.rev = ~~~ofFin a
    source
    @[simp]
    theorem UInt16.ofFin_rev (a : Fin size) :
    ofFin a.rev = ~~~ofFin a
    source
    @[simp]
    theorem UInt32.ofFin_rev (a : Fin size) :
    ofFin a.rev = ~~~ofFin a
    source
    @[simp]
    theorem UInt64.ofFin_rev (a : Fin size) :
    ofFin a.rev = ~~~ofFin a
    source
    @[simp]
    theorem USize.ofFin_rev (a : Fin size) :
    ofFin a.rev = ~~~ofFin a
    source
    @[simp]
    theorem UInt8.ofBitVec_shiftLeft (a : BitVec 8) (b : Nat) (hb : b < 8) :
    { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem UInt16.ofBitVec_shiftLeft (a : BitVec 16) (b : Nat) (hb : b < 16) :
    { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem UInt32.ofBitVec_shiftLeft (a : BitVec 32) (b : Nat) (hb : b < 32) :
    { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem UInt64.ofBitVec_shiftLeft (a : BitVec 64) (b : Nat) (hb : b < 64) :
    { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem USize.ofBitVec_shiftLeft (a : BitVec System.Platform.numBits) (b : Nat) (hb : b < System.Platform.numBits) :
    { toBitVec := a <<< b } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem UInt8.ofBitVec_shiftLeft_mod (a : BitVec 8) (b : Nat) :
    { toBitVec := a <<< (b % 8) } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem UInt16.ofBitVec_shiftLeft_mod (a : BitVec 16) (b : Nat) :
    { toBitVec := a <<< (b % 16) } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem UInt32.ofBitVec_shiftLeft_mod (a : BitVec 32) (b : Nat) :
    { toBitVec := a <<< (b % 32) } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem UInt64.ofBitVec_shiftLeft_mod (a : BitVec 64) (b : Nat) :
    { toBitVec := a <<< (b % 64) } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem USize.ofBitVec_shiftLeft_mod (a : BitVec System.Platform.numBits) (b : Nat) :
    { toBitVec := a <<< (b % System.Platform.numBits) } = { toBitVec := a } <<< ofNat b
    source
    @[simp]
    theorem UInt8.ofFin_shiftLeft (a b : Fin size) (hb : ↑b < 8) :
    ofFin (a <<< b) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem UInt16.ofFin_shiftLeft (a b : Fin size) (hb : ↑b < 16) :
    ofFin (a <<< b) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem UInt32.ofFin_shiftLeft (a b : Fin size) (hb : ↑b < 32) :
    ofFin (a <<< b) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem UInt64.ofFin_shiftLeft (a b : Fin size) (hb : ↑b < 64) :
    ofFin (a <<< b) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem USize.ofFin_shiftLeft (a b : Fin size) (hb : ↑b < System.Platform.numBits) :
    ofFin (a <<< b) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem UInt8.ofFin_shiftLeft_mod (a b : Fin size) :
    ofFin (a <<< (b % 8)) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem UInt16.ofFin_shiftLeft_mod (a b : Fin size) :
    ofFin (a <<< (b % 16)) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem UInt32.ofFin_shiftLeft_mod (a b : Fin size) :
    ofFin (a <<< (b % 32)) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem UInt64.ofFin_shiftLeft_mod (a b : Fin size) :
    ofFin (a <<< (b % 64)) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem USize.ofFin_shiftLeft_mod (a b : Fin size) :
    ofFin (a <<< (b % ⟨System.Platform.numBits, ofFin_shiftLeft_mod._proof_1⟩)) = ofFin a <<< ofFin b
    source
    @[simp]
    theorem UInt8.ofNat_shiftLeft (a b : Nat) (hb : b < 8) :
    ofNat (a <<< b) = ofNat a <<< ofNat b
    source
    @[simp]
    theorem UInt16.ofNat_shiftLeft (a b : Nat) (hb : b < 16) :
    ofNat (a <<< b) = ofNat a <<< ofNat b
    source
    @[simp]
    theorem UInt32.ofNat_shiftLeft (a b : Nat) (hb : b < 32) :
    ofNat (a <<< b) = ofNat a <<< ofNat b
    source
    @[simp]
    theorem UInt64.ofNat_shiftLeft (a b : Nat) (hb : b < 64) :
    ofNat (a <<< b) = ofNat a <<< ofNat b
    source
    @[simp]
    theorem USize.ofNat_shiftLeft (a b : Nat) (hb : b < System.Platform.numBits) :
    ofNat (a <<< b) = ofNat a <<< ofNat b
    source
    @[simp]
    theorem UInt8.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < 8) :
    ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯
    source
    @[simp]
    theorem UInt16.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < 16) :
    ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯
    source
    @[simp]
    theorem UInt32.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < 32) :
    ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯
    source
    @[simp]
    theorem UInt64.ofNatLT_shiftLeft {a b : Nat} (ha : a <<< b < size) (hb : b < 64) :
    ofNatLT (a <<< b) ha = ofNatLT a ⋯ <<< ofNatLT b ⋯
    source
    @[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 ⋯
    source
    @[simp]
    theorem UInt8.ofBitVec_shiftRight (a : BitVec 8) (b : Nat) (hb : b < 8) :
    { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem UInt16.ofBitVec_shiftRight (a : BitVec 16) (b : Nat) (hb : b < 16) :
    { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem UInt32.ofBitVec_shiftRight (a : BitVec 32) (b : Nat) (hb : b < 32) :
    { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem UInt64.ofBitVec_shiftRight (a : BitVec 64) (b : Nat) (hb : b < 64) :
    { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem USize.ofBitVec_shiftRight (a : BitVec System.Platform.numBits) (b : Nat) (hb : b < System.Platform.numBits) :
    { toBitVec := a >>> b } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem UInt8.ofBitVec_shiftRight_mod (a : BitVec 8) (b : Nat) :
    { toBitVec := a >>> (b % 8) } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem UInt16.ofBitVec_shiftRight_mod (a : BitVec 16) (b : Nat) :
    { toBitVec := a >>> (b % 16) } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem UInt32.ofBitVec_shiftRight_mod (a : BitVec 32) (b : Nat) :
    { toBitVec := a >>> (b % 32) } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem UInt64.ofBitVec_shiftRight_mod (a : BitVec 64) (b : Nat) :
    { toBitVec := a >>> (b % 64) } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem USize.ofBitVec_shiftRight_mod (a : BitVec System.Platform.numBits) (b : Nat) :
    { toBitVec := a >>> (b % System.Platform.numBits) } = { toBitVec := a } >>> ofNat b
    source
    @[simp]
    theorem UInt8.ofFin_shiftRight (a b : Fin size) (hb : ↑b < 8) :
    ofFin (a >>> b) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem UInt16.ofFin_shiftRight (a b : Fin size) (hb : ↑b < 16) :
    ofFin (a >>> b) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem UInt32.ofFin_shiftRight (a b : Fin size) (hb : ↑b < 32) :
    ofFin (a >>> b) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem UInt64.ofFin_shiftRight (a b : Fin size) (hb : ↑b < 64) :
    ofFin (a >>> b) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem USize.ofFin_shiftRight (a b : Fin size) (hb : ↑b < System.Platform.numBits) :
    ofFin (a >>> b) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem UInt8.ofFin_shiftRight_mod (a b : Fin size) :
    ofFin (a >>> (b % 8)) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem UInt16.ofFin_shiftRight_mod (a b : Fin size) :
    ofFin (a >>> (b % 16)) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem UInt32.ofFin_shiftRight_mod (a b : Fin size) :
    ofFin (a >>> (b % 32)) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem UInt64.ofFin_shiftRight_mod (a b : Fin size) :
    ofFin (a >>> (b % 64)) = ofFin a >>> ofFin b
    source
    @[simp]
    theorem USize.ofFin_shiftRight_mod (a b : Fin size) :
    ofFin (a >>> (b % ⟨System.Platform.numBits, ofFin_shiftLeft_mod._proof_1⟩)) = ofFin a >>> ofFin b
    source
    theorem UInt8.neg_eq_not_add (a : UInt8) :
    -a = ~~~a + 1
    source
    theorem UInt16.neg_eq_not_add (a : UInt16) :
    -a = ~~~a + 1
    source
    theorem UInt32.neg_eq_not_add (a : UInt32) :
    -a = ~~~a + 1
    source
    theorem UInt64.neg_eq_not_add (a : UInt64) :
    -a = ~~~a + 1
    source
    theorem USize.neg_eq_not_add (a : USize) :
    -a = ~~~a + 1
    source
    theorem UInt8.not_eq_neg_sub (a : UInt8) :
    ~~~a = -a - 1
    source
    theorem UInt16.not_eq_neg_sub (a : UInt16) :
    ~~~a = -a - 1
    source
    theorem UInt32.not_eq_neg_sub (a : UInt32) :
    ~~~a = -a - 1
    source
    theorem UInt64.not_eq_neg_sub (a : UInt64) :
    ~~~a = -a - 1
    source
    theorem USize.not_eq_neg_sub (a : USize) :
    ~~~a = -a - 1
    source
    theorem UInt8.or_assoc (a b c : UInt8) :
    a ||| b ||| c = a ||| (b ||| c)
    source
    theorem UInt16.or_assoc (a b c : UInt16) :
    a ||| b ||| c = a ||| (b ||| c)
    source
    theorem UInt32.or_assoc (a b c : UInt32) :
    a ||| b ||| c = a ||| (b ||| c)
    source
    theorem UInt64.or_assoc (a b c : UInt64) :
    a ||| b ||| c = a ||| (b ||| c)
    source
    theorem USize.or_assoc (a b c : USize) :
    a ||| b ||| c = a ||| (b ||| c)
    source
    instance instAssociativeUInt8HOr :
    Std.Associative fun (x1 x2 : UInt8) => x1 ||| x2
    source
    instance instAssociativeUInt16HOr :
    Std.Associative fun (x1 x2 : UInt16) => x1 ||| x2
    source
    instance instAssociativeUInt32HOr :
    Std.Associative fun (x1 x2 : UInt32) => x1 ||| x2
    source
    instance instAssociativeUInt64HOr :
    Std.Associative fun (x1 x2 : UInt64) => x1 ||| x2
    source
    instance instAssociativeUSizeHOr :
    Std.Associative fun (x1 x2 : USize) => x1 ||| x2
    source
    theorem UInt8.or_comm (a b : UInt8) :
    a ||| b = b ||| a
    source
    theorem UInt16.or_comm (a b : UInt16) :
    a ||| b = b ||| a
    source
    theorem UInt32.or_comm (a b : UInt32) :
    a ||| b = b ||| a
    source
    theorem UInt64.or_comm (a b : UInt64) :
    a ||| b = b ||| a
    source
    theorem USize.or_comm (a b : USize) :
    a ||| b = b ||| a
    source
    instance instCommutativeUInt8HOr :
    Std.Commutative fun (x1 x2 : UInt8) => x1 ||| x2
    source
    instance instCommutativeUInt16HOr :
    Std.Commutative fun (x1 x2 : UInt16) => x1 ||| x2
    source
    instance instCommutativeUInt32HOr :
    Std.Commutative fun (x1 x2 : UInt32) => x1 ||| x2
    source
    instance instCommutativeUInt64HOr :
    Std.Commutative fun (x1 x2 : UInt64) => x1 ||| x2
    source
    instance instCommutativeUSizeHOr :
    Std.Commutative fun (x1 x2 : USize) => x1 ||| x2
    source
    @[simp]
    theorem UInt8.or_self {a : UInt8} :
    a ||| a = a
    source
    @[simp]
    theorem UInt16.or_self {a : UInt16} :
    a ||| a = a
    source
    @[simp]
    theorem UInt32.or_self {a : UInt32} :
    a ||| a = a
    source
    @[simp]
    theorem UInt64.or_self {a : UInt64} :
    a ||| a = a
    source
    @[simp]
    theorem USize.or_self {a : USize} :
    a ||| a = a
    source
    instance instIdempotentOpUInt8HOr :
    Std.IdempotentOp fun (x1 x2 : UInt8) => x1 ||| x2
    source
    instance instIdempotentOpUInt16HOr :
    Std.IdempotentOp fun (x1 x2 : UInt16) => x1 ||| x2
    source
    instance instIdempotentOpUInt32HOr :
    Std.IdempotentOp fun (x1 x2 : UInt32) => x1 ||| x2
    source
    instance instIdempotentOpUInt64HOr :
    Std.IdempotentOp fun (x1 x2 : UInt64) => x1 ||| x2
    source
    instance instIdempotentOpUSizeHOr :
    Std.IdempotentOp fun (x1 x2 : USize) => x1 ||| x2
    source
    @[simp]
    theorem UInt8.or_zero {a : UInt8} :
    a ||| 0 = a
    source
    @[simp]
    theorem UInt16.or_zero {a : UInt16} :
    a ||| 0 = a
    source
    @[simp]
    theorem UInt32.or_zero {a : UInt32} :
    a ||| 0 = a
    source
    @[simp]
    theorem UInt64.or_zero {a : UInt64} :
    a ||| 0 = a
    source
    @[simp]
    theorem USize.or_zero {a : USize} :
    a ||| 0 = a
    source
    @[simp]
    theorem UInt8.zero_or {a : UInt8} :
    0 ||| a = a
    source
    @[simp]
    theorem UInt16.zero_or {a : UInt16} :
    0 ||| a = a
    source
    @[simp]
    theorem UInt32.zero_or {a : UInt32} :
    0 ||| a = a
    source
    @[simp]
    theorem UInt64.zero_or {a : UInt64} :
    0 ||| a = a
    source
    @[simp]
    theorem USize.zero_or {a : USize} :
    0 ||| a = a
    source
    instance instLawfulCommIdentityUInt8HOrOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => x1 ||| x2) 0
    source
    instance instLawfulCommIdentityUInt16HOrOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => x1 ||| x2) 0
    source
    instance instLawfulCommIdentityUInt32HOrOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => x1 ||| x2) 0
    source
    instance instLawfulCommIdentityUInt64HOrOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => x1 ||| x2) 0
    source
    instance instLawfulCommIdentityUSizeHOrOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : USize) => x1 ||| x2) 0
    source
    @[simp]
    theorem UInt8.neg_one_or {a : UInt8} :
    -1 ||| a = -1
    source
    @[simp]
    theorem UInt16.neg_one_or {a : UInt16} :
    -1 ||| a = -1
    source
    @[simp]
    theorem UInt32.neg_one_or {a : UInt32} :
    -1 ||| a = -1
    source
    @[simp]
    theorem UInt64.neg_one_or {a : UInt64} :
    -1 ||| a = -1
    source
    @[simp]
    theorem USize.neg_one_or {a : USize} :
    -1 ||| a = -1
    source
    @[simp]
    theorem UInt8.or_neg_one {a : UInt8} :
    a ||| -1 = -1
    source
    @[simp]
    theorem UInt16.or_neg_one {a : UInt16} :
    a ||| -1 = -1
    source
    @[simp]
    theorem UInt32.or_neg_one {a : UInt32} :
    a ||| -1 = -1
    source
    @[simp]
    theorem UInt64.or_neg_one {a : UInt64} :
    a ||| -1 = -1
    source
    @[simp]
    theorem USize.or_neg_one {a : USize} :
    a ||| -1 = -1
    source
    @[simp]
    theorem UInt8.or_eq_zero_iff {a b : UInt8} :
    a ||| b = 0 ↔ a = 0 ∧ b = 0
    source
    @[simp]
    theorem UInt16.or_eq_zero_iff {a b : UInt16} :
    a ||| b = 0 ↔ a = 0 ∧ b = 0
    source
    @[simp]
    theorem UInt32.or_eq_zero_iff {a b : UInt32} :
    a ||| b = 0 ↔ a = 0 ∧ b = 0
    source
    @[simp]
    theorem UInt64.or_eq_zero_iff {a b : UInt64} :
    a ||| b = 0 ↔ a = 0 ∧ b = 0
    source
    @[simp]
    theorem USize.or_eq_zero_iff {a b : USize} :
    a ||| b = 0 ↔ a = 0 ∧ b = 0
    source
    theorem UInt8.and_assoc (a b c : UInt8) :
    a &&& b &&& c = a &&& (b &&& c)
    source
    theorem UInt16.and_assoc (a b c : UInt16) :
    a &&& b &&& c = a &&& (b &&& c)
    source
    theorem UInt32.and_assoc (a b c : UInt32) :
    a &&& b &&& c = a &&& (b &&& c)
    source
    theorem UInt64.and_assoc (a b c : UInt64) :
    a &&& b &&& c = a &&& (b &&& c)
    source
    theorem USize.and_assoc (a b c : USize) :
    a &&& b &&& c = a &&& (b &&& c)
    source
    instance instAssociativeUInt8HAnd :
    Std.Associative fun (x1 x2 : UInt8) => x1 &&& x2
    source
    instance instAssociativeUInt16HAnd :
    Std.Associative fun (x1 x2 : UInt16) => x1 &&& x2
    source
    instance instAssociativeUInt32HAnd :
    Std.Associative fun (x1 x2 : UInt32) => x1 &&& x2
    source
    instance instAssociativeUInt64HAnd :
    Std.Associative fun (x1 x2 : UInt64) => x1 &&& x2
    source
    instance instAssociativeUSizeHAnd :
    Std.Associative fun (x1 x2 : USize) => x1 &&& x2
    source
    theorem UInt8.and_comm (a b : UInt8) :
    a &&& b = b &&& a
    source
    theorem UInt16.and_comm (a b : UInt16) :
    a &&& b = b &&& a
    source
    theorem UInt32.and_comm (a b : UInt32) :
    a &&& b = b &&& a
    source
    theorem UInt64.and_comm (a b : UInt64) :
    a &&& b = b &&& a
    source
    theorem USize.and_comm (a b : USize) :
    a &&& b = b &&& a
    source
    instance instCommutativeUInt8HAnd :
    Std.Commutative fun (x1 x2 : UInt8) => x1 &&& x2
    source
    instance instCommutativeUInt16HAnd :
    Std.Commutative fun (x1 x2 : UInt16) => x1 &&& x2
    source
    instance instCommutativeUInt32HAnd :
    Std.Commutative fun (x1 x2 : UInt32) => x1 &&& x2
    source
    instance instCommutativeUInt64HAnd :
    Std.Commutative fun (x1 x2 : UInt64) => x1 &&& x2
    source
    instance instCommutativeUSizeHAnd :
    Std.Commutative fun (x1 x2 : USize) => x1 &&& x2
    source
    @[simp]
    theorem UInt8.and_self {a : UInt8} :
    a &&& a = a
    source
    @[simp]
    theorem UInt16.and_self {a : UInt16} :
    a &&& a = a
    source
    @[simp]
    theorem UInt32.and_self {a : UInt32} :
    a &&& a = a
    source
    @[simp]
    theorem UInt64.and_self {a : UInt64} :
    a &&& a = a
    source
    @[simp]
    theorem USize.and_self {a : USize} :
    a &&& a = a
    source
    instance instIdempotentOpUInt8HAnd :
    Std.IdempotentOp fun (x1 x2 : UInt8) => x1 &&& x2
    source
    instance instIdempotentOpUInt16HAnd :
    Std.IdempotentOp fun (x1 x2 : UInt16) => x1 &&& x2
    source
    instance instIdempotentOpUInt32HAnd :
    Std.IdempotentOp fun (x1 x2 : UInt32) => x1 &&& x2
    source
    instance instIdempotentOpUInt64HAnd :
    Std.IdempotentOp fun (x1 x2 : UInt64) => x1 &&& x2
    source
    instance instIdempotentOpUSizeHAnd :
    Std.IdempotentOp fun (x1 x2 : USize) => x1 &&& x2
    source
    @[simp]
    theorem UInt8.and_zero {a : UInt8} :
    a &&& 0 = 0
    source
    @[simp]
    theorem UInt16.and_zero {a : UInt16} :
    a &&& 0 = 0
    source
    @[simp]
    theorem UInt32.and_zero {a : UInt32} :
    a &&& 0 = 0
    source
    @[simp]
    theorem UInt64.and_zero {a : UInt64} :
    a &&& 0 = 0
    source
    @[simp]
    theorem USize.and_zero {a : USize} :
    a &&& 0 = 0
    source
    @[simp]
    theorem UInt8.zero_and {a : UInt8} :
    0 &&& a = 0
    source
    @[simp]
    theorem UInt16.zero_and {a : UInt16} :
    0 &&& a = 0
    source
    @[simp]
    theorem UInt32.zero_and {a : UInt32} :
    0 &&& a = 0
    source
    @[simp]
    theorem UInt64.zero_and {a : UInt64} :
    0 &&& a = 0
    source
    @[simp]
    theorem USize.zero_and {a : USize} :
    0 &&& a = 0
    source
    @[simp]
    theorem UInt8.neg_one_and {a : UInt8} :
    -1 &&& a = a
    source
    @[simp]
    theorem UInt16.neg_one_and {a : UInt16} :
    -1 &&& a = a
    source
    @[simp]
    theorem UInt32.neg_one_and {a : UInt32} :
    -1 &&& a = a
    source
    @[simp]
    theorem UInt64.neg_one_and {a : UInt64} :
    -1 &&& a = a
    source
    @[simp]
    theorem USize.neg_one_and {a : USize} :
    -1 &&& a = a
    source
    @[simp]
    theorem UInt8.and_neg_one {a : UInt8} :
    a &&& -1 = a
    source
    @[simp]
    theorem UInt16.and_neg_one {a : UInt16} :
    a &&& -1 = a
    source
    @[simp]
    theorem UInt32.and_neg_one {a : UInt32} :
    a &&& -1 = a
    source
    @[simp]
    theorem UInt64.and_neg_one {a : UInt64} :
    a &&& -1 = a
    source
    @[simp]
    theorem USize.and_neg_one {a : USize} :
    a &&& -1 = a
    source
    instance instLawfulCommIdentityUInt8HAndNegOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => x1 &&& x2) (-1)
    source
    instance instLawfulCommIdentityUInt16HAndNegOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => x1 &&& x2) (-1)
    source
    instance instLawfulCommIdentityUInt32HAndNegOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => x1 &&& x2) (-1)
    source
    instance instLawfulCommIdentityUInt64HAndNegOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => x1 &&& x2) (-1)
    source
    instance instLawfulCommIdentityUSizeHAndNegOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : USize) => x1 &&& x2) (-1)
    source
    @[simp]
    theorem UInt8.and_eq_neg_one_iff {a b : UInt8} :
    a &&& b = -1 ↔ a = -1 ∧ b = -1
    source
    @[simp]
    theorem UInt16.and_eq_neg_one_iff {a b : UInt16} :
    a &&& b = -1 ↔ a = -1 ∧ b = -1
    source
    @[simp]
    theorem UInt32.and_eq_neg_one_iff {a b : UInt32} :
    a &&& b = -1 ↔ a = -1 ∧ b = -1
    source
    @[simp]
    theorem UInt64.and_eq_neg_one_iff {a b : UInt64} :
    a &&& b = -1 ↔ a = -1 ∧ b = -1
    source
    @[simp]
    theorem USize.and_eq_neg_one_iff {a b : USize} :
    a &&& b = -1 ↔ a = -1 ∧ b = -1
    source
    theorem UInt8.xor_assoc (a b c : UInt8) :
    a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
    source
    theorem UInt16.xor_assoc (a b c : UInt16) :
    a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
    source
    theorem UInt32.xor_assoc (a b c : UInt32) :
    a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
    source
    theorem UInt64.xor_assoc (a b c : UInt64) :
    a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
    source
    theorem USize.xor_assoc (a b c : USize) :
    a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
    source
    instance instAssociativeUInt8HXor :
    Std.Associative fun (x1 x2 : UInt8) => x1 ^^^ x2
    source
    instance instAssociativeUInt16HXor :
    Std.Associative fun (x1 x2 : UInt16) => x1 ^^^ x2
    source
    instance instAssociativeUInt32HXor :
    Std.Associative fun (x1 x2 : UInt32) => x1 ^^^ x2
    source
    instance instAssociativeUInt64HXor :
    Std.Associative fun (x1 x2 : UInt64) => x1 ^^^ x2
    source
    instance instAssociativeUSizeHXor :
    Std.Associative fun (x1 x2 : USize) => x1 ^^^ x2
    source
    theorem UInt8.xor_comm (a b : UInt8) :
    a ^^^ b = b ^^^ a
    source
    theorem UInt16.xor_comm (a b : UInt16) :
    a ^^^ b = b ^^^ a
    source
    theorem UInt32.xor_comm (a b : UInt32) :
    a ^^^ b = b ^^^ a
    source
    theorem UInt64.xor_comm (a b : UInt64) :
    a ^^^ b = b ^^^ a
    source
    theorem USize.xor_comm (a b : USize) :
    a ^^^ b = b ^^^ a
    source
    instance instCommutativeUInt8HXor :
    Std.Commutative fun (x1 x2 : UInt8) => x1 ^^^ x2
    source
    instance instCommutativeUInt16HXor :
    Std.Commutative fun (x1 x2 : UInt16) => x1 ^^^ x2
    source
    instance instCommutativeUInt32HXor :
    Std.Commutative fun (x1 x2 : UInt32) => x1 ^^^ x2
    source
    instance instCommutativeUInt64HXor :
    Std.Commutative fun (x1 x2 : UInt64) => x1 ^^^ x2
    source
    instance instCommutativeUSizeHXor :
    Std.Commutative fun (x1 x2 : USize) => x1 ^^^ x2
    source
    @[simp]
    theorem UInt8.xor_self {a : UInt8} :
    a ^^^ a = 0
    source
    @[simp]
    theorem UInt16.xor_self {a : UInt16} :
    a ^^^ a = 0
    source
    @[simp]
    theorem UInt32.xor_self {a : UInt32} :
    a ^^^ a = 0
    source
    @[simp]
    theorem UInt64.xor_self {a : UInt64} :
    a ^^^ a = 0
    source
    @[simp]
    theorem USize.xor_self {a : USize} :
    a ^^^ a = 0
    source
    @[simp]
    theorem UInt8.xor_zero {a : UInt8} :
    a ^^^ 0 = a
    source
    @[simp]
    theorem UInt16.xor_zero {a : UInt16} :
    a ^^^ 0 = a
    source
    @[simp]
    theorem UInt32.xor_zero {a : UInt32} :
    a ^^^ 0 = a
    source
    @[simp]
    theorem UInt64.xor_zero {a : UInt64} :
    a ^^^ 0 = a
    source
    @[simp]
    theorem USize.xor_zero {a : USize} :
    a ^^^ 0 = a
    source
    @[simp]
    theorem UInt8.zero_xor {a : UInt8} :
    0 ^^^ a = a
    source
    @[simp]
    theorem UInt16.zero_xor {a : UInt16} :
    0 ^^^ a = a
    source
    @[simp]
    theorem UInt32.zero_xor {a : UInt32} :
    0 ^^^ a = a
    source
    @[simp]
    theorem UInt64.zero_xor {a : UInt64} :
    0 ^^^ a = a
    source
    @[simp]
    theorem USize.zero_xor {a : USize} :
    0 ^^^ a = a
    source
    @[simp]
    theorem UInt8.neg_one_xor {a : UInt8} :
    -1 ^^^ a = ~~~a
    source
    @[simp]
    theorem UInt16.neg_one_xor {a : UInt16} :
    -1 ^^^ a = ~~~a
    source
    @[simp]
    theorem UInt32.neg_one_xor {a : UInt32} :
    -1 ^^^ a = ~~~a
    source
    @[simp]
    theorem UInt64.neg_one_xor {a : UInt64} :
    -1 ^^^ a = ~~~a
    source
    @[simp]
    theorem USize.neg_one_xor {a : USize} :
    -1 ^^^ a = ~~~a
    source
    @[simp]
    theorem UInt8.xor_neg_one {a : UInt8} :
    a ^^^ -1 = ~~~a
    source
    @[simp]
    theorem UInt16.xor_neg_one {a : UInt16} :
    a ^^^ -1 = ~~~a
    source
    @[simp]
    theorem UInt32.xor_neg_one {a : UInt32} :
    a ^^^ -1 = ~~~a
    source
    @[simp]
    theorem UInt64.xor_neg_one {a : UInt64} :
    a ^^^ -1 = ~~~a
    source
    @[simp]
    theorem USize.xor_neg_one {a : USize} :
    a ^^^ -1 = ~~~a
    source
    instance instLawfulCommIdentityUInt8HXorOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => x1 ^^^ x2) 0
    source
    instance instLawfulCommIdentityUInt16HXorOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => x1 ^^^ x2) 0
    source
    instance instLawfulCommIdentityUInt32HXorOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => x1 ^^^ x2) 0
    source
    instance instLawfulCommIdentityUInt64HXorOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => x1 ^^^ x2) 0
    source
    instance instLawfulCommIdentityUSizeHXorOfNat :
    Std.LawfulCommIdentity (fun (x1 x2 : USize) => x1 ^^^ x2) 0
    source
    @[simp]
    theorem UInt8.xor_eq_zero_iff {a b : UInt8} :
    a ^^^ b = 0 ↔ a = b
    source
    @[simp]
    theorem UInt16.xor_eq_zero_iff {a b : UInt16} :
    a ^^^ b = 0 ↔ a = b
    source
    @[simp]
    theorem UInt32.xor_eq_zero_iff {a b : UInt32} :
    a ^^^ b = 0 ↔ a = b
    source
    @[simp]
    theorem UInt64.xor_eq_zero_iff {a b : UInt64} :
    a ^^^ b = 0 ↔ a = b
    source
    @[simp]
    theorem USize.xor_eq_zero_iff {a b : USize} :
    a ^^^ b = 0 ↔ a = b
    source
    @[simp]
    theorem UInt8.xor_left_inj {a b : UInt8} (c : UInt8) :
    a ^^^ c = b ^^^ c ↔ a = b
    source
    @[simp]
    theorem UInt16.xor_left_inj {a b : UInt16} (c : UInt16) :
    a ^^^ c = b ^^^ c ↔ a = b
    source
    @[simp]
    theorem UInt32.xor_left_inj {a b : UInt32} (c : UInt32) :
    a ^^^ c = b ^^^ c ↔ a = b
    source
    @[simp]
    theorem UInt64.xor_left_inj {a b : UInt64} (c : UInt64) :
    a ^^^ c = b ^^^ c ↔ a = b
    source
    @[simp]
    theorem USize.xor_left_inj {a b : USize} (c : USize) :
    a ^^^ c = b ^^^ c ↔ a = b
    source
    @[simp]
    theorem UInt8.xor_right_inj {a b : UInt8} (c : UInt8) :
    c ^^^ a = c ^^^ b ↔ a = b
    source
    @[simp]
    theorem UInt16.xor_right_inj {a b : UInt16} (c : UInt16) :
    c ^^^ a = c ^^^ b ↔ a = b
    source
    @[simp]
    theorem UInt32.xor_right_inj {a b : UInt32} (c : UInt32) :
    c ^^^ a = c ^^^ b ↔ a = b
    source
    @[simp]
    theorem UInt64.xor_right_inj {a b : UInt64} (c : UInt64) :
    c ^^^ a = c ^^^ b ↔ a = b
    source
    @[simp]
    theorem USize.xor_right_inj {a b : USize} (c : USize) :
    c ^^^ a = c ^^^ b ↔ a = b
    source
    @[simp]
    theorem UInt8.not_zero :
    ~~~0 = -1
    source
    @[simp]
    theorem UInt16.not_zero :
    ~~~0 = -1
    source
    @[simp]
    theorem UInt32.not_zero :
    ~~~0 = -1
    source
    @[simp]
    theorem UInt64.not_zero :
    ~~~0 = -1
    source
    @[simp]
    theorem USize.not_zero :
    ~~~0 = -1
    source
    @[simp]
    theorem UInt8.not_neg_one :
    ~~~(-1) = 0
    source
    @[simp]
    theorem UInt16.not_neg_one :
    ~~~(-1) = 0
    source
    @[simp]
    theorem UInt32.not_neg_one :
    ~~~(-1) = 0
    source
    @[simp]
    theorem UInt64.not_neg_one :
    ~~~(-1) = 0
    source
    @[simp]
    theorem USize.not_neg_one :
    ~~~(-1) = 0
    source
    @[simp]
    theorem UInt8.not_not {a : UInt8} :
    ~~~~~~a = a
    source
    @[simp]
    theorem UInt16.not_not {a : UInt16} :
    ~~~~~~a = a
    source
    @[simp]
    theorem UInt32.not_not {a : UInt32} :
    ~~~~~~a = a
    source
    @[simp]
    theorem UInt64.not_not {a : UInt64} :
    ~~~~~~a = a
    source
    @[simp]
    theorem USize.not_not {a : USize} :
    ~~~~~~a = a
    source
    @[simp]
    theorem UInt8.not_inj {a b : UInt8} :
    ~~~a = ~~~b ↔ a = b
    source
    @[simp]
    theorem UInt16.not_inj {a b : UInt16} :
    ~~~a = ~~~b ↔ a = b
    source
    @[simp]
    theorem UInt32.not_inj {a b : UInt32} :
    ~~~a = ~~~b ↔ a = b
    source
    @[simp]
    theorem UInt64.not_inj {a b : UInt64} :
    ~~~a = ~~~b ↔ a = b
    source
    @[simp]
    theorem USize.not_inj {a b : USize} :
    ~~~a = ~~~b ↔ a = b
    source
    @[simp]
    theorem UInt8.and_not_self {a : UInt8} :
    a &&& ~~~a = 0
    source
    @[simp]
    theorem UInt16.and_not_self {a : UInt16} :
    a &&& ~~~a = 0
    source
    @[simp]
    theorem UInt32.and_not_self {a : UInt32} :
    a &&& ~~~a = 0
    source
    @[simp]
    theorem UInt64.and_not_self {a : UInt64} :
    a &&& ~~~a = 0
    source
    @[simp]
    theorem USize.and_not_self {a : USize} :
    a &&& ~~~a = 0
    source
    @[simp]
    theorem UInt8.not_and_self {a : UInt8} :
    ~~~a &&& a = 0
    source
    @[simp]
    theorem UInt16.not_and_self {a : UInt16} :
    ~~~a &&& a = 0
    source
    @[simp]
    theorem UInt32.not_and_self {a : UInt32} :
    ~~~a &&& a = 0
    source
    @[simp]
    theorem UInt64.not_and_self {a : UInt64} :
    ~~~a &&& a = 0
    source
    @[simp]
    theorem USize.not_and_self {a : USize} :
    ~~~a &&& a = 0
    source
    @[simp]
    theorem UInt8.or_not_self {a : UInt8} :
    a ||| ~~~a = -1
    source
    @[simp]
    theorem UInt16.or_not_self {a : UInt16} :
    a ||| ~~~a = -1
    source
    @[simp]
    theorem UInt32.or_not_self {a : UInt32} :
    a ||| ~~~a = -1
    source
    @[simp]
    theorem UInt64.or_not_self {a : UInt64} :
    a ||| ~~~a = -1
    source
    @[simp]
    theorem USize.or_not_self {a : USize} :
    a ||| ~~~a = -1
    source
    @[simp]
    theorem UInt8.not_or_self {a : UInt8} :
    ~~~a ||| a = -1
    source
    @[simp]
    theorem UInt16.not_or_self {a : UInt16} :
    ~~~a ||| a = -1
    source
    @[simp]
    theorem UInt32.not_or_self {a : UInt32} :
    ~~~a ||| a = -1
    source
    @[simp]
    theorem UInt64.not_or_self {a : UInt64} :
    ~~~a ||| a = -1
    source
    @[simp]
    theorem USize.not_or_self {a : USize} :
    ~~~a ||| a = -1
    source
    theorem UInt8.not_eq_comm {a b : UInt8} :
    ~~~a = b ↔ a = ~~~b
    source
    theorem UInt16.not_eq_comm {a b : UInt16} :
    ~~~a = b ↔ a = ~~~b
    source
    theorem UInt32.not_eq_comm {a b : UInt32} :
    ~~~a = b ↔ a = ~~~b
    source
    theorem UInt64.not_eq_comm {a b : UInt64} :
    ~~~a = b ↔ a = ~~~b
    source
    theorem USize.not_eq_comm {a b : USize} :
    ~~~a = b ↔ a = ~~~b
    source
    @[simp]
    theorem UInt8.ne_not_self {a : UInt8} :
    a ≠ ~~~a
    source
    @[simp]
    theorem UInt16.ne_not_self {a : UInt16} :
    a ≠ ~~~a
    source
    @[simp]
    theorem UInt32.ne_not_self {a : UInt32} :
    a ≠ ~~~a
    source
    @[simp]
    theorem UInt64.ne_not_self {a : UInt64} :
    a ≠ ~~~a
    source
    @[simp]
    theorem USize.ne_not_self {a : USize} :
    a ≠ ~~~a
    source
    @[simp]
    theorem UInt8.not_ne_self {a : UInt8} :
    ~~~a ≠ a
    source
    @[simp]
    theorem UInt16.not_ne_self {a : UInt16} :
    ~~~a ≠ a
    source
    @[simp]
    theorem UInt32.not_ne_self {a : UInt32} :
    ~~~a ≠ a
    source
    @[simp]
    theorem UInt64.not_ne_self {a : UInt64} :
    ~~~a ≠ a
    source
    @[simp]
    theorem USize.not_ne_self {a : USize} :
    ~~~a ≠ a
    source
    theorem UInt8.not_xor {a b : UInt8} :
    ~~~a ^^^ b = ~~~(a ^^^ b)
    source
    theorem UInt16.not_xor {a b : UInt16} :
    ~~~a ^^^ b = ~~~(a ^^^ b)
    source
    theorem UInt32.not_xor {a b : UInt32} :
    ~~~a ^^^ b = ~~~(a ^^^ b)
    source
    theorem UInt64.not_xor {a b : UInt64} :
    ~~~a ^^^ b = ~~~(a ^^^ b)
    source
    theorem USize.not_xor {a b : USize} :
    ~~~a ^^^ b = ~~~(a ^^^ b)
    source
    theorem UInt8.xor_not {a b : UInt8} :
    a ^^^ ~~~b = ~~~(a ^^^ b)
    source
    theorem UInt16.xor_not {a b : UInt16} :
    a ^^^ ~~~b = ~~~(a ^^^ b)
    source
    theorem UInt32.xor_not {a b : UInt32} :
    a ^^^ ~~~b = ~~~(a ^^^ b)
    source
    theorem UInt64.xor_not {a b : UInt64} :
    a ^^^ ~~~b = ~~~(a ^^^ b)
    source
    theorem USize.xor_not {a b : USize} :
    a ^^^ ~~~b = ~~~(a ^^^ b)
    source
    @[simp]
    theorem UInt8.shiftLeft_zero {a : UInt8} :
    a <<< 0 = a
    source
    @[simp]
    theorem UInt16.shiftLeft_zero {a : UInt16} :
    a <<< 0 = a
    source
    @[simp]
    theorem UInt32.shiftLeft_zero {a : UInt32} :
    a <<< 0 = a
    source
    @[simp]
    theorem UInt64.shiftLeft_zero {a : UInt64} :
    a <<< 0 = a
    source
    @[simp]
    theorem USize.shiftLeft_zero {a : USize} :
    a <<< 0 = a
    source
    @[simp]
    theorem UInt8.zero_shiftLeft {a : UInt8} :
    0 <<< a = 0
    source
    @[simp]
    theorem UInt16.zero_shiftLeft {a : UInt16} :
    0 <<< a = 0
    source
    @[simp]
    theorem UInt32.zero_shiftLeft {a : UInt32} :
    0 <<< a = 0
    source
    @[simp]
    theorem UInt64.zero_shiftLeft {a : UInt64} :
    0 <<< a = 0
    source
    @[simp]
    theorem USize.zero_shiftLeft {a : USize} :
    0 <<< a = 0
    source
    theorem UInt8.shiftLeft_xor {a b c : UInt8} :
    (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
    source
    theorem UInt16.shiftLeft_xor {a b c : UInt16} :
    (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
    source
    theorem UInt32.shiftLeft_xor {a b c : UInt32} :
    (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
    source
    theorem UInt64.shiftLeft_xor {a b c : UInt64} :
    (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
    source
    theorem USize.shiftLeft_xor {a b c : USize} :
    (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
    source
    theorem UInt8.shiftLeft_and {a b c : UInt8} :
    (a &&& b) <<< c = a <<< c &&& b <<< c
    source
    theorem UInt16.shiftLeft_and {a b c : UInt16} :
    (a &&& b) <<< c = a <<< c &&& b <<< c
    source
    theorem UInt32.shiftLeft_and {a b c : UInt32} :
    (a &&& b) <<< c = a <<< c &&& b <<< c
    source
    theorem UInt64.shiftLeft_and {a b c : UInt64} :
    (a &&& b) <<< c = a <<< c &&& b <<< c
    source
    theorem USize.shiftLeft_and {a b c : USize} :
    (a &&& b) <<< c = a <<< c &&& b <<< c
    source
    theorem UInt8.shiftLeft_or {a b c : UInt8} :
    (a ||| b) <<< c = a <<< c ||| b <<< c
    source
    theorem UInt16.shiftLeft_or {a b c : UInt16} :
    (a ||| b) <<< c = a <<< c ||| b <<< c
    source
    theorem UInt32.shiftLeft_or {a b c : UInt32} :
    (a ||| b) <<< c = a <<< c ||| b <<< c
    source
    theorem UInt64.shiftLeft_or {a b c : UInt64} :
    (a ||| b) <<< c = a <<< c ||| b <<< c
    source
    theorem USize.shiftLeft_or {a b c : USize} :
    (a ||| b) <<< c = a <<< c ||| b <<< c
    source
    theorem UInt8.shiftLeft_add_of_toNat_lt {a b c : UInt8} (h : b.toNat + c.toNat < 8) :
    a <<< (b + c) = a <<< b <<< c
    source
    theorem UInt16.shiftLeft_add_of_toNat_lt {a b c : UInt16} (h : b.toNat + c.toNat < 16) :
    a <<< (b + c) = a <<< b <<< c
    source
    theorem UInt32.shiftLeft_add_of_toNat_lt {a b c : UInt32} (h : b.toNat + c.toNat < 32) :
    a <<< (b + c) = a <<< b <<< c
    source
    theorem UInt64.shiftLeft_add_of_toNat_lt {a b c : UInt64} (h : b.toNat + c.toNat < 64) :
    a <<< (b + c) = a <<< b <<< c
    source
    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
    source
    theorem UInt8.shiftLeft_add {a b c : UInt8} (hb : b < 8) (hc : c < 8) (hbc : b + c < 8) :
    a <<< (b + c) = a <<< b <<< c
    source
    theorem UInt16.shiftLeft_add {a b c : UInt16} (hb : b < 16) (hc : c < 16) (hbc : b + c < 16) :
    a <<< (b + c) = a <<< b <<< c
    source
    theorem UInt32.shiftLeft_add {a b c : UInt32} (hb : b < 32) (hc : c < 32) (hbc : b + c < 32) :
    a <<< (b + c) = a <<< b <<< c
    source
    theorem UInt64.shiftLeft_add {a b c : UInt64} (hb : b < 64) (hc : c < 64) (hbc : b + c < 64) :
    a <<< (b + c) = a <<< b <<< c
    source
    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
    source
    @[simp]
    theorem UInt8.neg_one_shiftLeft_and_shiftLeft {a b : UInt8} :
    (-1) <<< b &&& a <<< b = a <<< b
    source
    @[simp]
    theorem UInt16.neg_one_shiftLeft_and_shiftLeft {a b : UInt16} :
    (-1) <<< b &&& a <<< b = a <<< b
    source
    @[simp]
    theorem UInt32.neg_one_shiftLeft_and_shiftLeft {a b : UInt32} :
    (-1) <<< b &&& a <<< b = a <<< b
    source
    @[simp]
    theorem UInt64.neg_one_shiftLeft_and_shiftLeft {a b : UInt64} :
    (-1) <<< b &&& a <<< b = a <<< b
    source
    @[simp]
    theorem USize.neg_one_shiftLeft_and_shiftLeft {a b : USize} :
    (-1) <<< b &&& a <<< b = a <<< b
    source
    @[simp]
    theorem UInt8.neg_one_shiftLeft_or_shiftLeft {a b : UInt8} :
    (-1) <<< b ||| a <<< b = (-1) <<< b
    source
    @[simp]
    theorem UInt16.neg_one_shiftLeft_or_shiftLeft {a b : UInt16} :
    (-1) <<< b ||| a <<< b = (-1) <<< b
    source
    @[simp]
    theorem UInt32.neg_one_shiftLeft_or_shiftLeft {a b : UInt32} :
    (-1) <<< b ||| a <<< b = (-1) <<< b
    source
    @[simp]
    theorem UInt64.neg_one_shiftLeft_or_shiftLeft {a b : UInt64} :
    (-1) <<< b ||| a <<< b = (-1) <<< b
    source
    @[simp]
    theorem USize.neg_one_shiftLeft_or_shiftLeft {a b : USize} :
    (-1) <<< b ||| a <<< b = (-1) <<< b
    source
    @[simp]
    theorem UInt8.shiftRight_zero {a : UInt8} :
    a >>> 0 = a
    source
    @[simp]
    theorem UInt16.shiftRight_zero {a : UInt16} :
    a >>> 0 = a
    source
    @[simp]
    theorem UInt32.shiftRight_zero {a : UInt32} :
    a >>> 0 = a
    source
    @[simp]
    theorem UInt64.shiftRight_zero {a : UInt64} :
    a >>> 0 = a
    source
    @[simp]
    theorem USize.shiftRight_zero {a : USize} :
    a >>> 0 = a
    source
    @[simp]
    theorem UInt8.zero_shiftRight {a : UInt8} :
    0 >>> a = 0
    source
    @[simp]
    theorem UInt16.zero_shiftRight {a : UInt16} :
    0 >>> a = 0
    source
    @[simp]
    theorem UInt32.zero_shiftRight {a : UInt32} :
    0 >>> a = 0
    source
    @[simp]
    theorem UInt64.zero_shiftRight {a : UInt64} :
    0 >>> a = 0
    source
    @[simp]
    theorem USize.zero_shiftRight {a : USize} :
    0 >>> a = 0
    source
    theorem UInt8.shiftRight_xor {a b c : UInt8} :
    (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
    source
    theorem UInt16.shiftRight_xor {a b c : UInt16} :
    (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
    source
    theorem UInt32.shiftRight_xor {a b c : UInt32} :
    (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
    source
    theorem UInt64.shiftRight_xor {a b c : UInt64} :
    (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
    source
    theorem USize.shiftRight_xor {a b c : USize} :
    (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
    source
    theorem UInt8.shiftRight_and {a b c : UInt8} :
    (a &&& b) >>> c = a >>> c &&& b >>> c
    source
    theorem UInt16.shiftRight_and {a b c : UInt16} :
    (a &&& b) >>> c = a >>> c &&& b >>> c
    source
    theorem UInt32.shiftRight_and {a b c : UInt32} :
    (a &&& b) >>> c = a >>> c &&& b >>> c
    source
    theorem UInt64.shiftRight_and {a b c : UInt64} :
    (a &&& b) >>> c = a >>> c &&& b >>> c
    source
    theorem USize.shiftRight_and {a b c : USize} :
    (a &&& b) >>> c = a >>> c &&& b >>> c
    source
    theorem UInt8.shiftRight_or {a b c : UInt8} :
    (a ||| b) >>> c = a >>> c ||| b >>> c
    source
    theorem UInt16.shiftRight_or {a b c : UInt16} :
    (a ||| b) >>> c = a >>> c ||| b >>> c
    source
    theorem UInt32.shiftRight_or {a b c : UInt32} :
    (a ||| b) >>> c = a >>> c ||| b >>> c
    source
    theorem UInt64.shiftRight_or {a b c : UInt64} :
    (a ||| b) >>> c = a >>> c ||| b >>> c
    source
    theorem USize.shiftRight_or {a b c : USize} :
    (a ||| b) >>> c = a >>> c ||| b >>> c
    source
    theorem UInt8.and_le_right {a b : UInt8} :
    a &&& b ≤ b
    source
    theorem UInt16.and_le_right {a b : UInt16} :
    a &&& b ≤ b
    source
    theorem UInt32.and_le_right {a b : UInt32} :
    a &&& b ≤ b
    source
    theorem UInt64.and_le_right {a b : UInt64} :
    a &&& b ≤ b
    source
    theorem USize.and_le_right {a b : USize} :
    a &&& b ≤ b
    source
    theorem UInt8.and_le_left {a b : UInt8} :
    a &&& b ≤ a
    source
    theorem UInt16.and_le_left {a b : UInt16} :
    a &&& b ≤ a
    source
    theorem UInt32.and_le_left {a b : UInt32} :
    a &&& b ≤ a
    source
    theorem UInt64.and_le_left {a b : UInt64} :
    a &&& b ≤ a
    source
    theorem USize.and_le_left {a b : USize} :
    a &&& b ≤ a
    source
    theorem UInt8.left_le_or {a b : UInt8} :
    a ≤ a ||| b
    source
    theorem UInt16.left_le_or {a b : UInt16} :
    a ≤ a ||| b
    source
    theorem UInt32.left_le_or {a b : UInt32} :
    a ≤ a ||| b
    source
    theorem UInt64.left_le_or {a b : UInt64} :
    a ≤ a ||| b
    source
    theorem USize.left_le_or {a b : USize} :
    a ≤ a ||| b
    source
    theorem UInt8.right_le_or {a b : UInt8} :
    b ≤ a ||| b
    source
    theorem UInt16.right_le_or {a b : UInt16} :
    b ≤ a ||| b
    source
    theorem UInt32.right_le_or {a b : UInt32} :
    b ≤ a ||| b
    source
    theorem UInt64.right_le_or {a b : UInt64} :
    b ≤ a ||| b
    source
    theorem USize.right_le_or {a b : USize} :
    b ≤ a ||| b
    source
    theorem UInt8.and_lt_add_one {b c : UInt8} (h : c ≠ -1) :
    b &&& c < c + 1
    source
    theorem UInt16.and_lt_add_one {b c : UInt16} (h : c ≠ -1) :
    b &&& c < c + 1
    source
    theorem UInt32.and_lt_add_one {b c : UInt32} (h : c ≠ -1) :
    b &&& c < c + 1
    source
    theorem UInt64.and_lt_add_one {b c : UInt64} (h : c ≠ -1) :
    b &&& c < c + 1
    source
    theorem USize.and_lt_add_one {b c : USize} (h : c ≠ -1) :
    b &&& c < c + 1