def commandDeclare_bitwise_int_theorems__ : Lean.ParserDescr

Equations

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

@[simp]

theorem Int8.toBitVec_shiftRight (a b : Int8) : (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 8)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int8.toBitVec_shiftLeft (a b : Int8) : (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 8

@[simp]

theorem Int8.toBitVec_abs (a : Int8) : a.abs.toBitVec = a.toBitVec.abs

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int16.toBitVec_shiftLeft (a b : Int16) : (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 16

@[simp]

theorem Int16.toBitVec_shiftRight (a b : Int16) : (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 16)

@[simp]

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

@[simp]

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

@[simp]

theorem Int16.toBitVec_abs (a : Int16) : a.abs.toBitVec = a.toBitVec.abs

@[simp]

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

@[simp]

theorem Int32.toBitVec_shiftRight (a b : Int32) : (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 32)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int32.toBitVec_abs (a : Int32) : a.abs.toBitVec = a.toBitVec.abs

@[simp]

theorem Int32.toBitVec_shiftLeft (a b : Int32) : (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 32

@[simp]

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

@[simp]

theorem Int64.toBitVec_shiftRight (a b : Int64) : (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 64)

@[simp]

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

@[simp]

theorem Int64.toBitVec_shiftLeft (a b : Int64) : (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 64

@[simp]

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

@[simp]

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

@[simp]

theorem Int64.toBitVec_abs (a : Int64) : a.abs.toBitVec = a.toBitVec.abs

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ISize.toBitVec_shiftLeft (a b : ISize) : (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod ↑System.Platform.numBits

@[simp]

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

@[simp]

theorem ISize.toBitVec_abs (a : ISize) : a.abs.toBitVec = a.toBitVec.abs

@[simp]

theorem ISize.toBitVec_shiftRight (a b : ISize) : (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod ↑System.Platform.numBits)

@[simp]

theorem Bool.toBitVec_toInt8 {b : Bool} : b.toInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)

@[simp]

theorem Bool.toBitVec_toInt16 {b : Bool} : b.toInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)

@[simp]

theorem Bool.toBitVec_toInt32 {b : Bool} : b.toInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)

@[simp]

theorem Bool.toBitVec_toInt64 {b : Bool} : b.toInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)

@[simp]

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

@[simp]

theorem UInt8.toInt8_and (a b : UInt8) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8

@[simp]

theorem UInt16.toInt16_and (a b : UInt16) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16

@[simp]

theorem UInt32.toInt32_and (a b : UInt32) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32

@[simp]

theorem UInt64.toInt64_and (a b : UInt64) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64

@[simp]

theorem USize.toISize_and (a b : USize) : (a &&& b).toISize = a.toISize &&& b.toISize

@[simp]

theorem UInt8.toInt8_or (a b : UInt8) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8

@[simp]

theorem UInt16.toInt16_or (a b : UInt16) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16

@[simp]

theorem UInt32.toInt32_or (a b : UInt32) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32

@[simp]

theorem UInt64.toInt64_or (a b : UInt64) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64

@[simp]

theorem USize.toISize_or (a b : USize) : (a ||| b).toISize = a.toISize ||| b.toISize

@[simp]

theorem UInt8.toInt8_xor (a b : UInt8) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8

@[simp]

theorem UInt16.toInt16_xor (a b : UInt16) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16

@[simp]

theorem UInt32.toInt32_xor (a b : UInt32) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32

@[simp]

theorem UInt64.toInt64_xor (a b : UInt64) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64

@[simp]

theorem USize.toISize_xor (a b : USize) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize

@[simp]

theorem UInt8.toInt8_not (a : UInt8) : (~~~a).toInt8 = ~~~a.toInt8

@[simp]

theorem UInt16.toInt16_not (a : UInt16) : (~~~a).toInt16 = ~~~a.toInt16

@[simp]

theorem UInt32.toInt32_not (a : UInt32) : (~~~a).toInt32 = ~~~a.toInt32

@[simp]

theorem UInt64.toInt64_not (a : UInt64) : (~~~a).toInt64 = ~~~a.toInt64

@[simp]

theorem USize.toISize_not (a : USize) : (~~~a).toISize = ~~~a.toISize

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int64.toUInt64_not (a : Int64) : (~~~a).toUInt64 = ~~~a.toUInt64

@[simp]

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

@[simp]

theorem Int8.toInt16_and (a b : Int8) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16

@[simp]

theorem Int8.toInt32_and (a b : Int8) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32

@[simp]

theorem Int8.toInt64_and (a b : Int8) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64

@[simp]

theorem Int8.toISize_and (a b : Int8) : (a &&& b).toISize = a.toISize &&& b.toISize

@[simp]

theorem Int16.toInt8_and (a b : Int16) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8

@[simp]

theorem Int16.toInt32_and (a b : Int16) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32

@[simp]

theorem Int16.toInt64_and (a b : Int16) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64

@[simp]

theorem Int16.toISize_and (a b : Int16) : (a &&& b).toISize = a.toISize &&& b.toISize

@[simp]

theorem Int32.toInt8_and (a b : Int32) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8

@[simp]

theorem Int32.toInt16_and (a b : Int32) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16

@[simp]

theorem Int32.toInt64_and (a b : Int32) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64

@[simp]

theorem Int32.toISize_and (a b : Int32) : (a &&& b).toISize = a.toISize &&& b.toISize

@[simp]

theorem ISize.toInt8_and (a b : ISize) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8

@[simp]

theorem ISize.toInt16_and (a b : ISize) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16

@[simp]

theorem ISize.toInt32_and (a b : ISize) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32

@[simp]

theorem ISize.toInt64_and (a b : ISize) : (a &&& b).toInt64 = a.toInt64 &&& b.toInt64

@[simp]

theorem Int64.toInt8_and (a b : Int64) : (a &&& b).toInt8 = a.toInt8 &&& b.toInt8

@[simp]

theorem Int64.toInt16_and (a b : Int64) : (a &&& b).toInt16 = a.toInt16 &&& b.toInt16

@[simp]

theorem Int64.toInt32_and (a b : Int64) : (a &&& b).toInt32 = a.toInt32 &&& b.toInt32

@[simp]

theorem Int64.toISize_and (a b : Int64) : (a &&& b).toISize = a.toISize &&& b.toISize

@[simp]

theorem Int8.toInt16_or (a b : Int8) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16

@[simp]

theorem Int8.toInt32_or (a b : Int8) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32

@[simp]

theorem Int8.toInt64_or (a b : Int8) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64

@[simp]

theorem Int8.toISize_or (a b : Int8) : (a ||| b).toISize = a.toISize ||| b.toISize

@[simp]

theorem Int16.toInt8_or (a b : Int16) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8

@[simp]

theorem Int16.toInt32_or (a b : Int16) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32

@[simp]

theorem Int16.toInt64_or (a b : Int16) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64

@[simp]

theorem Int16.toISize_or (a b : Int16) : (a ||| b).toISize = a.toISize ||| b.toISize

@[simp]

theorem Int32.toInt8_or (a b : Int32) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8

@[simp]

theorem Int32.toInt16_or (a b : Int32) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16

@[simp]

theorem Int32.toInt64_or (a b : Int32) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64

@[simp]

theorem Int32.toISize_or (a b : Int32) : (a ||| b).toISize = a.toISize ||| b.toISize

@[simp]

theorem ISize.toInt8_or (a b : ISize) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8

@[simp]

theorem ISize.toInt16_or (a b : ISize) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16

@[simp]

theorem ISize.toInt32_or (a b : ISize) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32

@[simp]

theorem ISize.toInt64_or (a b : ISize) : (a ||| b).toInt64 = a.toInt64 ||| b.toInt64

@[simp]

theorem Int64.toInt8_or (a b : Int64) : (a ||| b).toInt8 = a.toInt8 ||| b.toInt8

@[simp]

theorem Int64.toInt16_or (a b : Int64) : (a ||| b).toInt16 = a.toInt16 ||| b.toInt16

@[simp]

theorem Int64.toInt32_or (a b : Int64) : (a ||| b).toInt32 = a.toInt32 ||| b.toInt32

@[simp]

theorem Int64.toISize_or (a b : Int64) : (a ||| b).toISize = a.toISize ||| b.toISize

@[simp]

theorem Int8.toInt16_xor (a b : Int8) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16

@[simp]

theorem Int8.toInt32_xor (a b : Int8) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32

@[simp]

theorem Int8.toInt64_xor (a b : Int8) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64

@[simp]

theorem Int8.toISize_xor (a b : Int8) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize

@[simp]

theorem Int16.toInt8_xor (a b : Int16) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8

@[simp]

theorem Int16.toInt32_xor (a b : Int16) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32

@[simp]

theorem Int16.toInt64_xor (a b : Int16) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64

@[simp]

theorem Int16.toISize_xor (a b : Int16) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize

@[simp]

theorem Int32.toInt8_xor (a b : Int32) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8

@[simp]

theorem Int32.toInt16_xor (a b : Int32) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16

@[simp]

theorem Int32.toInt64_xor (a b : Int32) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64

@[simp]

theorem Int32.toISize_xor (a b : Int32) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize

@[simp]

theorem ISize.toInt8_xor (a b : ISize) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8

@[simp]

theorem ISize.toInt16_xor (a b : ISize) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16

@[simp]

theorem ISize.toInt32_xor (a b : ISize) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32

@[simp]

theorem ISize.toInt64_xor (a b : ISize) : (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64

@[simp]

theorem Int64.toInt8_xor (a b : Int64) : (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8

@[simp]

theorem Int64.toInt16_xor (a b : Int64) : (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16

@[simp]

theorem Int64.toInt32_xor (a b : Int64) : (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32

@[simp]

theorem Int64.toISize_xor (a b : Int64) : (a ^^^ b).toISize = a.toISize ^^^ b.toISize

theorem Int8.not_eq_neg_add (a : Int8) : ~~~a = -a - 1

theorem Int16.not_eq_neg_add (a : Int16) : ~~~a = -a - 1

theorem Int32.not_eq_neg_add (a : Int32) : ~~~a = -a - 1

theorem Int64.not_eq_neg_add (a : Int64) : ~~~a = -a - 1

theorem ISize.not_eq_neg_add (a : ISize) : ~~~a = -a - 1

@[simp]

theorem Int8.toInt_not (a : Int8) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 8)

@[simp]

theorem Int16.toInt_not (a : Int16) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 16)

@[simp]

theorem Int32.toInt_not (a : Int32) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 32)

@[simp]

theorem Int64.toInt_not (a : Int64) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 64)

@[simp]

theorem ISize.toInt_not (a : ISize) : (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ System.Platform.numBits)

@[simp]

theorem Int16.toInt8_not (a : Int16) : (~~~a).toInt8 = ~~~a.toInt8

@[simp]

theorem Int32.toInt8_not (a : Int32) : (~~~a).toInt8 = ~~~a.toInt8

@[simp]

theorem Int64.toInt8_not (a : Int64) : (~~~a).toInt8 = ~~~a.toInt8

@[simp]

theorem ISize.toInt8_not (a : ISize) : (~~~a).toInt8 = ~~~a.toInt8

@[simp]

theorem Int32.toInt16_not (a : Int32) : (~~~a).toInt16 = ~~~a.toInt16

@[simp]

theorem Int64.toInt16_not (a : Int64) : (~~~a).toInt16 = ~~~a.toInt16

@[simp]

theorem ISize.toInt16_not (a : ISize) : (~~~a).toInt16 = ~~~a.toInt16

@[simp]

theorem Int64.toInt32_not (a : Int64) : (~~~a).toInt32 = ~~~a.toInt32

@[simp]

theorem ISize.toInt32_not (a : ISize) : (~~~a).toInt32 = ~~~a.toInt32

@[simp]

theorem Int64.toISize_not (a : Int64) : (~~~a).toISize = ~~~a.toISize

@[simp]

theorem Int8.ofBitVec_and (a b : BitVec 8) : ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b

@[simp]

theorem Int16.ofBitVec_and (a b : BitVec 16) : ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b

@[simp]

theorem Int32.ofBitVec_and (a b : BitVec 32) : ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b

@[simp]

theorem Int64.ofBitVec_and (a b : BitVec 64) : ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b

@[simp]

theorem ISize.ofBitVec_and (a b : BitVec System.Platform.numBits) : ofBitVec (a &&& b) = ofBitVec a &&& ofBitVec b

@[simp]

theorem Int8.ofBitVec_or (a b : BitVec 8) : ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b

@[simp]

theorem Int16.ofBitVec_or (a b : BitVec 16) : ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b

@[simp]

theorem Int32.ofBitVec_or (a b : BitVec 32) : ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b

@[simp]

theorem Int64.ofBitVec_or (a b : BitVec 64) : ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b

@[simp]

theorem ISize.ofBitVec_or (a b : BitVec System.Platform.numBits) : ofBitVec (a ||| b) = ofBitVec a ||| ofBitVec b

@[simp]

theorem Int8.ofBitVec_xor (a b : BitVec 8) : ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b

@[simp]

theorem Int16.ofBitVec_xor (a b : BitVec 16) : ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b

@[simp]

theorem Int32.ofBitVec_xor (a b : BitVec 32) : ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b

@[simp]

theorem Int64.ofBitVec_xor (a b : BitVec 64) : ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b

@[simp]

theorem ISize.ofBitVec_xor (a b : BitVec System.Platform.numBits) : ofBitVec (a ^^^ b) = ofBitVec a ^^^ ofBitVec b

@[simp]

theorem Int8.ofBitVec_not (a : BitVec 8) : ofBitVec (~~~a) = ~~~ofBitVec a

@[simp]

theorem Int16.ofBitVec_not (a : BitVec 16) : ofBitVec (~~~a) = ~~~ofBitVec a

@[simp]

theorem Int32.ofBitVec_not (a : BitVec 32) : ofBitVec (~~~a) = ~~~ofBitVec a

@[simp]

theorem Int64.ofBitVec_not (a : BitVec 64) : ofBitVec (~~~a) = ~~~ofBitVec a

@[simp]

theorem ISize.ofBitVec_not (a : BitVec System.Platform.numBits) : ofBitVec (~~~a) = ~~~ofBitVec a

@[simp]

theorem Int8.ofBitVec_intMin : ofBitVec (BitVec.intMin 8) = minValue

@[simp]

theorem Int16.ofBitVec_intMin : ofBitVec (BitVec.intMin 16) = minValue

@[simp]

theorem Int32.ofBitVec_intMin : ofBitVec (BitVec.intMin 32) = minValue

@[simp]

theorem Int64.ofBitVec_intMin : ofBitVec (BitVec.intMin 64) = minValue

@[simp]

theorem ISize.ofBitVec_intMin : ofBitVec (BitVec.intMin System.Platform.numBits) = minValue

@[simp]

theorem Int8.ofBitVec_intMax : ofBitVec (BitVec.intMax 8) = maxValue

@[simp]

theorem Int16.ofBitVec_intMax : ofBitVec (BitVec.intMax 16) = maxValue

@[simp]

theorem Int32.ofBitVec_intMax : ofBitVec (BitVec.intMax 32) = maxValue

@[simp]

theorem Int64.ofBitVec_intMax : ofBitVec (BitVec.intMax 64) = maxValue

@[simp]

theorem ISize.ofBitVec_intMax : ofBitVec (BitVec.intMax System.Platform.numBits) = maxValue

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance instAssociativeInt8HOr : Std.Associative fun (x1 x2 : Int8) => x1 ||| x2

instance instAssociativeInt16HOr : Std.Associative fun (x1 x2 : Int16) => x1 ||| x2

instance instAssociativeInt32HOr : Std.Associative fun (x1 x2 : Int32) => x1 ||| x2

instance instAssociativeInt64HOr : Std.Associative fun (x1 x2 : Int64) => x1 ||| x2

instance instAssociativeISizeHOr : Std.Associative fun (x1 x2 : ISize) => x1 ||| x2

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

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

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

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

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

instance instCommutativeInt8HOr : Std.Commutative fun (x1 x2 : Int8) => x1 ||| x2

instance instCommutativeInt16HOr : Std.Commutative fun (x1 x2 : Int16) => x1 ||| x2

instance instCommutativeInt32HOr : Std.Commutative fun (x1 x2 : Int32) => x1 ||| x2

instance instCommutativeInt64HOr : Std.Commutative fun (x1 x2 : Int64) => x1 ||| x2

instance instCommutativeISizeHOr : Std.Commutative fun (x1 x2 : ISize) => x1 ||| x2

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance instIdempotentOpInt8HOr : Std.IdempotentOp fun (x1 x2 : Int8) => x1 ||| x2

instance instIdempotentOpInt16HOr : Std.IdempotentOp fun (x1 x2 : Int16) => x1 ||| x2

instance instIdempotentOpInt32HOr : Std.IdempotentOp fun (x1 x2 : Int32) => x1 ||| x2

instance instIdempotentOpInt64HOr : Std.IdempotentOp fun (x1 x2 : Int64) => x1 ||| x2

instance instIdempotentOpISizeHOr : Std.IdempotentOp fun (x1 x2 : ISize) => x1 ||| x2

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance instLawfulCommIdentityInt8HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int8) => x1 ||| x2) 0

instance instLawfulCommIdentityInt16HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int16) => x1 ||| x2) 0

instance instLawfulCommIdentityInt32HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int32) => x1 ||| x2) 0

instance instLawfulCommIdentityInt64HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int64) => x1 ||| x2) 0

instance instLawfulCommIdentityISizeHOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : ISize) => x1 ||| x2) 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

instance instAssociativeInt8HAnd : Std.Associative fun (x1 x2 : Int8) => x1 &&& x2

instance instAssociativeInt16HAnd : Std.Associative fun (x1 x2 : Int16) => x1 &&& x2

instance instAssociativeInt32HAnd : Std.Associative fun (x1 x2 : Int32) => x1 &&& x2

instance instAssociativeInt64HAnd : Std.Associative fun (x1 x2 : Int64) => x1 &&& x2

instance instAssociativeISizeHAnd : Std.Associative fun (x1 x2 : ISize) => x1 &&& x2

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

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

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

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

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

instance instCommutativeInt8HAnd : Std.Commutative fun (x1 x2 : Int8) => x1 &&& x2

instance instCommutativeInt16HAnd : Std.Commutative fun (x1 x2 : Int16) => x1 &&& x2

instance instCommutativeInt32HAnd : Std.Commutative fun (x1 x2 : Int32) => x1 &&& x2

instance instCommutativeInt64HAnd : Std.Commutative fun (x1 x2 : Int64) => x1 &&& x2

instance instCommutativeISizeHAnd : Std.Commutative fun (x1 x2 : ISize) => x1 &&& x2

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance instIdempotentOpInt8HAnd : Std.IdempotentOp fun (x1 x2 : Int8) => x1 &&& x2

instance instIdempotentOpInt16HAnd : Std.IdempotentOp fun (x1 x2 : Int16) => x1 &&& x2

instance instIdempotentOpInt32HAnd : Std.IdempotentOp fun (x1 x2 : Int32) => x1 &&& x2

instance instIdempotentOpInt64HAnd : Std.IdempotentOp fun (x1 x2 : Int64) => x1 &&& x2

instance instIdempotentOpISizeHAnd : Std.IdempotentOp fun (x1 x2 : ISize) => x1 &&& x2

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance instLawfulCommIdentityInt8HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int8) => x1 &&& x2) (-1)

instance instLawfulCommIdentityInt16HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int16) => x1 &&& x2) (-1)

instance instLawfulCommIdentityInt32HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int32) => x1 &&& x2) (-1)

instance instLawfulCommIdentityInt64HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int64) => x1 &&& x2) (-1)

instance instLawfulCommIdentityISizeHAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : ISize) => x1 &&& x2) (-1)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

instance instAssociativeInt8HXor : Std.Associative fun (x1 x2 : Int8) => x1 ^^^ x2

instance instAssociativeInt16HXor : Std.Associative fun (x1 x2 : Int16) => x1 ^^^ x2

instance instAssociativeInt32HXor : Std.Associative fun (x1 x2 : Int32) => x1 ^^^ x2

instance instAssociativeInt64HXor : Std.Associative fun (x1 x2 : Int64) => x1 ^^^ x2

instance instAssociativeISizeHXor : Std.Associative fun (x1 x2 : ISize) => x1 ^^^ x2

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

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

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

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

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

instance instCommutativeInt8HXor : Std.Commutative fun (x1 x2 : Int8) => x1 ^^^ x2

instance instCommutativeInt16HXor : Std.Commutative fun (x1 x2 : Int16) => x1 ^^^ x2

instance instCommutativeInt32HXor : Std.Commutative fun (x1 x2 : Int32) => x1 ^^^ x2

instance instCommutativeInt64HXor : Std.Commutative fun (x1 x2 : Int64) => x1 ^^^ x2

instance instCommutativeISizeHXor : Std.Commutative fun (x1 x2 : ISize) => x1 ^^^ x2

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance instLawfulCommIdentityInt8HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int8) => x1 ^^^ x2) 0

instance instLawfulCommIdentityInt16HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int16) => x1 ^^^ x2) 0

instance instLawfulCommIdentityInt32HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int32) => x1 ^^^ x2) 0

instance instLawfulCommIdentityInt64HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int64) => x1 ^^^ x2) 0

instance instLawfulCommIdentityISizeHXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : ISize) => x1 ^^^ x2) 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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