>>350
> Seq の定義は、定義式の数を減らすため、>>347 の定義と微妙に変えてあります。

C0(Ｘ, B, □, a) = lim { 初項 a / 2項目以降 C0(X, B_n, 1個前の項, □) }

といった感じですか？

どうしてこれが順序数の収束列になるのかがまだよく分かりませんが、
もう少しよく考えてみます。