@[simp]
theorem
rbnode.balance1_eq₁
{α : Type u}
(l : rbnode α)
(x : α)
(r₁ : rbnode α)
(y : α)
(r₂ : rbnode α)
(v : α)
(t : rbnode α) :
(l.red_node x r₁).balance1 y r₂ v t = (l.black_node x r₁).red_node y (r₂.black_node v t)
@[simp]
theorem
rbnode.balance1_eq₂
{α : Type u}
(l₁ : rbnode α)
(y : α)
(l₂ : rbnode α)
(x : α)
(r : rbnode α)
(v : α)
(t : rbnode α) :
l₁.get_color ≠ rbnode.color.red → l₁.balance1 y (l₂.red_node x r) v t = (l₁.black_node y l₂).red_node x (r.black_node v t)
@[simp]
theorem
rbnode.balance1_eq₃
{α : Type u}
(l : rbnode α)
(y : α)
(r : rbnode α)
(v : α)
(t : rbnode α) :
l.get_color ≠ rbnode.color.red → r.get_color ≠ rbnode.color.red → l.balance1 y r v t = (l.red_node y r).black_node v t
@[simp]
theorem
rbnode.balance2_eq₁
{α : Type u}
(l : rbnode α)
(x₁ : α)
(r₁ : rbnode α)
(y : α)
(r₂ : rbnode α)
(v : α)
(t : rbnode α) :
(l.red_node x₁ r₁).balance2 y r₂ v t = (t.black_node v l).red_node x₁ (r₁.black_node y r₂)
@[simp]
theorem
rbnode.balance2_eq₂
{α : Type u}
(l₁ : rbnode α)
(y : α)
(l₂ : rbnode α)
(x₂ : α)
(r₂ : rbnode α)
(v : α)
(t : rbnode α) :
l₁.get_color ≠ rbnode.color.red → l₁.balance2 y (l₂.red_node x₂ r₂) v t = (t.black_node v l₁).red_node y (l₂.black_node x₂ r₂)
@[simp]
theorem
rbnode.balance2_eq₃
{α : Type u}
(l : rbnode α)
(y : α)
(r : rbnode α)
(v : α)
(t : rbnode α) :
l.get_color ≠ rbnode.color.red → r.get_color ≠ rbnode.color.red → l.balance2 y r v t = t.black_node v (l.red_node y r)
theorem
rbnode.balance.cases
{α : Type u}
{p : rbnode α → α → rbnode α → Prop}
(l : rbnode α)
(y : α)
(r : rbnode α)
(red_left : ∀ (l : rbnode α) (x : α) (r₁ : rbnode α) (y : α) (r₂ : rbnode α), p (l.red_node x r₁) y r₂)
(red_right : ∀ (l₁ : rbnode α) (y : α) (l₂ : rbnode α) (x : α) (r : rbnode α), l₁.get_color ≠ rbnode.color.red → p l₁ y (l₂.red_node x r))
(other : ∀ (l : rbnode α) (y : α) (r : rbnode α), l.get_color ≠ rbnode.color.red → r.get_color ≠ rbnode.color.red → p l y r) :
p l y r
theorem
rbnode.balance1_ne_leaf
{α : Type u}
(l : rbnode α)
(x : α)
(r : rbnode α)
(v : α)
(t : rbnode α) :
l.balance1 x r v t ≠ rbnode.leaf
theorem
rbnode.balance1_node_ne_leaf
{α : Type u}
{s : rbnode α}
(a : α)
(t : rbnode α) :
s ≠ rbnode.leaf → s.balance1_node a t ≠ rbnode.leaf
theorem
rbnode.balance2_ne_leaf
{α : Type u}
(l : rbnode α)
(x : α)
(r : rbnode α)
(v : α)
(t : rbnode α) :
l.balance2 x r v t ≠ rbnode.leaf
theorem
rbnode.balance2_node_ne_leaf
{α : Type u}
{s : rbnode α}
(a : α)
(t : rbnode α) :
s ≠ rbnode.leaf → s.balance2_node a t ≠ rbnode.leaf
theorem
rbnode.ins.induction
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{p : rbnode α → Prop}
(t : rbnode α)
(x : α)
(is_leaf : p rbnode.leaf)
(is_red_lt : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.lt → p a → p (a.red_node y b))
(is_red_eq : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.eq → p (a.red_node y b))
(is_red_gt : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gt → p b → p (a.red_node y b))
(is_black_lt_red : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.lt → a.get_color = rbnode.color.red → p a → p (a.black_node y b))
(is_black_lt_not_red : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.lt → a.get_color ≠ rbnode.color.red → p a → p (a.black_node y b))
(is_black_eq : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.eq → p (a.black_node y b))
(is_black_gt_red : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gt → b.get_color = rbnode.color.red → p b → p (a.black_node y b))
(is_black_gt_not_red : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gt → b.get_color ≠ rbnode.color.red → p b → p (a.black_node y b)) :
p t
theorem
rbnode.is_searchable_balance1
{α : Type u}
(lt : α → α → Prop)
{l : rbnode α}
{y : α}
{r : rbnode α}
{v : α}
{t : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt l lo (option.some y) → rbnode.is_searchable lt r (option.some y) (option.some v) → rbnode.is_searchable lt t (option.some v) hi → rbnode.is_searchable lt (l.balance1 y r v t) lo hi
theorem
rbnode.is_searchable_balance1_node
{α : Type u}
(lt : α → α → Prop)
{t : rbnode α}
[is_trans α lt]
{y : α}
{s : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo (option.some y) → rbnode.is_searchable lt s (option.some y) hi → rbnode.is_searchable lt (t.balance1_node y s) lo hi
theorem
rbnode.is_searchable_balance2
{α : Type u}
(lt : α → α → Prop)
{l : rbnode α}
{y : α}
{r : rbnode α}
{v : α}
{t : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo (option.some v) → rbnode.is_searchable lt l (option.some v) (option.some y) → rbnode.is_searchable lt r (option.some y) hi → rbnode.is_searchable lt (l.balance2 y r v t) lo hi
theorem
rbnode.is_searchable_balance2_node
{α : Type u}
(lt : α → α → Prop)
{t : rbnode α}
[is_trans α lt]
{y : α}
{s : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt s lo (option.some y) → rbnode.is_searchable lt t (option.some y) hi → rbnode.is_searchable lt (t.balance2_node y s) lo hi
theorem
rbnode.is_searchable_ins
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{t : rbnode α}
{x : α}
[is_strict_weak_order α lt]
{lo hi : option α}
(h : rbnode.is_searchable lt t lo hi) :
rbnode.lift lt lo (option.some x) → rbnode.lift lt (option.some x) hi → rbnode.is_searchable lt (rbnode.ins lt t x) lo hi
theorem
rbnode.is_searchable_mk_insert_result
{α : Type u}
(lt : α → α → Prop)
{c : rbnode.color}
{t : rbnode α} :
theorem
rbnode.is_searchable_insert
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{t : rbnode α}
{x : α}
[is_strict_weak_order α lt] :
theorem
rbnode.mem_balance1_node_of_mem_left
{α : Type u}
(lt : α → α → Prop)
{x : α}
{s : rbnode α}
(v : α)
(t : rbnode α) :
rbnode.mem lt x s → rbnode.mem lt x (s.balance1_node v t)
theorem
rbnode.mem_balance2_node_of_mem_left
{α : Type u}
(lt : α → α → Prop)
{x : α}
{s : rbnode α}
(v : α)
(t : rbnode α) :
rbnode.mem lt x s → rbnode.mem lt x (s.balance2_node v t)
theorem
rbnode.mem_balance1_node_of_mem_right
{α : Type u}
(lt : α → α → Prop)
{x : α}
{t : rbnode α}
(v : α)
(s : rbnode α) :
rbnode.mem lt x t → rbnode.mem lt x (s.balance1_node v t)
theorem
rbnode.mem_balance2_node_of_mem_right
{α : Type u}
(lt : α → α → Prop)
{x : α}
{t : rbnode α}
(v : α)
(s : rbnode α) :
rbnode.mem lt x t → rbnode.mem lt x (s.balance2_node v t)
theorem
rbnode.mem_balance1_node_of_incomp
{α : Type u}
(lt : α → α → Prop)
{x v : α}
(s t : rbnode α) :
¬lt x v ∧ ¬lt v x → s ≠ rbnode.leaf → rbnode.mem lt x (s.balance1_node v t)
theorem
rbnode.mem_balance2_node_of_incomp
{α : Type u}
(lt : α → α → Prop)
{x v : α}
(s t : rbnode α) :
¬lt v x ∧ ¬lt x v → s ≠ rbnode.leaf → rbnode.mem lt x (s.balance2_node v t)
theorem
rbnode.ins_ne_leaf
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
(t : rbnode α)
(x : α) :
rbnode.ins lt t x ≠ rbnode.leaf
theorem
rbnode.insert_ne_leaf
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
(t : rbnode α)
(x : α) :
rbnode.insert lt t x ≠ rbnode.leaf
theorem
rbnode.mem_ins_of_incomp
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
(t : rbnode α)
{x y : α}
(h : ¬lt x y ∧ ¬lt y x) :
rbnode.mem lt x (rbnode.ins lt t y)
theorem
rbnode.mem_ins_of_mem
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_weak_order α lt]
{t : rbnode α}
(z : α)
{x : α}
(h : rbnode.mem lt x t) :
rbnode.mem lt x (rbnode.ins lt t z)
theorem
rbnode.mem_mk_insert_result
{α : Type u}
(lt : α → α → Prop)
{a : α}
{t : rbnode α}
(c : rbnode.color) :
rbnode.mem lt a t → rbnode.mem lt a (rbnode.mk_insert_result c t)
theorem
rbnode.mem_of_mem_mk_insert_result
{α : Type u}
(lt : α → α → Prop)
{a : α}
{t : rbnode α}
{c : rbnode.color} :
rbnode.mem lt a (rbnode.mk_insert_result c t) → rbnode.mem lt a t
theorem
rbnode.mem_insert_of_incomp
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
(t : rbnode α)
{x y : α}
(h : ¬lt x y ∧ ¬lt y x) :
rbnode.mem lt x (rbnode.insert lt t y)
theorem
rbnode.mem_insert_of_mem
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_weak_order α lt]
{t : rbnode α}
{x : α}
(z : α) :
rbnode.mem lt x t → rbnode.mem lt x (rbnode.insert lt t z)
theorem
rbnode.of_mem_balance1_node
{α : Type u}
(lt : α → α → Prop)
{x : α}
{s : rbnode α}
{v : α}
{t : rbnode α} :
rbnode.mem lt x (s.balance1_node v t) → rbnode.mem lt x s ∨ ¬lt x v ∧ ¬lt v x ∨ rbnode.mem lt x t
theorem
rbnode.of_mem_balance2_node
{α : Type u}
(lt : α → α → Prop)
{x : α}
{s : rbnode α}
{v : α}
{t : rbnode α} :
rbnode.mem lt x (s.balance2_node v t) → rbnode.mem lt x s ∨ ¬lt x v ∧ ¬lt v x ∨ rbnode.mem lt x t
theorem
rbnode.equiv_or_mem_of_mem_ins
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{t : rbnode α}
{x z : α}
(h : rbnode.mem lt x (rbnode.ins lt t z)) :
strict_weak_order.equiv x z ∨ rbnode.mem lt x t
theorem
rbnode.equiv_or_mem_of_mem_insert
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{t : rbnode α}
{x z : α}
(h : rbnode.mem lt x (rbnode.insert lt t z)) :
strict_weak_order.equiv x z ∨ rbnode.mem lt x t
theorem
rbnode.mem_exact_balance1_node_of_mem_exact
{α : Type u}
{x : α}
{s : rbnode α}
(v : α)
(t : rbnode α) :
rbnode.mem_exact x s → rbnode.mem_exact x (s.balance1_node v t)
theorem
rbnode.mem_exact_balance2_node_of_mem_exact
{α : Type u}
{x : α}
{s : rbnode α}
(v : α)
(t : rbnode α) :
rbnode.mem_exact x s → rbnode.mem_exact x (s.balance2_node v t)
theorem
rbnode.find_balance1_node
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_weak_order α lt]
{x y z : α}
{t s : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo (option.some z) → rbnode.is_searchable lt s (option.some z) hi → rbnode.find lt t y = option.some x → strict_weak_order.equiv y x → rbnode.find lt (t.balance1_node z s) y = option.some x
theorem
rbnode.find_balance2_node
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_weak_order α lt]
{x y z : α}
{s t : rbnode α}
[is_trans α lt]
{lo hi : option α} :
rbnode.is_searchable lt s lo (option.some z) → rbnode.is_searchable lt t (option.some z) hi → rbnode.find lt t y = option.some x → strict_weak_order.equiv y x → rbnode.find lt (t.balance2_node z s) y = option.some x
theorem
rbnode.ite_eq_of_not_lt
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_order α lt]
{a b : α}
{β : Type v}
(t s : β)
(h : lt b a) :
theorem
rbnode.find_ins_of_eqv
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_weak_order α lt]
{x y : α}
{t : rbnode α}
(he : strict_weak_order.equiv x y)
{lo hi : option α}
(hs : rbnode.is_searchable lt t lo hi)
(hlt₁ : rbnode.lift lt lo (option.some x))
(hlt₂ : rbnode.lift lt (option.some x) hi) :
rbnode.find lt (rbnode.ins lt t x) y = option.some x
theorem
rbnode.find_mk_insert_result
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
(c : rbnode.color)
(t : rbnode α)
(x : α) :
rbnode.find lt (rbnode.mk_insert_result c t) x = rbnode.find lt t x
theorem
rbnode.find_insert_of_eqv
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_weak_order α lt]
{x y : α}
{t : rbnode α}
(he : strict_weak_order.equiv x y) :
rbnode.is_searchable lt t option.none option.none → rbnode.find lt (rbnode.insert lt t x) y = option.some x
theorem
rbnode.find_black_eq_find_red
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{l : rbnode α}
{y : α}
{r : rbnode α}
{x : α} :
rbnode.find lt (l.black_node y r) x = rbnode.find lt (l.red_node y r) x
theorem
rbnode.find_red_of_lt
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{l : rbnode α}
{y : α}
{r : rbnode α}
{x : α}
(h : lt x y) :
rbnode.find lt (l.red_node y r) x = rbnode.find lt l x
theorem
rbnode.find_red_of_gt
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_order α lt]
{l : rbnode α}
{y : α}
{r : rbnode α}
{x : α}
(h : lt y x) :
rbnode.find lt (l.red_node y r) x = rbnode.find lt r x
theorem
rbnode.find_red_of_incomp
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{l : rbnode α}
{y : α}
{r : rbnode α}
{x : α}
(h : ¬lt x y ∧ ¬lt y x) :
rbnode.find lt (l.red_node y r) x = option.some y
theorem
rbnode.find_balance1_lt
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{l r t : rbnode α}
{v x y : α}
{lo hi : option α}
(h : lt x y)
(hl : rbnode.is_searchable lt l lo (option.some v))
(hr : rbnode.is_searchable lt r (option.some v) (option.some y))
(ht : rbnode.is_searchable lt t (option.some y) hi) :
rbnode.find lt (l.balance1 v r y t) x = rbnode.find lt (l.red_node v r) x
theorem
rbnode.find_balance1_node_lt
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{t s : rbnode α}
{x y : α}
{lo hi : option α}
(hlt : lt y x)
(ht : rbnode.is_searchable lt t lo (option.some x))
(hs : rbnode.is_searchable lt s (option.some x) hi)
(hne : t ≠ rbnode.leaf . "ins_ne_leaf_tac") :
rbnode.find lt (t.balance1_node x s) y = rbnode.find lt t y
theorem
rbnode.find_balance1_gt
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{l r t : rbnode α}
{v x y : α}
{lo hi : option α}
(h : lt y x)
(hl : rbnode.is_searchable lt l lo (option.some v))
(hr : rbnode.is_searchable lt r (option.some v) (option.some y))
(ht : rbnode.is_searchable lt t (option.some y) hi) :
rbnode.find lt (l.balance1 v r y t) x = rbnode.find lt t x
theorem
rbnode.find_balance1_node_gt
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{t s : rbnode α}
{x y : α}
{lo hi : option α}
(h : lt x y)
(ht : rbnode.is_searchable lt t lo (option.some x))
(hs : rbnode.is_searchable lt s (option.some x) hi)
(hne : t ≠ rbnode.leaf . "ins_ne_leaf_tac") :
rbnode.find lt (t.balance1_node x s) y = rbnode.find lt s y
theorem
rbnode.find_balance1_eqv
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{l r t : rbnode α}
{v x y : α}
{lo hi : option α}
(h : ¬lt x y ∧ ¬lt y x)
(hl : rbnode.is_searchable lt l lo (option.some v))
(hr : rbnode.is_searchable lt r (option.some v) (option.some y))
(ht : rbnode.is_searchable lt t (option.some y) hi) :
rbnode.find lt (l.balance1 v r y t) x = option.some y
theorem
rbnode.find_balance1_node_eqv
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{t s : rbnode α}
{x y : α}
{lo hi : option α}
(h : ¬lt x y ∧ ¬lt y x)
(ht : rbnode.is_searchable lt t lo (option.some y))
(hs : rbnode.is_searchable lt s (option.some y) hi)
(hne : t ≠ rbnode.leaf . "ins_ne_leaf_tac") :
rbnode.find lt (t.balance1_node y s) x = option.some y
theorem
rbnode.find_balance2_lt
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{l : rbnode α}
{v : α}
{r t : rbnode α}
{x y : α}
{lo hi : option α}
(h : lt x y)
(hl : rbnode.is_searchable lt l (option.some y) (option.some v))
(hr : rbnode.is_searchable lt r (option.some v) hi)
(ht : rbnode.is_searchable lt t lo (option.some y)) :
rbnode.find lt (l.balance2 v r y t) x = rbnode.find lt t x
theorem
rbnode.find_balance2_node_lt
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{s t : rbnode α}
{x y : α}
{lo hi : option α}
(h : lt x y)
(ht : rbnode.is_searchable lt t (option.some y) hi)
(hs : rbnode.is_searchable lt s lo (option.some y))
(hne : t ≠ rbnode.leaf . "ins_ne_leaf_tac") :
rbnode.find lt (t.balance2_node y s) x = rbnode.find lt s x
theorem
rbnode.find_balance2_gt
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{l : rbnode α}
{v : α}
{r t : rbnode α}
{x y : α}
{lo hi : option α}
(h : lt y x)
(hl : rbnode.is_searchable lt l (option.some y) (option.some v))
(hr : rbnode.is_searchable lt r (option.some v) hi)
(ht : rbnode.is_searchable lt t lo (option.some y)) :
rbnode.find lt (l.balance2 v r y t) x = rbnode.find lt (l.red_node v r) x
theorem
rbnode.find_balance2_node_gt
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{s t : rbnode α}
{x y : α}
{lo hi : option α}
(h : lt y x)
(ht : rbnode.is_searchable lt t (option.some y) hi)
(hs : rbnode.is_searchable lt s lo (option.some y))
(hne : t ≠ rbnode.leaf . "ins_ne_leaf_tac") :
rbnode.find lt (t.balance2_node y s) x = rbnode.find lt t x
theorem
rbnode.find_balance2_eqv
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{l : rbnode α}
{v : α}
{r t : rbnode α}
{x y : α}
{lo hi : option α}
(h : ¬lt x y ∧ ¬lt y x)
(hl : rbnode.is_searchable lt l (option.some y) (option.some v))
(hr : rbnode.is_searchable lt r (option.some v) hi)
(ht : rbnode.is_searchable lt t lo (option.some y)) :
rbnode.find lt (l.balance2 v r y t) x = option.some y
theorem
rbnode.find_balance2_node_eqv
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{t s : rbnode α}
{x y : α}
{lo hi : option α}
(h : ¬lt x y ∧ ¬lt y x)
(ht : rbnode.is_searchable lt t (option.some y) hi)
(hs : rbnode.is_searchable lt s lo (option.some y))
(hne : t ≠ rbnode.leaf . "ins_ne_leaf_tac") :
rbnode.find lt (t.balance2_node y s) x = option.some y
theorem
rbnode.find_ins_of_disj
{α : Type u}
(lt : α → α → Prop)
[is_strict_weak_order α lt]
[decidable_rel lt]
{x y : α}
{t : rbnode α}
(hn : lt x y ∨ lt y x)
{lo hi : option α}
(hs : rbnode.is_searchable lt t lo hi)
(hlt₁ : rbnode.lift lt lo (option.some x))
(hlt₂ : rbnode.lift lt (option.some x) hi) :
rbnode.find lt (rbnode.ins lt t x) y = rbnode.find lt t y
theorem
rbnode.find_insert_of_disj
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_weak_order α lt]
{x y : α}
{t : rbnode α}
(hd : lt x y ∨ lt y x) :
rbnode.is_searchable lt t option.none option.none → rbnode.find lt (rbnode.insert lt t x) y = rbnode.find lt t y
theorem
rbnode.find_insert_of_not_eqv
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
[is_strict_weak_order α lt]
{x y : α}
{t : rbnode α}
(hn : ¬strict_weak_order.equiv x y) :
rbnode.is_searchable lt t option.none option.none → rbnode.find lt (rbnode.insert lt t x) y = rbnode.find lt t y
- bad_red : ∀ {α : Type u} {c₁ c₂ : rbnode.color} {n : ℕ} {l r : rbnode α} {v : α}, l.is_red_black c₁ n → r.is_red_black c₂ n → (l.red_node v r).is_bad_red_black n
theorem
rbnode.balance1_rb
{α : Type u}
{l r t : rbnode α}
{y v : α}
{c_l c_r c_t : rbnode.color}
{n : ℕ} :
l.is_red_black c_l n → r.is_red_black c_r n → t.is_red_black c_t n → (∃ (c : rbnode.color), (l.balance1 y r v t).is_red_black c n.succ)
theorem
rbnode.balance2_rb
{α : Type u}
{l r t : rbnode α}
{y v : α}
{c_l c_r c_t : rbnode.color}
{n : ℕ} :
l.is_red_black c_l n → r.is_red_black c_r n → t.is_red_black c_t n → (∃ (c : rbnode.color), (l.balance2 y r v t).is_red_black c n.succ)
theorem
rbnode.balance1_node_rb
{α : Type u}
{t s : rbnode α}
{y : α}
{c : rbnode.color}
{n : ℕ} :
t.is_bad_red_black n → s.is_red_black c n → (∃ (c : rbnode.color), (t.balance1_node y s).is_red_black c n.succ)
theorem
rbnode.balance2_node_rb
{α : Type u}
{t s : rbnode α}
{y : α}
{c : rbnode.color}
{n : ℕ} :
t.is_bad_red_black n → s.is_red_black c n → (∃ (c : rbnode.color), (t.balance2_node y s).is_red_black c n.succ)
Equations
- t.ins_rb_result rbnode.color.black n = ∃ (c : rbnode.color), t.is_red_black c n
- t.ins_rb_result rbnode.color.red n = t.is_bad_red_black n
theorem
rbnode.of_get_color_eq_red
{α : Type u}
{t : rbnode α}
{c : rbnode.color}
{n : ℕ} :
t.get_color = rbnode.color.red → t.is_red_black c n → c = rbnode.color.red
theorem
rbnode.of_get_color_ne_red
{α : Type u}
{t : rbnode α}
{c : rbnode.color}
{n : ℕ} :
t.get_color ≠ rbnode.color.red → t.is_red_black c n → c = rbnode.color.black
theorem
rbnode.ins_rb
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{t : rbnode α}
(x : α)
{c : rbnode.color}
{n : ℕ}
(h : t.is_red_black c n) :
(rbnode.ins lt t x).ins_rb_result c n
Equations
- t.insert_rb_result rbnode.color.black n = ∃ (c : rbnode.color), t.is_red_black c n
- t.insert_rb_result rbnode.color.red n = t.is_red_black rbnode.color.black n.succ
theorem
rbnode.insert_rb
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{t : rbnode α}
(x : α)
{c : rbnode.color}
{n : ℕ}
(h : t.is_red_black c n) :
(rbnode.insert lt t x).insert_rb_result c n
theorem
rbnode.insert_is_red_black
{α : Type u}
(lt : α → α → Prop)
[decidable_rel lt]
{t : rbnode α}
{c : rbnode.color}
{n : ℕ}
(x : α) :
t.is_red_black c n → (∃ (c : rbnode.color) (n : ℕ), (rbnode.insert lt t x).is_red_black c n)