def commandDeclare_bitwise_uint_theorems__ : Lean.ParserDescr

Equations

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

theorem UInt8.toNat_shiftRight (a b : UInt8) : Eq (HShiftRight.hShiftRight a b).toNat (HShiftRight.hShiftRight a.toNat (HMod.hMod b.toNat 8))

theorem UInt8.toBitVec_or (a b : UInt8) : Eq (HOr.hOr a b).toBitVec (HOr.hOr a.toBitVec b.toBitVec)

@[deprecated UInt8.toNat_and (since := "2024-11-28")]

theorem UInt8.and_toNat (a b : UInt8) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem UInt8.toNat_xor (a b : UInt8) : Eq (HXor.hXor a b).toNat (HXor.hXor a.toNat b.toNat)

theorem UInt8.toBitVec_and (a b : UInt8) : Eq (HAnd.hAnd a b).toBitVec (HAnd.hAnd a.toBitVec b.toBitVec)

theorem UInt8.toNat_or (a b : UInt8) : Eq (HOr.hOr a b).toNat (HOr.hOr a.toNat b.toNat)

theorem UInt8.toNat_and (a b : UInt8) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem UInt8.toBitVec_not {a : UInt8} : Eq (Complement.complement a).toBitVec (Complement.complement a.toBitVec)

theorem UInt8.toNat_shiftLeft (a b : UInt8) : Eq (HShiftLeft.hShiftLeft a b).toNat (HMod.hMod (HShiftLeft.hShiftLeft a.toNat (HMod.hMod b.toNat 8)) (HPow.hPow 2 8))

theorem UInt8.toBitVec_xor (a b : UInt8) : Eq (HXor.hXor a b).toBitVec (HXor.hXor a.toBitVec b.toBitVec)

theorem UInt8.toBitVec_shiftRight (a b : UInt8) : Eq (HShiftRight.hShiftRight a b).toBitVec (HShiftRight.hShiftRight a.toBitVec (HMod.hMod b.toBitVec 8))

theorem UInt8.toBitVec_shiftLeft (a b : UInt8) : Eq (HShiftLeft.hShiftLeft a b).toBitVec (HShiftLeft.hShiftLeft a.toBitVec (HMod.hMod b.toBitVec 8))

theorem UInt16.toNat_xor (a b : UInt16) : Eq (HXor.hXor a b).toNat (HXor.hXor a.toNat b.toNat)

theorem UInt16.toNat_shiftRight (a b : UInt16) : Eq (HShiftRight.hShiftRight a b).toNat (HShiftRight.hShiftRight a.toNat (HMod.hMod b.toNat 16))

theorem UInt16.toNat_or (a b : UInt16) : Eq (HOr.hOr a b).toNat (HOr.hOr a.toNat b.toNat)

theorem UInt16.toBitVec_or (a b : UInt16) : Eq (HOr.hOr a b).toBitVec (HOr.hOr a.toBitVec b.toBitVec)

theorem UInt16.toBitVec_shiftLeft (a b : UInt16) : Eq (HShiftLeft.hShiftLeft a b).toBitVec (HShiftLeft.hShiftLeft a.toBitVec (HMod.hMod b.toBitVec 16))

theorem UInt16.toBitVec_and (a b : UInt16) : Eq (HAnd.hAnd a b).toBitVec (HAnd.hAnd a.toBitVec b.toBitVec)

theorem UInt16.toBitVec_shiftRight (a b : UInt16) : Eq (HShiftRight.hShiftRight a b).toBitVec (HShiftRight.hShiftRight a.toBitVec (HMod.hMod b.toBitVec 16))

theorem UInt16.toBitVec_not {a : UInt16} : Eq (Complement.complement a).toBitVec (Complement.complement a.toBitVec)

@[deprecated UInt16.toNat_and (since := "2024-11-28")]

theorem UInt16.and_toNat (a b : UInt16) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem UInt16.toBitVec_xor (a b : UInt16) : Eq (HXor.hXor a b).toBitVec (HXor.hXor a.toBitVec b.toBitVec)

theorem UInt16.toNat_and (a b : UInt16) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem UInt16.toNat_shiftLeft (a b : UInt16) : Eq (HShiftLeft.hShiftLeft a b).toNat (HMod.hMod (HShiftLeft.hShiftLeft a.toNat (HMod.hMod b.toNat 16)) (HPow.hPow 2 16))

theorem UInt32.toBitVec_not {a : UInt32} : Eq (Complement.complement a).toBitVec (Complement.complement a.toBitVec)

theorem UInt32.toNat_or (a b : UInt32) : Eq (HOr.hOr a b).toNat (HOr.hOr a.toNat b.toNat)

theorem UInt32.toNat_shiftLeft (a b : UInt32) : Eq (HShiftLeft.hShiftLeft a b).toNat (HMod.hMod (HShiftLeft.hShiftLeft a.toNat (HMod.hMod b.toNat 32)) (HPow.hPow 2 32))

theorem UInt32.toNat_xor (a b : UInt32) : Eq (HXor.hXor a b).toNat (HXor.hXor a.toNat b.toNat)

theorem UInt32.toBitVec_xor (a b : UInt32) : Eq (HXor.hXor a b).toBitVec (HXor.hXor a.toBitVec b.toBitVec)

theorem UInt32.toBitVec_shiftRight (a b : UInt32) : Eq (HShiftRight.hShiftRight a b).toBitVec (HShiftRight.hShiftRight a.toBitVec (HMod.hMod b.toBitVec 32))

theorem UInt32.toBitVec_and (a b : UInt32) : Eq (HAnd.hAnd a b).toBitVec (HAnd.hAnd a.toBitVec b.toBitVec)

theorem UInt32.toBitVec_shiftLeft (a b : UInt32) : Eq (HShiftLeft.hShiftLeft a b).toBitVec (HShiftLeft.hShiftLeft a.toBitVec (HMod.hMod b.toBitVec 32))

theorem UInt32.toBitVec_or (a b : UInt32) : Eq (HOr.hOr a b).toBitVec (HOr.hOr a.toBitVec b.toBitVec)

theorem UInt32.toNat_shiftRight (a b : UInt32) : Eq (HShiftRight.hShiftRight a b).toNat (HShiftRight.hShiftRight a.toNat (HMod.hMod b.toNat 32))

@[deprecated UInt32.toNat_and (since := "2024-11-28")]

theorem UInt32.and_toNat (a b : UInt32) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem UInt32.toNat_and (a b : UInt32) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem UInt64.toBitVec_and (a b : UInt64) : Eq (HAnd.hAnd a b).toBitVec (HAnd.hAnd a.toBitVec b.toBitVec)

theorem UInt64.toNat_xor (a b : UInt64) : Eq (HXor.hXor a b).toNat (HXor.hXor a.toNat b.toNat)

theorem UInt64.toNat_or (a b : UInt64) : Eq (HOr.hOr a b).toNat (HOr.hOr a.toNat b.toNat)

theorem UInt64.toBitVec_shiftLeft (a b : UInt64) : Eq (HShiftLeft.hShiftLeft a b).toBitVec (HShiftLeft.hShiftLeft a.toBitVec (HMod.hMod b.toBitVec 64))

theorem UInt64.toNat_and (a b : UInt64) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem UInt64.toBitVec_not {a : UInt64} : Eq (Complement.complement a).toBitVec (Complement.complement a.toBitVec)

theorem UInt64.toBitVec_shiftRight (a b : UInt64) : Eq (HShiftRight.hShiftRight a b).toBitVec (HShiftRight.hShiftRight a.toBitVec (HMod.hMod b.toBitVec 64))

theorem UInt64.toBitVec_or (a b : UInt64) : Eq (HOr.hOr a b).toBitVec (HOr.hOr a.toBitVec b.toBitVec)

@[deprecated UInt64.toNat_and (since := "2024-11-28")]

theorem UInt64.and_toNat (a b : UInt64) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem UInt64.toNat_shiftRight (a b : UInt64) : Eq (HShiftRight.hShiftRight a b).toNat (HShiftRight.hShiftRight a.toNat (HMod.hMod b.toNat 64))

theorem UInt64.toBitVec_xor (a b : UInt64) : Eq (HXor.hXor a b).toBitVec (HXor.hXor a.toBitVec b.toBitVec)

theorem UInt64.toNat_shiftLeft (a b : UInt64) : Eq (HShiftLeft.hShiftLeft a b).toNat (HMod.hMod (HShiftLeft.hShiftLeft a.toNat (HMod.hMod b.toNat 64)) (HPow.hPow 2 64))

theorem USize.toBitVec_and (a b : USize) : Eq (HAnd.hAnd a b).toBitVec (HAnd.hAnd a.toBitVec b.toBitVec)

theorem USize.toNat_and (a b : USize) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

@[deprecated USize.toNat_and (since := "2024-11-28")]

theorem USize.and_toNat (a b : USize) : Eq (HAnd.hAnd a b).toNat (HAnd.hAnd a.toNat b.toNat)

theorem USize.toBitVec_xor (a b : USize) : Eq (HXor.hXor a b).toBitVec (HXor.hXor a.toBitVec b.toBitVec)

theorem USize.toNat_shiftRight (a b : USize) : Eq (HShiftRight.hShiftRight a b).toNat (HShiftRight.hShiftRight a.toNat (HMod.hMod b.toNat System.Platform.numBits))

theorem USize.toBitVec_shiftRight (a b : USize) : Eq (HShiftRight.hShiftRight a b).toBitVec (HShiftRight.hShiftRight a.toBitVec (HMod.hMod b.toBitVec System.Platform.numBits.cast))

theorem USize.toNat_or (a b : USize) : Eq (HOr.hOr a b).toNat (HOr.hOr a.toNat b.toNat)

theorem USize.toBitVec_or (a b : USize) : Eq (HOr.hOr a b).toBitVec (HOr.hOr a.toBitVec b.toBitVec)

theorem USize.toNat_xor (a b : USize) : Eq (HXor.hXor a b).toNat (HXor.hXor a.toNat b.toNat)

theorem USize.toNat_shiftLeft (a b : USize) : Eq (HShiftLeft.hShiftLeft a b).toNat (HMod.hMod (HShiftLeft.hShiftLeft a.toNat (HMod.hMod b.toNat System.Platform.numBits)) (HPow.hPow 2 System.Platform.numBits))

theorem USize.toBitVec_not {a : USize} : Eq (Complement.complement a).toBitVec (Complement.complement a.toBitVec)

theorem USize.toBitVec_shiftLeft (a b : USize) : Eq (HShiftLeft.hShiftLeft a b).toBitVec (HShiftLeft.hShiftLeft a.toBitVec (HMod.hMod b.toBitVec System.Platform.numBits.cast))

theorem Bool.toBitVec_toUInt8 {b : Bool} : Eq b.toUInt8.toBitVec (BitVec.setWidth 8 (BitVec.ofBool b))

theorem Bool.toBitVec_toUInt16 {b : Bool} : Eq b.toUInt16.toBitVec (BitVec.setWidth 16 (BitVec.ofBool b))

theorem Bool.toBitVec_toUInt32 {b : Bool} : Eq b.toUInt32.toBitVec (BitVec.setWidth 32 (BitVec.ofBool b))

theorem Bool.toBitVec_toUInt64 {b : Bool} : Eq b.toUInt64.toBitVec (BitVec.setWidth 64 (BitVec.ofBool b))

theorem Bool.toBitVec_toUSize {b : Bool} : Eq b.toUSize.toBitVec (BitVec.setWidth System.Platform.numBits (BitVec.ofBool b))

theorem UInt8.toFin_and (a b : UInt8) : Eq (HAnd.hAnd a b).toFin (HAnd.hAnd a.toFin b.toFin)

theorem UInt16.toFin_and (a b : UInt16) : Eq (HAnd.hAnd a b).toFin (HAnd.hAnd a.toFin b.toFin)

theorem UInt32.toFin_and (a b : UInt32) : Eq (HAnd.hAnd a b).toFin (HAnd.hAnd a.toFin b.toFin)

theorem UInt64.toFin_and (a b : UInt64) : Eq (HAnd.hAnd a b).toFin (HAnd.hAnd a.toFin b.toFin)

theorem USize.toFin_and (a b : USize) : Eq (HAnd.hAnd a b).toFin (HAnd.hAnd a.toFin b.toFin)

theorem UInt8.toUInt16_and (a b : UInt8) : Eq (HAnd.hAnd a b).toUInt16 (HAnd.hAnd a.toUInt16 b.toUInt16)

theorem UInt8.toUInt32_and (a b : UInt8) : Eq (HAnd.hAnd a b).toUInt32 (HAnd.hAnd a.toUInt32 b.toUInt32)

theorem UInt8.toUInt64_and (a b : UInt8) : Eq (HAnd.hAnd a b).toUInt64 (HAnd.hAnd a.toUInt64 b.toUInt64)

theorem UInt8.toUSize_and (a b : UInt8) : Eq (HAnd.hAnd a b).toUSize (HAnd.hAnd a.toUSize b.toUSize)

theorem UInt16.toUInt8_and (a b : UInt16) : Eq (HAnd.hAnd a b).toUInt8 (HAnd.hAnd a.toUInt8 b.toUInt8)

theorem UInt16.toUInt32_and (a b : UInt16) : Eq (HAnd.hAnd a b).toUInt32 (HAnd.hAnd a.toUInt32 b.toUInt32)

theorem UInt16.toUInt64_and (a b : UInt16) : Eq (HAnd.hAnd a b).toUInt64 (HAnd.hAnd a.toUInt64 b.toUInt64)

theorem UInt16.toUSize_and (a b : UInt16) : Eq (HAnd.hAnd a b).toUSize (HAnd.hAnd a.toUSize b.toUSize)

theorem UInt32.toUInt8_and (a b : UInt32) : Eq (HAnd.hAnd a b).toUInt8 (HAnd.hAnd a.toUInt8 b.toUInt8)

theorem UInt32.toUInt16_and (a b : UInt32) : Eq (HAnd.hAnd a b).toUInt16 (HAnd.hAnd a.toUInt16 b.toUInt16)

theorem UInt32.toUInt64_and (a b : UInt32) : Eq (HAnd.hAnd a b).toUInt64 (HAnd.hAnd a.toUInt64 b.toUInt64)

theorem UInt32.toUSize_and (a b : UInt32) : Eq (HAnd.hAnd a b).toUSize (HAnd.hAnd a.toUSize b.toUSize)

theorem USize.toUInt8_and (a b : USize) : Eq (HAnd.hAnd a b).toUInt8 (HAnd.hAnd a.toUInt8 b.toUInt8)

theorem USize.toUInt16_and (a b : USize) : Eq (HAnd.hAnd a b).toUInt16 (HAnd.hAnd a.toUInt16 b.toUInt16)

theorem USize.toUInt32_and (a b : USize) : Eq (HAnd.hAnd a b).toUInt32 (HAnd.hAnd a.toUInt32 b.toUInt32)

theorem USize.toUInt64_and (a b : USize) : Eq (HAnd.hAnd a b).toUInt64 (HAnd.hAnd a.toUInt64 b.toUInt64)

theorem UInt64.toUInt8_and (a b : UInt64) : Eq (HAnd.hAnd a b).toUInt8 (HAnd.hAnd a.toUInt8 b.toUInt8)

theorem UInt64.toUInt16_and (a b : UInt64) : Eq (HAnd.hAnd a b).toUInt16 (HAnd.hAnd a.toUInt16 b.toUInt16)

theorem UInt64.toUInt32_and (a b : UInt64) : Eq (HAnd.hAnd a b).toUInt32 (HAnd.hAnd a.toUInt32 b.toUInt32)

theorem UInt64.toUSize_and (a b : UInt64) : Eq (HAnd.hAnd a b).toUSize (HAnd.hAnd a.toUSize b.toUSize)

theorem UInt8.toFin_or (a b : UInt8) : Eq (HOr.hOr a b).toFin (HOr.hOr a.toFin b.toFin)

theorem UInt16.toFin_or (a b : UInt16) : Eq (HOr.hOr a b).toFin (HOr.hOr a.toFin b.toFin)

theorem UInt32.toFin_or (a b : UInt32) : Eq (HOr.hOr a b).toFin (HOr.hOr a.toFin b.toFin)

theorem UInt64.toFin_or (a b : UInt64) : Eq (HOr.hOr a b).toFin (HOr.hOr a.toFin b.toFin)

theorem USize.toFin_or (a b : USize) : Eq (HOr.hOr a b).toFin (HOr.hOr a.toFin b.toFin)

theorem UInt8.toUInt16_or (a b : UInt8) : Eq (HOr.hOr a b).toUInt16 (HOr.hOr a.toUInt16 b.toUInt16)

theorem UInt8.toUInt32_or (a b : UInt8) : Eq (HOr.hOr a b).toUInt32 (HOr.hOr a.toUInt32 b.toUInt32)

theorem UInt8.toUInt64_or (a b : UInt8) : Eq (HOr.hOr a b).toUInt64 (HOr.hOr a.toUInt64 b.toUInt64)

theorem UInt8.toUSize_or (a b : UInt8) : Eq (HOr.hOr a b).toUSize (HOr.hOr a.toUSize b.toUSize)

theorem UInt16.toUInt8_or (a b : UInt16) : Eq (HOr.hOr a b).toUInt8 (HOr.hOr a.toUInt8 b.toUInt8)

theorem UInt16.toUInt32_or (a b : UInt16) : Eq (HOr.hOr a b).toUInt32 (HOr.hOr a.toUInt32 b.toUInt32)

theorem UInt16.toUInt64_or (a b : UInt16) : Eq (HOr.hOr a b).toUInt64 (HOr.hOr a.toUInt64 b.toUInt64)

theorem UInt16.toUSize_or (a b : UInt16) : Eq (HOr.hOr a b).toUSize (HOr.hOr a.toUSize b.toUSize)

theorem UInt32.toUInt8_or (a b : UInt32) : Eq (HOr.hOr a b).toUInt8 (HOr.hOr a.toUInt8 b.toUInt8)

theorem UInt32.toUInt16_or (a b : UInt32) : Eq (HOr.hOr a b).toUInt16 (HOr.hOr a.toUInt16 b.toUInt16)

theorem UInt32.toUInt64_or (a b : UInt32) : Eq (HOr.hOr a b).toUInt64 (HOr.hOr a.toUInt64 b.toUInt64)

theorem UInt32.toUSize_or (a b : UInt32) : Eq (HOr.hOr a b).toUSize (HOr.hOr a.toUSize b.toUSize)

theorem USize.toUInt8_or (a b : USize) : Eq (HOr.hOr a b).toUInt8 (HOr.hOr a.toUInt8 b.toUInt8)

theorem USize.toUInt16_or (a b : USize) : Eq (HOr.hOr a b).toUInt16 (HOr.hOr a.toUInt16 b.toUInt16)

theorem USize.toUInt32_or (a b : USize) : Eq (HOr.hOr a b).toUInt32 (HOr.hOr a.toUInt32 b.toUInt32)

theorem USize.toUInt64_or (a b : USize) : Eq (HOr.hOr a b).toUInt64 (HOr.hOr a.toUInt64 b.toUInt64)

theorem UInt64.toUInt8_or (a b : UInt64) : Eq (HOr.hOr a b).toUInt8 (HOr.hOr a.toUInt8 b.toUInt8)

theorem UInt64.toUInt16_or (a b : UInt64) : Eq (HOr.hOr a b).toUInt16 (HOr.hOr a.toUInt16 b.toUInt16)

theorem UInt64.toUInt32_or (a b : UInt64) : Eq (HOr.hOr a b).toUInt32 (HOr.hOr a.toUInt32 b.toUInt32)

theorem UInt64.toUSize_or (a b : UInt64) : Eq (HOr.hOr a b).toUSize (HOr.hOr a.toUSize b.toUSize)

theorem UInt8.toFin_xor (a b : UInt8) : Eq (HXor.hXor a b).toFin (HXor.hXor a.toFin b.toFin)

theorem UInt16.toFin_xor (a b : UInt16) : Eq (HXor.hXor a b).toFin (HXor.hXor a.toFin b.toFin)

theorem UInt32.toFin_xor (a b : UInt32) : Eq (HXor.hXor a b).toFin (HXor.hXor a.toFin b.toFin)

theorem UInt64.toFin_xor (a b : UInt64) : Eq (HXor.hXor a b).toFin (HXor.hXor a.toFin b.toFin)

theorem USize.toFin_xor (a b : USize) : Eq (HXor.hXor a b).toFin (HXor.hXor a.toFin b.toFin)

theorem UInt8.toUInt16_xor (a b : UInt8) : Eq (HXor.hXor a b).toUInt16 (HXor.hXor a.toUInt16 b.toUInt16)

theorem UInt8.toUInt32_xor (a b : UInt8) : Eq (HXor.hXor a b).toUInt32 (HXor.hXor a.toUInt32 b.toUInt32)

theorem UInt8.toUInt64_xor (a b : UInt8) : Eq (HXor.hXor a b).toUInt64 (HXor.hXor a.toUInt64 b.toUInt64)

theorem UInt8.toUSize_xor (a b : UInt8) : Eq (HXor.hXor a b).toUSize (HXor.hXor a.toUSize b.toUSize)

theorem UInt16.toUInt8_xor (a b : UInt16) : Eq (HXor.hXor a b).toUInt8 (HXor.hXor a.toUInt8 b.toUInt8)

theorem UInt16.toUInt32_xor (a b : UInt16) : Eq (HXor.hXor a b).toUInt32 (HXor.hXor a.toUInt32 b.toUInt32)

theorem UInt16.toUInt64_xor (a b : UInt16) : Eq (HXor.hXor a b).toUInt64 (HXor.hXor a.toUInt64 b.toUInt64)

theorem UInt16.toUSize_xor (a b : UInt16) : Eq (HXor.hXor a b).toUSize (HXor.hXor a.toUSize b.toUSize)

theorem UInt32.toUInt8_xor (a b : UInt32) : Eq (HXor.hXor a b).toUInt8 (HXor.hXor a.toUInt8 b.toUInt8)

theorem UInt32.toUInt16_xor (a b : UInt32) : Eq (HXor.hXor a b).toUInt16 (HXor.hXor a.toUInt16 b.toUInt16)

theorem UInt32.toUInt64_xor (a b : UInt32) : Eq (HXor.hXor a b).toUInt64 (HXor.hXor a.toUInt64 b.toUInt64)

theorem UInt32.toUSize_xor (a b : UInt32) : Eq (HXor.hXor a b).toUSize (HXor.hXor a.toUSize b.toUSize)

theorem USize.toUInt8_xor (a b : USize) : Eq (HXor.hXor a b).toUInt8 (HXor.hXor a.toUInt8 b.toUInt8)

theorem USize.toUInt16_xor (a b : USize) : Eq (HXor.hXor a b).toUInt16 (HXor.hXor a.toUInt16 b.toUInt16)

theorem USize.toUInt32_xor (a b : USize) : Eq (HXor.hXor a b).toUInt32 (HXor.hXor a.toUInt32 b.toUInt32)

theorem USize.toUInt64_xor (a b : USize) : Eq (HXor.hXor a b).toUInt64 (HXor.hXor a.toUInt64 b.toUInt64)

theorem UInt64.toUInt8_xor (a b : UInt64) : Eq (HXor.hXor a b).toUInt8 (HXor.hXor a.toUInt8 b.toUInt8)

theorem UInt64.toUInt16_xor (a b : UInt64) : Eq (HXor.hXor a b).toUInt16 (HXor.hXor a.toUInt16 b.toUInt16)

theorem UInt64.toUInt32_xor (a b : UInt64) : Eq (HXor.hXor a b).toUInt32 (HXor.hXor a.toUInt32 b.toUInt32)

theorem UInt64.toUSize_xor (a b : UInt64) : Eq (HXor.hXor a b).toUSize (HXor.hXor a.toUSize b.toUSize)

theorem UInt8.toNat_not (a : UInt8) : Eq (Complement.complement a).toNat (HSub.hSub (HSub.hSub size 1) a.toNat)

theorem UInt16.toNat_not (a : UInt16) : Eq (Complement.complement a).toNat (HSub.hSub (HSub.hSub size 1) a.toNat)

theorem UInt32.toNat_not (a : UInt32) : Eq (Complement.complement a).toNat (HSub.hSub (HSub.hSub size 1) a.toNat)

theorem UInt64.toNat_not (a : UInt64) : Eq (Complement.complement a).toNat (HSub.hSub (HSub.hSub size 1) a.toNat)

theorem USize.toNat_not (a : USize) : Eq (Complement.complement a).toNat (HSub.hSub (HSub.hSub size 1) a.toNat)

theorem UInt8.toFin_not (a : UInt8) : Eq (Complement.complement a).toFin a.toFin.rev

theorem UInt16.toFin_not (a : UInt16) : Eq (Complement.complement a).toFin a.toFin.rev

theorem UInt32.toFin_not (a : UInt32) : Eq (Complement.complement a).toFin a.toFin.rev

theorem UInt64.toFin_not (a : UInt64) : Eq (Complement.complement a).toFin a.toFin.rev

theorem USize.toFin_not (a : USize) : Eq (Complement.complement a).toFin a.toFin.rev

theorem UInt16.toUInt8_not (a : UInt16) : Eq (Complement.complement a).toUInt8 (Complement.complement a.toUInt8)

theorem UInt32.toUInt8_not (a : UInt32) : Eq (Complement.complement a).toUInt8 (Complement.complement a.toUInt8)

theorem UInt64.toUInt8_not (a : UInt64) : Eq (Complement.complement a).toUInt8 (Complement.complement a.toUInt8)

theorem USize.toUInt8_not (a : USize) : Eq (Complement.complement a).toUInt8 (Complement.complement a.toUInt8)

theorem UInt32.toUInt16_not (a : UInt32) : Eq (Complement.complement a).toUInt16 (Complement.complement a.toUInt16)

theorem UInt64.toUInt16_not (a : UInt64) : Eq (Complement.complement a).toUInt16 (Complement.complement a.toUInt16)

theorem USize.toUInt16_not (a : USize) : Eq (Complement.complement a).toUInt16 (Complement.complement a.toUInt16)

theorem UInt64.toUInt32_not (a : UInt64) : Eq (Complement.complement a).toUInt32 (Complement.complement a.toUInt32)

theorem USize.toUInt32_not (a : USize) : Eq (Complement.complement a).toUInt32 (Complement.complement a.toUInt32)

theorem UInt64.toUSize_not (a : UInt64) : Eq (Complement.complement a).toUSize (Complement.complement a.toUSize)

theorem UInt8.toUInt16_not (a : UInt8) : Eq (Complement.complement a).toUInt16 (HMod.hMod (Complement.complement a.toUInt16) 256)

theorem UInt8.toUInt32_not (a : UInt8) : Eq (Complement.complement a).toUInt32 (HMod.hMod (Complement.complement a.toUInt32) 256)

theorem UInt8.toUInt64_not (a : UInt8) : Eq (Complement.complement a).toUInt64 (HMod.hMod (Complement.complement a.toUInt64) 256)

theorem UInt8.toUSize_not (a : UInt8) : Eq (Complement.complement a).toUSize (HMod.hMod (Complement.complement a.toUSize) 256)

theorem UInt16.toUInt32_not (a : UInt16) : Eq (Complement.complement a).toUInt32 (HMod.hMod (Complement.complement a.toUInt32) 65536)

theorem UInt16.toUInt64_not (a : UInt16) : Eq (Complement.complement a).toUInt64 (HMod.hMod (Complement.complement a.toUInt64) 65536)

theorem UInt16.toUSize_not (a : UInt16) : Eq (Complement.complement a).toUSize (HMod.hMod (Complement.complement a.toUSize) 65536)

theorem UInt32.toUInt64_not (a : UInt32) : Eq (Complement.complement a).toUInt64 (HMod.hMod (Complement.complement a.toUInt64) 4294967296)

theorem UInt32.toUSize_not (a : UInt32) : Eq (Complement.complement a).toUSize (HMod.hMod (Complement.complement a.toUSize) 4294967296)

theorem USize.toUInt64_not (a : USize) : Eq (Complement.complement a).toUInt64 (HMod.hMod (Complement.complement a.toUInt64) (UInt64.ofNat size))

theorem UInt8.toFin_shiftLeft (a b : UInt8) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toFin (HShiftLeft.hShiftLeft a.toFin b.toFin)

theorem UInt16.toFin_shiftLeft (a b : UInt16) (hb : LT.lt b 16) : Eq (HShiftLeft.hShiftLeft a b).toFin (HShiftLeft.hShiftLeft a.toFin b.toFin)

theorem UInt32.toFin_shiftLeft (a b : UInt32) (hb : LT.lt b 32) : Eq (HShiftLeft.hShiftLeft a b).toFin (HShiftLeft.hShiftLeft a.toFin b.toFin)

theorem UInt64.toFin_shiftLeft (a b : UInt64) (hb : LT.lt b 64) : Eq (HShiftLeft.hShiftLeft a b).toFin (HShiftLeft.hShiftLeft a.toFin b.toFin)

theorem USize.toFin_shiftLeft (a b : USize) (hb : LT.lt b.toNat System.Platform.numBits) : Eq (HShiftLeft.hShiftLeft a b).toFin (HShiftLeft.hShiftLeft a.toFin b.toFin)

theorem UInt8.shiftLeft_eq_shiftLeft_mod (a b : UInt8) : Eq (HShiftLeft.hShiftLeft a b) (HShiftLeft.hShiftLeft a (HMod.hMod b 8))

theorem UInt16.shiftLeft_eq_shiftLeft_mod (a b : UInt16) : Eq (HShiftLeft.hShiftLeft a b) (HShiftLeft.hShiftLeft a (HMod.hMod b 16))

theorem UInt32.shiftLeft_eq_shiftLeft_mod (a b : UInt32) : Eq (HShiftLeft.hShiftLeft a b) (HShiftLeft.hShiftLeft a (HMod.hMod b 32))

theorem UInt64.shiftLeft_eq_shiftLeft_mod (a b : UInt64) : Eq (HShiftLeft.hShiftLeft a b) (HShiftLeft.hShiftLeft a (HMod.hMod b 64))

theorem USize.shiftLeft_eq_shiftLeft_mod (a b : USize) : Eq (HShiftLeft.hShiftLeft a b) (HShiftLeft.hShiftLeft a (HMod.hMod b (ofNat System.Platform.numBits)))

theorem UInt8.shiftRight_eq_shiftRight_mod (a b : UInt8) : Eq (HShiftRight.hShiftRight a b) (HShiftRight.hShiftRight a (HMod.hMod b 8))

theorem UInt16.shiftRight_eq_shiftRight_mod (a b : UInt16) : Eq (HShiftRight.hShiftRight a b) (HShiftRight.hShiftRight a (HMod.hMod b 16))

theorem UInt32.shiftRight_eq_shiftRight_mod (a b : UInt32) : Eq (HShiftRight.hShiftRight a b) (HShiftRight.hShiftRight a (HMod.hMod b 32))

theorem UInt64.shiftRight_eq_shiftRight_mod (a b : UInt64) : Eq (HShiftRight.hShiftRight a b) (HShiftRight.hShiftRight a (HMod.hMod b 64))

theorem USize.shiftRight_eq_shiftRight_mod (a b : USize) : Eq (HShiftRight.hShiftRight a b) (HShiftRight.hShiftRight a (HMod.hMod b (ofNat System.Platform.numBits)))

theorem UInt16.toUInt8_shiftLeft (a b : UInt16) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toUInt8 (HShiftLeft.hShiftLeft a.toUInt8 b.toUInt8)

theorem UInt32.toUInt8_shiftLeft (a b : UInt32) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toUInt8 (HShiftLeft.hShiftLeft a.toUInt8 b.toUInt8)

theorem UInt32.toUInt16_shiftLeft (a b : UInt32) (hb : LT.lt b 16) : Eq (HShiftLeft.hShiftLeft a b).toUInt16 (HShiftLeft.hShiftLeft a.toUInt16 b.toUInt16)

theorem USize.toUInt8_shiftLeft (a b : USize) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toUInt8 (HShiftLeft.hShiftLeft a.toUInt8 b.toUInt8)

theorem USize.toUInt16_shiftLeft (a b : USize) (hb : LT.lt b 16) : Eq (HShiftLeft.hShiftLeft a b).toUInt16 (HShiftLeft.hShiftLeft a.toUInt16 b.toUInt16)

theorem USize.toUInt32_shiftLeft (a b : USize) (hb : LT.lt b 32) : Eq (HShiftLeft.hShiftLeft a b).toUInt32 (HShiftLeft.hShiftLeft a.toUInt32 b.toUInt32)

theorem UInt64.toUInt8_shiftLeft (a b : UInt64) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toUInt8 (HShiftLeft.hShiftLeft a.toUInt8 b.toUInt8)

theorem UInt64.toUInt16_shiftLeft (a b : UInt64) (hb : LT.lt b 16) : Eq (HShiftLeft.hShiftLeft a b).toUInt16 (HShiftLeft.hShiftLeft a.toUInt16 b.toUInt16)

theorem UInt64.toUInt32_shiftLeft (a b : UInt64) (hb : LT.lt b 32) : Eq (HShiftLeft.hShiftLeft a b).toUInt32 (HShiftLeft.hShiftLeft a.toUInt32 b.toUInt32)

theorem UInt64.toUSize_shiftLeft (a b : UInt64) (hb : LT.lt b.toNat System.Platform.numBits) : Eq (HShiftLeft.hShiftLeft a b).toUSize (HShiftLeft.hShiftLeft a.toUSize b.toUSize)

theorem UInt16.toUInt8_shiftLeft_mod (a b : UInt16) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 8)).toUInt8 (HShiftLeft.hShiftLeft a.toUInt8 b.toUInt8)

theorem UInt32.toUInt8_shiftLeft_mod (a b : UInt32) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 8)).toUInt8 (HShiftLeft.hShiftLeft a.toUInt8 b.toUInt8)

theorem UInt32.toUInt16_shiftLeft_mod (a b : UInt32) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 16)).toUInt16 (HShiftLeft.hShiftLeft a.toUInt16 b.toUInt16)

theorem USize.toUInt8_shiftLeft_mod (a b : USize) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 8)).toUInt8 (HShiftLeft.hShiftLeft a.toUInt8 b.toUInt8)

theorem USize.toUInt16_shiftLeft_mod (a b : USize) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 16)).toUInt16 (HShiftLeft.hShiftLeft a.toUInt16 b.toUInt16)

theorem USize.toUInt32_shiftLeft_mod (a b : USize) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 32)).toUInt32 (HShiftLeft.hShiftLeft a.toUInt32 b.toUInt32)

theorem UInt64.toUInt8_shiftLeft_mod (a b : UInt64) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 8)).toUInt8 (HShiftLeft.hShiftLeft a.toUInt8 b.toUInt8)

theorem UInt64.toUInt16_shiftLeft_mod (a b : UInt64) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 16)).toUInt16 (HShiftLeft.hShiftLeft a.toUInt16 b.toUInt16)

theorem UInt64.toUInt32_shiftLeft_mod (a b : UInt64) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b 32)).toUInt32 (HShiftLeft.hShiftLeft a.toUInt32 b.toUInt32)

theorem UInt64.toUSize_shiftLeft_mod (a b : UInt64) : Eq (HShiftLeft.hShiftLeft a (HMod.hMod b (ofNat System.Platform.numBits))).toUSize (HShiftLeft.hShiftLeft a.toUSize b.toUSize)

theorem UInt8.toUInt16_shiftLeft_of_lt (a b : UInt8) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toUInt16 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt16 b.toUInt16) 256)

theorem UInt8.toUInt32_shiftLeft_of_lt (a b : UInt8) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toUInt32 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt32 b.toUInt32) 256)

theorem UInt8.toUInt64_shiftLeft_of_lt (a b : UInt8) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toUInt64 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt64 b.toUInt64) 256)

theorem UInt8.toUSize_shiftLeft_of_lt (a b : UInt8) (hb : LT.lt b 8) : Eq (HShiftLeft.hShiftLeft a b).toUSize (HMod.hMod (HShiftLeft.hShiftLeft a.toUSize b.toUSize) 256)

theorem UInt16.toUInt32_shiftLeft_of_lt (a b : UInt16) (hb : LT.lt b 16) : Eq (HShiftLeft.hShiftLeft a b).toUInt32 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt32 b.toUInt32) 65536)

theorem UInt16.toUInt64_shiftLeft_of_lt (a b : UInt16) (hb : LT.lt b 16) : Eq (HShiftLeft.hShiftLeft a b).toUInt64 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt64 b.toUInt64) 65536)

theorem UInt16.toUSize_shiftLeft_of_lt (a b : UInt16) (hb : LT.lt b 16) : Eq (HShiftLeft.hShiftLeft a b).toUSize (HMod.hMod (HShiftLeft.hShiftLeft a.toUSize b.toUSize) 65536)

theorem UInt32.toUInt64_shiftLeft_of_lt (a b : UInt32) (hb : LT.lt b 32) : Eq (HShiftLeft.hShiftLeft a b).toUInt64 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt64 b.toUInt64) 4294967296)

theorem UInt32.toUSize_shiftLeft_of_lt (a b : UInt32) (hb : LT.lt b 32) : Eq (HShiftLeft.hShiftLeft a b).toUSize (HMod.hMod (HShiftLeft.hShiftLeft a.toUSize b.toUSize) 4294967296)

theorem USize.toUInt64_shiftLeft_of_lt (a b : USize) (hb : LT.lt b.toNat System.Platform.numBits) : Eq (HShiftLeft.hShiftLeft a b).toUInt64 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt64 b.toUInt64) (UInt64.ofNat size))

theorem UInt8.toUInt16_shiftLeft (a b : UInt8) : Eq (HShiftLeft.hShiftLeft a b).toUInt16 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt16 (HMod.hMod b 8).toUInt16) 256)

theorem UInt8.toUInt32_shiftLeft (a b : UInt8) : Eq (HShiftLeft.hShiftLeft a b).toUInt32 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt32 (HMod.hMod b 8).toUInt32) 256)

theorem UInt8.toUInt64_shiftLeft (a b : UInt8) : Eq (HShiftLeft.hShiftLeft a b).toUInt64 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt64 (HMod.hMod b 8).toUInt64) 256)

theorem UInt8.toUSize_shiftLeft (a b : UInt8) : Eq (HShiftLeft.hShiftLeft a b).toUSize (HMod.hMod (HShiftLeft.hShiftLeft a.toUSize (HMod.hMod b 8).toUSize) 256)

theorem UInt16.toUInt32_shiftLeft (a b : UInt16) : Eq (HShiftLeft.hShiftLeft a b).toUInt32 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt32 (HMod.hMod b 16).toUInt32) 65536)

theorem UInt16.toUInt64_shiftLeft (a b : UInt16) : Eq (HShiftLeft.hShiftLeft a b).toUInt64 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt64 (HMod.hMod b 16).toUInt64) 65536)

theorem UInt16.toUSize_shiftLeft (a b : UInt16) : Eq (HShiftLeft.hShiftLeft a b).toUSize (HMod.hMod (HShiftLeft.hShiftLeft a.toUSize (HMod.hMod b 16).toUSize) 65536)

theorem UInt32.toUInt64_shiftLeft (a b : UInt32) : Eq (HShiftLeft.hShiftLeft a b).toUInt64 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt64 (HMod.hMod b 32).toUInt64) 4294967296)

theorem UInt32.toUSize_shiftLeft (a b : UInt32) : Eq (HShiftLeft.hShiftLeft a b).toUSize (HMod.hMod (HShiftLeft.hShiftLeft a.toUSize (HMod.hMod b 32).toUSize) 4294967296)

theorem USize.toUInt64_shiftLeft (a b : USize) : Eq (HShiftLeft.hShiftLeft a b).toUInt64 (HMod.hMod (HShiftLeft.hShiftLeft a.toUInt64 (HMod.hMod b (ofNat System.Platform.numBits)).toUInt64) (UInt64.ofNat size))

theorem UInt8.toFin_shiftRight (a b : UInt8) (hb : LT.lt b 8) : Eq (HShiftRight.hShiftRight a b).toFin (HShiftRight.hShiftRight a.toFin b.toFin)

theorem UInt16.toFin_shiftRight (a b : UInt16) (hb : LT.lt b 16) : Eq (HShiftRight.hShiftRight a b).toFin (HShiftRight.hShiftRight a.toFin b.toFin)

theorem UInt32.toFin_shiftRight (a b : UInt32) (hb : LT.lt b 32) : Eq (HShiftRight.hShiftRight a b).toFin (HShiftRight.hShiftRight a.toFin b.toFin)

theorem UInt64.toFin_shiftRight (a b : UInt64) (hb : LT.lt b 64) : Eq (HShiftRight.hShiftRight a b).toFin (HShiftRight.hShiftRight a.toFin b.toFin)

theorem USize.toFin_shiftRight (a b : USize) (hb : LT.lt b.toNat System.Platform.numBits) : Eq (HShiftRight.hShiftRight a b).toFin (HShiftRight.hShiftRight a.toFin b.toFin)

theorem UInt8.toUInt16_shiftRight (a b : UInt8) : Eq (HShiftRight.hShiftRight a b).toUInt16 (HShiftRight.hShiftRight a.toUInt16 (HMod.hMod b.toUInt16 8))

theorem UInt8.toUInt32_shiftRight (a b : UInt8) : Eq (HShiftRight.hShiftRight a b).toUInt32 (HShiftRight.hShiftRight a.toUInt32 (HMod.hMod b.toUInt32 8))

theorem UInt8.toUInt64_shiftRight (a b : UInt8) : Eq (HShiftRight.hShiftRight a b).toUInt64 (HShiftRight.hShiftRight a.toUInt64 (HMod.hMod b.toUInt64 8))

theorem UInt8.toUSize_shiftRight (a b : UInt8) : Eq (HShiftRight.hShiftRight a b).toUSize (HShiftRight.hShiftRight a.toUSize (HMod.hMod b.toUSize 8))

theorem UInt16.toUInt32_shiftRight (a b : UInt16) : Eq (HShiftRight.hShiftRight a b).toUInt32 (HShiftRight.hShiftRight a.toUInt32 (HMod.hMod b.toUInt32 16))

theorem UInt16.toUInt64_shiftRight (a b : UInt16) : Eq (HShiftRight.hShiftRight a b).toUInt64 (HShiftRight.hShiftRight a.toUInt64 (HMod.hMod b.toUInt64 16))

theorem UInt16.toUSize_shiftRight (a b : UInt16) : Eq (HShiftRight.hShiftRight a b).toUSize (HShiftRight.hShiftRight a.toUSize (HMod.hMod b.toUSize 16))

theorem UInt32.toUInt64_shiftRight (a b : UInt32) : Eq (HShiftRight.hShiftRight a b).toUInt64 (HShiftRight.hShiftRight a.toUInt64 (HMod.hMod b.toUInt64 32))

theorem UInt32.toUSize_shiftRight (a b : UInt32) : Eq (HShiftRight.hShiftRight a b).toUSize (HShiftRight.hShiftRight a.toUSize (HMod.hMod b.toUSize 32))

theorem USize.toUInt64_shiftRight (a b : USize) : Eq (HShiftRight.hShiftRight a b).toUInt64 (HShiftRight.hShiftRight a.toUInt64 (HMod.hMod b.toUInt64 (UInt64.ofNat System.Platform.numBits)))

There is no reasonable statement forUInt16.toUInt8_shiftRight; in fact for a b : UInt16 the expression (a >>> b).toUInt8 is not a function of a.toUInt8 and b.toUInt8.

theorem UInt8.ofFin_and (a b : Fin size) : Eq (ofFin (HAnd.hAnd a b)) (HAnd.hAnd (ofFin a) (ofFin b))

theorem UInt16.ofFin_and (a b : Fin size) : Eq (ofFin (HAnd.hAnd a b)) (HAnd.hAnd (ofFin a) (ofFin b))

theorem UInt32.ofFin_and (a b : Fin size) : Eq (ofFin (HAnd.hAnd a b)) (HAnd.hAnd (ofFin a) (ofFin b))

theorem UInt64.ofFin_and (a b : Fin size) : Eq (ofFin (HAnd.hAnd a b)) (HAnd.hAnd (ofFin a) (ofFin b))

theorem USize.ofFin_and (a b : Fin size) : Eq (ofFin (HAnd.hAnd a b)) (HAnd.hAnd (ofFin a) (ofFin b))

theorem UInt8.ofBitVec_and (a b : BitVec 8) : Eq { toBitVec := HAnd.hAnd a b } (HAnd.hAnd { toBitVec := a } { toBitVec := b })

theorem UInt16.ofBitVec_and (a b : BitVec 16) : Eq { toBitVec := HAnd.hAnd a b } (HAnd.hAnd { toBitVec := a } { toBitVec := b })

theorem UInt32.ofBitVec_and (a b : BitVec 32) : Eq { toBitVec := HAnd.hAnd a b } (HAnd.hAnd { toBitVec := a } { toBitVec := b })

theorem UInt64.ofBitVec_and (a b : BitVec 64) : Eq { toBitVec := HAnd.hAnd a b } (HAnd.hAnd { toBitVec := a } { toBitVec := b })

theorem USize.ofBitVec_and (a b : BitVec System.Platform.numBits) : Eq { toBitVec := HAnd.hAnd a b } (HAnd.hAnd { toBitVec := a } { toBitVec := b })

theorem UInt8.ofNat_and (a b : Nat) : Eq (ofNat (HAnd.hAnd a b)) (HAnd.hAnd (ofNat a) (ofNat b))

theorem UInt16.ofNat_and (a b : Nat) : Eq (ofNat (HAnd.hAnd a b)) (HAnd.hAnd (ofNat a) (ofNat b))

theorem UInt32.ofNat_and (a b : Nat) : Eq (ofNat (HAnd.hAnd a b)) (HAnd.hAnd (ofNat a) (ofNat b))

theorem UInt64.ofNat_and (a b : Nat) : Eq (ofNat (HAnd.hAnd a b)) (HAnd.hAnd (ofNat a) (ofNat b))

theorem USize.ofNat_and (a b : Nat) : Eq (ofNat (HAnd.hAnd a b)) (HAnd.hAnd (ofNat a) (ofNat b))

theorem UInt8.ofNatLT_and (a b : Nat) (ha : LT.lt a (HPow.hPow 2 8)) (hb : LT.lt b (HPow.hPow 2 8)) : Eq (ofNatLT (HAnd.hAnd a b) ⋯) (HAnd.hAnd (ofNatLT a ha) (ofNatLT b hb))

theorem UInt16.ofNatLT_and (a b : Nat) (ha : LT.lt a (HPow.hPow 2 16)) (hb : LT.lt b (HPow.hPow 2 16)) : Eq (ofNatLT (HAnd.hAnd a b) ⋯) (HAnd.hAnd (ofNatLT a ha) (ofNatLT b hb))

theorem UInt32.ofNatLT_and (a b : Nat) (ha : LT.lt a (HPow.hPow 2 32)) (hb : LT.lt b (HPow.hPow 2 32)) : Eq (ofNatLT (HAnd.hAnd a b) ⋯) (HAnd.hAnd (ofNatLT a ha) (ofNatLT b hb))

theorem UInt64.ofNatLT_and (a b : Nat) (ha : LT.lt a (HPow.hPow 2 64)) (hb : LT.lt b (HPow.hPow 2 64)) : Eq (ofNatLT (HAnd.hAnd a b) ⋯) (HAnd.hAnd (ofNatLT a ha) (ofNatLT b hb))

theorem UInt8.ofFin_or (a b : Fin size) : Eq (ofFin (HOr.hOr a b)) (HOr.hOr (ofFin a) (ofFin b))

theorem UInt16.ofFin_or (a b : Fin size) : Eq (ofFin (HOr.hOr a b)) (HOr.hOr (ofFin a) (ofFin b))

theorem UInt32.ofFin_or (a b : Fin size) : Eq (ofFin (HOr.hOr a b)) (HOr.hOr (ofFin a) (ofFin b))

theorem UInt64.ofFin_or (a b : Fin size) : Eq (ofFin (HOr.hOr a b)) (HOr.hOr (ofFin a) (ofFin b))

theorem USize.ofFin_or (a b : Fin size) : Eq (ofFin (HOr.hOr a b)) (HOr.hOr (ofFin a) (ofFin b))

theorem UInt8.ofBitVec_or (a b : BitVec 8) : Eq { toBitVec := HOr.hOr a b } (HOr.hOr { toBitVec := a } { toBitVec := b })

theorem UInt16.ofBitVec_or (a b : BitVec 16) : Eq { toBitVec := HOr.hOr a b } (HOr.hOr { toBitVec := a } { toBitVec := b })

theorem UInt32.ofBitVec_or (a b : BitVec 32) : Eq { toBitVec := HOr.hOr a b } (HOr.hOr { toBitVec := a } { toBitVec := b })

theorem UInt64.ofBitVec_or (a b : BitVec 64) : Eq { toBitVec := HOr.hOr a b } (HOr.hOr { toBitVec := a } { toBitVec := b })

theorem USize.ofBitVec_or (a b : BitVec System.Platform.numBits) : Eq { toBitVec := HOr.hOr a b } (HOr.hOr { toBitVec := a } { toBitVec := b })

theorem UInt8.ofNat_or (a b : Nat) : Eq (ofNat (HOr.hOr a b)) (HOr.hOr (ofNat a) (ofNat b))

theorem UInt16.ofNat_or (a b : Nat) : Eq (ofNat (HOr.hOr a b)) (HOr.hOr (ofNat a) (ofNat b))

theorem UInt32.ofNat_or (a b : Nat) : Eq (ofNat (HOr.hOr a b)) (HOr.hOr (ofNat a) (ofNat b))

theorem UInt64.ofNat_or (a b : Nat) : Eq (ofNat (HOr.hOr a b)) (HOr.hOr (ofNat a) (ofNat b))

theorem USize.ofNat_or (a b : Nat) : Eq (ofNat (HOr.hOr a b)) (HOr.hOr (ofNat a) (ofNat b))

theorem UInt8.ofNatLT_or (a b : Nat) (ha : LT.lt a (HPow.hPow 2 8)) (hb : LT.lt b (HPow.hPow 2 8)) : Eq (ofNatLT (HOr.hOr a b) ⋯) (HOr.hOr (ofNatLT a ha) (ofNatLT b hb))

theorem UInt16.ofNatLT_or (a b : Nat) (ha : LT.lt a (HPow.hPow 2 16)) (hb : LT.lt b (HPow.hPow 2 16)) : Eq (ofNatLT (HOr.hOr a b) ⋯) (HOr.hOr (ofNatLT a ha) (ofNatLT b hb))

theorem UInt32.ofNatLT_or (a b : Nat) (ha : LT.lt a (HPow.hPow 2 32)) (hb : LT.lt b (HPow.hPow 2 32)) : Eq (ofNatLT (HOr.hOr a b) ⋯) (HOr.hOr (ofNatLT a ha) (ofNatLT b hb))

theorem UInt64.ofNatLT_or (a b : Nat) (ha : LT.lt a (HPow.hPow 2 64)) (hb : LT.lt b (HPow.hPow 2 64)) : Eq (ofNatLT (HOr.hOr a b) ⋯) (HOr.hOr (ofNatLT a ha) (ofNatLT b hb))

theorem UInt8.ofFin_xor (a b : Fin size) : Eq (ofFin (HXor.hXor a b)) (HXor.hXor (ofFin a) (ofFin b))

theorem UInt16.ofFin_xor (a b : Fin size) : Eq (ofFin (HXor.hXor a b)) (HXor.hXor (ofFin a) (ofFin b))

theorem UInt32.ofFin_xor (a b : Fin size) : Eq (ofFin (HXor.hXor a b)) (HXor.hXor (ofFin a) (ofFin b))

theorem UInt64.ofFin_xor (a b : Fin size) : Eq (ofFin (HXor.hXor a b)) (HXor.hXor (ofFin a) (ofFin b))

theorem USize.ofFin_xor (a b : Fin size) : Eq (ofFin (HXor.hXor a b)) (HXor.hXor (ofFin a) (ofFin b))

theorem UInt8.ofBitVec_xor (a b : BitVec 8) : Eq { toBitVec := HXor.hXor a b } (HXor.hXor { toBitVec := a } { toBitVec := b })

theorem UInt16.ofBitVec_xor (a b : BitVec 16) : Eq { toBitVec := HXor.hXor a b } (HXor.hXor { toBitVec := a } { toBitVec := b })

theorem UInt32.ofBitVec_xor (a b : BitVec 32) : Eq { toBitVec := HXor.hXor a b } (HXor.hXor { toBitVec := a } { toBitVec := b })

theorem UInt64.ofBitVec_xor (a b : BitVec 64) : Eq { toBitVec := HXor.hXor a b } (HXor.hXor { toBitVec := a } { toBitVec := b })

theorem USize.ofBitVec_xor (a b : BitVec System.Platform.numBits) : Eq { toBitVec := HXor.hXor a b } (HXor.hXor { toBitVec := a } { toBitVec := b })

theorem UInt8.ofNat_xor (a b : Nat) : Eq (ofNat (HXor.hXor a b)) (HXor.hXor (ofNat a) (ofNat b))

theorem UInt16.ofNat_xor (a b : Nat) : Eq (ofNat (HXor.hXor a b)) (HXor.hXor (ofNat a) (ofNat b))

theorem UInt32.ofNat_xor (a b : Nat) : Eq (ofNat (HXor.hXor a b)) (HXor.hXor (ofNat a) (ofNat b))

theorem UInt64.ofNat_xor (a b : Nat) : Eq (ofNat (HXor.hXor a b)) (HXor.hXor (ofNat a) (ofNat b))

theorem USize.ofNat_xor (a b : Nat) : Eq (ofNat (HXor.hXor a b)) (HXor.hXor (ofNat a) (ofNat b))

theorem UInt8.ofNatLT_xor (a b : Nat) (ha : LT.lt a (HPow.hPow 2 8)) (hb : LT.lt b (HPow.hPow 2 8)) : Eq (ofNatLT (HXor.hXor a b) ⋯) (HXor.hXor (ofNatLT a ha) (ofNatLT b hb))

theorem UInt16.ofNatLT_xor (a b : Nat) (ha : LT.lt a (HPow.hPow 2 16)) (hb : LT.lt b (HPow.hPow 2 16)) : Eq (ofNatLT (HXor.hXor a b) ⋯) (HXor.hXor (ofNatLT a ha) (ofNatLT b hb))

theorem UInt32.ofNatLT_xor (a b : Nat) (ha : LT.lt a (HPow.hPow 2 32)) (hb : LT.lt b (HPow.hPow 2 32)) : Eq (ofNatLT (HXor.hXor a b) ⋯) (HXor.hXor (ofNatLT a ha) (ofNatLT b hb))

theorem UInt64.ofNatLT_xor (a b : Nat) (ha : LT.lt a (HPow.hPow 2 64)) (hb : LT.lt b (HPow.hPow 2 64)) : Eq (ofNatLT (HXor.hXor a b) ⋯) (HXor.hXor (ofNatLT a ha) (ofNatLT b hb))

theorem UInt8.ofBitVec_not (a : BitVec 8) : Eq { toBitVec := Complement.complement a } (Complement.complement { toBitVec := a })

theorem UInt16.ofBitVec_not (a : BitVec 16) : Eq { toBitVec := Complement.complement a } (Complement.complement { toBitVec := a })

theorem UInt32.ofBitVec_not (a : BitVec 32) : Eq { toBitVec := Complement.complement a } (Complement.complement { toBitVec := a })

theorem UInt64.ofBitVec_not (a : BitVec 64) : Eq { toBitVec := Complement.complement a } (Complement.complement { toBitVec := a })

theorem USize.ofBitVec_not (a : BitVec System.Platform.numBits) : Eq { toBitVec := Complement.complement a } (Complement.complement { toBitVec := a })

theorem UInt8.ofFin_rev (a : Fin size) : Eq (ofFin a.rev) (Complement.complement (ofFin a))

theorem UInt16.ofFin_rev (a : Fin size) : Eq (ofFin a.rev) (Complement.complement (ofFin a))

theorem UInt32.ofFin_rev (a : Fin size) : Eq (ofFin a.rev) (Complement.complement (ofFin a))

theorem UInt64.ofFin_rev (a : Fin size) : Eq (ofFin a.rev) (Complement.complement (ofFin a))

theorem USize.ofFin_rev (a : Fin size) : Eq (ofFin a.rev) (Complement.complement (ofFin a))

theorem UInt8.ofBitVec_shiftLeft (a : BitVec 8) (b : Nat) (hb : LT.lt b 8) : Eq { toBitVec := HShiftLeft.hShiftLeft a b } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem UInt16.ofBitVec_shiftLeft (a : BitVec 16) (b : Nat) (hb : LT.lt b 16) : Eq { toBitVec := HShiftLeft.hShiftLeft a b } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem UInt32.ofBitVec_shiftLeft (a : BitVec 32) (b : Nat) (hb : LT.lt b 32) : Eq { toBitVec := HShiftLeft.hShiftLeft a b } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem UInt64.ofBitVec_shiftLeft (a : BitVec 64) (b : Nat) (hb : LT.lt b 64) : Eq { toBitVec := HShiftLeft.hShiftLeft a b } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem USize.ofBitVec_shiftLeft (a : BitVec System.Platform.numBits) (b : Nat) (hb : LT.lt b System.Platform.numBits) : Eq { toBitVec := HShiftLeft.hShiftLeft a b } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem UInt8.ofBitVec_shiftLeft_mod (a : BitVec 8) (b : Nat) : Eq { toBitVec := HShiftLeft.hShiftLeft a (HMod.hMod b 8) } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem UInt16.ofBitVec_shiftLeft_mod (a : BitVec 16) (b : Nat) : Eq { toBitVec := HShiftLeft.hShiftLeft a (HMod.hMod b 16) } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem UInt32.ofBitVec_shiftLeft_mod (a : BitVec 32) (b : Nat) : Eq { toBitVec := HShiftLeft.hShiftLeft a (HMod.hMod b 32) } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem UInt64.ofBitVec_shiftLeft_mod (a : BitVec 64) (b : Nat) : Eq { toBitVec := HShiftLeft.hShiftLeft a (HMod.hMod b 64) } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem USize.ofBitVec_shiftLeft_mod (a : BitVec System.Platform.numBits) (b : Nat) : Eq { toBitVec := HShiftLeft.hShiftLeft a (HMod.hMod b System.Platform.numBits) } (HShiftLeft.hShiftLeft { toBitVec := a } (ofNat b))

theorem UInt8.ofFin_shiftLeft (a b : Fin size) (hb : LT.lt b 8) : Eq (ofFin (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem UInt16.ofFin_shiftLeft (a b : Fin size) (hb : LT.lt b 16) : Eq (ofFin (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem UInt32.ofFin_shiftLeft (a b : Fin size) (hb : LT.lt b 32) : Eq (ofFin (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem UInt64.ofFin_shiftLeft (a b : Fin size) (hb : LT.lt b 64) : Eq (ofFin (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem USize.ofFin_shiftLeft (a b : Fin size) (hb : LT.lt b.val System.Platform.numBits) : Eq (ofFin (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem UInt8.ofFin_shiftLeft_mod (a b : Fin size) : Eq (ofFin (HShiftLeft.hShiftLeft a (HMod.hMod b 8))) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem UInt16.ofFin_shiftLeft_mod (a b : Fin size) : Eq (ofFin (HShiftLeft.hShiftLeft a (HMod.hMod b 16))) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem UInt32.ofFin_shiftLeft_mod (a b : Fin size) : Eq (ofFin (HShiftLeft.hShiftLeft a (HMod.hMod b 32))) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem UInt64.ofFin_shiftLeft_mod (a b : Fin size) : Eq (ofFin (HShiftLeft.hShiftLeft a (HMod.hMod b 64))) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem USize.ofFin_shiftLeft_mod (a b : Fin size) : Eq (ofFin (HShiftLeft.hShiftLeft a (HMod.hMod b ⟨System.Platform.numBits, ⋯⟩))) (HShiftLeft.hShiftLeft (ofFin a) (ofFin b))

theorem UInt8.ofNat_shiftLeft (a b : Nat) (hb : LT.lt b 8) : Eq (ofNat (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofNat a) (ofNat b))

theorem UInt16.ofNat_shiftLeft (a b : Nat) (hb : LT.lt b 16) : Eq (ofNat (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofNat a) (ofNat b))

theorem UInt32.ofNat_shiftLeft (a b : Nat) (hb : LT.lt b 32) : Eq (ofNat (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofNat a) (ofNat b))

theorem UInt64.ofNat_shiftLeft (a b : Nat) (hb : LT.lt b 64) : Eq (ofNat (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofNat a) (ofNat b))

theorem USize.ofNat_shiftLeft (a b : Nat) (hb : LT.lt b System.Platform.numBits) : Eq (ofNat (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (ofNat a) (ofNat b))

theorem UInt8.ofNatLT_shiftLeft {a b : Nat} (ha : LT.lt (HShiftLeft.hShiftLeft a b) size) (hb : LT.lt b 8) : Eq (ofNatLT (HShiftLeft.hShiftLeft a b) ha) (HShiftLeft.hShiftLeft (ofNatLT a ⋯) (ofNatLT b ⋯))

theorem UInt16.ofNatLT_shiftLeft {a b : Nat} (ha : LT.lt (HShiftLeft.hShiftLeft a b) size) (hb : LT.lt b 16) : Eq (ofNatLT (HShiftLeft.hShiftLeft a b) ha) (HShiftLeft.hShiftLeft (ofNatLT a ⋯) (ofNatLT b ⋯))

theorem UInt32.ofNatLT_shiftLeft {a b : Nat} (ha : LT.lt (HShiftLeft.hShiftLeft a b) size) (hb : LT.lt b 32) : Eq (ofNatLT (HShiftLeft.hShiftLeft a b) ha) (HShiftLeft.hShiftLeft (ofNatLT a ⋯) (ofNatLT b ⋯))

theorem UInt64.ofNatLT_shiftLeft {a b : Nat} (ha : LT.lt (HShiftLeft.hShiftLeft a b) size) (hb : LT.lt b 64) : Eq (ofNatLT (HShiftLeft.hShiftLeft a b) ha) (HShiftLeft.hShiftLeft (ofNatLT a ⋯) (ofNatLT b ⋯))

theorem USize.ofNatLT_shiftLeft {a b : Nat} (ha : LT.lt (HShiftLeft.hShiftLeft a b) size) (hb : LT.lt b System.Platform.numBits) : Eq (ofNatLT (HShiftLeft.hShiftLeft a b) ha) (HShiftLeft.hShiftLeft (ofNatLT a ⋯) (ofNatLT b ⋯))

theorem UInt8.ofBitVec_shiftRight (a : BitVec 8) (b : Nat) (hb : LT.lt b 8) : Eq { toBitVec := HShiftRight.hShiftRight a b } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem UInt16.ofBitVec_shiftRight (a : BitVec 16) (b : Nat) (hb : LT.lt b 16) : Eq { toBitVec := HShiftRight.hShiftRight a b } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem UInt32.ofBitVec_shiftRight (a : BitVec 32) (b : Nat) (hb : LT.lt b 32) : Eq { toBitVec := HShiftRight.hShiftRight a b } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem UInt64.ofBitVec_shiftRight (a : BitVec 64) (b : Nat) (hb : LT.lt b 64) : Eq { toBitVec := HShiftRight.hShiftRight a b } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem USize.ofBitVec_shiftRight (a : BitVec System.Platform.numBits) (b : Nat) (hb : LT.lt b System.Platform.numBits) : Eq { toBitVec := HShiftRight.hShiftRight a b } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem UInt8.ofBitVec_shiftRight_mod (a : BitVec 8) (b : Nat) : Eq { toBitVec := HShiftRight.hShiftRight a (HMod.hMod b 8) } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem UInt16.ofBitVec_shiftRight_mod (a : BitVec 16) (b : Nat) : Eq { toBitVec := HShiftRight.hShiftRight a (HMod.hMod b 16) } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem UInt32.ofBitVec_shiftRight_mod (a : BitVec 32) (b : Nat) : Eq { toBitVec := HShiftRight.hShiftRight a (HMod.hMod b 32) } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem UInt64.ofBitVec_shiftRight_mod (a : BitVec 64) (b : Nat) : Eq { toBitVec := HShiftRight.hShiftRight a (HMod.hMod b 64) } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem USize.ofBitVec_shiftRight_mod (a : BitVec System.Platform.numBits) (b : Nat) : Eq { toBitVec := HShiftRight.hShiftRight a (HMod.hMod b System.Platform.numBits) } (HShiftRight.hShiftRight { toBitVec := a } (ofNat b))

theorem UInt8.ofFin_shiftRight (a b : Fin size) (hb : LT.lt b 8) : Eq (ofFin (HShiftRight.hShiftRight a b)) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem UInt16.ofFin_shiftRight (a b : Fin size) (hb : LT.lt b 16) : Eq (ofFin (HShiftRight.hShiftRight a b)) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem UInt32.ofFin_shiftRight (a b : Fin size) (hb : LT.lt b 32) : Eq (ofFin (HShiftRight.hShiftRight a b)) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem UInt64.ofFin_shiftRight (a b : Fin size) (hb : LT.lt b 64) : Eq (ofFin (HShiftRight.hShiftRight a b)) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem USize.ofFin_shiftRight (a b : Fin size) (hb : LT.lt b.val System.Platform.numBits) : Eq (ofFin (HShiftRight.hShiftRight a b)) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem UInt8.ofFin_shiftRight_mod (a b : Fin size) : Eq (ofFin (HShiftRight.hShiftRight a (HMod.hMod b 8))) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem UInt16.ofFin_shiftRight_mod (a b : Fin size) : Eq (ofFin (HShiftRight.hShiftRight a (HMod.hMod b 16))) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem UInt32.ofFin_shiftRight_mod (a b : Fin size) : Eq (ofFin (HShiftRight.hShiftRight a (HMod.hMod b 32))) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem UInt64.ofFin_shiftRight_mod (a b : Fin size) : Eq (ofFin (HShiftRight.hShiftRight a (HMod.hMod b 64))) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem USize.ofFin_shiftRight_mod (a b : Fin size) : Eq (ofFin (HShiftRight.hShiftRight a (HMod.hMod b ⟨System.Platform.numBits, ⋯⟩))) (HShiftRight.hShiftRight (ofFin a) (ofFin b))

theorem UInt8.neg_eq_not_add (a : UInt8) : Eq (Neg.neg a) (HAdd.hAdd (Complement.complement a) 1)

theorem UInt16.neg_eq_not_add (a : UInt16) : Eq (Neg.neg a) (HAdd.hAdd (Complement.complement a) 1)

theorem UInt32.neg_eq_not_add (a : UInt32) : Eq (Neg.neg a) (HAdd.hAdd (Complement.complement a) 1)

theorem UInt64.neg_eq_not_add (a : UInt64) : Eq (Neg.neg a) (HAdd.hAdd (Complement.complement a) 1)

theorem USize.neg_eq_not_add (a : USize) : Eq (Neg.neg a) (HAdd.hAdd (Complement.complement a) 1)

theorem UInt8.not_eq_neg_sub (a : UInt8) : Eq (Complement.complement a) (HSub.hSub (Neg.neg a) 1)

theorem UInt16.not_eq_neg_sub (a : UInt16) : Eq (Complement.complement a) (HSub.hSub (Neg.neg a) 1)

theorem UInt32.not_eq_neg_sub (a : UInt32) : Eq (Complement.complement a) (HSub.hSub (Neg.neg a) 1)

theorem UInt64.not_eq_neg_sub (a : UInt64) : Eq (Complement.complement a) (HSub.hSub (Neg.neg a) 1)

theorem USize.not_eq_neg_sub (a : USize) : Eq (Complement.complement a) (HSub.hSub (Neg.neg a) 1)

theorem UInt8.or_assoc (a b c : UInt8) : Eq (HOr.hOr (HOr.hOr a b) c) (HOr.hOr a (HOr.hOr b c))

theorem UInt16.or_assoc (a b c : UInt16) : Eq (HOr.hOr (HOr.hOr a b) c) (HOr.hOr a (HOr.hOr b c))

theorem UInt32.or_assoc (a b c : UInt32) : Eq (HOr.hOr (HOr.hOr a b) c) (HOr.hOr a (HOr.hOr b c))

theorem UInt64.or_assoc (a b c : UInt64) : Eq (HOr.hOr (HOr.hOr a b) c) (HOr.hOr a (HOr.hOr b c))

theorem USize.or_assoc (a b c : USize) : Eq (HOr.hOr (HOr.hOr a b) c) (HOr.hOr a (HOr.hOr b c))

theorem instAssociativeUInt8HOr : Std.Associative fun (x1 x2 : UInt8) => HOr.hOr x1 x2

theorem instAssociativeUInt16HOr : Std.Associative fun (x1 x2 : UInt16) => HOr.hOr x1 x2

theorem instAssociativeUInt32HOr : Std.Associative fun (x1 x2 : UInt32) => HOr.hOr x1 x2

theorem instAssociativeUInt64HOr : Std.Associative fun (x1 x2 : UInt64) => HOr.hOr x1 x2

theorem instAssociativeUSizeHOr : Std.Associative fun (x1 x2 : USize) => HOr.hOr x1 x2

theorem UInt8.or_comm (a b : UInt8) : Eq (HOr.hOr a b) (HOr.hOr b a)

theorem UInt16.or_comm (a b : UInt16) : Eq (HOr.hOr a b) (HOr.hOr b a)

theorem UInt32.or_comm (a b : UInt32) : Eq (HOr.hOr a b) (HOr.hOr b a)

theorem UInt64.or_comm (a b : UInt64) : Eq (HOr.hOr a b) (HOr.hOr b a)

theorem USize.or_comm (a b : USize) : Eq (HOr.hOr a b) (HOr.hOr b a)

theorem instCommutativeUInt8HOr : Std.Commutative fun (x1 x2 : UInt8) => HOr.hOr x1 x2

theorem instCommutativeUInt16HOr : Std.Commutative fun (x1 x2 : UInt16) => HOr.hOr x1 x2

theorem instCommutativeUInt32HOr : Std.Commutative fun (x1 x2 : UInt32) => HOr.hOr x1 x2

theorem instCommutativeUInt64HOr : Std.Commutative fun (x1 x2 : UInt64) => HOr.hOr x1 x2

theorem instCommutativeUSizeHOr : Std.Commutative fun (x1 x2 : USize) => HOr.hOr x1 x2

theorem UInt8.or_self {a : UInt8} : Eq (HOr.hOr a a) a

theorem UInt16.or_self {a : UInt16} : Eq (HOr.hOr a a) a

theorem UInt32.or_self {a : UInt32} : Eq (HOr.hOr a a) a

theorem UInt64.or_self {a : UInt64} : Eq (HOr.hOr a a) a

theorem USize.or_self {a : USize} : Eq (HOr.hOr a a) a

theorem instIdempotentOpUInt8HOr : Std.IdempotentOp fun (x1 x2 : UInt8) => HOr.hOr x1 x2

theorem instIdempotentOpUInt16HOr : Std.IdempotentOp fun (x1 x2 : UInt16) => HOr.hOr x1 x2

theorem instIdempotentOpUInt32HOr : Std.IdempotentOp fun (x1 x2 : UInt32) => HOr.hOr x1 x2

theorem instIdempotentOpUInt64HOr : Std.IdempotentOp fun (x1 x2 : UInt64) => HOr.hOr x1 x2

theorem instIdempotentOpUSizeHOr : Std.IdempotentOp fun (x1 x2 : USize) => HOr.hOr x1 x2

theorem UInt8.or_zero {a : UInt8} : Eq (HOr.hOr a 0) a

theorem UInt16.or_zero {a : UInt16} : Eq (HOr.hOr a 0) a

theorem UInt32.or_zero {a : UInt32} : Eq (HOr.hOr a 0) a

theorem UInt64.or_zero {a : UInt64} : Eq (HOr.hOr a 0) a

theorem USize.or_zero {a : USize} : Eq (HOr.hOr a 0) a

theorem UInt8.zero_or {a : UInt8} : Eq (HOr.hOr 0 a) a

theorem UInt16.zero_or {a : UInt16} : Eq (HOr.hOr 0 a) a

theorem UInt32.zero_or {a : UInt32} : Eq (HOr.hOr 0 a) a

theorem UInt64.zero_or {a : UInt64} : Eq (HOr.hOr 0 a) a

theorem USize.zero_or {a : USize} : Eq (HOr.hOr 0 a) a

theorem instLawfulCommIdentityUInt8HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => HOr.hOr x1 x2) 0

theorem instLawfulCommIdentityUInt16HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => HOr.hOr x1 x2) 0

theorem instLawfulCommIdentityUInt32HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => HOr.hOr x1 x2) 0

theorem instLawfulCommIdentityUInt64HOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => HOr.hOr x1 x2) 0

theorem instLawfulCommIdentityUSizeHOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : USize) => HOr.hOr x1 x2) 0

theorem UInt8.neg_one_or {a : UInt8} : Eq (HOr.hOr (-1) a) (-1)

theorem UInt16.neg_one_or {a : UInt16} : Eq (HOr.hOr (-1) a) (-1)

theorem UInt32.neg_one_or {a : UInt32} : Eq (HOr.hOr (-1) a) (-1)

theorem UInt64.neg_one_or {a : UInt64} : Eq (HOr.hOr (-1) a) (-1)

theorem USize.neg_one_or {a : USize} : Eq (HOr.hOr (-1) a) (-1)

theorem UInt8.or_neg_one {a : UInt8} : Eq (HOr.hOr a (-1)) (-1)

theorem UInt16.or_neg_one {a : UInt16} : Eq (HOr.hOr a (-1)) (-1)

theorem UInt32.or_neg_one {a : UInt32} : Eq (HOr.hOr a (-1)) (-1)

theorem UInt64.or_neg_one {a : UInt64} : Eq (HOr.hOr a (-1)) (-1)

theorem USize.or_neg_one {a : USize} : Eq (HOr.hOr a (-1)) (-1)

theorem UInt8.or_eq_zero_iff {a b : UInt8} : Iff (Eq (HOr.hOr a b) 0) (And (Eq a 0) (Eq b 0))

theorem UInt16.or_eq_zero_iff {a b : UInt16} : Iff (Eq (HOr.hOr a b) 0) (And (Eq a 0) (Eq b 0))

theorem UInt32.or_eq_zero_iff {a b : UInt32} : Iff (Eq (HOr.hOr a b) 0) (And (Eq a 0) (Eq b 0))

theorem UInt64.or_eq_zero_iff {a b : UInt64} : Iff (Eq (HOr.hOr a b) 0) (And (Eq a 0) (Eq b 0))

theorem USize.or_eq_zero_iff {a b : USize} : Iff (Eq (HOr.hOr a b) 0) (And (Eq a 0) (Eq b 0))

theorem UInt8.and_assoc (a b c : UInt8) : Eq (HAnd.hAnd (HAnd.hAnd a b) c) (HAnd.hAnd a (HAnd.hAnd b c))

theorem UInt16.and_assoc (a b c : UInt16) : Eq (HAnd.hAnd (HAnd.hAnd a b) c) (HAnd.hAnd a (HAnd.hAnd b c))

theorem UInt32.and_assoc (a b c : UInt32) : Eq (HAnd.hAnd (HAnd.hAnd a b) c) (HAnd.hAnd a (HAnd.hAnd b c))

theorem UInt64.and_assoc (a b c : UInt64) : Eq (HAnd.hAnd (HAnd.hAnd a b) c) (HAnd.hAnd a (HAnd.hAnd b c))

theorem USize.and_assoc (a b c : USize) : Eq (HAnd.hAnd (HAnd.hAnd a b) c) (HAnd.hAnd a (HAnd.hAnd b c))

theorem instAssociativeUInt8HAnd : Std.Associative fun (x1 x2 : UInt8) => HAnd.hAnd x1 x2

theorem instAssociativeUInt16HAnd : Std.Associative fun (x1 x2 : UInt16) => HAnd.hAnd x1 x2

theorem instAssociativeUInt32HAnd : Std.Associative fun (x1 x2 : UInt32) => HAnd.hAnd x1 x2

theorem instAssociativeUInt64HAnd : Std.Associative fun (x1 x2 : UInt64) => HAnd.hAnd x1 x2

theorem instAssociativeUSizeHAnd : Std.Associative fun (x1 x2 : USize) => HAnd.hAnd x1 x2

theorem UInt8.and_comm (a b : UInt8) : Eq (HAnd.hAnd a b) (HAnd.hAnd b a)

theorem UInt16.and_comm (a b : UInt16) : Eq (HAnd.hAnd a b) (HAnd.hAnd b a)

theorem UInt32.and_comm (a b : UInt32) : Eq (HAnd.hAnd a b) (HAnd.hAnd b a)

theorem UInt64.and_comm (a b : UInt64) : Eq (HAnd.hAnd a b) (HAnd.hAnd b a)

theorem USize.and_comm (a b : USize) : Eq (HAnd.hAnd a b) (HAnd.hAnd b a)

theorem instCommutativeUInt8HAnd : Std.Commutative fun (x1 x2 : UInt8) => HAnd.hAnd x1 x2

theorem instCommutativeUInt16HAnd : Std.Commutative fun (x1 x2 : UInt16) => HAnd.hAnd x1 x2

theorem instCommutativeUInt32HAnd : Std.Commutative fun (x1 x2 : UInt32) => HAnd.hAnd x1 x2

theorem instCommutativeUInt64HAnd : Std.Commutative fun (x1 x2 : UInt64) => HAnd.hAnd x1 x2

theorem instCommutativeUSizeHAnd : Std.Commutative fun (x1 x2 : USize) => HAnd.hAnd x1 x2

theorem UInt8.and_self {a : UInt8} : Eq (HAnd.hAnd a a) a

theorem UInt16.and_self {a : UInt16} : Eq (HAnd.hAnd a a) a

theorem UInt32.and_self {a : UInt32} : Eq (HAnd.hAnd a a) a

theorem UInt64.and_self {a : UInt64} : Eq (HAnd.hAnd a a) a

theorem USize.and_self {a : USize} : Eq (HAnd.hAnd a a) a

theorem instIdempotentOpUInt8HAnd : Std.IdempotentOp fun (x1 x2 : UInt8) => HAnd.hAnd x1 x2

theorem instIdempotentOpUInt16HAnd : Std.IdempotentOp fun (x1 x2 : UInt16) => HAnd.hAnd x1 x2

theorem instIdempotentOpUInt32HAnd : Std.IdempotentOp fun (x1 x2 : UInt32) => HAnd.hAnd x1 x2

theorem instIdempotentOpUInt64HAnd : Std.IdempotentOp fun (x1 x2 : UInt64) => HAnd.hAnd x1 x2

theorem instIdempotentOpUSizeHAnd : Std.IdempotentOp fun (x1 x2 : USize) => HAnd.hAnd x1 x2

theorem UInt8.and_zero {a : UInt8} : Eq (HAnd.hAnd a 0) 0

theorem UInt16.and_zero {a : UInt16} : Eq (HAnd.hAnd a 0) 0

theorem UInt32.and_zero {a : UInt32} : Eq (HAnd.hAnd a 0) 0

theorem UInt64.and_zero {a : UInt64} : Eq (HAnd.hAnd a 0) 0

theorem USize.and_zero {a : USize} : Eq (HAnd.hAnd a 0) 0

theorem UInt8.zero_and {a : UInt8} : Eq (HAnd.hAnd 0 a) 0

theorem UInt16.zero_and {a : UInt16} : Eq (HAnd.hAnd 0 a) 0

theorem UInt32.zero_and {a : UInt32} : Eq (HAnd.hAnd 0 a) 0

theorem UInt64.zero_and {a : UInt64} : Eq (HAnd.hAnd 0 a) 0

theorem USize.zero_and {a : USize} : Eq (HAnd.hAnd 0 a) 0

theorem UInt8.neg_one_and {a : UInt8} : Eq (HAnd.hAnd (-1) a) a

theorem UInt16.neg_one_and {a : UInt16} : Eq (HAnd.hAnd (-1) a) a

theorem UInt32.neg_one_and {a : UInt32} : Eq (HAnd.hAnd (-1) a) a

theorem UInt64.neg_one_and {a : UInt64} : Eq (HAnd.hAnd (-1) a) a

theorem USize.neg_one_and {a : USize} : Eq (HAnd.hAnd (-1) a) a

theorem UInt8.and_neg_one {a : UInt8} : Eq (HAnd.hAnd a (-1)) a

theorem UInt16.and_neg_one {a : UInt16} : Eq (HAnd.hAnd a (-1)) a

theorem UInt32.and_neg_one {a : UInt32} : Eq (HAnd.hAnd a (-1)) a

theorem UInt64.and_neg_one {a : UInt64} : Eq (HAnd.hAnd a (-1)) a

theorem USize.and_neg_one {a : USize} : Eq (HAnd.hAnd a (-1)) a

theorem instLawfulCommIdentityUInt8HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => HAnd.hAnd x1 x2) (-1)

theorem instLawfulCommIdentityUInt16HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => HAnd.hAnd x1 x2) (-1)

theorem instLawfulCommIdentityUInt32HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => HAnd.hAnd x1 x2) (-1)

theorem instLawfulCommIdentityUInt64HAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => HAnd.hAnd x1 x2) (-1)

theorem instLawfulCommIdentityUSizeHAndNegOfNat : Std.LawfulCommIdentity (fun (x1 x2 : USize) => HAnd.hAnd x1 x2) (-1)

theorem UInt8.and_eq_neg_one_iff {a b : UInt8} : Iff (Eq (HAnd.hAnd a b) (-1)) (And (Eq a (-1)) (Eq b (-1)))

theorem UInt16.and_eq_neg_one_iff {a b : UInt16} : Iff (Eq (HAnd.hAnd a b) (-1)) (And (Eq a (-1)) (Eq b (-1)))

theorem UInt32.and_eq_neg_one_iff {a b : UInt32} : Iff (Eq (HAnd.hAnd a b) (-1)) (And (Eq a (-1)) (Eq b (-1)))

theorem UInt64.and_eq_neg_one_iff {a b : UInt64} : Iff (Eq (HAnd.hAnd a b) (-1)) (And (Eq a (-1)) (Eq b (-1)))

theorem USize.and_eq_neg_one_iff {a b : USize} : Iff (Eq (HAnd.hAnd a b) (-1)) (And (Eq a (-1)) (Eq b (-1)))

theorem UInt8.xor_assoc (a b c : UInt8) : Eq (HXor.hXor (HXor.hXor a b) c) (HXor.hXor a (HXor.hXor b c))

theorem UInt16.xor_assoc (a b c : UInt16) : Eq (HXor.hXor (HXor.hXor a b) c) (HXor.hXor a (HXor.hXor b c))

theorem UInt32.xor_assoc (a b c : UInt32) : Eq (HXor.hXor (HXor.hXor a b) c) (HXor.hXor a (HXor.hXor b c))

theorem UInt64.xor_assoc (a b c : UInt64) : Eq (HXor.hXor (HXor.hXor a b) c) (HXor.hXor a (HXor.hXor b c))

theorem USize.xor_assoc (a b c : USize) : Eq (HXor.hXor (HXor.hXor a b) c) (HXor.hXor a (HXor.hXor b c))

theorem instAssociativeUInt8HXor : Std.Associative fun (x1 x2 : UInt8) => HXor.hXor x1 x2

theorem instAssociativeUInt16HXor : Std.Associative fun (x1 x2 : UInt16) => HXor.hXor x1 x2

theorem instAssociativeUInt32HXor : Std.Associative fun (x1 x2 : UInt32) => HXor.hXor x1 x2

theorem instAssociativeUInt64HXor : Std.Associative fun (x1 x2 : UInt64) => HXor.hXor x1 x2

theorem instAssociativeUSizeHXor : Std.Associative fun (x1 x2 : USize) => HXor.hXor x1 x2

theorem UInt8.xor_comm (a b : UInt8) : Eq (HXor.hXor a b) (HXor.hXor b a)

theorem UInt16.xor_comm (a b : UInt16) : Eq (HXor.hXor a b) (HXor.hXor b a)

theorem UInt32.xor_comm (a b : UInt32) : Eq (HXor.hXor a b) (HXor.hXor b a)

theorem UInt64.xor_comm (a b : UInt64) : Eq (HXor.hXor a b) (HXor.hXor b a)

theorem USize.xor_comm (a b : USize) : Eq (HXor.hXor a b) (HXor.hXor b a)

theorem instCommutativeUInt8HXor : Std.Commutative fun (x1 x2 : UInt8) => HXor.hXor x1 x2

theorem instCommutativeUInt16HXor : Std.Commutative fun (x1 x2 : UInt16) => HXor.hXor x1 x2

theorem instCommutativeUInt32HXor : Std.Commutative fun (x1 x2 : UInt32) => HXor.hXor x1 x2

theorem instCommutativeUInt64HXor : Std.Commutative fun (x1 x2 : UInt64) => HXor.hXor x1 x2

theorem instCommutativeUSizeHXor : Std.Commutative fun (x1 x2 : USize) => HXor.hXor x1 x2

theorem UInt8.xor_self {a : UInt8} : Eq (HXor.hXor a a) 0

theorem UInt16.xor_self {a : UInt16} : Eq (HXor.hXor a a) 0

theorem UInt32.xor_self {a : UInt32} : Eq (HXor.hXor a a) 0

theorem UInt64.xor_self {a : UInt64} : Eq (HXor.hXor a a) 0

theorem USize.xor_self {a : USize} : Eq (HXor.hXor a a) 0

theorem UInt8.xor_zero {a : UInt8} : Eq (HXor.hXor a 0) a

theorem UInt16.xor_zero {a : UInt16} : Eq (HXor.hXor a 0) a

theorem UInt32.xor_zero {a : UInt32} : Eq (HXor.hXor a 0) a

theorem UInt64.xor_zero {a : UInt64} : Eq (HXor.hXor a 0) a

theorem USize.xor_zero {a : USize} : Eq (HXor.hXor a 0) a

theorem UInt8.zero_xor {a : UInt8} : Eq (HXor.hXor 0 a) a

theorem UInt16.zero_xor {a : UInt16} : Eq (HXor.hXor 0 a) a

theorem UInt32.zero_xor {a : UInt32} : Eq (HXor.hXor 0 a) a

theorem UInt64.zero_xor {a : UInt64} : Eq (HXor.hXor 0 a) a

theorem USize.zero_xor {a : USize} : Eq (HXor.hXor 0 a) a

theorem UInt8.neg_one_xor {a : UInt8} : Eq (HXor.hXor (-1) a) (Complement.complement a)

theorem UInt16.neg_one_xor {a : UInt16} : Eq (HXor.hXor (-1) a) (Complement.complement a)

theorem UInt32.neg_one_xor {a : UInt32} : Eq (HXor.hXor (-1) a) (Complement.complement a)

theorem UInt64.neg_one_xor {a : UInt64} : Eq (HXor.hXor (-1) a) (Complement.complement a)

theorem USize.neg_one_xor {a : USize} : Eq (HXor.hXor (-1) a) (Complement.complement a)

theorem UInt8.xor_neg_one {a : UInt8} : Eq (HXor.hXor a (-1)) (Complement.complement a)

theorem UInt16.xor_neg_one {a : UInt16} : Eq (HXor.hXor a (-1)) (Complement.complement a)

theorem UInt32.xor_neg_one {a : UInt32} : Eq (HXor.hXor a (-1)) (Complement.complement a)

theorem UInt64.xor_neg_one {a : UInt64} : Eq (HXor.hXor a (-1)) (Complement.complement a)

theorem USize.xor_neg_one {a : USize} : Eq (HXor.hXor a (-1)) (Complement.complement a)

theorem instLawfulCommIdentityUInt8HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => HXor.hXor x1 x2) 0

theorem instLawfulCommIdentityUInt16HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => HXor.hXor x1 x2) 0

theorem instLawfulCommIdentityUInt32HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => HXor.hXor x1 x2) 0

theorem instLawfulCommIdentityUInt64HXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => HXor.hXor x1 x2) 0

theorem instLawfulCommIdentityUSizeHXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : USize) => HXor.hXor x1 x2) 0

theorem UInt8.xor_eq_zero_iff {a b : UInt8} : Iff (Eq (HXor.hXor a b) 0) (Eq a b)

theorem UInt16.xor_eq_zero_iff {a b : UInt16} : Iff (Eq (HXor.hXor a b) 0) (Eq a b)

theorem UInt32.xor_eq_zero_iff {a b : UInt32} : Iff (Eq (HXor.hXor a b) 0) (Eq a b)

theorem UInt64.xor_eq_zero_iff {a b : UInt64} : Iff (Eq (HXor.hXor a b) 0) (Eq a b)

theorem USize.xor_eq_zero_iff {a b : USize} : Iff (Eq (HXor.hXor a b) 0) (Eq a b)

theorem UInt8.xor_left_inj {a b : UInt8} (c : UInt8) : Iff (Eq (HXor.hXor a c) (HXor.hXor b c)) (Eq a b)

theorem UInt16.xor_left_inj {a b : UInt16} (c : UInt16) : Iff (Eq (HXor.hXor a c) (HXor.hXor b c)) (Eq a b)

theorem UInt32.xor_left_inj {a b : UInt32} (c : UInt32) : Iff (Eq (HXor.hXor a c) (HXor.hXor b c)) (Eq a b)

theorem UInt64.xor_left_inj {a b : UInt64} (c : UInt64) : Iff (Eq (HXor.hXor a c) (HXor.hXor b c)) (Eq a b)

theorem USize.xor_left_inj {a b : USize} (c : USize) : Iff (Eq (HXor.hXor a c) (HXor.hXor b c)) (Eq a b)

theorem UInt8.xor_right_inj {a b : UInt8} (c : UInt8) : Iff (Eq (HXor.hXor c a) (HXor.hXor c b)) (Eq a b)

theorem UInt16.xor_right_inj {a b : UInt16} (c : UInt16) : Iff (Eq (HXor.hXor c a) (HXor.hXor c b)) (Eq a b)

theorem UInt32.xor_right_inj {a b : UInt32} (c : UInt32) : Iff (Eq (HXor.hXor c a) (HXor.hXor c b)) (Eq a b)

theorem UInt64.xor_right_inj {a b : UInt64} (c : UInt64) : Iff (Eq (HXor.hXor c a) (HXor.hXor c b)) (Eq a b)

theorem USize.xor_right_inj {a b : USize} (c : USize) : Iff (Eq (HXor.hXor c a) (HXor.hXor c b)) (Eq a b)

theorem UInt8.not_zero : Eq (Complement.complement 0) (-1)

theorem UInt16.not_zero : Eq (Complement.complement 0) (-1)

theorem UInt32.not_zero : Eq (Complement.complement 0) (-1)

theorem UInt64.not_zero : Eq (Complement.complement 0) (-1)

theorem USize.not_zero : Eq (Complement.complement 0) (-1)

theorem UInt8.not_neg_one : Eq (Complement.complement (-1)) 0

theorem UInt16.not_neg_one : Eq (Complement.complement (-1)) 0

theorem UInt32.not_neg_one : Eq (Complement.complement (-1)) 0

theorem UInt64.not_neg_one : Eq (Complement.complement (-1)) 0

theorem USize.not_neg_one : Eq (Complement.complement (-1)) 0

theorem UInt8.not_not {a : UInt8} : Eq (Complement.complement (Complement.complement a)) a

theorem UInt16.not_not {a : UInt16} : Eq (Complement.complement (Complement.complement a)) a

theorem UInt32.not_not {a : UInt32} : Eq (Complement.complement (Complement.complement a)) a

theorem UInt64.not_not {a : UInt64} : Eq (Complement.complement (Complement.complement a)) a

theorem USize.not_not {a : USize} : Eq (Complement.complement (Complement.complement a)) a

theorem UInt8.not_inj {a b : UInt8} : Iff (Eq (Complement.complement a) (Complement.complement b)) (Eq a b)

theorem UInt16.not_inj {a b : UInt16} : Iff (Eq (Complement.complement a) (Complement.complement b)) (Eq a b)

theorem UInt32.not_inj {a b : UInt32} : Iff (Eq (Complement.complement a) (Complement.complement b)) (Eq a b)

theorem UInt64.not_inj {a b : UInt64} : Iff (Eq (Complement.complement a) (Complement.complement b)) (Eq a b)

theorem USize.not_inj {a b : USize} : Iff (Eq (Complement.complement a) (Complement.complement b)) (Eq a b)

theorem UInt8.and_not_self {a : UInt8} : Eq (HAnd.hAnd a (Complement.complement a)) 0

theorem UInt16.and_not_self {a : UInt16} : Eq (HAnd.hAnd a (Complement.complement a)) 0

theorem UInt32.and_not_self {a : UInt32} : Eq (HAnd.hAnd a (Complement.complement a)) 0

theorem UInt64.and_not_self {a : UInt64} : Eq (HAnd.hAnd a (Complement.complement a)) 0

theorem USize.and_not_self {a : USize} : Eq (HAnd.hAnd a (Complement.complement a)) 0

theorem UInt8.not_and_self {a : UInt8} : Eq (HAnd.hAnd (Complement.complement a) a) 0

theorem UInt16.not_and_self {a : UInt16} : Eq (HAnd.hAnd (Complement.complement a) a) 0

theorem UInt32.not_and_self {a : UInt32} : Eq (HAnd.hAnd (Complement.complement a) a) 0

theorem UInt64.not_and_self {a : UInt64} : Eq (HAnd.hAnd (Complement.complement a) a) 0

theorem USize.not_and_self {a : USize} : Eq (HAnd.hAnd (Complement.complement a) a) 0

theorem UInt8.or_not_self {a : UInt8} : Eq (HOr.hOr a (Complement.complement a)) (-1)

theorem UInt16.or_not_self {a : UInt16} : Eq (HOr.hOr a (Complement.complement a)) (-1)

theorem UInt32.or_not_self {a : UInt32} : Eq (HOr.hOr a (Complement.complement a)) (-1)

theorem UInt64.or_not_self {a : UInt64} : Eq (HOr.hOr a (Complement.complement a)) (-1)

theorem USize.or_not_self {a : USize} : Eq (HOr.hOr a (Complement.complement a)) (-1)

theorem UInt8.not_or_self {a : UInt8} : Eq (HOr.hOr (Complement.complement a) a) (-1)

theorem UInt16.not_or_self {a : UInt16} : Eq (HOr.hOr (Complement.complement a) a) (-1)

theorem UInt32.not_or_self {a : UInt32} : Eq (HOr.hOr (Complement.complement a) a) (-1)

theorem UInt64.not_or_self {a : UInt64} : Eq (HOr.hOr (Complement.complement a) a) (-1)

theorem USize.not_or_self {a : USize} : Eq (HOr.hOr (Complement.complement a) a) (-1)

theorem UInt8.not_eq_comm {a b : UInt8} : Iff (Eq (Complement.complement a) b) (Eq a (Complement.complement b))

theorem UInt16.not_eq_comm {a b : UInt16} : Iff (Eq (Complement.complement a) b) (Eq a (Complement.complement b))

theorem UInt32.not_eq_comm {a b : UInt32} : Iff (Eq (Complement.complement a) b) (Eq a (Complement.complement b))

theorem UInt64.not_eq_comm {a b : UInt64} : Iff (Eq (Complement.complement a) b) (Eq a (Complement.complement b))

theorem USize.not_eq_comm {a b : USize} : Iff (Eq (Complement.complement a) b) (Eq a (Complement.complement b))

theorem UInt8.ne_not_self {a : UInt8} : Ne a (Complement.complement a)

theorem UInt16.ne_not_self {a : UInt16} : Ne a (Complement.complement a)

theorem UInt32.ne_not_self {a : UInt32} : Ne a (Complement.complement a)

theorem UInt64.ne_not_self {a : UInt64} : Ne a (Complement.complement a)

theorem USize.ne_not_self {a : USize} : Ne a (Complement.complement a)

theorem UInt8.not_ne_self {a : UInt8} : Ne (Complement.complement a) a

theorem UInt16.not_ne_self {a : UInt16} : Ne (Complement.complement a) a

theorem UInt32.not_ne_self {a : UInt32} : Ne (Complement.complement a) a

theorem UInt64.not_ne_self {a : UInt64} : Ne (Complement.complement a) a

theorem USize.not_ne_self {a : USize} : Ne (Complement.complement a) a

theorem UInt8.not_xor {a b : UInt8} : Eq (HXor.hXor (Complement.complement a) b) (Complement.complement (HXor.hXor a b))

theorem UInt16.not_xor {a b : UInt16} : Eq (HXor.hXor (Complement.complement a) b) (Complement.complement (HXor.hXor a b))

theorem UInt32.not_xor {a b : UInt32} : Eq (HXor.hXor (Complement.complement a) b) (Complement.complement (HXor.hXor a b))

theorem UInt64.not_xor {a b : UInt64} : Eq (HXor.hXor (Complement.complement a) b) (Complement.complement (HXor.hXor a b))

theorem USize.not_xor {a b : USize} : Eq (HXor.hXor (Complement.complement a) b) (Complement.complement (HXor.hXor a b))

theorem UInt8.xor_not {a b : UInt8} : Eq (HXor.hXor a (Complement.complement b)) (Complement.complement (HXor.hXor a b))

theorem UInt16.xor_not {a b : UInt16} : Eq (HXor.hXor a (Complement.complement b)) (Complement.complement (HXor.hXor a b))

theorem UInt32.xor_not {a b : UInt32} : Eq (HXor.hXor a (Complement.complement b)) (Complement.complement (HXor.hXor a b))

theorem UInt64.xor_not {a b : UInt64} : Eq (HXor.hXor a (Complement.complement b)) (Complement.complement (HXor.hXor a b))

theorem USize.xor_not {a b : USize} : Eq (HXor.hXor a (Complement.complement b)) (Complement.complement (HXor.hXor a b))

theorem UInt8.shiftLeft_zero {a : UInt8} : Eq (HShiftLeft.hShiftLeft a 0) a

theorem UInt16.shiftLeft_zero {a : UInt16} : Eq (HShiftLeft.hShiftLeft a 0) a

theorem UInt32.shiftLeft_zero {a : UInt32} : Eq (HShiftLeft.hShiftLeft a 0) a

theorem UInt64.shiftLeft_zero {a : UInt64} : Eq (HShiftLeft.hShiftLeft a 0) a

theorem USize.shiftLeft_zero {a : USize} : Eq (HShiftLeft.hShiftLeft a 0) a

theorem UInt8.zero_shiftLeft {a : UInt8} : Eq (HShiftLeft.hShiftLeft 0 a) 0

theorem UInt16.zero_shiftLeft {a : UInt16} : Eq (HShiftLeft.hShiftLeft 0 a) 0

theorem UInt32.zero_shiftLeft {a : UInt32} : Eq (HShiftLeft.hShiftLeft 0 a) 0

theorem UInt64.zero_shiftLeft {a : UInt64} : Eq (HShiftLeft.hShiftLeft 0 a) 0

theorem USize.zero_shiftLeft {a : USize} : Eq (HShiftLeft.hShiftLeft 0 a) 0

theorem UInt8.shiftLeft_xor {a b c : UInt8} : Eq (HShiftLeft.hShiftLeft (HXor.hXor a b) c) (HXor.hXor (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt16.shiftLeft_xor {a b c : UInt16} : Eq (HShiftLeft.hShiftLeft (HXor.hXor a b) c) (HXor.hXor (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt32.shiftLeft_xor {a b c : UInt32} : Eq (HShiftLeft.hShiftLeft (HXor.hXor a b) c) (HXor.hXor (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt64.shiftLeft_xor {a b c : UInt64} : Eq (HShiftLeft.hShiftLeft (HXor.hXor a b) c) (HXor.hXor (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem USize.shiftLeft_xor {a b c : USize} : Eq (HShiftLeft.hShiftLeft (HXor.hXor a b) c) (HXor.hXor (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt8.shiftLeft_and {a b c : UInt8} : Eq (HShiftLeft.hShiftLeft (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt16.shiftLeft_and {a b c : UInt16} : Eq (HShiftLeft.hShiftLeft (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt32.shiftLeft_and {a b c : UInt32} : Eq (HShiftLeft.hShiftLeft (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt64.shiftLeft_and {a b c : UInt64} : Eq (HShiftLeft.hShiftLeft (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem USize.shiftLeft_and {a b c : USize} : Eq (HShiftLeft.hShiftLeft (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt8.shiftLeft_or {a b c : UInt8} : Eq (HShiftLeft.hShiftLeft (HOr.hOr a b) c) (HOr.hOr (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt16.shiftLeft_or {a b c : UInt16} : Eq (HShiftLeft.hShiftLeft (HOr.hOr a b) c) (HOr.hOr (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt32.shiftLeft_or {a b c : UInt32} : Eq (HShiftLeft.hShiftLeft (HOr.hOr a b) c) (HOr.hOr (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt64.shiftLeft_or {a b c : UInt64} : Eq (HShiftLeft.hShiftLeft (HOr.hOr a b) c) (HOr.hOr (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem USize.shiftLeft_or {a b c : USize} : Eq (HShiftLeft.hShiftLeft (HOr.hOr a b) c) (HOr.hOr (HShiftLeft.hShiftLeft a c) (HShiftLeft.hShiftLeft b c))

theorem UInt8.shiftLeft_add_of_toNat_lt {a b c : UInt8} (h : LT.lt (HAdd.hAdd b.toNat c.toNat) 8) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem UInt16.shiftLeft_add_of_toNat_lt {a b c : UInt16} (h : LT.lt (HAdd.hAdd b.toNat c.toNat) 16) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem UInt32.shiftLeft_add_of_toNat_lt {a b c : UInt32} (h : LT.lt (HAdd.hAdd b.toNat c.toNat) 32) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem UInt64.shiftLeft_add_of_toNat_lt {a b c : UInt64} (h : LT.lt (HAdd.hAdd b.toNat c.toNat) 64) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem USize.shiftLeft_add_of_toNat_lt {a b c : USize} (h : LT.lt (HAdd.hAdd b.toNat c.toNat) System.Platform.numBits) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem UInt8.shiftLeft_add {a b c : UInt8} (hb : LT.lt b 8) (hc : LT.lt c 8) (hbc : LT.lt (HAdd.hAdd b c) 8) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem UInt16.shiftLeft_add {a b c : UInt16} (hb : LT.lt b 16) (hc : LT.lt c 16) (hbc : LT.lt (HAdd.hAdd b c) 16) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem UInt32.shiftLeft_add {a b c : UInt32} (hb : LT.lt b 32) (hc : LT.lt c 32) (hbc : LT.lt (HAdd.hAdd b c) 32) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem UInt64.shiftLeft_add {a b c : UInt64} (hb : LT.lt b 64) (hc : LT.lt c 64) (hbc : LT.lt (HAdd.hAdd b c) 64) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem USize.shiftLeft_add {a b c : USize} (hb : LT.lt b (ofNat System.Platform.numBits)) (hc : LT.lt c (ofNat System.Platform.numBits)) (hbc : LT.lt (HAdd.hAdd b c) (ofNat System.Platform.numBits)) : Eq (HShiftLeft.hShiftLeft a (HAdd.hAdd b c)) (HShiftLeft.hShiftLeft (HShiftLeft.hShiftLeft a b) c)

theorem UInt8.neg_one_shiftLeft_and_shiftLeft {a b : UInt8} : Eq (HAnd.hAnd (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft a b)

theorem UInt16.neg_one_shiftLeft_and_shiftLeft {a b : UInt16} : Eq (HAnd.hAnd (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft a b)

theorem UInt32.neg_one_shiftLeft_and_shiftLeft {a b : UInt32} : Eq (HAnd.hAnd (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft a b)

theorem UInt64.neg_one_shiftLeft_and_shiftLeft {a b : UInt64} : Eq (HAnd.hAnd (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft a b)

theorem USize.neg_one_shiftLeft_and_shiftLeft {a b : USize} : Eq (HAnd.hAnd (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft a b)

theorem UInt8.neg_one_shiftLeft_or_shiftLeft {a b : UInt8} : Eq (HOr.hOr (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (-1) b)

theorem UInt16.neg_one_shiftLeft_or_shiftLeft {a b : UInt16} : Eq (HOr.hOr (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (-1) b)

theorem UInt32.neg_one_shiftLeft_or_shiftLeft {a b : UInt32} : Eq (HOr.hOr (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (-1) b)

theorem UInt64.neg_one_shiftLeft_or_shiftLeft {a b : UInt8} : Eq (HOr.hOr (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (-1) b)

theorem USize.neg_one_shiftLeft_or_shiftLeft {a b : USize} : Eq (HOr.hOr (HShiftLeft.hShiftLeft (-1) b) (HShiftLeft.hShiftLeft a b)) (HShiftLeft.hShiftLeft (-1) b)

theorem UInt8.shiftRight_zero {a : UInt8} : Eq (HShiftRight.hShiftRight a 0) a

theorem UInt16.shiftRight_zero {a : UInt16} : Eq (HShiftRight.hShiftRight a 0) a

theorem UInt32.shiftRight_zero {a : UInt32} : Eq (HShiftRight.hShiftRight a 0) a

theorem UInt64.shiftRight_zero {a : UInt64} : Eq (HShiftRight.hShiftRight a 0) a

theorem USize.shiftRight_zero {a : USize} : Eq (HShiftRight.hShiftRight a 0) a

theorem UInt8.zero_shiftRight {a : UInt8} : Eq (HShiftRight.hShiftRight 0 a) 0

theorem UInt16.zero_shiftRight {a : UInt16} : Eq (HShiftRight.hShiftRight 0 a) 0

theorem UInt32.zero_shiftRight {a : UInt32} : Eq (HShiftRight.hShiftRight 0 a) 0

theorem UInt64.zero_shiftRight {a : UInt64} : Eq (HShiftRight.hShiftRight 0 a) 0

theorem USize.zero_shiftRight {a : USize} : Eq (HShiftRight.hShiftRight 0 a) 0

theorem UInt8.shiftRight_xor {a b c : UInt8} : Eq (HShiftRight.hShiftRight (HXor.hXor a b) c) (HXor.hXor (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt16.shiftRight_xor {a b c : UInt16} : Eq (HShiftRight.hShiftRight (HXor.hXor a b) c) (HXor.hXor (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt32.shiftRight_xor {a b c : UInt32} : Eq (HShiftRight.hShiftRight (HXor.hXor a b) c) (HXor.hXor (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt64.shiftRight_xor {a b c : UInt64} : Eq (HShiftRight.hShiftRight (HXor.hXor a b) c) (HXor.hXor (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem USize.shiftRight_xor {a b c : USize} : Eq (HShiftRight.hShiftRight (HXor.hXor a b) c) (HXor.hXor (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt8.shiftRight_and {a b c : UInt8} : Eq (HShiftRight.hShiftRight (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt16.shiftRight_and {a b c : UInt16} : Eq (HShiftRight.hShiftRight (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt32.shiftRight_and {a b c : UInt32} : Eq (HShiftRight.hShiftRight (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt64.shiftRight_and {a b c : UInt64} : Eq (HShiftRight.hShiftRight (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem USize.shiftRight_and {a b c : USize} : Eq (HShiftRight.hShiftRight (HAnd.hAnd a b) c) (HAnd.hAnd (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt8.shiftRight_or {a b c : UInt8} : Eq (HShiftRight.hShiftRight (HOr.hOr a b) c) (HOr.hOr (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt16.shiftRight_or {a b c : UInt16} : Eq (HShiftRight.hShiftRight (HOr.hOr a b) c) (HOr.hOr (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt32.shiftRight_or {a b c : UInt32} : Eq (HShiftRight.hShiftRight (HOr.hOr a b) c) (HOr.hOr (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt64.shiftRight_or {a b c : UInt64} : Eq (HShiftRight.hShiftRight (HOr.hOr a b) c) (HOr.hOr (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem USize.shiftRight_or {a b c : USize} : Eq (HShiftRight.hShiftRight (HOr.hOr a b) c) (HOr.hOr (HShiftRight.hShiftRight a c) (HShiftRight.hShiftRight b c))

theorem UInt8.and_le_right {a b : UInt8} : LE.le (HAnd.hAnd a b) b

theorem UInt16.and_le_right {a b : UInt16} : LE.le (HAnd.hAnd a b) b

theorem UInt32.and_le_right {a b : UInt32} : LE.le (HAnd.hAnd a b) b

theorem UInt64.and_le_right {a b : UInt64} : LE.le (HAnd.hAnd a b) b

theorem USize.and_le_right {a b : USize} : LE.le (HAnd.hAnd a b) b

theorem UInt8.and_le_left {a b : UInt8} : LE.le (HAnd.hAnd a b) a

theorem UInt16.and_le_left {a b : UInt16} : LE.le (HAnd.hAnd a b) a

theorem UInt32.and_le_left {a b : UInt32} : LE.le (HAnd.hAnd a b) a

theorem UInt64.and_le_left {a b : UInt64} : LE.le (HAnd.hAnd a b) a

theorem USize.and_le_left {a b : USize} : LE.le (HAnd.hAnd a b) a

theorem UInt8.left_le_or {a b : UInt8} : LE.le a (HOr.hOr a b)

theorem UInt16.left_le_or {a b : UInt16} : LE.le a (HOr.hOr a b)

theorem UInt32.left_le_or {a b : UInt32} : LE.le a (HOr.hOr a b)

theorem UInt64.left_le_or {a b : UInt64} : LE.le a (HOr.hOr a b)

theorem USize.left_le_or {a b : USize} : LE.le a (HOr.hOr a b)

theorem UInt8.right_le_or {a b : UInt8} : LE.le b (HOr.hOr a b)

theorem UInt16.right_le_or {a b : UInt16} : LE.le b (HOr.hOr a b)

theorem UInt32.right_le_or {a b : UInt32} : LE.le b (HOr.hOr a b)

theorem UInt64.right_le_or {a b : UInt64} : LE.le b (HOr.hOr a b)

theorem USize.right_le_or {a b : USize} : LE.le b (HOr.hOr a b)