def commandDeclare_uint_theorems__ : Lean.ParserDescr

Equations

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

@[simp]

theorem UInt8.toFin_toBitVec (x : UInt8) : x.toBitVec.toFin = x.toFin

theorem UInt8.add_def (a b : UInt8) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

@[deprecated UInt8.toNat_toBitVec (since := "2025-02-21")]

theorem UInt8.toNat_toBitVec_eq_toNat (x : UInt8) : x.toBitVec.toNat = x.toNat

@[simp]

theorem UInt8.toNat_mul (a b : UInt8) : (a * b).toNat = a.toNat * b.toNat % 2 ^ 8

theorem UInt8.toBitVec_ne_of_ne {a b : UInt8} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

theorem UInt8.mod_lt (a : UInt8) {b : UInt8} : 0 < b → a % b < b

theorem UInt8.le_iff_toNat_le {a b : UInt8} : a ≤ b ↔ a.toNat ≤ b.toNat

@[deprecated UInt8.toFin_ofNat (since := "2025-02-12")]

theorem UInt8.val_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

theorem UInt8.toNat_mod_lt {m : Nat} (u : UInt8) : m > 0 → (u % ofNat m).toNat < m

@[simp]

theorem UInt8.not_le {a b : UInt8} : ¬a ≤ b ↔ b < a

@[simp]

theorem UInt8.toNat_ofBitVec {a : BitVec 8} : { toBitVec := a }.toNat = a.toNat

theorem UInt8.toBitVec_inj {a b : UInt8} : a.toBitVec = b.toBitVec ↔ a = b

theorem UInt8.le_antisymm {a b : UInt8} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

theorem UInt8.ne_of_toBitVec_ne {a b : UInt8} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

@[deprecated UInt8.toFin_inj (since := "2025-02-12")]

theorem UInt8.val_inj {a b : UInt8} : a.toFin = b.toFin ↔ a = b

@[simp]

theorem UInt8.ofNat_toNat {x : UInt8} : ofNat x.toNat = x

theorem UInt8.lt_iff_toNat_lt {a b : UInt8} : a < b ↔ a.toNat < b.toNat

theorem UInt8.one_def : 1 = { toBitVec := 1 }

@[simp]

theorem UInt8.toNat_toUInt64 (x : UInt8) : x.toUInt64.toNat = x.toNat

@[simp]

theorem UInt8.toNat_zero : toNat 0 = 0

theorem UInt8.lt_def {a b : UInt8} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt8.toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a

theorem UInt8.zero_def : 0 = { toBitVec := 0 }

theorem UInt8.le_antisymm_iff {a b : UInt8} : a = b ↔ a ≤ b ∧ b ≤ a

theorem UInt8.toNat.inj {a b : UInt8} : a.toNat = b.toNat → a = b

@[simp]

theorem UInt8.toNat_mod (a b : UInt8) : (a % b).toNat = a.toNat % b.toNat

theorem UInt8.ne_iff_toBitVec_ne {a b : UInt8} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

@[deprecated UInt8.ofBitVec_toBitVec (since := "2025-02-21")]

theorem UInt8.ofBitVec_toBitVec_eq (a : UInt8) : { toBitVec := a.toBitVec } = a

theorem UInt8.lt_trans {a b c : UInt8} : a < b → b < c → a < c

theorem UInt8.mod_def (a b : UInt8) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

@[simp]

theorem UInt8.le_refl (a : UInt8) : a ≤ a

theorem UInt8.toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n

theorem UInt8.eq_of_toBitVec_eq {a b : UInt8} (h : a.toBitVec = b.toBitVec) : a = b

theorem UInt8.mul_def (a b : UInt8) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

@[simp]

theorem UInt8.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 8 n } = OfNat.ofNat n

@[deprecated UInt8.ofBitVec_ofNat (since := "2025-02-12")]

theorem UInt8.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 8 n } = OfNat.ofNat n

@[simp]

theorem UInt8.toNat_sub_of_le (a b : UInt8) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

theorem UInt8.le_total (a b : UInt8) : a ≤ b ∨ b ≤ a

theorem UInt8.lt_asymm {a b : UInt8} : a < b → ¬b < a

@[simp]

theorem UInt8.toNat_add (a b : UInt8) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 8

@[deprecated UInt8.toNat_ofNatLT (since := "2025-02-13")]

theorem UInt8.toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[deprecated UInt8.ofBitVec_toBitVec_eq (since := "2025-02-12")]

theorem UInt8.mk_toBitVec_eq (a : UInt8) : { toBitVec := a.toBitVec } = a

@[deprecated UInt8.toNat_mod_lt (since := "2024-09-24")]

theorem UInt8.modn_lt {m : Nat} (u : UInt8) : m > 0 → (u % m).toNat < m

@[simp]

theorem UInt8.toNat_div (a b : UInt8) : (a / b).toNat = a.toNat / b.toNat

@[deprecated UInt8.toNat_ofBitVec (since := "2025-02-12")]

theorem UInt8.toNat_mk {a : BitVec 8} : { toBitVec := a }.toNat = a.toNat

@[deprecated UInt8.eq_of_toFin_eq (since := "2025-02-12")]

theorem UInt8.eq_of_val_eq {a b : UInt8} (h : a.toFin = b.toFin) : a = b

@[simp]

theorem UInt8.toNat_toUInt32 (x : UInt8) : x.toUInt32.toNat = x.toNat

@[simp]

theorem UInt8.lt_irrefl (a : UInt8) : ¬a < a

theorem UInt8.sub_def (a b : UInt8) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

theorem UInt8.ne_of_lt {a b : UInt8} (h : a < b) : a ≠ b

theorem UInt8.toFin_inj {a b : UInt8} : a.toFin = b.toFin ↔ a = b

theorem UInt8.le_trans {a b c : UInt8} : a ≤ b → b ≤ c → a ≤ c

theorem UInt8.le_def {a b : UInt8} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem UInt8.eq_of_toFin_eq {a b : UInt8} (h : a.toFin = b.toFin) : a = b

@[simp]

theorem UInt8.toNat_toBitVec (x : UInt8) : x.toBitVec.toNat = x.toNat

@[simp]

theorem UInt8.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 8 n

@[simp]

theorem UInt8.ofNat_one : ofNat 1 = 1

theorem UInt8.toNat_sub (a b : UInt8) : (a - b).toNat = (2 ^ 8 - b.toNat + a.toNat) % 2 ^ 8

@[simp]

theorem UInt8.toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ 8

@[simp]

theorem UInt8.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem UInt8.toFin_val (x : UInt8) : ↑x.toFin = x.toNat

theorem UInt8.eq_iff_toBitVec_eq {a b : UInt8} : a = b ↔ a.toBitVec = b.toBitVec

@[simp]

theorem UInt8.toNat_toUSize (x : UInt8) : x.toUSize.toNat = x.toNat

theorem UInt8.toBitVec_eq_of_eq {a b : UInt8} (h : a = b) : a.toBitVec = b.toBitVec

theorem UInt8.toNat_lt_size (a : UInt8) : a.toNat < size

theorem UInt8.toNat_inj {a b : UInt8} : a.toNat = b.toNat ↔ a = b

@[simp]

theorem UInt8.not_lt {a b : UInt8} : ¬a < b ↔ b ≤ a

@[simp]

theorem UInt8.toNat_toUInt16 (x : UInt8) : x.toUInt16.toNat = x.toNat

@[deprecated UInt8.toFin_val (since := "2025-02-12")]

theorem UInt8.val_val_eq_toNat (x : UInt8) : ↑x.toFin = x.toNat

@[simp]

theorem UInt8.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[simp]

theorem UInt8.ofBitVec_toBitVec (a : UInt8) : { toBitVec := a.toBitVec } = a

@[deprecated UInt16.toFin_inj (since := "2025-02-12")]

theorem UInt16.val_inj {a b : UInt16} : a.toFin = b.toFin ↔ a = b

@[simp]

theorem UInt16.toNat_toUInt8 (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8

theorem UInt16.le_antisymm {a b : UInt16} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

theorem UInt16.lt_trans {a b c : UInt16} : a < b → b < c → a < c

@[simp]

theorem UInt16.toNat_mod (a b : UInt16) : (a % b).toNat = a.toNat % b.toNat

theorem UInt16.lt_def {a b : UInt16} : a < b ↔ a.toBitVec < b.toBitVec

@[deprecated UInt16.toFin_ofNat (since := "2025-02-12")]

theorem UInt16.val_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem UInt16.toNat_toUInt32 (x : UInt16) : x.toUInt32.toNat = x.toNat

theorem UInt16.ne_iff_toBitVec_ne {a b : UInt16} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem UInt16.toNat_sub (a b : UInt16) : (a - b).toNat = (2 ^ 16 - b.toNat + a.toNat) % 2 ^ 16

@[simp]

theorem UInt16.lt_irrefl (a : UInt16) : ¬a < a

theorem UInt16.le_antisymm_iff {a b : UInt16} : a = b ↔ a ≤ b ∧ b ≤ a

@[simp]

theorem UInt16.toNat_mul (a b : UInt16) : (a * b).toNat = a.toNat * b.toNat % 2 ^ 16

theorem UInt16.sub_def (a b : UInt16) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

@[simp]

theorem UInt16.toNat_add (a b : UInt16) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 16

@[simp]

theorem UInt16.toFin_val (x : UInt16) : ↑x.toFin = x.toNat

@[deprecated UInt16.ofBitVec_toBitVec_eq (since := "2025-02-12")]

theorem UInt16.mk_toBitVec_eq (a : UInt16) : { toBitVec := a.toBitVec } = a

theorem UInt16.le_iff_toNat_le {a b : UInt16} : a ≤ b ↔ a.toNat ≤ b.toNat

@[simp]

theorem UInt16.toNat_ofBitVec {a : BitVec 16} : { toBitVec := a }.toNat = a.toNat

theorem UInt16.le_trans {a b c : UInt16} : a ≤ b → b ≤ c → a ≤ c

theorem UInt16.toBitVec_eq_of_eq {a b : UInt16} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem UInt16.le_refl (a : UInt16) : a ≤ a

theorem UInt16.toNat_lt_size (a : UInt16) : a.toNat < size

@[deprecated UInt16.toNat_ofBitVec (since := "2025-02-12")]

theorem UInt16.toNat_mk {a : BitVec 16} : { toBitVec := a }.toNat = a.toNat

theorem UInt16.eq_iff_toBitVec_eq {a b : UInt16} : a = b ↔ a.toBitVec = b.toBitVec

@[simp]

theorem UInt16.not_lt {a b : UInt16} : ¬a < b ↔ b ≤ a

@[simp]

theorem UInt16.toNat_toUSize (x : UInt16) : x.toUSize.toNat = x.toNat

theorem UInt16.toBitVec_inj {a b : UInt16} : a.toBitVec = b.toBitVec ↔ a = b

theorem UInt16.le_def {a b : UInt16} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem UInt16.lt_iff_toNat_lt {a b : UInt16} : a < b ↔ a.toNat < b.toNat

theorem UInt16.toNat_inj {a b : UInt16} : a.toNat = b.toNat ↔ a = b

theorem UInt16.le_total (a b : UInt16) : a ≤ b ∨ b ≤ a

@[simp]

theorem UInt16.toNat_toUInt64 (x : UInt16) : x.toUInt64.toNat = x.toNat

@[deprecated UInt16.toNat_toBitVec (since := "2025-02-21")]

theorem UInt16.toNat_toBitVec_eq_toNat (x : UInt16) : x.toBitVec.toNat = x.toNat

@[simp]

theorem UInt16.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem UInt16.toNat_zero : toNat 0 = 0

@[simp]

theorem UInt16.toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ 16

@[deprecated UInt16.ofBitVec_toBitVec (since := "2025-02-21")]

theorem UInt16.ofBitVec_toBitVec_eq (a : UInt16) : { toBitVec := a.toBitVec } = a

@[deprecated UInt16.eq_of_toFin_eq (since := "2025-02-12")]

theorem UInt16.eq_of_val_eq {a b : UInt16} (h : a.toFin = b.toFin) : a = b

theorem UInt16.lt_asymm {a b : UInt16} : a < b → ¬b < a

theorem UInt16.toNat_mod_lt {m : Nat} (u : UInt16) : m > 0 → (u % ofNat m).toNat < m

@[simp]

theorem UInt16.toNat_div (a b : UInt16) : (a / b).toNat = a.toNat / b.toNat

theorem UInt16.mul_def (a b : UInt16) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

@[simp]

theorem UInt16.ofNat_toNat {x : UInt16} : ofNat x.toNat = x

@[deprecated UInt16.toNat_mod_lt (since := "2024-09-24")]

theorem UInt16.modn_lt {m : Nat} (u : UInt16) : m > 0 → (u % m).toNat < m

theorem UInt16.ne_of_lt {a b : UInt16} (h : a < b) : a ≠ b

@[simp]

theorem UInt16.ofNat_one : ofNat 1 = 1

@[deprecated UInt16.ofBitVec_ofNat (since := "2025-02-12")]

theorem UInt16.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 16 n } = OfNat.ofNat n

theorem UInt16.one_def : 1 = { toBitVec := 1 }

theorem UInt16.mod_lt (a : UInt16) {b : UInt16} : 0 < b → a % b < b

@[deprecated UInt16.toNat_ofNatLT (since := "2025-02-13")]

theorem UInt16.toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

theorem UInt16.toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a

theorem UInt16.eq_of_toFin_eq {a b : UInt16} (h : a.toFin = b.toFin) : a = b

theorem UInt16.toNat.inj {a b : UInt16} : a.toNat = b.toNat → a = b

theorem UInt16.toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n

theorem UInt16.eq_of_toBitVec_eq {a b : UInt16} (h : a.toBitVec = b.toBitVec) : a = b

@[deprecated UInt16.toFin_val (since := "2025-02-12")]

theorem UInt16.val_val_eq_toNat (x : UInt16) : ↑x.toFin = x.toNat

@[simp]

theorem UInt16.toNat_toBitVec (x : UInt16) : x.toBitVec.toNat = x.toNat

@[simp]

theorem UInt16.toNat_sub_of_le (a b : UInt16) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

@[simp]

theorem UInt16.toFin_toBitVec (x : UInt16) : x.toBitVec.toFin = x.toFin

theorem UInt16.toFin_inj {a b : UInt16} : a.toFin = b.toFin ↔ a = b

theorem UInt16.add_def (a b : UInt16) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem UInt16.toBitVec_ne_of_ne {a b : UInt16} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

@[simp]

theorem UInt16.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[simp]

theorem UInt16.not_le {a b : UInt16} : ¬a ≤ b ↔ b < a

@[simp]

theorem UInt16.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 16 n } = OfNat.ofNat n

@[simp]

theorem UInt16.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 16 n

theorem UInt16.ne_of_toBitVec_ne {a b : UInt16} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

theorem UInt16.zero_def : 0 = { toBitVec := 0 }

theorem UInt16.mod_def (a b : UInt16) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

@[simp]

theorem UInt16.ofBitVec_toBitVec (a : UInt16) : { toBitVec := a.toBitVec } = a

theorem UInt32.ne_of_toBitVec_ne {a b : UInt32} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

theorem UInt32.sub_def (a b : UInt32) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

@[deprecated UInt32.toFin_val (since := "2025-02-12")]

theorem UInt32.val_val_eq_toNat (x : UInt32) : ↑x.toFin = x.toNat

theorem UInt32.le_antisymm {a b : UInt32} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

@[simp]

theorem UInt32.not_le {a b : UInt32} : ¬a ≤ b ↔ b < a

@[deprecated UInt32.ofBitVec_toBitVec_eq (since := "2025-02-12")]

theorem UInt32.mk_toBitVec_eq (a : UInt32) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt32.le_refl (a : UInt32) : a ≤ a

@[deprecated UInt32.toNat_ofBitVec (since := "2025-02-12")]

theorem UInt32.toNat_mk {a : BitVec 32} : { toBitVec := a }.toNat = a.toNat

@[simp]

theorem UInt32.toNat_toBitVec (x : UInt32) : x.toBitVec.toNat = x.toNat

@[simp]

theorem UInt32.ofNat_toNat {x : UInt32} : ofNat x.toNat = x

theorem UInt32.toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a

theorem UInt32.le_def {a b : UInt32} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem UInt32.lt_def {a b : UInt32} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt32.lt_asymm {a b : UInt32} : a < b → ¬b < a

@[simp]

theorem UInt32.toFin_toBitVec (x : UInt32) : x.toBitVec.toFin = x.toFin

@[deprecated UInt32.toNat_mod_lt (since := "2024-09-24")]

theorem UInt32.modn_lt {m : Nat} (u : UInt32) : m > 0 → (u % m).toNat < m

theorem UInt32.toNat_inj {a b : UInt32} : a.toNat = b.toNat ↔ a = b

@[simp]

theorem UInt32.toNat_mul (a b : UInt32) : (a * b).toNat = a.toNat * b.toNat % 2 ^ 32

theorem UInt32.lt_iff_toNat_lt {a b : UInt32} : a < b ↔ a.toNat < b.toNat

theorem UInt32.toNat_mod_lt {m : Nat} (u : UInt32) : m > 0 → (u % ofNat m).toNat < m

theorem UInt32.toBitVec_ne_of_ne {a b : UInt32} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

theorem UInt32.le_antisymm_iff {a b : UInt32} : a = b ↔ a ≤ b ∧ b ≤ a

@[simp]

theorem UInt32.toNat_add (a b : UInt32) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 32

@[simp]

theorem UInt32.not_lt {a b : UInt32} : ¬a < b ↔ b ≤ a

@[deprecated UInt32.ofBitVec_ofNat (since := "2025-02-12")]

theorem UInt32.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 32 n } = OfNat.ofNat n

theorem UInt32.toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n

@[simp]

theorem UInt32.toNat_zero : toNat 0 = 0

theorem UInt32.le_trans {a b c : UInt32} : a ≤ b → b ≤ c → a ≤ c

theorem UInt32.ne_iff_toBitVec_ne {a b : UInt32} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem UInt32.eq_iff_toBitVec_eq {a b : UInt32} : a = b ↔ a.toBitVec = b.toBitVec

theorem UInt32.toFin_inj {a b : UInt32} : a.toFin = b.toFin ↔ a = b

@[simp]

theorem UInt32.toNat_toUSize (x : UInt32) : x.toUSize.toNat = x.toNat

theorem UInt32.ne_of_lt {a b : UInt32} (h : a < b) : a ≠ b

theorem UInt32.toBitVec_inj {a b : UInt32} : a.toBitVec = b.toBitVec ↔ a = b

@[simp]

theorem UInt32.toNat_div (a b : UInt32) : (a / b).toNat = a.toNat / b.toNat

theorem UInt32.lt_trans {a b c : UInt32} : a < b → b < c → a < c

@[deprecated UInt32.toNat_toBitVec (since := "2025-02-21")]

theorem UInt32.toNat_toBitVec_eq_toNat (x : UInt32) : x.toBitVec.toNat = x.toNat

@[simp]

theorem UInt32.toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ 32

@[simp]

theorem UInt32.toNat_toUInt8 (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8

@[simp]

theorem UInt32.ofNat_one : ofNat 1 = 1

theorem UInt32.eq_of_toBitVec_eq {a b : UInt32} (h : a.toBitVec = b.toBitVec) : a = b

theorem UInt32.one_def : 1 = { toBitVec := 1 }

@[simp]

theorem UInt32.toFin_val (x : UInt32) : ↑x.toFin = x.toNat

@[deprecated UInt32.eq_of_toFin_eq (since := "2025-02-12")]

theorem UInt32.eq_of_val_eq {a b : UInt32} (h : a.toFin = b.toFin) : a = b

theorem UInt32.toBitVec_eq_of_eq {a b : UInt32} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem UInt32.toNat_toUInt16 (x : UInt32) : x.toUInt16.toNat = x.toNat % 2 ^ 16

@[simp]

theorem UInt32.lt_irrefl (a : UInt32) : ¬a < a

theorem UInt32.mod_lt (a : UInt32) {b : UInt32} : 0 < b → a % b < b

@[simp]

theorem UInt32.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 32 n

theorem UInt32.add_def (a b : UInt32) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

@[deprecated UInt32.toNat_ofNatLT (since := "2025-02-13")]

theorem UInt32.toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[simp]

theorem UInt32.toNat_mod (a b : UInt32) : (a % b).toNat = a.toNat % b.toNat

@[simp]

theorem UInt32.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 32 n } = OfNat.ofNat n

theorem UInt32.zero_def : 0 = { toBitVec := 0 }

@[simp]

theorem UInt32.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

theorem UInt32.mul_def (a b : UInt32) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

@[simp]

theorem UInt32.toNat_ofBitVec {a : BitVec 32} : { toBitVec := a }.toNat = a.toNat

theorem UInt32.toNat_lt_size (a : UInt32) : a.toNat < size

@[simp]

theorem UInt32.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

theorem UInt32.le_iff_toNat_le {a b : UInt32} : a ≤ b ↔ a.toNat ≤ b.toNat

theorem UInt32.eq_of_toFin_eq {a b : UInt32} (h : a.toFin = b.toFin) : a = b

theorem UInt32.toNat_sub (a b : UInt32) : (a - b).toNat = (2 ^ 32 - b.toNat + a.toNat) % 2 ^ 32

theorem UInt32.mod_def (a b : UInt32) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

@[deprecated UInt32.ofBitVec_toBitVec (since := "2025-02-21")]

theorem UInt32.ofBitVec_toBitVec_eq (a : UInt32) : { toBitVec := a.toBitVec } = a

@[deprecated UInt32.toFin_inj (since := "2025-02-12")]

theorem UInt32.val_inj {a b : UInt32} : a.toFin = b.toFin ↔ a = b

theorem UInt32.le_total (a b : UInt32) : a ≤ b ∨ b ≤ a

theorem UInt32.toNat.inj {a b : UInt32} : a.toNat = b.toNat → a = b

@[simp]

theorem UInt32.toNat_toUInt64 (x : UInt32) : x.toUInt64.toNat = x.toNat

@[simp]

theorem UInt32.ofBitVec_toBitVec (a : UInt32) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt32.toNat_sub_of_le (a b : UInt32) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

@[deprecated UInt32.toFin_ofNat (since := "2025-02-12")]

theorem UInt32.val_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem UInt64.toNat_sub_of_le (a b : UInt64) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

@[deprecated UInt64.toNat_ofBitVec (since := "2025-02-12")]

theorem UInt64.toNat_mk {a : BitVec 64} : { toBitVec := a }.toNat = a.toNat

@[simp]

theorem UInt64.toNat_toUSize (x : UInt64) : x.toUSize.toNat = x.toNat % 2 ^ System.Platform.numBits

theorem UInt64.toBitVec_ne_of_ne {a b : UInt64} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

@[simp]

theorem UInt64.toNat_zero : toNat 0 = 0

@[simp]

theorem UInt64.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 64 n

@[deprecated UInt64.toNat_ofNatLT (since := "2025-02-13")]

theorem UInt64.toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[simp]

theorem UInt64.lt_irrefl (a : UInt64) : ¬a < a

theorem UInt64.eq_of_toBitVec_eq {a b : UInt64} (h : a.toBitVec = b.toBitVec) : a = b

@[deprecated UInt64.toFin_val (since := "2025-02-12")]

theorem UInt64.val_val_eq_toNat (x : UInt64) : ↑x.toFin = x.toNat

theorem UInt64.le_iff_toNat_le {a b : UInt64} : a ≤ b ↔ a.toNat ≤ b.toNat

@[simp]

theorem UInt64.toNat_toUInt32 (x : UInt64) : x.toUInt32.toNat = x.toNat % 2 ^ 32

@[deprecated UInt64.ofBitVec_ofNat (since := "2025-02-12")]

theorem UInt64.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 64 n } = OfNat.ofNat n

theorem UInt64.toBitVec_eq_of_eq {a b : UInt64} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem UInt64.not_lt {a b : UInt64} : ¬a < b ↔ b ≤ a

theorem UInt64.le_total (a b : UInt64) : a ≤ b ∨ b ≤ a

theorem UInt64.ne_of_lt {a b : UInt64} (h : a < b) : a ≠ b

@[simp]

theorem UInt64.toNat_ofBitVec {a : BitVec 64} : { toBitVec := a }.toNat = a.toNat

theorem UInt64.le_antisymm {a b : UInt64} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

@[deprecated UInt64.ofBitVec_toBitVec (since := "2025-02-21")]

theorem UInt64.ofBitVec_toBitVec_eq (a : UInt64) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt64.le_refl (a : UInt64) : a ≤ a

theorem UInt64.le_antisymm_iff {a b : UInt64} : a = b ↔ a ≤ b ∧ b ≤ a

theorem UInt64.toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a

theorem UInt64.mod_lt (a : UInt64) {b : UInt64} : 0 < b → a % b < b

theorem UInt64.toNat_inj {a b : UInt64} : a.toNat = b.toNat ↔ a = b

@[simp]

theorem UInt64.toNat_div (a b : UInt64) : (a / b).toNat = a.toNat / b.toNat

@[simp]

theorem UInt64.toFin_toBitVec (x : UInt64) : x.toBitVec.toFin = x.toFin

theorem UInt64.toNat_lt_size (a : UInt64) : a.toNat < size

@[deprecated UInt64.eq_of_toFin_eq (since := "2025-02-12")]

theorem UInt64.eq_of_val_eq {a b : UInt64} (h : a.toFin = b.toFin) : a = b

@[simp]

theorem UInt64.toNat_mul (a b : UInt64) : (a * b).toNat = a.toNat * b.toNat % 2 ^ 64

@[simp]

theorem UInt64.ofBitVec_toBitVec (a : UInt64) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt64.toNat_toBitVec (x : UInt64) : x.toBitVec.toNat = x.toNat

@[deprecated UInt64.toFin_ofNat (since := "2025-02-12")]

theorem UInt64.val_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem UInt64.toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ 64

theorem UInt64.toNat.inj {a b : UInt64} : a.toNat = b.toNat → a = b

theorem UInt64.add_def (a b : UInt64) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem UInt64.toFin_inj {a b : UInt64} : a.toFin = b.toFin ↔ a = b

theorem UInt64.toNat_sub (a b : UInt64) : (a - b).toNat = (2 ^ 64 - b.toNat + a.toNat) % 2 ^ 64

theorem UInt64.one_def : 1 = { toBitVec := 1 }

theorem UInt64.lt_trans {a b c : UInt64} : a < b → b < c → a < c

@[deprecated UInt64.toNat_toBitVec (since := "2025-02-21")]

theorem UInt64.toNat_toBitVec_eq_toNat (x : UInt64) : x.toBitVec.toNat = x.toNat

@[simp]

theorem UInt64.toNat_toUInt8 (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8

theorem UInt64.lt_def {a b : UInt64} : a < b ↔ a.toBitVec < b.toBitVec

@[deprecated UInt64.ofBitVec_toBitVec_eq (since := "2025-02-12")]

theorem UInt64.mk_toBitVec_eq (a : UInt64) : { toBitVec := a.toBitVec } = a

theorem UInt64.toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n

@[simp]

theorem UInt64.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 64 n } = OfNat.ofNat n

theorem UInt64.lt_iff_toNat_lt {a b : UInt64} : a < b ↔ a.toNat < b.toNat

theorem UInt64.eq_of_toFin_eq {a b : UInt64} (h : a.toFin = b.toFin) : a = b

theorem UInt64.toBitVec_inj {a b : UInt64} : a.toBitVec = b.toBitVec ↔ a = b

@[deprecated UInt64.toFin_inj (since := "2025-02-12")]

theorem UInt64.val_inj {a b : UInt64} : a.toFin = b.toFin ↔ a = b

@[simp]

theorem UInt64.toNat_mod (a b : UInt64) : (a % b).toNat = a.toNat % b.toNat

@[simp]

theorem UInt64.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

theorem UInt64.lt_asymm {a b : UInt64} : a < b → ¬b < a

theorem UInt64.toNat_mod_lt {m : Nat} (u : UInt64) : m > 0 → (u % ofNat m).toNat < m

@[simp]

theorem UInt64.toNat_add (a b : UInt64) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 64

theorem UInt64.ne_iff_toBitVec_ne {a b : UInt64} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem UInt64.le_trans {a b c : UInt64} : a ≤ b → b ≤ c → a ≤ c

theorem UInt64.mul_def (a b : UInt64) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

theorem UInt64.zero_def : 0 = { toBitVec := 0 }

theorem UInt64.le_def {a b : UInt64} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

@[deprecated UInt64.toNat_mod_lt (since := "2024-09-24")]

theorem UInt64.modn_lt {m : Nat} (u : UInt64) : m > 0 → (u % m).toNat < m

@[simp]

theorem UInt64.ofNat_toNat {x : UInt64} : ofNat x.toNat = x

theorem UInt64.mod_def (a b : UInt64) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

@[simp]

theorem UInt64.not_le {a b : UInt64} : ¬a ≤ b ↔ b < a

@[simp]

theorem UInt64.ofNat_one : ofNat 1 = 1

theorem UInt64.eq_iff_toBitVec_eq {a b : UInt64} : a = b ↔ a.toBitVec = b.toBitVec

theorem UInt64.sub_def (a b : UInt64) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

theorem UInt64.ne_of_toBitVec_ne {a b : UInt64} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

@[simp]

theorem UInt64.toFin_val (x : UInt64) : ↑x.toFin = x.toNat

@[simp]

theorem UInt64.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[simp]

theorem UInt64.toNat_toUInt16 (x : UInt64) : x.toUInt16.toNat = x.toNat % 2 ^ 16

@[deprecated USize.toNat_ofNatLT (since := "2025-02-13")]

theorem USize.toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

theorem USize.le_def {a b : USize} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem USize.lt_def {a b : USize} : a < b ↔ a.toBitVec < b.toBitVec

@[simp]

theorem USize.toNat_mod (a b : USize) : (a % b).toNat = a.toNat % b.toNat

@[simp]

theorem USize.toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ System.Platform.numBits

@[simp]

theorem USize.toNat_zero : toNat 0 = 0

theorem USize.toBitVec_eq_of_eq {a b : USize} (h : a = b) : a.toBitVec = b.toBitVec

theorem USize.one_def : 1 = { toBitVec := 1 }

@[simp]

theorem USize.ofBitVec_toBitVec (a : USize) : { toBitVec := a.toBitVec } = a

theorem USize.zero_def : 0 = { toBitVec := 0 }

theorem USize.ne_iff_toBitVec_ne {a b : USize} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem USize.toNat_mod_lt {m : Nat} (u : USize) : m > 0 → (u % ofNat m).toNat < m

@[deprecated USize.toNat_ofBitVec (since := "2025-02-12")]

theorem USize.toNat_mk {a : BitVec System.Platform.numBits} : { toBitVec := a }.toNat = a.toNat

@[deprecated USize.ofBitVec_ofNat (since := "2025-02-12")]

theorem USize.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat System.Platform.numBits n } = OfNat.ofNat n

@[simp]

theorem USize.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n

theorem USize.sub_def (a b : USize) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

@[simp]

theorem USize.toNat_mul (a b : USize) : (a * b).toNat = a.toNat * b.toNat % 2 ^ System.Platform.numBits

theorem USize.toNat_sub (a b : USize) : (a - b).toNat = (2 ^ System.Platform.numBits - b.toNat + a.toNat) % 2 ^ System.Platform.numBits

@[simp]

theorem USize.ofNat_one : ofNat 1 = 1

theorem USize.toBitVec_ne_of_ne {a b : USize} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

@[simp]

theorem USize.toNat_toBitVec (x : USize) : x.toBitVec.toNat = x.toNat

@[deprecated USize.toNat_mod_lt (since := "2024-09-24")]

theorem USize.modn_lt {m : Nat} (u : USize) : m > 0 → (u % m).toNat < m

@[deprecated USize.ofBitVec_toBitVec_eq (since := "2025-02-12")]

theorem USize.mk_toBitVec_eq (a : USize) : { toBitVec := a.toBitVec } = a

theorem USize.ne_of_toBitVec_ne {a b : USize} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

theorem USize.eq_iff_toBitVec_eq {a b : USize} : a = b ↔ a.toBitVec = b.toBitVec

@[simp]

theorem USize.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

theorem USize.mul_def (a b : USize) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

theorem USize.lt_asymm {a b : USize} : a < b → ¬b < a

theorem USize.toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a

theorem USize.lt_trans {a b c : USize} : a < b → b < c → a < c

@[deprecated USize.ofBitVec_toBitVec (since := "2025-02-21")]

theorem USize.ofBitVec_toBitVec_eq (a : USize) : { toBitVec := a.toBitVec } = a

@[simp]

theorem USize.toFin_val (x : USize) : ↑x.toFin = x.toNat

@[simp]

theorem USize.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[deprecated USize.toFin_inj (since := "2025-02-12")]

theorem USize.val_inj {a b : USize} : a.toFin = b.toFin ↔ a = b

@[simp]

theorem USize.toNat_add (a b : USize) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ System.Platform.numBits

theorem USize.add_def (a b : USize) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem USize.eq_of_toBitVec_eq {a b : USize} (h : a.toBitVec = b.toBitVec) : a = b

theorem USize.ne_of_lt {a b : USize} (h : a < b) : a ≠ b

@[deprecated USize.toFin_ofNat (since := "2025-02-12")]

theorem USize.val_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

theorem USize.le_trans {a b c : USize} : a ≤ b → b ≤ c → a ≤ c

@[simp]

theorem USize.le_refl (a : USize) : a ≤ a

@[simp]

theorem USize.toNat_div (a b : USize) : (a / b).toNat = a.toNat / b.toNat

theorem USize.le_total (a b : USize) : a ≤ b ∨ b ≤ a

@[simp]

theorem USize.lt_irrefl (a : USize) : ¬a < a

theorem USize.mod_def (a b : USize) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

theorem USize.le_iff_toNat_le {a b : USize} : a ≤ b ↔ a.toNat ≤ b.toNat

@[simp]

theorem USize.not_le {a b : USize} : ¬a ≤ b ↔ b < a

theorem USize.le_antisymm {a b : USize} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

theorem USize.toNat.inj {a b : USize} : a.toNat = b.toNat → a = b

@[simp]

theorem USize.toNat_sub_of_le (a b : USize) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

@[deprecated USize.eq_of_toFin_eq (since := "2025-02-12")]

theorem USize.eq_of_val_eq {a b : USize} (h : a.toFin = b.toFin) : a = b

@[simp]

theorem USize.not_lt {a b : USize} : ¬a < b ↔ b ≤ a

theorem USize.toFin_inj {a b : USize} : a.toFin = b.toFin ↔ a = b

@[simp]

theorem USize.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat System.Platform.numBits n } = OfNat.ofNat n

theorem USize.le_antisymm_iff {a b : USize} : a = b ↔ a ≤ b ∧ b ≤ a

@[simp]

theorem USize.toNat_ofBitVec {a : BitVec System.Platform.numBits} : { toBitVec := a }.toNat = a.toNat

theorem USize.toNat_inj {a b : USize} : a.toNat = b.toNat ↔ a = b

theorem USize.toNat_lt_size (a : USize) : a.toNat < size

theorem USize.mod_lt (a : USize) {b : USize} : 0 < b → a % b < b

@[deprecated USize.toNat_toBitVec (since := "2025-02-21")]

theorem USize.toNat_toBitVec_eq_toNat (x : USize) : x.toBitVec.toNat = x.toNat

@[simp]

theorem USize.ofNat_toNat {x : USize} : ofNat x.toNat = x

theorem USize.toBitVec_inj {a b : USize} : a.toBitVec = b.toBitVec ↔ a = b

theorem USize.lt_iff_toNat_lt {a b : USize} : a < b ↔ a.toNat < b.toNat

theorem USize.eq_of_toFin_eq {a b : USize} (h : a.toFin = b.toFin) : a = b

theorem USize.toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n

@[simp]

theorem USize.toFin_toBitVec (x : USize) : x.toBitVec.toFin = x.toFin

@[deprecated USize.toFin_val (since := "2025-02-12")]

theorem USize.val_val_eq_toNat (x : USize) : ↑x.toFin = x.toNat

@[simp]

theorem USize.toNat_ofNat32 {n : Nat} {h : n < 4294967296} : (ofNat32 n h).toNat = n

@[simp]

theorem USize.toNat_toUInt8 (x : USize) : x.toUInt8.toNat = x.toNat % 2 ^ 8

@[simp]

theorem USize.toNat_toUInt16 (x : USize) : x.toUInt16.toNat = x.toNat % 2 ^ 16

@[simp]

theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32

@[simp]

theorem USize.toNat_toUInt64 (x : USize) : x.toUInt64.toNat = x.toNat

theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : (ofNat n).toNat = n

theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m

theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat

theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m

theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat

@[simp]

theorem UInt8.toNat_lt (n : UInt8) : n.toNat < 2 ^ 8

@[simp]

theorem UInt16.toNat_lt (n : UInt16) : n.toNat < 2 ^ 16

@[simp]

theorem UInt32.toNat_lt (n : UInt32) : n.toNat < 2 ^ 32

@[simp]

theorem UInt64.toNat_lt (n : UInt64) : n.toNat < 2 ^ 64

theorem UInt8.size_lt_usizeSize : size < USize.size

theorem UInt8.size_le_usizeSize : size ≤ USize.size

theorem UInt16.size_lt_usizeSize : size < USize.size

theorem UInt16.size_le_usizeSize : size ≤ USize.size

theorem UInt32.size_le_usizeSize : size ≤ USize.size

theorem USize.size_eq_two_pow : size = 2 ^ System.Platform.numBits

theorem USize.toNat_lt_two_pow_numBits (n : USize) : n.toNat < 2 ^ System.Platform.numBits

@[simp]

theorem USize.toNat_lt (n : USize) : n.toNat < 2 ^ 64

theorem USize.size_le_uint64Size : size ≤ UInt64.size

theorem UInt8.toNat_lt_usizeSize (n : UInt8) : n.toNat < USize.size

theorem UInt16.toNat_lt_usizeSize (n : UInt16) : n.toNat < USize.size

theorem UInt32.toNat_lt_usizeSize (n : UInt32) : n.toNat < USize.size

theorem UInt8.size_dvd_usizeSize : size ∣ USize.size

theorem UInt16.size_dvd_usizeSize : size ∣ USize.size

theorem UInt32.size_dvd_usizeSize : size ∣ USize.size

theorem USize.size_dvd_uInt64Size : size ∣ UInt64.size

@[simp]

theorem mod_usizeSize_uInt8Size (n : Nat) : n % USize.size % UInt8.size = n % UInt8.size

@[simp]

theorem mod_usizeSize_uInt16Size (n : Nat) : n % USize.size % UInt16.size = n % UInt16.size

@[simp]

theorem mod_usizeSize_uInt32Size (n : Nat) : n % USize.size % UInt32.size = n % UInt32.size

@[simp]

theorem mod_uInt64Size_uSizeSize (n : Nat) : n % UInt64.size % USize.size = n % USize.size

@[simp]

theorem UInt8.toNat_mod_size (n : UInt8) : n.toNat % size = n.toNat

@[simp]

theorem UInt8.toNat_mod_uInt16Size (n : UInt8) : n.toNat % UInt16.size = n.toNat

@[simp]

theorem UInt8.toNat_mod_uInt32Size (n : UInt8) : n.toNat % UInt32.size = n.toNat

@[simp]

theorem UInt8.toNat_mod_uInt64Size (n : UInt8) : n.toNat % UInt64.size = n.toNat

@[simp]

theorem UInt8.toNat_mod_uSizeSize (n : UInt8) : n.toNat % USize.size = n.toNat

@[simp]

theorem UInt16.toNat_mod_size (n : UInt16) : n.toNat % size = n.toNat

@[simp]

theorem UInt16.toNat_mod_uInt32Size (n : UInt16) : n.toNat % UInt32.size = n.toNat

@[simp]

theorem UInt16.toNat_mod_uInt64Size (n : UInt16) : n.toNat % UInt64.size = n.toNat

@[simp]

theorem UInt16.toNat_mod_uSizeSize (n : UInt16) : n.toNat % USize.size = n.toNat

@[simp]

theorem UInt32.toNat_mod_size (n : UInt32) : n.toNat % size = n.toNat

@[simp]

theorem UInt32.toNat_mod_uInt64Size (n : UInt32) : n.toNat % UInt64.size = n.toNat

@[simp]

theorem UInt32.toNat_mod_uSizeSize (n : UInt32) : n.toNat % USize.size = n.toNat

@[simp]

theorem UInt64.toNat_mod_size (n : UInt64) : n.toNat % size = n.toNat

@[simp]

theorem USize.toNat_mod_size (n : USize) : n.toNat % size = n.toNat

@[simp]

theorem USize.toNat_mod_uInt64Size (n : USize) : n.toNat % UInt64.size = n.toNat

@[simp]

theorem UInt8.toUInt16_mod_256 (n : UInt8) : n.toUInt16 % 256 = n.toUInt16

@[simp]

theorem UInt8.toUInt32_mod_256 (n : UInt8) : n.toUInt32 % 256 = n.toUInt32

@[simp]

theorem UInt8.toUInt64_mod_256 (n : UInt8) : n.toUInt64 % 256 = n.toUInt64

@[simp]

theorem UInt8.toUSize_mod_256 (n : UInt8) : n.toUSize % 256 = n.toUSize

@[simp]

theorem UInt16.toUInt32_mod_65536 (n : UInt16) : n.toUInt32 % 65536 = n.toUInt32

@[simp]

theorem UInt16.toUInt64_mod_65536 (n : UInt16) : n.toUInt64 % 65536 = n.toUInt64

@[simp]

theorem UInt16.toUSize_mod_65536 (n : UInt16) : n.toUSize % 65536 = n.toUSize

@[simp]

theorem UInt32.toUInt64_mod_4294967296 (n : UInt32) : n.toUInt64 % 4294967296 = n.toUInt64

@[simp]

theorem Fin.mk_uInt8ToNat (n : UInt8) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem Fin.mk_uInt16ToNat (n : UInt16) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem Fin.mk_uInt32ToNat (n : UInt32) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem Fin.mk_uInt64ToNat (n : UInt64) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem Fin.mk_uSizeToNat (n : USize) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem BitVec.ofNatLT_uInt8ToNat (n : UInt8) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofNatLT_uInt16ToNat (n : UInt16) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofNatLT_uInt32ToNat (n : UInt32) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofNatLT_uInt64ToNat (n : UInt64) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofNatLT_uSizeToNat (n : USize) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofFin_uInt8ToFin (n : UInt8) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem BitVec.ofFin_uInt16ToFin (n : UInt16) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem BitVec.ofFin_uInt32ToFin (n : UInt32) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem BitVec.ofFin_uInt64ToFin (n : UInt64) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem BitVec.ofFin_uSizeToFin (n : USize) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem UInt8.toFin_toUInt16 (n : UInt8) : n.toUInt16.toFin = Fin.castLE ⋯ n.toFin

@[simp]

theorem UInt8.toFin_toUInt32 (n : UInt8) : n.toUInt32.toFin = Fin.castLE ⋯ n.toFin

@[simp]

theorem UInt8.toFin_toUInt64 (n : UInt8) : n.toUInt64.toFin = Fin.castLE ⋯ n.toFin

@[simp]

theorem UInt8.toFin_toUSize (n : UInt8) : n.toUSize.toFin = Fin.castLE size_le_usizeSize n.toFin

@[simp]

theorem UInt16.toFin_toUInt32 (n : UInt16) : n.toUInt32.toFin = Fin.castLE ⋯ n.toFin

@[simp]

theorem UInt16.toFin_toUInt64 (n : UInt16) : n.toUInt64.toFin = Fin.castLE ⋯ n.toFin

@[simp]

theorem UInt16.toFin_toUSize (n : UInt16) : n.toUSize.toFin = Fin.castLE size_le_usizeSize n.toFin

@[simp]

theorem UInt32.toFin_toUInt64 (n : UInt32) : n.toUInt64.toFin = Fin.castLE ⋯ n.toFin

@[simp]

theorem UInt32.toFin_toUSize (n : UInt32) : n.toUSize.toFin = Fin.castLE size_le_usizeSize n.toFin

@[simp]

theorem USize.toFin_toUInt64 (n : USize) : n.toUInt64.toFin = Fin.castLE size_le_uint64Size n.toFin

@[simp]

theorem UInt16.toBitVec_toUInt8 (n : UInt16) : n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec

@[simp]

theorem UInt32.toBitVec_toUInt8 (n : UInt32) : n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec

@[simp]

theorem UInt64.toBitVec_toUInt8 (n : UInt64) : n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec

@[simp]

theorem USize.toBitVec_toUInt8 (n : USize) : n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec

@[simp]

theorem UInt8.toBitVec_toUInt16 (n : UInt8) : n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec

@[simp]

theorem UInt32.toBitVec_toUInt16 (n : UInt32) : n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec

@[simp]

theorem UInt64.toBitVec_toUInt16 (n : UInt64) : n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec

@[simp]

theorem USize.toBitVec_toUInt16 (n : USize) : n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec

@[simp]

theorem UInt8.toBitVec_toUInt32 (n : UInt8) : n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec

@[simp]

theorem UInt16.toBitVec_toUInt32 (n : UInt16) : n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec

@[simp]

theorem UInt64.toBitVec_toUInt32 (n : UInt64) : n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec

@[simp]

theorem USize.toBitVec_toUInt32 (n : USize) : n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec

@[simp]

theorem UInt8.toBitVec_toUInt64 (n : UInt8) : n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec

@[simp]

theorem UInt16.toBitVec_toUInt64 (n : UInt16) : n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec

@[simp]

theorem UInt32.toBitVec_toUInt64 (n : UInt32) : n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec

@[simp]

theorem USize.toBitVec_toUInt64 (n : USize) : n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec

@[simp]

theorem UInt8.toBitVec_toUSize (n : UInt8) : n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec

@[simp]

theorem UInt16.toBitVec_toUSize (n : UInt16) : n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec

@[simp]

theorem UInt32.toBitVec_toUSize (n : UInt32) : n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec

@[simp]

theorem UInt64.toBitVec_toUSize (n : UInt64) : n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec

@[simp]

theorem UInt8.ofNatLT_toNat (n : UInt8) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem UInt16.ofNatLT_uInt8ToNat (n : UInt8) : ofNatLT n.toNat ⋯ = n.toUInt16

@[simp]

theorem UInt32.ofNatLT_uInt8ToNat (n : UInt8) : ofNatLT n.toNat ⋯ = n.toUInt32

@[simp]

theorem UInt64.ofNatLT_uInt8ToNat (n : UInt8) : ofNatLT n.toNat ⋯ = n.toUInt64

@[simp]

theorem USize.ofNatLT_uInt8ToNat (n : UInt8) : ofNatLT n.toNat ⋯ = n.toUSize

@[simp]

theorem UInt16.ofNatLT_toNat (n : UInt16) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem UInt32.ofNatLT_uInt16ToNat (n : UInt16) : ofNatLT n.toNat ⋯ = n.toUInt32

@[simp]

theorem UInt64.ofNatLT_uInt16ToNat (n : UInt16) : ofNatLT n.toNat ⋯ = n.toUInt64

@[simp]

theorem USize.ofNatLT_uInt16ToNat (n : UInt16) : ofNatLT n.toNat ⋯ = n.toUSize

@[simp]

theorem UInt32.ofNatLT_toNat (n : UInt32) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem UInt64.ofNatLT_uInt32ToNat (n : UInt32) : ofNatLT n.toNat ⋯ = n.toUInt64

@[simp]

theorem USize.ofNatLT_uInt32ToNat (n : UInt32) : ofNatLT n.toNat ⋯ = n.toUSize

@[simp]

theorem UInt64.ofNatLT_toNat (n : UInt64) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem USize.ofNatLT_toNat (n : USize) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem UInt64.ofNatLT_uSizeToNat (n : USize) : ofNatLT n.toNat ⋯ = n.toUInt64

theorem UInt8.ofNatLT_uInt16ToNat (n : UInt16) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt8

theorem UInt8.ofNatLT_uInt32ToNat (n : UInt32) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt8

theorem UInt8.ofNatLT_uInt64ToNat (n : UInt64) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt8

theorem UInt8.ofNatLT_uSizeToNat (n : USize) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt8

theorem UInt16.ofNatLT_uInt32ToNat (n : UInt32) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt16

theorem UInt16.ofNatLT_uInt64ToNat (n : UInt64) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt16

theorem UInt16.ofNatLT_uSizeToNat (n : USize) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt16

theorem UInt32.ofNatLT_uInt64ToNat (n : UInt64) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt32

theorem UInt32.ofNatLT_uSizeToNat (n : USize) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt32

theorem USize.ofNatLT_uInt64ToNat (n : UInt64) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUSize

@[simp]

theorem UInt8.ofFin_toFin (n : UInt8) : ofFin n.toFin = n

@[simp]

theorem UInt16.ofFin_toFin (n : UInt16) : ofFin n.toFin = n

@[simp]

theorem UInt32.ofFin_toFin (n : UInt32) : ofFin n.toFin = n

@[simp]

theorem UInt64.ofFin_toFin (n : UInt64) : ofFin n.toFin = n

@[simp]

theorem USize.ofFin_toFin (n : USize) : ofFin n.toFin = n

@[simp]

theorem UInt16.ofFin_uint8ToFin (n : UInt8) : ofFin (Fin.castLE ⋯ n.toFin) = n.toUInt16

@[simp]

theorem UInt32.ofFin_uint8ToFin (n : UInt8) : ofFin (Fin.castLE ⋯ n.toFin) = n.toUInt32

@[simp]

theorem UInt32.ofFin_uint16ToFin (n : UInt16) : ofFin (Fin.castLE ⋯ n.toFin) = n.toUInt32

@[simp]

theorem UInt64.ofFin_uint8ToFin (n : UInt8) : ofFin (Fin.castLE ⋯ n.toFin) = n.toUInt64

@[simp]

theorem UInt64.ofFin_uint16ToFin (n : UInt16) : ofFin (Fin.castLE ⋯ n.toFin) = n.toUInt64

@[simp]

theorem UInt64.ofFin_uint32ToFin (n : UInt32) : ofFin (Fin.castLE ⋯ n.toFin) = n.toUInt64

@[simp]

theorem USize.ofFin_uint8ToFin (n : UInt8) : ofFin (Fin.castLE UInt8.size_le_usizeSize n.toFin) = n.toUSize

@[simp]

theorem USize.ofFin_uint16ToFin (n : UInt16) : ofFin (Fin.castLE UInt16.size_le_usizeSize n.toFin) = n.toUSize

@[simp]

theorem USize.ofFin_uint32ToFin (n : UInt32) : ofFin (Fin.castLE UInt32.size_le_usizeSize n.toFin) = n.toUSize

@[simp]

theorem Nat.toUInt8_eq {n : Nat} : n.toUInt8 = UInt8.ofNat n

@[simp]

theorem Nat.toUInt16_eq {n : Nat} : n.toUInt16 = UInt16.ofNat n

@[simp]

theorem Nat.toUInt32_eq {n : Nat} : n.toUInt32 = UInt32.ofNat n

@[simp]

theorem Nat.toUInt64_eq {n : Nat} : n.toUInt64 = UInt64.ofNat n

@[simp]

theorem Nat.toUSize_eq {n : Nat} : n.toUSize = USize.ofNat n

@[simp]

theorem UInt8.ofBitVec_uInt16ToBitVec (n : UInt16) : { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8

@[simp]

theorem UInt8.ofBitVec_uInt32ToBitVec (n : UInt32) : { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8

@[simp]

theorem UInt8.ofBitVec_uInt64ToBitVec (n : UInt64) : { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8

@[simp]

theorem UInt8.ofBitVec_uSizeToBitVec (n : USize) : { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8

@[simp]

theorem UInt16.ofBitVec_uInt8ToBitVec (n : UInt8) : { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16

@[simp]

theorem UInt16.ofBitVec_uInt32ToBitVec (n : UInt32) : { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16

@[simp]

theorem UInt16.ofBitVec_uInt64ToBitVec (n : UInt64) : { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16

@[simp]

theorem UInt16.ofBitVec_uSizeToBitVec (n : USize) : { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16

@[simp]

theorem UInt32.ofBitVec_uInt8ToBitVec (n : UInt8) : { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32

@[simp]

theorem UInt32.ofBitVec_uInt16ToBitVec (n : UInt16) : { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32

@[simp]

theorem UInt32.ofBitVec_uInt64ToBitVec (n : UInt64) : { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32

@[simp]

theorem UInt32.ofBitVec_uSizeToBitVec (n : USize) : { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32

@[simp]

theorem UInt64.ofBitVec_uInt8ToBitVec (n : UInt8) : { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64

@[simp]

theorem UInt64.ofBitVec_uInt16ToBitVec (n : UInt16) : { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64

@[simp]

theorem UInt64.ofBitVec_uInt32ToBitVec (n : UInt32) : { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64

@[simp]

theorem UInt64.ofBitVec_uSizeToBitVec (n : USize) : { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64

@[simp]

theorem USize.ofBitVec_uInt8ToBitVec (n : UInt8) : { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize

@[simp]

theorem USize.ofBitVec_uInt16ToBitVec (n : UInt16) : { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize

@[simp]

theorem USize.ofBitVec_uInt32ToBitVec (n : UInt32) : { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize

@[simp]

theorem USize.ofBitVec_uInt64ToBitVec (n : UInt64) : { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize

@[simp]

theorem UInt8.ofNat_uInt16ToNat (n : UInt16) : ofNat n.toNat = n.toUInt8

@[simp]

theorem UInt8.ofNat_uInt32ToNat (n : UInt32) : ofNat n.toNat = n.toUInt8

@[simp]

theorem UInt8.ofNat_uInt64ToNat (n : UInt64) : ofNat n.toNat = n.toUInt8

@[simp]

theorem UInt8.ofNat_uSizeToNat (n : USize) : ofNat n.toNat = n.toUInt8

@[simp]

theorem UInt16.ofNat_uInt8ToNat (n : UInt8) : ofNat n.toNat = n.toUInt16

@[simp]

theorem UInt16.ofNat_uInt32ToNat (n : UInt32) : ofNat n.toNat = n.toUInt16

@[simp]

theorem UInt16.ofNat_uInt64ToNat (n : UInt64) : ofNat n.toNat = n.toUInt16

@[simp]

theorem UInt16.ofNat_uSizeToNat (n : USize) : ofNat n.toNat = n.toUInt16

@[simp]

theorem UInt32.ofNat_uInt8ToNat (n : UInt8) : ofNat n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNat_uInt16ToNat (n : UInt16) : ofNat n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNat_uInt64ToNat (n : UInt64) : ofNat n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNat_uSizeToNat (n : USize) : ofNat n.toNat = n.toUInt32

@[simp]

theorem UInt64.ofNat_uInt8ToNat (n : UInt8) : ofNat n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNat_uInt16ToNat (n : UInt16) : ofNat n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNat_uInt32ToNat (n : UInt32) : ofNat n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNat_uSizeToNat (n : USize) : ofNat n.toNat = n.toUInt64

@[simp]

theorem USize.ofNat_uInt8ToNat (n : UInt8) : ofNat n.toNat = n.toUSize

@[simp]

theorem USize.ofNat_uInt16ToNat (n : UInt16) : ofNat n.toNat = n.toUSize

@[simp]

theorem USize.ofNat_uInt32ToNat (n : UInt32) : ofNat n.toNat = n.toUSize

@[simp]

theorem USize.ofNat_uInt64ToNat (n : UInt64) : ofNat n.toNat = n.toUSize

theorem UInt8.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem UInt16.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem UInt32.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem UInt64.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem USize.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem UInt8.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatTruncate n = ofNat n

theorem UInt16.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatTruncate n = ofNat n

theorem UInt32.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatTruncate n = ofNat n

theorem UInt64.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatTruncate n = ofNat n

theorem USize.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatTruncate n = ofNat n

@[simp]

theorem UInt8.ofNatTruncate_toNat (n : UInt8) : ofNatTruncate n.toNat = n

@[simp]

theorem UInt16.ofNatTruncate_uInt8ToNat (n : UInt8) : ofNatTruncate n.toNat = n.toUInt16

@[simp]

theorem UInt16.ofNatTruncate_toNat (n : UInt16) : ofNatTruncate n.toNat = n

@[simp]

theorem UInt32.ofNatTruncate_uInt8ToNat (n : UInt8) : ofNatTruncate n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNatTruncate_uInt16ToNat (n : UInt16) : ofNatTruncate n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNatTruncate_toNat (n : UInt32) : ofNatTruncate n.toNat = n

@[simp]

theorem UInt64.ofNatTruncate_uInt8ToNat (n : UInt8) : ofNatTruncate n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNatTruncate_uInt16ToNat (n : UInt16) : ofNatTruncate n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNatTruncate_uInt32ToNat (n : UInt32) : ofNatTruncate n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNatTruncate_toNat (n : UInt64) : ofNatTruncate n.toNat = n

@[simp]

theorem UInt64.ofNatTruncate_uSizeToNat (n : USize) : ofNatTruncate n.toNat = n.toUInt64

@[simp]

theorem USize.ofNatTruncate_uInt8ToNat (n : UInt8) : ofNatTruncate n.toNat = n.toUSize

@[simp]

theorem USize.ofNatTruncate_uInt16ToNat (n : UInt16) : ofNatTruncate n.toNat = n.toUSize

@[simp]

theorem USize.ofNatTruncate_uInt32ToNat (n : UInt32) : ofNatTruncate n.toNat = n.toUSize

@[simp]

theorem USize.ofNatTruncate_toNat (n : USize) : ofNatTruncate n.toNat = n

@[simp]

theorem UInt8.toUInt8_toUInt16 (n : UInt8) : n.toUInt16.toUInt8 = n

@[simp]

theorem UInt8.toUInt8_toUInt32 (n : UInt8) : n.toUInt32.toUInt8 = n

@[simp]

theorem UInt8.toUInt8_toUInt64 (n : UInt8) : n.toUInt64.toUInt8 = n

@[simp]

theorem UInt8.toUInt8_toUSize (n : UInt8) : n.toUSize.toUInt8 = n

@[simp]

theorem UInt8.toUInt16_toUInt32 (n : UInt8) : n.toUInt32.toUInt16 = n.toUInt16

@[simp]

theorem UInt8.toUInt16_toUInt64 (n : UInt8) : n.toUInt64.toUInt16 = n.toUInt16

@[simp]

theorem UInt8.toUInt16_toUSize (n : UInt8) : n.toUSize.toUInt16 = n.toUInt16

@[simp]

theorem UInt8.toUInt32_toUInt16 (n : UInt8) : n.toUInt16.toUInt32 = n.toUInt32

@[simp]

theorem UInt8.toUInt32_toUInt64 (n : UInt8) : n.toUInt64.toUInt32 = n.toUInt32

@[simp]

theorem UInt8.toUInt32_toUSize (n : UInt8) : n.toUSize.toUInt32 = n.toUInt32

@[simp]

theorem UInt8.toUInt64_toUInt16 (n : UInt8) : n.toUInt16.toUInt64 = n.toUInt64

@[simp]

theorem UInt8.toUInt64_toUInt32 (n : UInt8) : n.toUInt32.toUInt64 = n.toUInt64

@[simp]

theorem UInt8.toUInt64_toUSize (n : UInt8) : n.toUSize.toUInt64 = n.toUInt64

@[simp]

theorem UInt8.toUSize_toUInt16 (n : UInt8) : n.toUInt16.toUSize = n.toUSize

@[simp]

theorem UInt8.toUSize_toUInt32 (n : UInt8) : n.toUInt32.toUSize = n.toUSize

@[simp]

theorem UInt8.toUSize_toUInt64 (n : UInt8) : n.toUInt64.toUSize = n.toUSize

@[simp]

theorem UInt16.toUInt8_toUInt32 (n : UInt16) : n.toUInt32.toUInt8 = n.toUInt8

@[simp]

theorem UInt16.toUInt8_toUInt64 (n : UInt16) : n.toUInt64.toUInt8 = n.toUInt8

@[simp]

theorem UInt16.toUInt8_toUSize (n : UInt16) : n.toUSize.toUInt8 = n.toUInt8

@[simp]

theorem UInt16.toUInt16_toUInt8 (n : UInt16) : n.toUInt8.toUInt16 = n % 256

@[simp]

theorem UInt16.toUInt16_toUInt32 (n : UInt16) : n.toUInt32.toUInt16 = n

@[simp]

theorem UInt16.toUInt16_toUInt64 (n : UInt16) : n.toUInt64.toUInt16 = n

@[simp]

theorem UInt16.toUInt16_toUSize (n : UInt16) : n.toUSize.toUInt16 = n

@[simp]

theorem UInt16.toUInt32_toUInt8 (n : UInt16) : n.toUInt8.toUInt32 = n.toUInt32 % 256

@[simp]

theorem UInt16.toUInt32_toUInt64 (n : UInt16) : n.toUInt64.toUInt32 = n.toUInt32

@[simp]

theorem UInt16.toUInt32_toUSize (n : UInt16) : n.toUSize.toUInt32 = n.toUInt32

@[simp]

theorem UInt16.toUInt64_toUInt8 (n : UInt16) : n.toUInt8.toUInt64 = n.toUInt64 % 256

@[simp]

theorem UInt16.toUInt64_toUInt32 (n : UInt16) : n.toUInt32.toUInt64 = n.toUInt64

@[simp]

theorem UInt16.toUInt64_toUSize (n : UInt16) : n.toUSize.toUInt64 = n.toUInt64

@[simp]

theorem UInt16.toUSize_toUInt8 (n : UInt16) : n.toUInt8.toUSize = n.toUSize % 256

@[simp]

theorem UInt16.toUSize_toUInt32 (n : UInt16) : n.toUInt32.toUSize = n.toUSize

@[simp]

theorem UInt16.toUSize_toUInt64 (n : UInt16) : n.toUInt64.toUSize = n.toUSize

@[simp]

theorem UInt32.toUInt8_toUInt16 (n : UInt32) : n.toUInt16.toUInt8 = n.toUInt8

@[simp]

theorem UInt32.toUInt8_toUInt64 (n : UInt32) : n.toUInt64.toUInt8 = n.toUInt8

@[simp]

theorem UInt32.toUInt8_toUSize (n : UInt32) : n.toUSize.toUInt8 = n.toUInt8

@[simp]

theorem UInt32.toUInt16_toUInt8 (n : UInt32) : n.toUInt8.toUInt16 = n.toUInt16 % 256

@[simp]

theorem UInt32.toUInt16_toUInt64 (n : UInt32) : n.toUInt64.toUInt16 = n.toUInt16

@[simp]

theorem UInt32.toUInt16_toUSize (n : UInt32) : n.toUSize.toUInt16 = n.toUInt16

@[simp]

theorem UInt32.toUInt32_toUInt8 (n : UInt32) : n.toUInt8.toUInt32 = n % 256

@[simp]

theorem UInt32.toUInt32_toUInt16 (n : UInt32) : n.toUInt16.toUInt32 = n % 65536

@[simp]

theorem UInt32.toUInt32_toUInt64 (n : UInt32) : n.toUInt64.toUInt32 = n

@[simp]

theorem UInt32.toUInt32_toUSize (n : UInt32) : n.toUSize.toUInt32 = n

@[simp]

theorem UInt32.toUInt64_toUInt8 (n : UInt32) : n.toUInt8.toUInt64 = n.toUInt64 % 256

@[simp]

theorem UInt32.toUInt64_toUInt16 (n : UInt32) : n.toUInt16.toUInt64 = n.toUInt64 % 65536

@[simp]

theorem UInt32.toUInt64_toUSize (n : UInt32) : n.toUSize.toUInt64 = n.toUInt64

@[simp]

theorem UInt32.toUSize_toUInt8 (n : UInt32) : n.toUInt8.toUSize = n.toUSize % 256

@[simp]

theorem UInt32.toUSize_toUInt16 (n : UInt32) : n.toUInt16.toUSize = n.toUSize % 65536

@[simp]

theorem UInt32.toUSize_toUInt64 (n : UInt32) : n.toUInt64.toUSize = n.toUSize

@[simp]

theorem UInt64.toUInt8_toUInt16 (n : UInt64) : n.toUInt16.toUInt8 = n.toUInt8

@[simp]

theorem UInt64.toUInt8_toUInt32 (n : UInt64) : n.toUInt32.toUInt8 = n.toUInt8

@[simp]

theorem UInt64.toUInt8_toUSize (n : UInt64) : n.toUSize.toUInt8 = n.toUInt8

@[simp]

theorem UInt64.toUInt16_toUInt8 (n : UInt64) : n.toUInt8.toUInt16 = n.toUInt16 % 256

@[simp]

theorem UInt64.toUInt16_toUInt32 (n : UInt64) : n.toUInt32.toUInt16 = n.toUInt16

@[simp]

theorem UInt64.toUInt16_toUSize (n : UInt64) : n.toUSize.toUInt16 = n.toUInt16

@[simp]

theorem UInt64.toUInt32_toUInt8 (n : UInt64) : n.toUInt8.toUInt32 = n.toUInt32 % 256

@[simp]

theorem UInt64.toUInt32_toUInt16 (n : UInt64) : n.toUInt16.toUInt32 = n.toUInt32 % 65536

@[simp]

theorem UInt64.toUInt32_toUSize (n : UInt64) : n.toUSize.toUInt32 = n.toUInt32

@[simp]

theorem UInt64.toUInt64_toUInt8 (n : UInt64) : n.toUInt8.toUInt64 = n % 256

@[simp]

theorem UInt64.toUInt64_toUInt16 (n : UInt64) : n.toUInt16.toUInt64 = n % 65536

@[simp]

theorem UInt64.toUInt64_toUInt32 (n : UInt64) : n.toUInt32.toUInt64 = n % 4294967296

@[simp]

theorem UInt64.toUSize_toUInt8 (n : UInt64) : n.toUInt8.toUSize = n.toUSize % 256

@[simp]

theorem UInt64.toUSize_toUInt16 (n : UInt64) : n.toUInt16.toUSize = n.toUSize % 65536

@[simp]

theorem USize.toUInt8_toUInt16 (n : USize) : n.toUInt16.toUInt8 = n.toUInt8

@[simp]

theorem USize.toUInt8_toUInt32 (n : USize) : n.toUInt32.toUInt8 = n.toUInt8

@[simp]

theorem USize.toUInt8_toUInt64 (n : USize) : n.toUInt64.toUInt8 = n.toUInt8

@[simp]

theorem USize.toUInt16_toUInt8 (n : USize) : n.toUInt8.toUInt16 = n.toUInt16 % 256

@[simp]

theorem USize.toUInt16_toUInt32 (n : USize) : n.toUInt32.toUInt16 = n.toUInt16

@[simp]

theorem USize.toUInt16_toUInt64 (n : USize) : n.toUInt64.toUInt16 = n.toUInt16

@[simp]

theorem USize.toUInt64_toUInt8 (n : USize) : n.toUInt8.toUInt64 = n.toUInt64 % 256

@[simp]

theorem USize.toUInt64_toUInt16 (n : USize) : n.toUInt16.toUInt64 = n.toUInt64 % 65536

@[simp]

theorem USize.toUInt32_toUInt8 (n : USize) : n.toUInt8.toUInt32 = n.toUInt32 % 256

@[simp]

theorem USize.toUInt32_toUInt16 (n : USize) : n.toUInt16.toUInt32 = n.toUInt32 % 65536

@[simp]

theorem USize.toUInt32_toUInt64 (n : USize) : n.toUInt64.toUInt32 = n.toUInt32

@[simp]

theorem USize.toUSize_toUInt8 (n : USize) : n.toUInt8.toUSize = n % 256

@[simp]

theorem USize.toUSize_toUInt16 (n : USize) : n.toUInt16.toUSize = n % 65536

@[simp]

theorem USize.toUSize_toUInt64 (n : USize) : n.toUInt64.toUSize = n