rotateL_size — Mathlib

English

If r is sized, then size(rotateL(l, x, r)) = size(l) + size(r) + 1.

Русский

Пусть r ограничено по размеру; тогда размер rotateL(l, x, r) равен size(l) + size(r) + 1.

LaTeX

$$\operatorname{Sized}(r) \Rightarrow \operatorname{size}(\mathrm{rotateL}(l, x, r)) = \operatorname{size}(l) + \operatorname{size}(r) + 1$$

Lean4

theorem rotateL_size {l x r} (hm : Sized r) : size (@Ordnode.rotateL α l x r) = size l + size r + 1 :=
  by
  cases r <;> simp [Ordnode.rotateL]
  simp only [hm.1]
  split_ifs <;> simp [node3L_size, node4L_size hm.2.1] <;> abel

Похожие утверждения