- of_red : ∀ {α : Type u} (l : rbnode α) (v : α) (r : rbnode α), (l.red_node v r).is_node_of l v r
- of_black : ∀ {α : Type u} (l : rbnode α) (v : α) (r : rbnode α), (l.black_node v r).is_node_of l v r
Equations
- rbnode.lift lt (some a) (some b) = lt a b
- rbnode.lift lt (some val) none = true
- rbnode.lift lt none _x = true
- leaf_s : ∀ {α : Type u} {lt : α → α → Prop} {lo hi : option α}, rbnode.lift lt lo hi → rbnode.is_searchable lt rbnode.leaf lo hi
- red_s : ∀ {α : Type u} {lt : α → α → Prop} {l r : rbnode α} {v : α} {lo hi : option α}, rbnode.is_searchable lt l lo (some v) → rbnode.is_searchable lt r (some v) hi → rbnode.is_searchable lt (l.red_node v r) lo hi
- black_s : ∀ {α : Type u} {lt : α → α → Prop} {l r : rbnode α} {v : α} {lo hi : option α}, rbnode.is_searchable lt l lo (some v) → rbnode.is_searchable lt r (some v) hi → rbnode.is_searchable lt (l.black_node v r) lo hi
theorem
rbnode.lo_lt_hi
{α : Type u}
{t : rbnode α}
{lt : α → α → Prop}
[is_trans α lt]
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → rbnode.lift lt lo hi
theorem
rbnode.is_searchable_of_is_searchable_of_incomp
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{t : rbnode α}
{lo : option α}
{hi hi' : α}
(hc : ¬lt hi' hi ∧ ¬lt hi hi')
(hs : rbnode.is_searchable lt t lo (some hi)) :
rbnode.is_searchable lt t lo (some hi')
theorem
rbnode.is_searchable_of_incomp_of_is_searchable
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{t : rbnode α}
{lo lo' : α}
{hi : option α}
(hc : ¬lt lo' lo ∧ ¬lt lo lo')
(hs : rbnode.is_searchable lt t (some lo) hi) :
rbnode.is_searchable lt t (some lo') hi
theorem
rbnode.is_searchable_some_low_of_is_searchable_of_lt
{α : Type u}
{lt : α → α → Prop}
{t : rbnode α}
[is_trans α lt]
{lo : α}
{hi : option α}
{lo' : α}
(hlt : lt lo' lo)
(hs : rbnode.is_searchable lt t (some lo) hi) :
rbnode.is_searchable lt t (some lo') hi
theorem
rbnode.is_searchable_none_low_of_is_searchable_some_low
{α : Type u}
{lt : α → α → Prop}
{t : rbnode α}
{y : α}
{hi : option α}
(hlt : rbnode.is_searchable lt t (some y) hi) :
rbnode.is_searchable lt t none hi
theorem
rbnode.is_searchable_some_high_of_is_searchable_of_lt
{α : Type u}
{lt : α → α → Prop}
{t : rbnode α}
[is_trans α lt]
{lo : option α}
{hi hi' : α}
(hlt : lt hi hi')
(hs : rbnode.is_searchable lt t lo (some hi)) :
rbnode.is_searchable lt t lo (some hi')
theorem
rbnode.is_searchable_none_high_of_is_searchable_some_high
{α : Type u}
{lt : α → α → Prop}
{t : rbnode α}
{lo : option α}
{y : α}
(hlt : rbnode.is_searchable lt t lo (some y)) :
rbnode.is_searchable lt t lo none
theorem
rbnode.range
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{t : rbnode α}
{x : α}
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → rbnode.mem lt x t → rbnode.lift lt lo (some x) ∧ rbnode.lift lt (some x) hi
theorem
rbnode.lt_of_mem_left
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{y : α}
{t l r : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → t.is_node_of l y r → ∀ {x : α}, rbnode.mem lt x l → lt x y
theorem
rbnode.lt_of_mem_right
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{y : α}
{t l r : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → t.is_node_of l y r → ∀ {z : α}, rbnode.mem lt z r → lt y z
theorem
rbnode.lt_of_mem_left_right
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{y : α}
{t l r : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → t.is_node_of l y r → ∀ {x z : α}, rbnode.mem lt x l → rbnode.mem lt z r → lt x z
- leaf_rb : ∀ {α : Type u}, rbnode.leaf.is_red_black rbnode.color.black 0
- red_rb : ∀ {α : Type u} {v : α} {l r : rbnode α} {n : ℕ}, l.is_red_black rbnode.color.black n → r.is_red_black rbnode.color.black n → (l.red_node v r).is_red_black rbnode.color.red n
- black_rb : ∀ {α : Type u} {v : α} {l r : rbnode α} {n : ℕ} {c₁ c₂ : rbnode.color}, l.is_red_black c₁ n → r.is_red_black c₂ n → (l.black_node v r).is_red_black rbnode.color.black n.succ
theorem
rbnode.depth_min
{α : Type u}
{c : rbnode.color}
{n : ℕ}
{t : rbnode α} :
t.is_red_black c n → n ≤ rbnode.depth min t
theorem
rbnode.depth_max'
{α : Type u}
{c : rbnode.color}
{n : ℕ}
{t : rbnode α} :
t.is_red_black c n → rbnode.depth max t ≤ upper c n
theorem
rbnode.depth_max
{α : Type u}
{c : rbnode.color}
{n : ℕ}
{t : rbnode α}
(h : t.is_red_black c n) :
rbnode.depth max t ≤ 2 * n + 1
theorem
rbnode.balanced
{α : Type u}
{c : rbnode.color}
{n : ℕ}
{t : rbnode α}
(h : t.is_red_black c n) :
rbnode.depth max t ≤ 2 * rbnode.depth min t + 1