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.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 UInt8.toNat_and (a b : UInt8) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem UInt16.toNat_or (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.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_xor (a b : UInt16) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.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.toNat_shiftLeft (a b : UInt16) : (a <<< b).toNat = a.toNat <<< (b.toNat % 16) % 2 ^ 16

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem UInt32.toNat_shiftLeft (a b : UInt32) : (a <<< b).toNat = a.toNat <<< (b.toNat % 32) % 2 ^ 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)

@[simp]

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

@[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.toBitVec_xor (a b : UInt32) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec

@[simp]

theorem UInt32.toNat_xor (a b : UInt32) : (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.toBitVec_or (a b : UInt64) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec

@[simp]

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

@[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.toBitVec_and (a b : UInt64) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec

@[simp]

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

@[simp]

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

@[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_xor (a b : UInt64) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat

@[simp]

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

@[simp]

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

@[simp]

theorem USize.toNat_xor (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.toBitVec_shiftRight (a b : USize) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % ↑System.Platform.numBits)

@[simp]

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

@[simp]

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

@[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.toNat_shiftLeft (a b : USize) : (a <<< b).toNat = a.toNat <<< (b.toNat % System.Platform.numBits) % 2 ^ System.Platform.numBits

@[simp]

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

@[simp]

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