Well-formedness proofs for raw tree maps

This file contains well-formedness proofs about Std.Data.TreeMap.Raw.Basic. Most of the lemmas require TransCmp cmp for the comparison function cmp.

theorem Std.TreeMap.Raw.WF.empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Raw.empty.WF

theorem Std.TreeMap.Raw.WF.emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} : ∅.WF

theorem Std.TreeMap.Raw.WF.erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} (h : t.WF) : (t.erase a).WF

theorem Std.TreeMap.Raw.WF.insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) : (t.insert a b).WF

theorem Std.TreeMap.Raw.WF.insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) : (t.insertIfNew a b).WF

theorem Std.TreeMap.Raw.WF.containsThenInsert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) : (t.containsThenInsert a b).snd.WF

theorem Std.TreeMap.Raw.WF.containsThenInsertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) : (t.containsThenInsertIfNew a b).snd.WF

theorem Std.TreeMap.Raw.WF.getThenInsertIfNew? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) : (t.getThenInsertIfNew? a b).snd.WF

theorem Std.TreeMap.Raw.WF.filter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {f : α → β → Bool} (h : t.WF) : (Raw.filter f t).WF

theorem Std.TreeMap.Raw.WF.filterMap {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {f : α → β → Option β} (h : t.WF) : (Raw.filterMap f t).WF

theorem Std.TreeMap.Raw.WF.partition_fst {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {f : α → β → Bool} : (partition f t).fst.WF

theorem Std.TreeMap.Raw.WF.partition_snd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {f : α → β → Bool} : (partition f t).snd.WF

theorem Std.TreeMap.Raw.WF.eraseMany {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Raw α β cmp} (h : t.WF) : (t.eraseMany l).WF

theorem Std.TreeMap.Raw.WF.insertMany {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ (α × β)] {l : ρ} {t : Raw α β cmp} (h : t.WF) : (t.insertMany l).WF

theorem Std.TreeMap.Raw.WF.insertManyIfNewUnit {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Raw α Unit cmp} (h : t.WF) : (t.insertManyIfNewUnit l).WF

theorem Std.TreeMap.Raw.WF.ofList {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {l : List (α × β)} : (Raw.ofList l cmp).WF

theorem Std.TreeMap.Raw.WF.ofArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {a : Array (α × β)} : (Raw.ofArray a cmp).WF

theorem Std.TreeMap.Raw.WF.alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} {f : Option β → Option β} {t : Raw α β cmp} (h : t.WF) : (t.alter a f).WF

theorem Std.TreeMap.Raw.WF.modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} {f : β → β} {t : Raw α β cmp} (h : t.WF) : (t.modify a f).WF

theorem Std.TreeMap.Raw.WF.unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} : (Raw.unitOfList l cmp).WF

theorem Std.TreeMap.Raw.WF.unitOfArray {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a : Array α} : (Raw.unitOfArray a cmp).WF

theorem Std.TreeMap.Raw.WF.mergeWith {α : Type u} {β : Type v} {cmp : α → α → Ordering} {mergeFn : α → β → β → β} {t₁ t₂ : Raw α β cmp} (h : t₁.WF) : (Raw.mergeWith mergeFn t₁ t₂).WF

theorem Std.TreeMap.Raw.WF.union {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ ∪ t₂).WF

theorem Std.TreeMap.Raw.WF.inter {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) : (t₁ ∩ t₂).WF

theorem Std.TreeMap.Raw.WF.diff {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) : (t₁ \ t₂).WF