@[simp]

theorem emptyc_eq_empty : ∅ = ByteArray.empty

@[simp]

theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty

@[simp]

theorem ByteArray.data_empty : empty.data = #[]

@[simp]

theorem ByteArray.data_extract {a : ByteArray} {b e : Nat} : (a.extract b e).data = a.data.extract b e

@[simp]

theorem ByteArray.extract_zero_size {b : ByteArray} : b.extract 0 b.size = b

@[simp]

theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = empty

theorem ByteArray.fastAppend_eq_copySlice {a b : ByteArray} : a.fastAppend b = b.copySlice 0 a a.size b.size false

@[simp]

theorem List.toByteArray_append {l l' : List UInt8} : (l ++ l').toByteArray = l.toByteArray ++ l'.toByteArray

@[simp]

theorem ByteArray.toList_data_append {l l' : ByteArray} : (l ++ l').data.toList = l.data.toList ++ l'.data.toList

@[simp]

theorem ByteArray.data_append {l l' : ByteArray} : (l ++ l').data = l.data ++ l'.data

@[simp]

theorem ByteArray.size_empty : empty.size = 0

@[simp]

theorem List.data_toByteArray {l : List UInt8} : l.toByteArray.data = l.toArray

@[simp]

theorem List.size_toByteArray {l : List UInt8} : l.toByteArray.size = l.length

@[simp]

theorem List.toByteArray_nil : [].toByteArray = ByteArray.empty

@[simp]

theorem ByteArray.empty_append {b : ByteArray} : empty ++ b = b

@[simp]

theorem ByteArray.append_empty {b : ByteArray} : b ++ empty = b

@[simp]

theorem ByteArray.size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size

@[simp]

theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = empty

theorem ByteArray.getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} : a[i] = a.data[i]

@[simp]

theorem ByteArray.getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} (hlt : i < a.size) : (a ++ b)[i] = a[i]

theorem ByteArray.getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]

@[simp]

theorem List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} : l.toByteArray[i] = l[i]

theorem List.getElem_eq_getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.length} : l[i] = l.toByteArray[i]

@[simp]

theorem ByteArray.size_extract {a : ByteArray} {b e : Nat} : (a.extract b e).size = min e a.size - b

@[simp]

theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = empty ↔ min j b.size ≤ i

@[simp]

theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = empty

@[simp]

theorem ByteArray.append_eq_empty_iff {a b : ByteArray} : a ++ b = empty ↔ a = empty ∧ b = empty

@[simp]

theorem List.toByteArray_eq_empty {l : List UInt8} : l.toByteArray = ByteArray.empty ↔ l = []

theorem ByteArray.append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) : xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂

@[simp]

theorem ByteArray.extract_append_extract {a : ByteArray} {i j k : Nat} : a.extract i j ++ a.extract j k = a.extract (min i j) (max j k)

theorem ByteArray.extract_eq_extract_append_extract {a : ByteArray} {i k : Nat} (j : Nat) (hi : i ≤ j) (hk : j ≤ k) : a.extract i k = a.extract i j ++ a.extract j k

theorem ByteArray.append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂

theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) : (a ++ b).extract i j = b

theorem ByteArray.extract_append_eq_left {a b : ByteArray} {i : Nat} (hi : i = a.size) : (a ++ b).extract 0 i = a

theorem ByteArray.extract_append_size_left {a b : ByteArray} {i : Nat} : (a ++ b).extract i a.size = a.extract i a.size

theorem ByteArray.extract_append_size_add {a b : ByteArray} {i j : Nat} : (a ++ b).extract (a.size + i) (a.size + j) = b.extract i j

theorem ByteArray.extract_append {as bs : ByteArray} {i j : Nat} : (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size)

theorem ByteArray.extract_append_size_add' {a b : ByteArray} {i j k : Nat} (h : k = a.size) : (a ++ b).extract (k + i) (k + j) = b.extract i j

theorem ByteArray.extract_extract {a : ByteArray} {i j k l : Nat} : (a.extract i j).extract k l = a.extract (i + k) (min (i + l) j)

theorem ByteArray.getElem_extract_aux {i : Nat} {xs : ByteArray} {start stop : Nat} (h : i < (xs.extract start stop).size) : start + i < xs.size

theorem ByteArray.getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat} (h : i < (b.extract start stop).size) : (b.extract start stop)[i] = b[start + i]

theorem ByteArray.extract_eq_extract_left {a : ByteArray} {i i' j : Nat} : a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i'

theorem ByteArray.extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) : a.extract i (i + 1) = [a[i]].toByteArray

theorem ByteArray.extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) : a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray

theorem ByteArray.extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) : a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray

theorem ByteArray.extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) : a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray

theorem ByteArray.append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c)

@[simp]

theorem ByteArray.toList_empty : empty.toList = []

theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} : src.copySlice srcOff dest destOff len exact = dest.extract 0 destOff ++ src.extract srcOff (srcOff + len) ++ dest.extract (destOff + min len (src.data.size - srcOff)) dest.data.size

@[simp]

theorem ByteArray.data_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} : (as.set i a h).data = as.data.set i a ⋯

theorem ByteArray.set_eq_push_extract_append_extract {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} : as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size

@[simp]

theorem ByteArray.append_toByteArray_singleton {as : ByteArray} {a : UInt8} : as ++ [a].toByteArray = as.push a