Documentation

Init.Data.SInt.Bitwise

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