Embedding EBOCF → EWBOCF
0 1 2 ω (<0,<0,0>>,<0,<0,0>>) ψ_0(ω) ψ_0(ω+1) <0,<<0,0>,0>> ψ_0(ψ_1(0)+ψ_0(ψ_1(0))) ψ_0(ψ_1(ω)) ψ_0(ψ_2(0)) ψ_0(ψ_ω(0)) ψ_0(ψ_ψ_0(ψ_1(0))(0)) ψ_0(ψ_ψ_1(0)(0)) ψ_0(ψ_ψ_ω(0)(0)) ψ_0(ψ_ψ_ψ_1(0)(0)(0))
Abbreviate:
(0,0)→1
(0,1)→ω
((0,0),y)→(1,y)
((0,1),y)→(ω,y)
Use ψ:
Implements an
embedding
from
Extended Buchholz's function
to
Extended Weak Buchholz's function
.
Last updated: 2022/04/12