English
If a tree is valid, then after erasing the maximum element and taking duals, the structure remains valid with a size relation between the original and erased trees.
Русский
Если дерево валидно, то после удаления максимального элемента и применения двойности структура остается валидной и соблюдается размерная зависимость между исходным и удаленным деревом.
LaTeX
$$$\\forall s l x r o_1 o_2,\\; \\mathrm{Valid'} o_1 (\\mathrm{node}~s~l~x~r) o_2 \\Rightarrow \\mathrm{Valid'} o_1 (l.eraseMax).eraseMax o_2 \\land \\mathrm{size}(\\mathrm{node}~l~x~r) = \\mathrm{size}(\\mathrm{eraseMax} (\\mathrm{node}~l~x~r)) + 1$$$
Lean4
theorem eraseMax_aux {s l x r o₁ o₂} (H : Valid' o₁ (.node s l x r) o₂) :
Valid' o₁ (@eraseMax α (.node' l x r)) ↑(findMax' x r) ∧ size (.node' l x r) = size (eraseMax (.node' l x r)) + 1 :=
by
have := H.2.eq_node'; rw [this] at H; clear this
induction r generalizing l x o₁ with
| nil => exact ⟨H.left, rfl⟩
| node rs rl rx rr _ IHrr =>
have := H.2.2.2.eq_node'; rw [this] at H ⊢
rcases IHrr H.right with ⟨h, e⟩
refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩
rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)]
rw [size_node, e]; rfl
