English
Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in `opow`, where the form of the output depends on the structure of the input pair, including cases for (0,0), (0,1), and (0,m+1) and (a, m).
Русский
Дополнительное определение для вычисления ординальной нотации показательной функции `opow` в зависимости от структуры входной пары, включая случаи (0,0), (0,1), (0,m+1) и (a,m).
LaTeX
$$$\text{opowAux2}: ONote \to (ONote \times \mathbb{N}) \to ONote$;\quad \text{определение по образцам}。$$
Lean4
/-- Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in `opow` -/
def opowAux2 (o₂ : ONote) (o₁ : ONote × ℕ) : ONote :=
match o₁ with
| (0, 0) => if o₂ = 0 then 1 else 0
| (0, 1) => 1
| (0, m + 1) =>
let (b', k) := split' o₂
oadd b' (m.succPNat ^ k) 0
| (a@(oadd a0 _ _), m) =>
match split o₂ with
| (b, 0) => oadd (a0 * b) 1 0
| (b, k + 1) =>
let eb := a0 * b
scale (eb + mulNat a0 k) a + opowAux eb a0 (mulNat a m) k m
