English
Defines a hierarchy of operations h(n,m,k) with base cases: h(0,m,k)=k+1, h(1,m,0)=m, h(2,m,0)=0, h(n+3,m,0)=1, and recursive step h(n+1,m,k+1)=h(n,m,h(n+1,m,k)).
Русский
Определяет иерархию операций h(n,m,k) со следующими базовыми случаями: h(0,m,k)=k+1, h(1,m,0)=m, h(2,m,0)=0, h(n+3,m,0)=1, рекурсивный шаг: h(n+1,m,k+1)=h(n,m,h(n+1,m,k)).
LaTeX
$$$\begin{aligned} &\text{def } \text{hyperoperation} : \mathbb{N} \to \mathbb{N} \to \mathbb{N} \to \mathbb{N} \\ &\text{with } \\ &\text{hyperoperation}(0,m,k) = k+1, \\ &\text{hyperoperation}(1,m,0) = m, \\ &\text{hyperoperation}(2,m,0) = 0, \\ &\text{hyperoperation}(n+3,m,0) = 1, \\ &\text{hyperoperation}(n+1,m,k+1) = \text{hyperoperation}(n,m,\text{hyperoperation}(n+1,m,k)). \end{aligned}$$$
Lean4
/-- Implementation of the hyperoperation sequence
where `hyperoperation n m k` is the `n`th hyperoperation between `m` and `k`.
-/
def hyperoperation : ℕ → ℕ → ℕ → ℕ
| 0, _, k => k + 1
| 1, m, 0 => m
| 2, _, 0 => 0
| _ + 3, _, 0 => 1
| n + 1, m, k + 1 => hyperoperation n m (hyperoperation (n + 1) m k)
