English
Let l, x, r be two valid subtrees; if H1, H2, H3 hold, then rotateR yields a valid configuration.
Русский
Пусть существуют два допустимых поддерева l и r; если выполняются условия H1, H2, H3, то rotateR даёт корректную конфигурацию.
LaTeX
$$$ \forall l,x,r \in \mathcal{O},\ H_1,H_2,H_3 \Rightarrow \mathrm{Valid}'(o_1, (l.rotateR\ x\ r))\, o_2 $$$
Lean4
theorem rotateR {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂) (H1 : ¬size l + size r ≤ 1)
(H2 : delta * size r < size l) (H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3) : Valid' o₁ (@rotateR α l x r) o₂ :=
by
refine Valid'.dual_iff.2 ?_
rw [dual_rotateR]
refine hr.dual.rotateL hl.dual ?_ ?_ ?_
· rwa [size_dual, size_dual, add_comm]
· rwa [size_dual, size_dual]
· rwa [size_dual, size_dual]
