English
The comparison between veBl en values satisfies a recursive rule depending on the comparison of the first arguments.
Русский
Сравнение значений veBl en удовлетворяет рекурсивному правилу, зависящему от сравнения первых аргументов.
LaTeX
$$$$\\operatorname{cmp}(\\operatorname{veblen}(o_1,a), \\operatorname{veblen}(o_2,b)) = \\begin{cases} \\operatorname{cmp}(a,b), & o_1 = o_2 \\\\ \\operatorname{cmp}(a, \\operatorname{veblen}(o_2,b)), & o_1 < o_2 \\\\ \\operatorname{cmp}(\\operatorname{veblen}(o_1,a), b), & o_1 > o_2 \\end{cases}.$$$$
Lean4
theorem cmp_veblen :
cmp (veblen o₁ a) (veblen o₂ b) =
match cmp o₁ o₂ with
| .eq => cmp a b
| .lt => cmp a (veblen o₂ b)
| .gt => cmp (veblen o₁ a) b :=
cmp_veblenWith (isNormal_opow one_lt_omega0)
