source
def commandDeclare_bitwise_int_theorems__ :
Lean.ParserDescr
Equations

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

Instances For

source
@[simp]
theorem Int8.toBitVec_shiftRight (a b : Int8) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 8)
source
@[simp]
theorem Int8.toBitVec_and (a b : Int8) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem Int8.toBitVec_xor (a b : Int8) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem Int8.toBitVec_or (a b : Int8) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Int8.toBitVec_shiftLeft (a b : Int8) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 8
source
@[simp]
theorem Int8.toBitVec_abs (a : Int8) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem Int8.toBitVec_not {a : Int8} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem Int16.toBitVec_xor (a b : Int16) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem Int16.toBitVec_or (a b : Int16) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Int16.toBitVec_shiftLeft (a b : Int16) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 16
source
@[simp]
theorem Int16.toBitVec_shiftRight (a b : Int16) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 16)
source
@[simp]
theorem Int16.toBitVec_and (a b : Int16) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem Int16.toBitVec_not {a : Int16} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem Int16.toBitVec_abs (a : Int16) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem Int32.toBitVec_or (a b : Int32) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Int32.toBitVec_shiftRight (a b : Int32) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 32)
source
@[simp]
theorem Int32.toBitVec_not {a : Int32} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem Int32.toBitVec_xor (a b : Int32) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem Int32.toBitVec_and (a b : Int32) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem Int32.toBitVec_abs (a : Int32) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem Int32.toBitVec_shiftLeft (a b : Int32) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 32
source
@[simp]
theorem Int64.toBitVec_or (a b : Int64) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Int64.toBitVec_shiftRight (a b : Int64) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 64)
source
@[simp]
theorem Int64.toBitVec_and (a b : Int64) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem Int64.toBitVec_shiftLeft (a b : Int64) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 64
source
@[simp]
theorem Int64.toBitVec_xor (a b : Int64) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem Int64.toBitVec_not {a : Int64} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem Int64.toBitVec_abs (a : Int64) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem ISize.toBitVec_or (a b : ISize) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem ISize.toBitVec_xor (a b : ISize) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem ISize.toBitVec_not {a : ISize} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem ISize.toBitVec_shiftLeft (a b : ISize) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod ↑System.Platform.numBits
source
@[simp]
theorem ISize.toBitVec_and (a b : ISize) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem ISize.toBitVec_abs (a : ISize) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem ISize.toBitVec_shiftRight (a b : ISize) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod ↑System.Platform.numBits)
source
@[simp]
theorem Bool.toBitVec_toInt8 {b : Bool} :
b.toInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)
source
@[simp]
theorem Bool.toBitVec_toInt16 {b : Bool} :
b.toInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)
source
@[simp]
theorem Bool.toBitVec_toInt32 {b : Bool} :
b.toInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)
source
@[simp]
theorem Bool.toBitVec_toInt64 {b : Bool} :
b.toInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)
source
@[simp]
theorem Bool.toBitVec_toISize {b : Bool} :
b.toISize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)
source
@[simp]
theorem UInt8.toInt8_and (a b : UInt8) :
(a &&& b).toInt8 = a.toInt8 &&& b.toInt8
source
@[simp]
theorem UInt16.toInt16_and (a b : UInt16) :
(a &&& b).toInt16 = a.toInt16 &&& b.toInt16
source
@[simp]
theorem UInt32.toInt32_and (a b : UInt32) :
(a &&& b).toInt32 = a.toInt32 &&& b.toInt32
source
@[simp]
theorem UInt64.toInt64_and (a b : UInt64) :
(a &&& b).toInt64 = a.toInt64 &&& b.toInt64
source
@[simp]
theorem USize.toISize_and (a b : USize) :
(a &&& b).toISize = a.toISize &&& b.toISize
source
@[simp]
theorem UInt8.toInt8_or (a b : UInt8) :
(a ||| b).toInt8 = a.toInt8 ||| b.toInt8
source
@[simp]
theorem UInt16.toInt16_or (a b : UInt16) :
(a ||| b).toInt16 = a.toInt16 ||| b.toInt16
source
@[simp]
theorem UInt32.toInt32_or (a b : UInt32) :
(a ||| b).toInt32 = a.toInt32 ||| b.toInt32
source
@[simp]
theorem UInt64.toInt64_or (a b : UInt64) :
(a ||| b).toInt64 = a.toInt64 ||| b.toInt64
source
@[simp]
theorem USize.toISize_or (a b : USize) :
(a ||| b).toISize = a.toISize ||| b.toISize
source
@[simp]
theorem UInt8.toInt8_xor (a b : UInt8) :
(a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
source
@[simp]
theorem UInt16.toInt16_xor (a b : UInt16) :
(a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
source
@[simp]
theorem UInt32.toInt32_xor (a b : UInt32) :
(a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
source
@[simp]
theorem UInt64.toInt64_xor (a b : UInt64) :
(a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
source
@[simp]
theorem USize.toISize_xor (a b : USize) :
(a ^^^ b).toISize = a.toISize ^^^ b.toISize
source
@[simp]
theorem UInt8.toInt8_not (a : UInt8) :
(~~~a).toInt8 = ~~~a.toInt8
source
@[simp]
theorem UInt16.toInt16_not (a : UInt16) :
(~~~a).toInt16 = ~~~a.toInt16
source
@[simp]
theorem UInt32.toInt32_not (a : UInt32) :
(~~~a).toInt32 = ~~~a.toInt32
source
@[simp]
theorem UInt64.toInt64_not (a : UInt64) :
(~~~a).toInt64 = ~~~a.toInt64
source
@[simp]
theorem USize.toISize_not (a : USize) :
(~~~a).toISize = ~~~a.toISize
source
@[simp]
theorem Int8.toUInt8_and (a b : Int8) :
(a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
source
@[simp]
theorem Int16.toUInt16_and (a b : Int16) :
(a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
source
@[simp]
theorem Int32.toUInt32_and (a b : Int32) :
(a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
source
@[simp]
theorem Int64.toUInt64_and (a b : Int64) :
(a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
source
@[simp]
theorem ISize.toUSize_and (a b : ISize) :
(a &&& b).toUSize = a.toUSize &&& b.toUSize
source
@[simp]
theorem Int8.toUInt8_or (a b : Int8) :
(a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
source
@[simp]
theorem Int16.toUInt16_or (a b : Int16) :
(a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
source
@[simp]
theorem Int32.toUInt32_or (a b : Int32) :
(a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
source
@[simp]
theorem Int64.toUInt64_or (a b : Int64) :
(a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
source
@[simp]
theorem ISize.toUSize_or (a b : ISize) :
(a ||| b).toUSize = a.toUSize ||| b.toUSize
source
@[simp]
theorem Int8.toUInt8_xor (a b : Int8) :
(a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
source
@[simp]
theorem Int16.toUInt16_xor (a b : Int16) :
(a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
source
@[simp]
theorem Int32.toUInt32_xor (a b : Int32) :
(a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
source
@[simp]
theorem Int64.toUInt64_xor (a b : Int64) :
(a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
source
@[simp]
theorem ISize.toUSize_xor (a b : ISize) :
(a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
source
@[simp]
theorem Int8.toUInt8_not (a : Int8) :
(~~~a).toUInt8 = ~~~a.toUInt8
source
@[simp]
theorem Int16.toUInt16_not (a : Int16) :
(~~~a).toUInt16 = ~~~a.toUInt16
source
@[simp]
theorem Int32.toUInt32_not (a : Int32) :
(~~~a).toUInt32 = ~~~a.toUInt32
source
@[simp]
theorem Int64.toUInt64_not (a : Int64) :
(~~~a).toUInt64 = ~~~a.toUInt64
source
@[simp]
theorem ISize.toUSize_not (a : ISize) :
(~~~a).toUSize = ~~~a.toUSize
source
@[simp]
theorem Int8.toInt16_and (a b : Int8) :
(a &&& b).toInt16 = a.toInt16 &&& b.toInt16
source
@[simp]
theorem Int8.toInt32_and (a b : Int8) :
(a &&& b).toInt32 = a.toInt32 &&& b.toInt32
source
@[simp]
theorem Int8.toInt64_and (a b : Int8) :
(a &&& b).toInt64 = a.toInt64 &&& b.toInt64
source
@[simp]
theorem Int8.toISize_and (a b : Int8) :
(a &&& b).toISize = a.toISize &&& b.toISize
source
@[simp]
theorem Int16.toInt8_and (a b : Int16) :
(a &&& b).toInt8 = a.toInt8 &&& b.toInt8
source
@[simp]
theorem Int16.toInt32_and (a b : Int16) :
(a &&& b).toInt32 = a.toInt32 &&& b.toInt32
source
@[simp]
theorem Int16.toInt64_and (a b : Int16) :
(a &&& b).toInt64 = a.toInt64 &&& b.toInt64
source
@[simp]
theorem Int16.toISize_and (a b : Int16) :
(a &&& b).toISize = a.toISize &&& b.toISize
source
@[simp]
theorem Int32.toInt8_and (a b : Int32) :
(a &&& b).toInt8 = a.toInt8 &&& b.toInt8
source
@[simp]
theorem Int32.toInt16_and (a b : Int32) :
(a &&& b).toInt16 = a.toInt16 &&& b.toInt16
source
@[simp]
theorem Int32.toInt64_and (a b : Int32) :
(a &&& b).toInt64 = a.toInt64 &&& b.toInt64
source
@[simp]
theorem Int32.toISize_and (a b : Int32) :
(a &&& b).toISize = a.toISize &&& b.toISize
source
@[simp]
theorem ISize.toInt8_and (a b : ISize) :
(a &&& b).toInt8 = a.toInt8 &&& b.toInt8
source
@[simp]
theorem ISize.toInt16_and (a b : ISize) :
(a &&& b).toInt16 = a.toInt16 &&& b.toInt16
source
@[simp]
theorem ISize.toInt32_and (a b : ISize) :
(a &&& b).toInt32 = a.toInt32 &&& b.toInt32
source
@[simp]
theorem ISize.toInt64_and (a b : ISize) :
(a &&& b).toInt64 = a.toInt64 &&& b.toInt64
source
@[simp]
theorem Int64.toInt8_and (a b : Int64) :
(a &&& b).toInt8 = a.toInt8 &&& b.toInt8
source
@[simp]
theorem Int64.toInt16_and (a b : Int64) :
(a &&& b).toInt16 = a.toInt16 &&& b.toInt16
source
@[simp]
theorem Int64.toInt32_and (a b : Int64) :
(a &&& b).toInt32 = a.toInt32 &&& b.toInt32
source
@[simp]
theorem Int64.toISize_and (a b : Int64) :
(a &&& b).toISize = a.toISize &&& b.toISize
source
@[simp]
theorem Int8.toInt16_or (a b : Int8) :
(a ||| b).toInt16 = a.toInt16 ||| b.toInt16
source
@[simp]
theorem Int8.toInt32_or (a b : Int8) :
(a ||| b).toInt32 = a.toInt32 ||| b.toInt32
source
@[simp]
theorem Int8.toInt64_or (a b : Int8) :
(a ||| b).toInt64 = a.toInt64 ||| b.toInt64
source
@[simp]
theorem Int8.toISize_or (a b : Int8) :
(a ||| b).toISize = a.toISize ||| b.toISize
source
@[simp]
theorem Int16.toInt8_or (a b : Int16) :
(a ||| b).toInt8 = a.toInt8 ||| b.toInt8
source
@[simp]
theorem Int16.toInt32_or (a b : Int16) :
(a ||| b).toInt32 = a.toInt32 ||| b.toInt32
source
@[simp]
theorem Int16.toInt64_or (a b : Int16) :
(a ||| b).toInt64 = a.toInt64 ||| b.toInt64
source
@[simp]
theorem Int16.toISize_or (a b : Int16) :
(a ||| b).toISize = a.toISize ||| b.toISize
source
@[simp]
theorem Int32.toInt8_or (a b : Int32) :
(a ||| b).toInt8 = a.toInt8 ||| b.toInt8
source
@[simp]
theorem Int32.toInt16_or (a b : Int32) :
(a ||| b).toInt16 = a.toInt16 ||| b.toInt16
source
@[simp]
theorem Int32.toInt64_or (a b : Int32) :
(a ||| b).toInt64 = a.toInt64 ||| b.toInt64
source
@[simp]
theorem Int32.toISize_or (a b : Int32) :
(a ||| b).toISize = a.toISize ||| b.toISize
source
@[simp]
theorem ISize.toInt8_or (a b : ISize) :
(a ||| b).toInt8 = a.toInt8 ||| b.toInt8
source
@[simp]
theorem ISize.toInt16_or (a b : ISize) :
(a ||| b).toInt16 = a.toInt16 ||| b.toInt16
source
@[simp]
theorem ISize.toInt32_or (a b : ISize) :
(a ||| b).toInt32 = a.toInt32 ||| b.toInt32
source
@[simp]
theorem ISize.toInt64_or (a b : ISize) :
(a ||| b).toInt64 = a.toInt64 ||| b.toInt64
source
@[simp]
theorem Int64.toInt8_or (a b : Int64) :
(a ||| b).toInt8 = a.toInt8 ||| b.toInt8
source
@[simp]
theorem Int64.toInt16_or (a b : Int64) :
(a ||| b).toInt16 = a.toInt16 ||| b.toInt16
source
@[simp]
theorem Int64.toInt32_or (a b : Int64) :
(a ||| b).toInt32 = a.toInt32 ||| b.toInt32
source
@[simp]
theorem Int64.toISize_or (a b : Int64) :
(a ||| b).toISize = a.toISize ||| b.toISize
source
@[simp]
theorem Int8.toInt16_xor (a b : Int8) :
(a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
source
@[simp]
theorem Int8.toInt32_xor (a b : Int8) :
(a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
source
@[simp]
theorem Int8.toInt64_xor (a b : Int8) :
(a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
source
@[simp]
theorem Int8.toISize_xor (a b : Int8) :
(a ^^^ b).toISize = a.toISize ^^^ b.toISize
source
@[simp]
theorem Int16.toInt8_xor (a b : Int16) :
(a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
source
@[simp]
theorem Int16.toInt32_xor (a b : Int16) :
(a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
source
@[simp]
theorem Int16.toInt64_xor (a b : Int16) :
(a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
source
@[simp]
theorem Int16.toISize_xor (a b : Int16) :
(a ^^^ b).toISize = a.toISize ^^^ b.toISize
source
@[simp]
theorem Int32.toInt8_xor (a b : Int32) :
(a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
source
@[simp]
theorem Int32.toInt16_xor (a b : Int32) :
(a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
source
@[simp]
theorem Int32.toInt64_xor (a b : Int32) :
(a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
source
@[simp]
theorem Int32.toISize_xor (a b : Int32) :
(a ^^^ b).toISize = a.toISize ^^^ b.toISize
source
@[simp]
theorem ISize.toInt8_xor (a b : ISize) :
(a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
source
@[simp]
theorem ISize.toInt16_xor (a b : ISize) :
(a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
source
@[simp]
theorem ISize.toInt32_xor (a b : ISize) :
(a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
source
@[simp]
theorem ISize.toInt64_xor (a b : ISize) :
(a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
source
@[simp]
theorem Int64.toInt8_xor (a b : Int64) :
(a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
source
@[simp]
theorem Int64.toInt16_xor (a b : Int64) :
(a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
source
@[simp]
theorem Int64.toInt32_xor (a b : Int64) :
(a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
source
@[simp]
theorem Int64.toISize_xor (a b : Int64) :
(a ^^^ b).toISize = a.toISize ^^^ b.toISize
source
theorem Int8.not_eq_neg_add (a : Int8) :
~~~a = -a - 1
source
theorem Int16.not_eq_neg_add (a : Int16) :
~~~a = -a - 1
source
theorem Int32.not_eq_neg_add (a : Int32) :
~~~a = -a - 1
source
theorem Int64.not_eq_neg_add (a : Int64) :
~~~a = -a - 1
source
theorem ISize.not_eq_neg_add (a : ISize) :
~~~a = -a - 1
source
@[simp]
theorem Int8.toInt_not (a : Int8) :
(~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 8)
source
@[simp]
theorem Int16.toInt_not (a : Int16) :
(~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 16)
source
@[simp]
theorem Int32.toInt_not (a : Int32) :
(~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 32)
source
@[simp]
theorem Int64.toInt_not (a : Int64) :
(~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 64)
source
@[simp]
theorem ISize.toInt_not (a : ISize) :
(~~~a).toInt = (-a.toInt - 1).bmod (2 ^ System.Platform.numBits)
source
@[simp]
theorem Int16.toInt8_not (a : Int16) :
(~~~a).toInt8 = ~~~a.toInt8
source
@[simp]
theorem Int32.toInt8_not (a : Int32) :
(~~~a).toInt8 = ~~~a.toInt8
source
@[simp]
theorem Int64.toInt8_not (a : Int64) :
(~~~a).toInt8 = ~~~a.toInt8
source
@[simp]
theorem ISize.toInt8_not (a : ISize) :
(~~~a).toInt8 = ~~~a.toInt8
source
@[simp]
theorem Int32.toInt16_not (a : Int32) :
(~~~a).toInt16 = ~~~a.toInt16
source
@[simp]
theorem Int64.toInt16_not (a : Int64) :
(~~~a).toInt16 = ~~~a.toInt16
source
@[simp]
theorem ISize.toInt16_not (a : ISize) :
(~~~a).toInt16 = ~~~a.toInt16
source
@[simp]
theorem Int64.toInt32_not (a : Int64) :
(~~~a).toInt32 = ~~~a.toInt32
source
@[simp]
theorem ISize.toInt32_not (a : ISize) :
(~~~a).toInt32 = ~~~a.toInt32
source
@[simp]
theorem Int64.toISize_not (a : Int64) :
(~~~a).toISize = ~~~a.toISize
source
@[simp]
theorem Int8.ofBitVec_and (a b : BitVec 8) :
ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b
source
@[simp]
theorem Int16.ofBitVec_and (a b : BitVec 16) :
ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b
source
@[simp]
theorem Int32.ofBitVec_and (a b : BitVec 32) :
ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b
source
@[simp]
theorem Int64.ofBitVec_and (a b : BitVec 64) :
ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b
source
@[simp]
theorem ISize.ofBitVec_and (a b : BitVec System.Platform.numBits) :
ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b
source
@[simp]
theorem Int8.ofBitVec_or (a b : BitVec 8) :
ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b
source
@[simp]
theorem Int16.ofBitVec_or (a b : BitVec 16) :
ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b
source
@[simp]
theorem Int32.ofBitVec_or (a b : BitVec 32) :
ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b
source
@[simp]
theorem Int64.ofBitVec_or (a b : BitVec 64) :
ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b
source
@[simp]
theorem ISize.ofBitVec_or (a b : BitVec System.Platform.numBits) :
ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b
source
@[simp]
theorem Int8.ofBitVec_xor (a b : BitVec 8) :
ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b
source
@[simp]
theorem Int16.ofBitVec_xor (a b : BitVec 16) :
ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b
source
@[simp]
theorem Int32.ofBitVec_xor (a b : BitVec 32) :
ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b
source
@[simp]
theorem Int64.ofBitVec_xor (a b : BitVec 64) :
ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b
source
@[simp]
theorem ISize.ofBitVec_xor (a b : BitVec System.Platform.numBits) :
ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b
source
@[simp]
theorem Int8.ofBitVec_not (a : BitVec 8) :
ofBitVec (~~~a) = ~~~ofBitVec a
source
@[simp]
theorem Int16.ofBitVec_not (a : BitVec 16) :
ofBitVec (~~~a) = ~~~ofBitVec a
source
@[simp]
theorem Int32.ofBitVec_not (a : BitVec 32) :
ofBitVec (~~~a) = ~~~ofBitVec a
source
@[simp]
theorem Int64.ofBitVec_not (a : BitVec 64) :
ofBitVec (~~~a) = ~~~ofBitVec a
source
@[simp]
theorem ISize.ofBitVec_not (a : BitVec System.Platform.numBits) :
ofBitVec (~~~a) = ~~~ofBitVec a
source
@[simp]
theorem Int8.ofBitVec_intMin :
ofBitVec (BitVec.intMin 8) = minValue
source
@[simp]
theorem Int16.ofBitVec_intMin :
ofBitVec (BitVec.intMin 16) = minValue
source
@[simp]
theorem Int32.ofBitVec_intMin :
ofBitVec (BitVec.intMin 32) = minValue
source
@[simp]
theorem Int64.ofBitVec_intMin :
ofBitVec (BitVec.intMin 64) = minValue
source
@[simp]
theorem ISize.ofBitVec_intMin :
ofBitVec (BitVec.intMin System.Platform.numBits) = minValue
source
@[simp]
theorem Int8.ofBitVec_intMax :
ofBitVec (BitVec.intMax 8) = maxValue
source
@[simp]
theorem Int16.ofBitVec_intMax :
ofBitVec (BitVec.intMax 16) = maxValue
source
@[simp]
theorem Int32.ofBitVec_intMax :
ofBitVec (BitVec.intMax 32) = maxValue
source
@[simp]
theorem Int64.ofBitVec_intMax :
ofBitVec (BitVec.intMax 64) = maxValue
source
@[simp]
theorem ISize.ofBitVec_intMax :
ofBitVec (BitVec.intMax System.Platform.numBits) = maxValue
source
theorem Int8.neg_eq_not_add (a : Int8) :
-a = ~~~a + 1
source
theorem Int16.neg_eq_not_add (a : Int16) :
-a = ~~~a + 1
source
theorem Int32.neg_eq_not_add (a : Int32) :
-a = ~~~a + 1
source
theorem Int64.neg_eq_not_add (a : Int64) :
-a = ~~~a + 1
source
theorem ISize.neg_eq_not_add (a : ISize) :
-a = ~~~a + 1
source
theorem Int8.not_eq_neg_sub (a : Int8) :
~~~a = -a - 1
source
theorem Int16.not_eq_neg_sub (a : Int16) :
~~~a = -a - 1
source
theorem Int32.not_eq_neg_sub (a : Int32) :
~~~a = -a - 1
source
theorem Int64.not_eq_neg_sub (a : Int64) :
~~~a = -a - 1
source
theorem ISize.not_eq_neg_sub (a : ISize) :
~~~a = -a - 1
source
theorem Int8.or_assoc (a b c : Int8) :
a ||| b ||| c = a ||| (b ||| c)
source
theorem Int16.or_assoc (a b c : Int16) :
a ||| b ||| c = a ||| (b ||| c)
source
theorem Int32.or_assoc (a b c : Int32) :
a ||| b ||| c = a ||| (b ||| c)
source
theorem Int64.or_assoc (a b c : Int64) :
a ||| b ||| c = a ||| (b ||| c)
source
theorem ISize.or_assoc (a b c : ISize) :
a ||| b ||| c = a ||| (b ||| c)
source
instance instAssociativeInt8HOr :
Std.Associative fun (x1 x2 : Int8) => x1 ||| x2
source
instance instAssociativeInt16HOr :
Std.Associative fun (x1 x2 : Int16) => x1 ||| x2
source
instance instAssociativeInt32HOr :
Std.Associative fun (x1 x2 : Int32) => x1 ||| x2
source
instance instAssociativeInt64HOr :
Std.Associative fun (x1 x2 : Int64) => x1 ||| x2
source
instance instAssociativeISizeHOr :
Std.Associative fun (x1 x2 : ISize) => x1 ||| x2
source
theorem Int8.or_comm (a b : Int8) :
a ||| b = b ||| a
source
theorem Int16.or_comm (a b : Int16) :
a ||| b = b ||| a
source
theorem Int32.or_comm (a b : Int32) :
a ||| b = b ||| a
source
theorem Int64.or_comm (a b : Int64) :
a ||| b = b ||| a
source
theorem ISize.or_comm (a b : ISize) :
a ||| b = b ||| a
source
instance instCommutativeInt8HOr :
Std.Commutative fun (x1 x2 : Int8) => x1 ||| x2
source
instance instCommutativeInt16HOr :
Std.Commutative fun (x1 x2 : Int16) => x1 ||| x2
source
instance instCommutativeInt32HOr :
Std.Commutative fun (x1 x2 : Int32) => x1 ||| x2
source
instance instCommutativeInt64HOr :
Std.Commutative fun (x1 x2 : Int64) => x1 ||| x2
source
instance instCommutativeISizeHOr :
Std.Commutative fun (x1 x2 : ISize) => x1 ||| x2
source
@[simp]
theorem Int8.or_self {a : Int8} :
a ||| a = a
source
@[simp]
theorem Int16.or_self {a : Int16} :
a ||| a = a
source
@[simp]
theorem Int32.or_self {a : Int32} :
a ||| a = a
source
@[simp]
theorem Int64.or_self {a : Int64} :
a ||| a = a
source
@[simp]
theorem ISize.or_self {a : ISize} :
a ||| a = a
source
instance instIdempotentOpInt8HOr :
Std.IdempotentOp fun (x1 x2 : Int8) => x1 ||| x2
source
instance instIdempotentOpInt16HOr :
Std.IdempotentOp fun (x1 x2 : Int16) => x1 ||| x2
source
instance instIdempotentOpInt32HOr :
Std.IdempotentOp fun (x1 x2 : Int32) => x1 ||| x2
source
instance instIdempotentOpInt64HOr :
Std.IdempotentOp fun (x1 x2 : Int64) => x1 ||| x2
source
instance instIdempotentOpISizeHOr :
Std.IdempotentOp fun (x1 x2 : ISize) => x1 ||| x2
source
@[simp]
theorem Int8.or_zero {a : Int8} :
a ||| 0 = a
source
@[simp]
theorem Int16.or_zero {a : Int16} :
a ||| 0 = a
source
@[simp]
theorem Int32.or_zero {a : Int32} :
a ||| 0 = a
source
@[simp]
theorem Int64.or_zero {a : Int64} :
a ||| 0 = a
source
@[simp]
theorem ISize.or_zero {a : ISize} :
a ||| 0 = a
source
@[simp]
theorem Int8.zero_or {a : Int8} :
0 ||| a = a
source
@[simp]
theorem Int16.zero_or {a : Int16} :
0 ||| a = a
source
@[simp]
theorem Int32.zero_or {a : Int32} :
0 ||| a = a
source
@[simp]
theorem Int64.zero_or {a : Int64} :
0 ||| a = a
source
@[simp]
theorem ISize.zero_or {a : ISize} :
0 ||| a = a
source
instance instLawfulCommIdentityInt8HOrOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int8) => x1 ||| x2) 0
source
instance instLawfulCommIdentityInt16HOrOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int16) => x1 ||| x2) 0
source
instance instLawfulCommIdentityInt32HOrOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int32) => x1 ||| x2) 0
source
instance instLawfulCommIdentityInt64HOrOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int64) => x1 ||| x2) 0
source
instance instLawfulCommIdentityISizeHOrOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : ISize) => x1 ||| x2) 0
source
@[simp]
theorem Int8.neg_one_or {a : Int8} :
-1 ||| a = -1
source
@[simp]
theorem Int16.neg_one_or {a : Int16} :
-1 ||| a = -1
source
@[simp]
theorem Int32.neg_one_or {a : Int32} :
-1 ||| a = -1
source
@[simp]
theorem Int64.neg_one_or {a : Int64} :
-1 ||| a = -1
source
@[simp]
theorem ISize.neg_one_or {a : ISize} :
-1 ||| a = -1
source
@[simp]
theorem Int8.or_neg_one {a : Int8} :
a ||| -1 = -1
source
@[simp]
theorem Int16.or_neg_one {a : Int16} :
a ||| -1 = -1
source
@[simp]
theorem Int32.or_neg_one {a : Int32} :
a ||| -1 = -1
source
@[simp]
theorem Int64.or_neg_one {a : Int64} :
a ||| -1 = -1
source
@[simp]
theorem ISize.or_neg_one {a : ISize} :
a ||| -1 = -1
source
@[simp]
theorem Int8.or_eq_zero_iff {a b : Int8} :
a ||| b = 0 ↔ a = 0 ∧ b = 0
source
@[simp]
theorem Int16.or_eq_zero_iff {a b : Int16} :
a ||| b = 0 ↔ a = 0 ∧ b = 0
source
@[simp]
theorem Int32.or_eq_zero_iff {a b : Int32} :
a ||| b = 0 ↔ a = 0 ∧ b = 0
source
@[simp]
theorem Int64.or_eq_zero_iff {a b : Int64} :
a ||| b = 0 ↔ a = 0 ∧ b = 0
source
@[simp]
theorem ISize.or_eq_zero_iff {a b : ISize} :
a ||| b = 0 ↔ a = 0 ∧ b = 0
source
theorem Int8.and_assoc (a b c : Int8) :
a &&& b &&& c = a &&& (b &&& c)
source
theorem Int16.and_assoc (a b c : Int16) :
a &&& b &&& c = a &&& (b &&& c)
source
theorem Int32.and_assoc (a b c : Int32) :
a &&& b &&& c = a &&& (b &&& c)
source
theorem Int64.and_assoc (a b c : Int64) :
a &&& b &&& c = a &&& (b &&& c)
source
theorem ISize.and_assoc (a b c : ISize) :
a &&& b &&& c = a &&& (b &&& c)
source
instance instAssociativeInt8HAnd :
Std.Associative fun (x1 x2 : Int8) => x1 &&& x2
source
instance instAssociativeInt16HAnd :
Std.Associative fun (x1 x2 : Int16) => x1 &&& x2
source
instance instAssociativeInt32HAnd :
Std.Associative fun (x1 x2 : Int32) => x1 &&& x2
source
instance instAssociativeInt64HAnd :
Std.Associative fun (x1 x2 : Int64) => x1 &&& x2
source
instance instAssociativeISizeHAnd :
Std.Associative fun (x1 x2 : ISize) => x1 &&& x2
source
theorem Int8.and_comm (a b : Int8) :
a &&& b = b &&& a
source
theorem Int16.and_comm (a b : Int16) :
a &&& b = b &&& a
source
theorem Int32.and_comm (a b : Int32) :
a &&& b = b &&& a
source
theorem Int64.and_comm (a b : Int64) :
a &&& b = b &&& a
source
theorem ISize.and_comm (a b : ISize) :
a &&& b = b &&& a
source
instance instCommutativeInt8HAnd :
Std.Commutative fun (x1 x2 : Int8) => x1 &&& x2
source
instance instCommutativeInt16HAnd :
Std.Commutative fun (x1 x2 : Int16) => x1 &&& x2
source
instance instCommutativeInt32HAnd :
Std.Commutative fun (x1 x2 : Int32) => x1 &&& x2
source
instance instCommutativeInt64HAnd :
Std.Commutative fun (x1 x2 : Int64) => x1 &&& x2
source
instance instCommutativeISizeHAnd :
Std.Commutative fun (x1 x2 : ISize) => x1 &&& x2
source
@[simp]
theorem Int8.and_self {a : Int8} :
a &&& a = a
source
@[simp]
theorem Int16.and_self {a : Int16} :
a &&& a = a
source
@[simp]
theorem Int32.and_self {a : Int32} :
a &&& a = a
source
@[simp]
theorem Int64.and_self {a : Int64} :
a &&& a = a
source
@[simp]
theorem ISize.and_self {a : ISize} :
a &&& a = a
source
instance instIdempotentOpInt8HAnd :
Std.IdempotentOp fun (x1 x2 : Int8) => x1 &&& x2
source
instance instIdempotentOpInt16HAnd :
Std.IdempotentOp fun (x1 x2 : Int16) => x1 &&& x2
source
instance instIdempotentOpInt32HAnd :
Std.IdempotentOp fun (x1 x2 : Int32) => x1 &&& x2
source
instance instIdempotentOpInt64HAnd :
Std.IdempotentOp fun (x1 x2 : Int64) => x1 &&& x2
source
instance instIdempotentOpISizeHAnd :
Std.IdempotentOp fun (x1 x2 : ISize) => x1 &&& x2
source
@[simp]
theorem Int8.and_zero {a : Int8} :
a &&& 0 = 0
source
@[simp]
theorem Int16.and_zero {a : Int16} :
a &&& 0 = 0
source
@[simp]
theorem Int32.and_zero {a : Int32} :
a &&& 0 = 0
source
@[simp]
theorem Int64.and_zero {a : Int64} :
a &&& 0 = 0
source
@[simp]
theorem ISize.and_zero {a : ISize} :
a &&& 0 = 0
source
@[simp]
theorem Int8.zero_and {a : Int8} :
0 &&& a = 0
source
@[simp]
theorem Int16.zero_and {a : Int16} :
0 &&& a = 0
source
@[simp]
theorem Int32.zero_and {a : Int32} :
0 &&& a = 0
source
@[simp]
theorem Int64.zero_and {a : Int64} :
0 &&& a = 0
source
@[simp]
theorem ISize.zero_and {a : ISize} :
0 &&& a = 0
source
@[simp]
theorem Int8.neg_one_and {a : Int8} :
-1 &&& a = a
source
@[simp]
theorem Int16.neg_one_and {a : Int16} :
-1 &&& a = a
source
@[simp]
theorem Int32.neg_one_and {a : Int32} :
-1 &&& a = a
source
@[simp]
theorem Int64.neg_one_and {a : Int64} :
-1 &&& a = a
source
@[simp]
theorem ISize.neg_one_and {a : ISize} :
-1 &&& a = a
source
@[simp]
theorem Int8.and_neg_one {a : Int8} :
a &&& -1 = a
source
@[simp]
theorem Int16.and_neg_one {a : Int16} :
a &&& -1 = a
source
@[simp]
theorem Int32.and_neg_one {a : Int32} :
a &&& -1 = a
source
@[simp]
theorem Int64.and_neg_one {a : Int64} :
a &&& -1 = a
source
@[simp]
theorem ISize.and_neg_one {a : ISize} :
a &&& -1 = a
source
instance instLawfulCommIdentityInt8HAndNegOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int8) => x1 &&& x2) (-1)
source
instance instLawfulCommIdentityInt16HAndNegOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int16) => x1 &&& x2) (-1)
source
instance instLawfulCommIdentityInt32HAndNegOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int32) => x1 &&& x2) (-1)
source
instance instLawfulCommIdentityInt64HAndNegOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int64) => x1 &&& x2) (-1)
source
instance instLawfulCommIdentityISizeHAndNegOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : ISize) => x1 &&& x2) (-1)
source
@[simp]
theorem Int8.and_eq_neg_one_iff {a b : Int8} :
a &&& b = -1 ↔ a = -1 ∧ b = -1
source
@[simp]
theorem Int16.and_eq_neg_one_iff {a b : Int16} :
a &&& b = -1 ↔ a = -1 ∧ b = -1
source
@[simp]
theorem Int32.and_eq_neg_one_iff {a b : Int32} :
a &&& b = -1 ↔ a = -1 ∧ b = -1
source
@[simp]
theorem Int64.and_eq_neg_one_iff {a b : Int64} :
a &&& b = -1 ↔ a = -1 ∧ b = -1
source
@[simp]
theorem ISize.and_eq_neg_one_iff {a b : ISize} :
a &&& b = -1 ↔ a = -1 ∧ b = -1
source
theorem Int8.xor_assoc (a b c : Int8) :
a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
source
theorem Int16.xor_assoc (a b c : Int16) :
a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
source
theorem Int32.xor_assoc (a b c : Int32) :
a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
source
theorem Int64.xor_assoc (a b c : Int64) :
a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
source
theorem ISize.xor_assoc (a b c : ISize) :
a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
source
instance instAssociativeInt8HXor :
Std.Associative fun (x1 x2 : Int8) => x1 ^^^ x2
source
instance instAssociativeInt16HXor :
Std.Associative fun (x1 x2 : Int16) => x1 ^^^ x2
source
instance instAssociativeInt32HXor :
Std.Associative fun (x1 x2 : Int32) => x1 ^^^ x2
source
instance instAssociativeInt64HXor :
Std.Associative fun (x1 x2 : Int64) => x1 ^^^ x2
source
instance instAssociativeISizeHXor :
Std.Associative fun (x1 x2 : ISize) => x1 ^^^ x2
source
theorem Int8.xor_comm (a b : Int8) :
a ^^^ b = b ^^^ a
source
theorem Int16.xor_comm (a b : Int16) :
a ^^^ b = b ^^^ a
source
theorem Int32.xor_comm (a b : Int32) :
a ^^^ b = b ^^^ a
source
theorem Int64.xor_comm (a b : Int64) :
a ^^^ b = b ^^^ a
source
theorem ISize.xor_comm (a b : ISize) :
a ^^^ b = b ^^^ a
source
instance instCommutativeInt8HXor :
Std.Commutative fun (x1 x2 : Int8) => x1 ^^^ x2
source
instance instCommutativeInt16HXor :
Std.Commutative fun (x1 x2 : Int16) => x1 ^^^ x2
source
instance instCommutativeInt32HXor :
Std.Commutative fun (x1 x2 : Int32) => x1 ^^^ x2
source
instance instCommutativeInt64HXor :
Std.Commutative fun (x1 x2 : Int64) => x1 ^^^ x2
source
instance instCommutativeISizeHXor :
Std.Commutative fun (x1 x2 : ISize) => x1 ^^^ x2
source
@[simp]
theorem Int8.xor_self {a : Int8} :
a ^^^ a = 0
source
@[simp]
theorem Int16.xor_self {a : Int16} :
a ^^^ a = 0
source
@[simp]
theorem Int32.xor_self {a : Int32} :
a ^^^ a = 0
source
@[simp]
theorem Int64.xor_self {a : Int64} :
a ^^^ a = 0
source
@[simp]
theorem ISize.xor_self {a : ISize} :
a ^^^ a = 0
source
@[simp]
theorem Int8.xor_zero {a : Int8} :
a ^^^ 0 = a
source
@[simp]
theorem Int16.xor_zero {a : Int16} :
a ^^^ 0 = a
source
@[simp]
theorem Int32.xor_zero {a : Int32} :
a ^^^ 0 = a
source
@[simp]
theorem Int64.xor_zero {a : Int64} :
a ^^^ 0 = a
source
@[simp]
theorem ISize.xor_zero {a : ISize} :
a ^^^ 0 = a
source
@[simp]
theorem Int8.zero_xor {a : Int8} :
0 ^^^ a = a
source
@[simp]
theorem Int16.zero_xor {a : Int16} :
0 ^^^ a = a
source
@[simp]
theorem Int32.zero_xor {a : Int32} :
0 ^^^ a = a
source
@[simp]
theorem Int64.zero_xor {a : Int64} :
0 ^^^ a = a
source
@[simp]
theorem ISize.zero_xor {a : ISize} :
0 ^^^ a = a
source
@[simp]
theorem Int8.neg_one_xor {a : Int8} :
-1 ^^^ a = ~~~a
source
@[simp]
theorem Int16.neg_one_xor {a : Int16} :
-1 ^^^ a = ~~~a
source
@[simp]
theorem Int32.neg_one_xor {a : Int32} :
-1 ^^^ a = ~~~a
source
@[simp]
theorem Int64.neg_one_xor {a : Int64} :
-1 ^^^ a = ~~~a
source
@[simp]
theorem ISize.neg_one_xor {a : ISize} :
-1 ^^^ a = ~~~a
source
@[simp]
theorem Int8.xor_neg_one {a : Int8} :
a ^^^ -1 = ~~~a
source
@[simp]
theorem Int16.xor_neg_one {a : Int16} :
a ^^^ -1 = ~~~a
source
@[simp]
theorem Int32.xor_neg_one {a : Int32} :
a ^^^ -1 = ~~~a
source
@[simp]
theorem Int64.xor_neg_one {a : Int64} :
a ^^^ -1 = ~~~a
source
@[simp]
theorem ISize.xor_neg_one {a : ISize} :
a ^^^ -1 = ~~~a
source
instance instLawfulCommIdentityInt8HXorOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int8) => x1 ^^^ x2) 0
source
instance instLawfulCommIdentityInt16HXorOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int16) => x1 ^^^ x2) 0
source
instance instLawfulCommIdentityInt32HXorOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int32) => x1 ^^^ x2) 0
source
instance instLawfulCommIdentityInt64HXorOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int64) => x1 ^^^ x2) 0
source
instance instLawfulCommIdentityISizeHXorOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : ISize) => x1 ^^^ x2) 0
source
@[simp]
theorem Int8.xor_eq_zero_iff {a b : Int8} :
a ^^^ b = 0 ↔ a = b
source
@[simp]
theorem Int16.xor_eq_zero_iff {a b : Int16} :
a ^^^ b = 0 ↔ a = b
source
@[simp]
theorem Int32.xor_eq_zero_iff {a b : Int32} :
a ^^^ b = 0 ↔ a = b
source
@[simp]
theorem Int64.xor_eq_zero_iff {a b : Int64} :
a ^^^ b = 0 ↔ a = b
source
@[simp]
theorem ISize.xor_eq_zero_iff {a b : ISize} :
a ^^^ b = 0 ↔ a = b
source
@[simp]
theorem Int8.xor_left_inj {a b : Int8} (c : Int8) :
a ^^^ c = b ^^^ c ↔ a = b
source
@[simp]
theorem Int16.xor_left_inj {a b : Int16} (c : Int16) :
a ^^^ c = b ^^^ c ↔ a = b
source
@[simp]
theorem Int32.xor_left_inj {a b : Int32} (c : Int32) :
a ^^^ c = b ^^^ c ↔ a = b
source
@[simp]
theorem Int64.xor_left_inj {a b : Int64} (c : Int64) :
a ^^^ c = b ^^^ c ↔ a = b
source
@[simp]
theorem ISize.xor_left_inj {a b : ISize} (c : ISize) :
a ^^^ c = b ^^^ c ↔ a = b
source
@[simp]
theorem Int8.xor_right_inj {a b : Int8} (c : Int8) :
c ^^^ a = c ^^^ b ↔ a = b
source
@[simp]
theorem Int16.xor_right_inj {a b : Int16} (c : Int16) :
c ^^^ a = c ^^^ b ↔ a = b
source
@[simp]
theorem Int32.xor_right_inj {a b : Int32} (c : Int32) :
c ^^^ a = c ^^^ b ↔ a = b
source
@[simp]
theorem Int64.xor_right_inj {a b : Int64} (c : Int64) :
c ^^^ a = c ^^^ b ↔ a = b
source
@[simp]
theorem ISize.xor_right_inj {a b : ISize} (c : ISize) :
c ^^^ a = c ^^^ b ↔ a = b
source
@[simp]
theorem Int8.not_zero :
~~~0 = -1
source
@[simp]
theorem Int16.not_zero :
~~~0 = -1
source
@[simp]
theorem Int32.not_zero :
~~~0 = -1
source
@[simp]
theorem Int64.not_zero :
~~~0 = -1
source
@[simp]
theorem ISize.not_zero :
~~~0 = -1
source
@[simp]
theorem Int8.not_neg_one :
~~~(-1) = 0
source
@[simp]
theorem Int16.not_neg_one :
~~~(-1) = 0
source
@[simp]
theorem Int32.not_neg_one :
~~~(-1) = 0
source
@[simp]
theorem Int64.not_neg_one :
~~~(-1) = 0
source
@[simp]
theorem ISize.not_neg_one :
~~~(-1) = 0
source
@[simp]
theorem Int8.not_not {a : Int8} :
~~~~~~a = a
source
@[simp]
theorem Int16.not_not {a : Int16} :
~~~~~~a = a
source
@[simp]
theorem Int32.not_not {a : Int32} :
~~~~~~a = a
source
@[simp]
theorem Int64.not_not {a : Int64} :
~~~~~~a = a
source
@[simp]
theorem ISize.not_not {a : ISize} :
~~~~~~a = a
source
@[simp]
theorem Int8.not_inj {a b : Int8} :
~~~a = ~~~b ↔ a = b
source
@[simp]
theorem Int16.not_inj {a b : Int16} :
~~~a = ~~~b ↔ a = b
source
@[simp]
theorem Int32.not_inj {a b : Int32} :
~~~a = ~~~b ↔ a = b
source
@[simp]
theorem Int64.not_inj {a b : Int64} :
~~~a = ~~~b ↔ a = b
source
@[simp]
theorem ISize.not_inj {a b : ISize} :
~~~a = ~~~b ↔ a = b
source
@[simp]
theorem Int8.and_not_self {a : Int8} :
a &&& ~~~a = 0
source
@[simp]
theorem Int16.and_not_self {a : Int16} :
a &&& ~~~a = 0
source
@[simp]
theorem Int32.and_not_self {a : Int32} :
a &&& ~~~a = 0
source
@[simp]
theorem Int64.and_not_self {a : Int64} :
a &&& ~~~a = 0
source
@[simp]
theorem ISize.and_not_self {a : ISize} :
a &&& ~~~a = 0
source
@[simp]
theorem Int8.not_and_self {a : Int8} :
~~~a &&& a = 0
source
@[simp]
theorem Int16.not_and_self {a : Int16} :
~~~a &&& a = 0
source
@[simp]
theorem Int32.not_and_self {a : Int32} :
~~~a &&& a = 0
source
@[simp]
theorem Int64.not_and_self {a : Int64} :
~~~a &&& a = 0
source
@[simp]
theorem ISize.not_and_self {a : ISize} :
~~~a &&& a = 0
source
@[simp]
theorem Int8.or_not_self {a : Int8} :
a ||| ~~~a = -1
source
@[simp]
theorem Int16.or_not_self {a : Int16} :
a ||| ~~~a = -1
source
@[simp]
theorem Int32.or_not_self {a : Int32} :
a ||| ~~~a = -1
source
@[simp]
theorem Int64.or_not_self {a : Int64} :
a ||| ~~~a = -1
source
@[simp]
theorem ISize.or_not_self {a : ISize} :
a ||| ~~~a = -1
source
@[simp]
theorem Int8.not_or_self {a : Int8} :
~~~a ||| a = -1
source
@[simp]
theorem Int16.not_or_self {a : Int16} :
~~~a ||| a = -1
source
@[simp]
theorem Int32.not_or_self {a : Int32} :
~~~a ||| a = -1
source
@[simp]
theorem Int64.not_or_self {a : Int64} :
~~~a ||| a = -1
source
@[simp]
theorem ISize.not_or_self {a : ISize} :
~~~a ||| a = -1
source
theorem Int8.not_eq_comm {a b : Int8} :
~~~a = b ↔ a = ~~~b
source
theorem Int16.not_eq_comm {a b : Int16} :
~~~a = b ↔ a = ~~~b
source
theorem Int32.not_eq_comm {a b : Int32} :
~~~a = b ↔ a = ~~~b
source
theorem Int64.not_eq_comm {a b : Int64} :
~~~a = b ↔ a = ~~~b
source
theorem ISize.not_eq_comm {a b : ISize} :
~~~a = b ↔ a = ~~~b
source
@[simp]
theorem Int8.ne_not_self {a : Int8} :
a ≠ ~~~a
source
@[simp]
theorem Int16.ne_not_self {a : Int16} :
a ≠ ~~~a
source
@[simp]
theorem Int32.ne_not_self {a : Int32} :
a ≠ ~~~a
source
@[simp]
theorem Int64.ne_not_self {a : Int64} :
a ≠ ~~~a
source
@[simp]
theorem ISize.ne_not_self {a : ISize} :
a ≠ ~~~a
source
@[simp]
theorem Int8.not_ne_self {a : Int8} :
~~~a ≠ a
source
@[simp]
theorem Int16.not_ne_self {a : Int16} :
~~~a ≠ a
source
@[simp]
theorem Int32.not_ne_self {a : Int32} :
~~~a ≠ a
source
@[simp]
theorem Int64.not_ne_self {a : Int64} :
~~~a ≠ a
source
@[simp]
theorem ISize.not_ne_self {a : ISize} :
~~~a ≠ a
source
theorem Int8.not_xor {a b : Int8} :
~~~a ^^^ b = ~~~(a ^^^ b)
source
theorem Int16.not_xor {a b : Int16} :
~~~a ^^^ b = ~~~(a ^^^ b)
source
theorem Int32.not_xor {a b : Int32} :
~~~a ^^^ b = ~~~(a ^^^ b)
source
theorem Int64.not_xor {a b : Int64} :
~~~a ^^^ b = ~~~(a ^^^ b)
source
theorem ISize.not_xor {a b : ISize} :
~~~a ^^^ b = ~~~(a ^^^ b)
source
theorem Int8.xor_not {a b : Int8} :
a ^^^ ~~~b = ~~~(a ^^^ b)
source
theorem Int16.xor_not {a b : Int16} :
a ^^^ ~~~b = ~~~(a ^^^ b)
source
theorem Int32.xor_not {a b : Int32} :
a ^^^ ~~~b = ~~~(a ^^^ b)
source
theorem Int64.xor_not {a b : Int64} :
a ^^^ ~~~b = ~~~(a ^^^ b)
source
theorem ISize.xor_not {a b : ISize} :
a ^^^ ~~~b = ~~~(a ^^^ b)
source
@[simp]
theorem Int8.shiftLeft_zero {a : Int8} :
a <<< 0 = a
source
@[simp]
theorem Int16.shiftLeft_zero {a : Int16} :
a <<< 0 = a
source
@[simp]
theorem Int32.shiftLeft_zero {a : Int32} :
a <<< 0 = a
source
@[simp]
theorem Int64.shiftLeft_zero {a : Int64} :
a <<< 0 = a
source
@[simp]
theorem ISize.shiftLeft_zero {a : ISize} :
a <<< 0 = a
source
@[simp]
theorem Int8.zero_shiftLeft {a : Int8} :
0 <<< a = 0
source
@[simp]
theorem Int16.zero_shiftLeft {a : Int16} :
0 <<< a = 0
source
@[simp]
theorem Int32.zero_shiftLeft {a : Int32} :
0 <<< a = 0
source
@[simp]
theorem Int64.zero_shiftLeft {a : Int64} :
0 <<< a = 0
source
@[simp]
theorem ISize.zero_shiftLeft {a : ISize} :
0 <<< a = 0
source
theorem Int8.shiftLeft_xor {a b c : Int8} :
(a ^^^ b) <<< c = a <<< c ^^^ b <<< c
source
theorem Int16.shiftLeft_xor {a b c : Int16} :
(a ^^^ b) <<< c = a <<< c ^^^ b <<< c
source
theorem Int32.shiftLeft_xor {a b c : Int32} :
(a ^^^ b) <<< c = a <<< c ^^^ b <<< c
source
theorem Int64.shiftLeft_xor {a b c : Int64} :
(a ^^^ b) <<< c = a <<< c ^^^ b <<< c
source
theorem ISize.shiftLeft_xor {a b c : ISize} :
(a ^^^ b) <<< c = a <<< c ^^^ b <<< c
source
theorem Int8.shiftLeft_and {a b c : Int8} :
(a &&& b) <<< c = a <<< c &&& b <<< c
source
theorem Int16.shiftLeft_and {a b c : Int16} :
(a &&& b) <<< c = a <<< c &&& b <<< c
source
theorem Int32.shiftLeft_and {a b c : Int32} :
(a &&& b) <<< c = a <<< c &&& b <<< c
source
theorem Int64.shiftLeft_and {a b c : Int64} :
(a &&& b) <<< c = a <<< c &&& b <<< c
source
theorem ISize.shiftLeft_and {a b c : ISize} :
(a &&& b) <<< c = a <<< c &&& b <<< c
source
theorem Int8.shiftLeft_or {a b c : Int8} :
(a ||| b) <<< c = a <<< c ||| b <<< c
source
theorem Int16.shiftLeft_or {a b c : Int16} :
(a ||| b) <<< c = a <<< c ||| b <<< c
source
theorem Int32.shiftLeft_or {a b c : Int32} :
(a ||| b) <<< c = a <<< c ||| b <<< c
source
theorem Int64.shiftLeft_or {a b c : Int64} :
(a ||| b) <<< c = a <<< c ||| b <<< c
source
theorem ISize.shiftLeft_or {a b c : ISize} :
(a ||| b) <<< c = a <<< c ||| b <<< c
source
@[simp]
theorem Int8.neg_one_shiftLeft_and_shiftLeft {a b : Int8} :
(-1) <<< b &&& a <<< b = a <<< b
source
@[simp]
theorem Int16.neg_one_shiftLeft_and_shiftLeft {a b : Int16} :
(-1) <<< b &&& a <<< b = a <<< b
source
@[simp]
theorem Int32.neg_one_shiftLeft_and_shiftLeft {a b : Int32} :
(-1) <<< b &&& a <<< b = a <<< b
source
@[simp]
theorem Int64.neg_one_shiftLeft_and_shiftLeft {a b : Int64} :
(-1) <<< b &&& a <<< b = a <<< b
source
@[simp]
theorem ISize.neg_one_shiftLeft_and_shiftLeft {a b : ISize} :
(-1) <<< b &&& a <<< b = a <<< b
source
@[simp]
theorem Int8.neg_one_shiftLeft_or_shiftLeft {a b : Int8} :
(-1) <<< b ||| a <<< b = (-1) <<< b
source
@[simp]
theorem Int16.neg_one_shiftLeft_or_shiftLeft {a b : Int16} :
(-1) <<< b ||| a <<< b = (-1) <<< b
source
@[simp]
theorem Int32.neg_one_shiftLeft_or_shiftLeft {a b : Int32} :
(-1) <<< b ||| a <<< b = (-1) <<< b
source
@[simp]
theorem Int64.neg_one_shiftLeft_or_shiftLeft {a b : Int8} :
(-1) <<< b ||| a <<< b = (-1) <<< b
source
@[simp]
theorem ISize.neg_one_shiftLeft_or_shiftLeft {a b : ISize} :
(-1) <<< b ||| a <<< b = (-1) <<< b
source
@[simp]
theorem Int8.shiftRight_zero {a : Int8} :
a >>> 0 = a
source
@[simp]
theorem Int16.shiftRight_zero {a : Int16} :
a >>> 0 = a
source
@[simp]
theorem Int32.shiftRight_zero {a : Int32} :
a >>> 0 = a
source
@[simp]
theorem Int64.shiftRight_zero {a : Int64} :
a >>> 0 = a
source
@[simp]
theorem ISize.shiftRight_zero {a : ISize} :
a >>> 0 = a
source
@[simp]
theorem Int8.zero_shiftRight {a : Int8} :
0 >>> a = 0
source
@[simp]
theorem Int16.zero_shiftRight {a : Int16} :
0 >>> a = 0
source
@[simp]
theorem Int32.zero_shiftRight {a : Int32} :
0 >>> a = 0
source
@[simp]
theorem Int64.zero_shiftRight {a : Int64} :
0 >>> a = 0
source
@[simp]
theorem ISize.zero_shiftRight {a : ISize} :
0 >>> a = 0
source
theorem Int8.shiftRight_xor {a b c : Int8} :
(a ^^^ b) >>> c = a >>> c ^^^ b >>> c
source
theorem Int16.shiftRight_xor {a b c : Int16} :
(a ^^^ b) >>> c = a >>> c ^^^ b >>> c
source
theorem Int32.shiftRight_xor {a b c : Int32} :
(a ^^^ b) >>> c = a >>> c ^^^ b >>> c
source
theorem Int64.shiftRight_xor {a b c : Int64} :
(a ^^^ b) >>> c = a >>> c ^^^ b >>> c
source
theorem ISize.shiftRight_xor {a b c : ISize} :
(a ^^^ b) >>> c = a >>> c ^^^ b >>> c
source
theorem Int8.shiftRight_and {a b c : Int8} :
(a &&& b) >>> c = a >>> c &&& b >>> c
source
theorem Int16.shiftRight_and {a b c : Int16} :
(a &&& b) >>> c = a >>> c &&& b >>> c
source
theorem Int32.shiftRight_and {a b c : Int32} :
(a &&& b) >>> c = a >>> c &&& b >>> c
source
theorem Int64.shiftRight_and {a b c : Int64} :
(a &&& b) >>> c = a >>> c &&& b >>> c
source
theorem ISize.shiftRight_and {a b c : ISize} :
(a &&& b) >>> c = a >>> c &&& b >>> c
source
theorem Int8.shiftRight_or {a b c : Int8} :
(a ||| b) >>> c = a >>> c ||| b >>> c
source
theorem Int16.shiftRight_or {a b c : Int16} :
(a ||| b) >>> c = a >>> c ||| b >>> c
source
theorem Int32.shiftRight_or {a b c : Int32} :
(a ||| b) >>> c = a >>> c ||| b >>> c
source
theorem Int64.shiftRight_or {a b c : Int64} :
(a ||| b) >>> c = a >>> c ||| b >>> c
source
theorem ISize.shiftRight_or {a b c : ISize} :
(a ||| b) >>> c = a >>> c ||| b >>> c