形式化大数数学（1.2-Veblen函数）二 (2-2)

φ-α-β-suc {α = lim _} {β = lim _} = refl

φ-α-β-lim : φ α β (lim h) ≡ jump λ δ → lim λ n → φ α β (h n) δ

φ-α-β-lim {α = zero} {β = zero} = refl

φ-α-β-lim {α = zero} {β = suc _} = refl

φ-α-β-lim {α = zero} {β = lim _} = refl

φ-α-β-lim {α = suc _} {β = zero} = refl

φ-α-β-lim {α = suc _} {β = suc _} = refl

φ-α-β-lim {α = suc _} {β = lim _} = refl

φ-α-β-lim {α = lim _} {β = zero} = refl

φ-α-β-lim {α = lim _} {β = suc _} = refl

φ-α-β-lim {α = lim _} {β = lim _} = refl

例 一个很大的大数：

ₒₒₘ₂：＝fφΓ₀，₀，₀ (0) (99)

oom₂ = FGH.f (QuaternaryVeblen.φ (BinaryVeblen.Γ 0) 0 0 0) 99

本文使用 WPL/s 发布 @GitHub

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。