English
Define split' by recursion: split'(0) = (0,0); split'(oadd e n a) = if e = 0 then (0,n) else let (a',m) := split' a in (oadd (e-1) n a', m).
Русский
Определение split' по рекурсии: split'(0) = (0,0); split'(oadd e n a) = если e=0, то (0,n), иначе разложение a = (a', m) и возвращаем (oadd (e-1) n a', m).
LaTeX
$$$\\text{split'}(0)=(0,0),\\qquad \\text{split'}(oadd\, e\, n\, a) = \\begin{cases} (0,n), & e=0,\\\\ (oadd (e-1)\, n\, a', m), & \\text{where } (a',m)=\\text{split'}(a). \\end{cases}$$$
Lean4
/-- Calculate division and remainder of `o` mod `ω`:
`split' o = (a, n)` means `o = ω * a + n`. -/
def split' : ONote → ONote × ℕ
| 0 => (0, 0)
| oadd e n a =>
if e = 0 then (0, n)
else
let (a', m) := split' a
(oadd (e - 1) n a', m)
