def commandDeclare_uint_theorems__ : Lean.ParserDescr

Equations

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

theorem UInt8.ofNat_toNat {x : UInt8} : 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 : UInt8.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 < UInt8.size → (UInt8.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.lt_trans {a b c : UInt8} : a < b → b < c → a < c

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[deprecated UInt8.toNat_mod_lt]

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

@[simp]

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

theorem UInt8.eq_of_val_eq {a b : UInt8} (h : a.val = b.val) : 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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem UInt8.ofNat_one : UInt8.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} : (UInt8.ofNat n).toNat = n % 2 ^ 8

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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 < UInt16.size

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

@[simp]

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

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

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

@[simp]

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

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.mod_lt (a : UInt16) {b : UInt16} : 0 < b → a % b < b

@[simp]

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

@[simp]

theorem UInt16.toNat_zero : UInt16.toNat 0 = 0

@[simp]

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

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

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

@[simp]

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

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

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

@[deprecated UInt16.toNat_mod_lt]

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 : UInt16.ofNat 1 = 1

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem UInt32.toNat_zero : UInt32.toNat 0 = 0

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

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

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

@[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.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

@[deprecated UInt32.toNat_mod_lt]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

theorem UInt32.ofNat_one : UInt32.ofNat 1 = 1

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem UInt64.ofNat_one : UInt64.ofNat 1 = 1

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem UInt64.toNat_zero : UInt64.toNat 0 = 0

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

theorem UInt64.lt_iff_toNat_lt {a b : UInt64} : a < b ↔ a.toNat < b.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

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

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.toNat_ofNat_of_lt {n : Nat} (h : n < UInt64.size) : (UInt64.ofNat n).toNat = n

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

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

@[deprecated UInt64.toNat_mod_lt]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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.lt_asymm {a b : UInt64} : a < b → ¬b < a

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

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

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

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

@[simp]

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

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 }

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

theorem USize.toNat_zero : USize.toNat 0 = 0

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem USize.ofNat_one : USize.ofNat 1 = 1

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[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 }

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

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

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

@[simp]

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

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.toNat_mod (a b : USize) : (a % b).toNat = a.toNat % b.toNat

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated USize.toNat_mod_lt]

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

@[simp]

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

@[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) : (USize.ofNat n).toNat = n

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

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

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

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

@[reducible, inline, deprecated UInt8.toNat_zero]

abbrev UInt8.zero_toNat : UInt8.toNat 0 = 0

Equations

• UInt8.zero_toNat = UInt8.toNat_zero

@[reducible, inline, deprecated UInt8.toNat_div]

abbrev UInt8.div_toNat (a b : UInt8) : (a / b).toNat = a.toNat / b.toNat

Equations

• UInt8.div_toNat = UInt8.toNat_div

@[reducible, inline, deprecated UInt8.toNat_mod]

abbrev UInt8.mod_toNat (a b : UInt8) : (a % b).toNat = a.toNat % b.toNat

Equations

• UInt8.mod_toNat = UInt8.toNat_mod

@[reducible, inline, deprecated UInt16.toNat_zero]

abbrev UInt16.zero_toNat : UInt16.toNat 0 = 0

Equations

• UInt16.zero_toNat = UInt16.toNat_zero

@[reducible, inline, deprecated UInt16.toNat_div]

abbrev UInt16.div_toNat (a b : UInt16) : (a / b).toNat = a.toNat / b.toNat

Equations

• UInt16.div_toNat = UInt16.toNat_div

@[reducible, inline, deprecated UInt16.toNat_mod]

abbrev UInt16.mod_toNat (a b : UInt16) : (a % b).toNat = a.toNat % b.toNat

Equations

• UInt16.mod_toNat = UInt16.toNat_mod

@[reducible, inline, deprecated UInt32.toNat_zero]

abbrev UInt32.zero_toNat : UInt32.toNat 0 = 0

Equations

• UInt32.zero_toNat = UInt32.toNat_zero

@[reducible, inline, deprecated UInt32.toNat_div]

abbrev UInt32.div_toNat (a b : UInt32) : (a / b).toNat = a.toNat / b.toNat

Equations

• UInt32.div_toNat = UInt32.toNat_div

@[reducible, inline, deprecated UInt32.toNat_mod]

abbrev UInt32.mod_toNat (a b : UInt32) : (a % b).toNat = a.toNat % b.toNat

Equations

• UInt32.mod_toNat = UInt32.toNat_mod

@[reducible, inline, deprecated UInt64.toNat_zero]

abbrev UInt64.zero_toNat : UInt64.toNat 0 = 0

Equations

• UInt64.zero_toNat = UInt64.toNat_zero

@[reducible, inline, deprecated UInt64.toNat_div]

abbrev UInt64.div_toNat (a b : UInt64) : (a / b).toNat = a.toNat / b.toNat

Equations

• UInt64.div_toNat = UInt64.toNat_div

@[reducible, inline, deprecated UInt64.toNat_mod]

abbrev UInt64.mod_toNat (a b : UInt64) : (a % b).toNat = a.toNat % b.toNat

Equations

• UInt64.mod_toNat = UInt64.toNat_mod

@[reducible, inline, deprecated USize.toNat_zero]

abbrev USize.zero_toNat : USize.toNat 0 = 0

Equations

• USize.zero_toNat = USize.toNat_zero

@[reducible, inline, deprecated USize.toNat_div]

abbrev USize.div_toNat (a b : USize) : (a / b).toNat = a.toNat / b.toNat

Equations

• USize.div_toNat = USize.toNat_div

@[reducible, inline, deprecated USize.toNat_mod]

abbrev USize.mod_toNat (a b : USize) : (a % b).toNat = a.toNat % b.toNat

Equations

• USize.mod_toNat = USize.toNat_mod