English
There exists a computable encoding encodeCode: Code → ℕ which assigns a unique natural number to each Code by cases: zero→0, succ→1, left→2, right→3, and for pair, comp, prec, rfind'.
Русский
Существует вычислимое кодирование encodeCode: Code → ℕ, которое сопоставляет каждому коду уникальное натуральное число по правилам: zero→0, succ→1, left→2, right→3, далее для pair, comp, prec, rfind'.
LaTeX
$$$\\operatorname{encodeCode} : \\text{Code} \\to \\mathbb{N}, \\quad \\mathrm{encodeCode}(\\mathrm{zero}) = 0, \\mathrm{encodeCode}(\\mathrm{succ}) = 1, \\mathrm{encodeCode}(\\mathrm{left}) = 2, \\mathrm{encodeCode}(\\mathrm{right}) = 3, \\mathrm{encodeCode}(\\mathrm{pair}(cf,cg)) = 2(2\\,\\mathrm{encodeCode}(cf)\\,\\mathrm{encodeCode}(cg)) + 4, \\mathrm{encodeCode}(\\mathrm{comp}(cf,cg)) = 2(2\\,\\mathrm{encodeCode}(cf)\\, (\\mathrm{encodeCode}(cg) + 1)) + 4, \\mathrm{encodeCode}(\\mathrm{prec}(cf,cg)) = (2(2\\,\\mathrm{encodeCode}(cf)\\,\\mathrm{encodeCode}(cg)) + 1) + 4, \\mathrm{encodeCode}(\\mathrm{rfind}'(cf)) = (2(2\\,\\mathrm{encodeCode}(cf) + 1) + 1) + 4$$$
Lean4
/-- An encoding of a `Nat.Partrec.Code` as a ℕ. -/
def encodeCode : Code → ℕ
| zero => 0
| succ => 1
| left => 2
| right => 3
| pair cf cg => 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
| comp cf cg => 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg) + 1) + 4
| prec cf cg => (2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 1) + 4
| rfind' cf => (2 * (2 * encodeCode cf + 1) + 1) + 4
