English
Let l, x, r be trees with Balanced l and Balanced r and suitable size constraints. Under the hypothesis H about possible lifts, the balance operation balanceR(l, x, r) equals balance'(l, x, r).
Русский
Пусть l, x, r — деревья с допустимым балансом для l и r и подходящими размерами. При условии H о возможных подъёмах операция balanceR(l, x, r) равна balance'(l, x, r).
LaTeX
$$$\forall l\ x\ r,\ hl:\ Balanced\ l\ ∧ hr:\ Balanced\ r\ ∧ sl:\ Sized\ l\ ∧ sr:\ Sized\ r\ ∧ H,\ balanceR\ l\ x\ r = balance'\ l\ x\ r$$$
Lean4
theorem balanceR_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r)
(H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
@balanceR α l x r = balance' l x r := by
rw [← dual_dual (balanceR l x r), dual_balanceR,
balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance', dual_dual]
