English
Let o1, o2 be contexts, with two subtrees of sizes ls and rs, and suppose hl and hr certify their validity. If h is a balance condition delta·ls < rs, and t is a valid subtree with size ls + size(rl), then the left-balanced merge produces a valid subtree with size ls + rs.
Русский
Пусть o1, o2 — контексты, два поддерева имеют размеры ls и rs, допустимость доказана hl и hr. При условии баланса delta·ls < rs и t валидно, размером t = ls + size(rl), левостороннее сбалансированное слияние даёт валидное поддерево размером ls + rs.
LaTeX
$$$\\forall o_1,o_2, ls, ll, lx, lr, rs, rl, rx, rr, t,\\ hl:\\mathrm{Valid}'(o_1(\\mathrm{node}\\;ls\\;ll\\;lx\\;lr)\\,o_2)\\ \\to\\ \\mathrm{Valid}'(o_1(\\mathrm{node}\\;rs\\;rl\\;rx\\;rr)\\,o_2)\\ \\to\\ h: \\delta \\cdot ls < rs \\to\\ v: \\mathrm{Valid}'(o_1\\,t\\,rx)\\to\\ e: |t| = ls + |rl| \\Rightarrow\\ \\mathrm{Valid}'(o_1(t.balanceL\\;rx\\;rr))\\;o_2 \\land |t.balanceL\\;rx\\;rr| = ls + rs$$$
Lean4
theorem merge_aux₁ {o₁ o₂ ls ll lx lr rs rl rx rr t} (hl : Valid' o₁ (@Ordnode.node α ls ll lx lr) o₂)
(hr : Valid' o₁ (.node rs rl rx rr) o₂) (h : delta * ls < rs) (v : Valid' o₁ t rx) (e : size t = ls + size rl) :
Valid' o₁ (.balanceL t rx rr) o₂ ∧ size (.balanceL t rx rr) = ls + rs :=
by
rw [hl.2.1] at e
rw [hl.2.1, hr.2.1, delta] at h
rcases hr.3.1 with (H | ⟨hr₁, hr₂⟩); · cutsat
suffices H₂ : _
by
suffices H₁ : _ by
refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
· rw [e]; exact Or.inl (Valid'.merge_lemma h hr₁)
· rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
abel
· rw [e, add_right_comm]; rintro ⟨⟩
intro _ _; rw [e]; unfold delta at hr₂ ⊢; cutsat
