ただ、現時点での問題として、F[ε0](ω)が
どの形の順序数で表されるかが問題になっています。
例えばF[1](x) = x + 1として、
F[ω](x) = x*2
F[ω*2](x) = x*2^x
F[ω*3](x) = ( ... (x*2^x)* ... )*2^(x*2^( ... (x*2^x) ...)) > x*2^^x
F[ω*2^ω](x) >= F[ω*ω](x) >= 2^^ ... ^^x = ak(2, x, x)
となり、途中で2^xとか2^2^ ... 2^xが出てくるところが曲者です。
今はF[λ(2^ω)](x) = F[λ(2^x)](x)としているところです。