no goals
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
h : WF cmp t
⊢ Ordered cmp t ∧ ∃ c n, Balanced t c n
induction h with
| mk o h => exact ⟨o, _, _, h⟩
| insert _ ih => have ⟨o, _, _, h⟩ := ih; exact ⟨o.insert, h.insert⟩
| erase _ ih => have ⟨o, _, _, h⟩ := ih; exact ⟨o.erase, _, h.erase⟩
no goals
case mk
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
c✝ : RBColor
n✝ : Nat
o : Ordered cmp t✝
h : Balanced t✝ c✝ n✝
⊢ Ordered cmp t✝ ∧ ∃ c n, Balanced t✝ c n
exact ⟨o, _, _, h⟩
case insert
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
a✝¹ : α
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, Balanced t✝ c n
o : Ordered cmp t✝
w✝¹ : RBColor
w✝ : Nat
h : Balanced t✝ w✝¹ w✝
⊢ Ordered cmp (RBNode.insert cmp t✝ a✝¹) ∧ ∃ c n, Balanced (RBNode.insert cmp t✝ a✝¹) c n
case insert
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
a✝¹ : α
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, Balanced t✝ c n
⊢ Ordered cmp (RBNode.insert cmp t✝ a✝¹) ∧ ∃ c n, Balanced (RBNode.insert cmp t✝ a✝¹) c n
have ⟨o, _, _, h⟩ := ih
no goals
case insert
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
a✝¹ : α
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, Balanced t✝ c n
o : Ordered cmp t✝
w✝¹ : RBColor
w✝ : Nat
h : Balanced t✝ w✝¹ w✝
⊢ Ordered cmp (RBNode.insert cmp t✝ a✝¹) ∧ ∃ c n, Balanced (RBNode.insert cmp t✝ a✝¹) c n
exact ⟨o.insert, h.insert⟩
case erase
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
cut✝ : α → Ordering
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, Balanced t✝ c n
o : Ordered cmp t✝
w✝¹ : RBColor
w✝ : Nat
h : Balanced t✝ w✝¹ w✝
⊢ Ordered cmp (RBNode.erase cut✝ t✝) ∧ ∃ c n, Balanced (RBNode.erase cut✝ t✝) c n
case erase
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
cut✝ : α → Ordering
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, Balanced t✝ c n
⊢ Ordered cmp (RBNode.erase cut✝ t✝) ∧ ∃ c n, Balanced (RBNode.erase cut✝ t✝) c n
have ⟨o, _, _, h⟩ := ih
no goals
case erase
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
cut✝ : α → Ordering
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, Balanced t✝ c n
o : Ordered cmp t✝
w✝¹ : RBColor
w✝ : Nat
h : Balanced t✝ w✝¹ w✝
⊢ Ordered cmp (RBNode.erase cut✝ t✝) ∧ ∃ c n, Balanced (RBNode.erase cut✝ t✝) c n
exact ⟨o.erase, _, h.erase⟩