ユーザーブログ:Hexirp/解析 (i LoVe Ordinal)

えのき氏により投稿された i LoVe Ordinal を解析します。定義は https://twitter.com/enoki_fugue/status/1227166763453947904 とします。

定義

定義をここに書き下す。一部改変しているが重要な部分はそのままである。

花を定義する。

• \( 0 \) は花である。
• \( [ ] \) は花である。これは便宜上 2 行 0 列の行列である。
• \( A \) と \( B \) が花であるとき \( A \oplus B \) は花である。
  • \( A \) が花であるとき、それと \( A \oplus 0 \) は花として等しい。
• \( A _ 1, A _ 2, \ldots, A _ n \) と \( B _ 1, B _ 2, \ldotp. B _ n \) が花ならば、この 2 行 n 列の行列 \( \left[ \begin{matrix} A _ 1 & A _ 2 & \cdots & A _ n \\ B _ 1 & B _ 2 & \cdots & B _ n \\ \end{matrix} \right] \) は花である。
  • 下の行の要素が \( 0 \) である場合、その列を削除しても花として等しい（逆も同様）。

関数 \( X \mapsto X' \) を定義する。まず、ここだけ定数として \( m \) を固定する。これは成長度と呼ぶ。

• \( X \) を花とする。
  • \( X = 0 \) であれば、 \( X' \) は未定義である。
  • \( X = [ ] \) であれば、 \( X' = 0 \) である。
  • \( X = A \oplus B \) であれば、 \( X' = A \oplus B' \) である。
  • \( X = \left[ \begin{matrix} 0 \\ B _ 1 \\ \end{matrix} \right] \) であれば、 \( X' = f ^ m ( 0 ) \) である。
    • ただし、 \( f ( Y ) = \left[ \begin{matrix} 0 \\ { B _ 1 }' \\ \end{matrix} \right] \oplus Y \) である。
  • \( X = \left[ \begin{matrix} A _ 1 & A _ 2 & \cdots & A _ n & 0 \\ B _ 1 & B _ 2 & \cdots & B _ n & B _ { n + 1 } \\ \end{matrix} \right] \) であれば、 \( X' = g ^ m ( B _ { n + 1 } ) \) である。
    • ただし、 \( g ( Y ) = \left[ \begin{matrix} A _ 1 & A _ 2 & \cdots & A _ n & { A _ n }' \\ B _ 1 & B _ 2 & \cdots & { B _ n }' & Y \\ \end{matrix} \right] \) である。

花 \( X \) と成長度 \( m \) の対を植木鉢 \( ( X, m ) \) とする

関数 \( ( X, m ) \mapsto { ( X, m ) } ^ * \) を定義する。

• \( ( X, m ) \) を植木鉢とする。
  • \( X = 0 \) であれば、 \( { ( X, m ) } ^ * = m \) である。
  • \( X \neq 0 \) であれば、 \( { ( X, m ) } ^ * = ( X', m + 1 ) \) である。

ここからも定義は続くが、必要な部分だけに限ることにする。

順序数表記

上記の定義には不完全な部分が多くある。それを完全な物にするために書き直す。なお、ここでは自然数には 0 が含まれるものとする。ちなみに、この順序数表記は「加算列と単項の相互再帰」「悪い非標準形を取り除くための比較関数との相互再帰」などの独自の手法を使っているため、スタンダードな定義の仕方ではない。

\( T _ \varphi \) と \( T _ \oplus \) と \( \_ < _ \varphi \_ \) と \( \_ < _ \oplus \_ \) を相互再帰により定義する。 \( T _ \oplus \) のルールにより項が組み立てられるたびに一つ増えるような指標を考えると、その指標が減少していくことにより、無限再帰にならないことが分かる。

\( T _ \varphi \) を定義する。

• 任意の自然数 \( n \) を取る。 \( A _ 0, A _ 1, \ldots, A _ n \in T _ \oplus \) と \( B _ 0, B _ 1, \ldots, B _ n \in T _ \oplus \) を取る。 \( A _ 0 > _ \oplus A _ 1 > _ \oplus \cdots > _ \oplus A _ n \) であるとする。 \( A _ n = 0 \) であるとする。このとき、 \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ n \\ B _ 0 & B _ 1 & \cdots & B _ n \\ \end{matrix} \right) \in T _ \varphi \) である。

\( T _ \oplus \) を定義する。

• \( 0 \in T _ \oplus \) である。
• \( X _ v \in T _ \varphi \) を取る。 \( X _ s \in T _ \oplus \) を取る。 \( X _ v \gg X _ s \) であるとする。このとき、 \( X _ v \oplus X _ s \in T _ \oplus \) である。
  • ただし、 \( X \gg Y \) は以下のように定義する。
  • \( Y \) の項の形で場合分けする。
  • \( Y = 0 \) であるとき、
    • \( X \gg Y \) である。
  • \( Y = Y _ v \oplus Y _ s \) であるとき、
    • \( X \ge _ \varphi Y _ v \) かつ \( X \gg Y _ s \) であれば、 \( X \gg Y \) である。

\( T _ \oplus \) に関する略記を定義する。これらは紛れがない時のみである。

• \( A \oplus 0 \) を \( A \) と略記してもよい。
  • ゆえに \( A _ 1 \oplus A _ 2 \oplus \cdots A _ n \oplus 0 \) を \( A _ 1 \oplus A _ 2 \oplus \cdots A _ n \) と略記してもよい。

\( \_ < _ \varphi \_ \) と \( \_ < _ \oplus \_ \) を相互再帰により定義する。

\( \_ < _ \varphi \_ \) を定義する。そのために比較演算子 \( \_ \sim _ \varphi \_ \) を定義する。この比較演算子の返り値は \( L \) と \( G \) と \( E \) の三種であり、それぞれ \( \_ < \_ \) と \( \_ > \_ \) と \( \_ = \_ \) に対応している。

• \( X, Y \in T _ \varphi \) を取る。
• \( X \) の行の長さを \( m \) とする。
• \( Y \) の行の長さを \( n \) とする。
• \( X = \left( \begin{matrix} A _ 0 ( X ) & A _ 1 ( X ) & \cdots & A _ { m - 1 } ( X ) \\ B _ 0 ( X ) & B _ 1 ( X ) & \cdots & B _ { m - 1 } ( X ) \\ \end{matrix} \right) \) とする。
• \( Y = \left( \begin{matrix} A _ 0 ( Y ) & A _ 1 ( Y ) & \cdots & A _ { n - 1 } ( Y ) \\ B _ 0 ( Y ) & B _ 1 ( Y ) & \cdots & B _ { n - 1 } ( Y ) \\ \end{matrix} \right) \) とする。
• \( m \) と \( n \) の値で場合分けする。
• \( m = 1 \) かつ \( n = 1 \) のとき、
  • \( A _ 0 ( X ) \sim _ \oplus A _ 0 ( Y ) \) の値で場合分けする。
  • \( L \) のとき、
    • あり得ない状態である。
  • \( G \) のとき、
    • あり得ない状態である。
  • \( E \) のとき、
    • \( X \sim _ \varphi Y \) の値は \( B _ 0 ( X ) \sim _ \oplus B _ 0 ( Y ) \) の値と等しい。
• \( m = 1 \) かつ \( n > 1 \) のとき、
  • \( A _ 0 ( X ) \sim _ \oplus A _ 0 ( Y ) \) の値で場合分けする。
  • \( L \) のとき、
    • \( X \sim _ \varphi Y \) の値は \( B _ 0 ( X ) \sim _ \oplus Y \oplus 0 \) の値と等しい。
  • \( G \) のとき、
    • あり得ない状態である。
  • \( E \) のとき、
    • あり得ない状態である。
• \( m > 1 \) かつ \( n = 1 \) のとき、
  • \( A _ 0 ( X ) \sim _ \oplus A _ 0 ( Y ) \) の値で場合分けする。
  • \( L \) のとき、
    • あり得ない状態である。
  • \( G \) のとき、
    • \( X \sim _ \varphi Y \) の値は \( X \oplus 0 \sim _ \oplus B _ 0 ( Y ) \) の値と等しい。
  • \( E \) のとき、
    • あり得ない状態である。
• \( m > 1 \) かつ \( n > 1 \) のとき、
  • \( A _ 0 ( X ) \sim _ \oplus A _ 0 ( Y ) \) の値で場合分けする。
  • \( L \) のとき、
    • \( X \sim _ \varphi Y \) の値は \( B _ { m - 1 } ( X ) \sim _ \oplus Y \oplus 0 \) の値と等しい。
  • \( G \) のとき、
    • \( X \sim _ \varphi Y \) の値は \( X \oplus 0 \sim _ \oplus B _ { n - 1 } ( Y ) \) の値と等しい。
  • \( E \) のとき、
    • \( B _ 0 ( X ) \sim _ \oplus B _ 0 ( Y ) \) の値で場合分けする。
    • \( L \) のとき、
      • \( X \sim _ \varphi Y \) の値は \( B _ { m - 1 } ( X ) \sim _ \oplus Y \oplus 0 \) の値と等しい。
    • \( G \) のとき、
      • \( X \sim _ \varphi Y \) の値は \( X \oplus 0 \sim _ \oplus B _ { n - 1 } ( Y ) \) の値と等しい。
    • \( E \) のとき、
      • \( X \sim _ \varphi Y \) の値は \( \left( \begin{matrix} A _ 1 ( X ) & \cdots & A _ { m - 1 } ( X ) \\ B _ 1 ( X ) & \cdots & B _ { m - 1 } ( X ) \\ \end{matrix} \right) \sim _ \varphi \left( \begin{matrix} A _ 1 ( Y ) & \cdots & A _ { n - 1 } ( Y ) \\ B _ 1 ( Y ) & \cdots & B _ { n - 1 } ( Y ) \\ \end{matrix} \right) \) の値と等しい。

\( \_ < _ \oplus \_ \) を定義する。そのために比較演算子 \( \_ \sim _ \oplus \_ \) を定義する。

• \( X, Y \in T _ \oplus \) を取る。
• \( X \) と \( Y \) の項の形で場合分けする。
• \( X = 0 \) かつ \( Y = 0 \) のとき、
  • \( X \sim _ \oplus Y \) の値は \( E \) と等しい。
• \( X = 0 \) かつ \( Y = Y _ v \oplus Y _ s \) のとき、
  • \( X \sim _ \oplus Y \) の値は \( L \) と等しい。
• \( X = X _ v \oplus X _ s \) かつ \( Y = 0 \) のとき、
  • \( X \sim _ \oplus Y \) の値は \( G \) と等しい。
• \( X = X _ v \oplus X _ s \) \( Y = Y _ v \oplus Y _ s \) のとき、
  • \( X _ v \sim _ \varphi Y _ v \) を比較する。
  • \( L \) のとき、
    • \( X \sim _ \oplus Y \) の値は \( L \) と等しい。
  • \( G \) のとき、
    • \( X \sim _ \oplus Y \) の値は \( G \) と等しい。
  • \( E \) のとき、
    • \( X \sim _ \oplus Y \) の値は \( X _ s \sim _ \oplus Y _ s \) の値と等しい。

\( O _ \varphi \) と \( O _ \oplus \) を相互再帰で定義する。

\( O _ \varphi \) を定義する。

• \( X \in T _ \varphi \) を取る。 \( X = \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ n \\ B _ 0 & B _ 1 & \cdots & B _ n \\ \end{matrix} \right) \) とする。 \( B _ 0, B _ 1, \ldots B _ n < _ \oplus X \oplus 0 \) であるとする。このとき、 \( X \in O _ \varphi \) である。

\( O _ \oplus \) を定義する。

• \( X \in T _ \oplus \) を取る。このとき、 \( X \in O _ \oplus \) である。

順序数表記を以下のように構築する。

• 項 \( \mathrm{T} \) は \( T _ \oplus \) である。
• 順序 \( \_ < \_ \) は \( \_ < _ \oplus \_ \) である。
• 標準形 \( \mathrm{OT} \) は \( O _ \oplus \) である。

基本列

順序数の形を判定する関数を定義する。ここで判定結果は、 \( O \) と \( S \) と \( L \) であり、それぞれゼロと後続順序数と可算濃度の極限順序数に対応する。

\( j _ \varphi ( \_ ) \) を定義する。

• \( X \in T _ \varphi \) を取る。
• \( X \) の行の長さを \( m \) とする。
• \( X = \left( \begin{matrix} A _ 0 ( X ) & A _ 1 ( X ) & \cdots & A _ { m - 1 } ( X ) \\ B _ 0 ( X ) & B _ 1 ( X ) & \cdots & B _ { m - 1 } ( X ) \\ \end{matrix} \right) \) とする。
• \( m \) の値で場合分けする。
• \( m = 1 \) のとき、
  • \( B _ 0 ( X ) \) の項の形で場合分けする。
  • \( B _ 0 ( X ) = 0 \) のとき、
    • \( j _ \varphi ( X ) \) の値は \( S \) である。
  • \( B _ 0 ( X ) = \_ \oplus \_ \) のとき、
    • \( j _ \varphi ( X ) \) の値は \( L \) である。
• \( m > 1 \) のとき、
  • \( j _ \varphi ( X ) \) の値は \( L \) である。

\( j _ \oplus ( \_ ) \) を定義する。

• \( X \in T _ \oplus \) を取る。
• \( X \) の項の形で場合分けする。
• \( 0 \) のとき、
  • \( j _ \oplus ( X ) \) の値は \( O \) である。
• \( X = X _ v \oplus X _ s \) のとき、
  • \( j ( X _ s ) \) の値で場合分けする。
  • \( O \) のとき、
    • \( j _ \oplus ( X ) \) の値は \( j _ \varphi ( X _ v ) \) の値に等しい。
  • \( S \) のとき、
    • \( j _ \oplus ( X ) \) の値は \( S \) である。
  • \( L \) のとき、
    • \( j _ \oplus ( X ) \) の値は \( L \) である。

基本列を求める関数を三つに分けて定義する。

ゼロに対する基本列は空関数により定められる。

後続順序数に対する基本列は \( X \mapsto X ^ - \) により定められる。

• \( X \in T _ \oplus \) を取る。
• \( X \) の項の形により場合分けする。
• \( X = 0 \) のとき、
  • \( X ^ - \) の値は \( 0 \) である。
• \( X = X _ v \oplus X _ s \) のとき、
  • \( X ^ - \) の値は \( \mathrm{init} ( X _ v, X _ s ) \) である。
    • ただし、 \( ( X, Y ) \mapsto \mathrm{init} ( X, Y ) \) は以下のように定義される関数である。
    • \( Y \) の項の形で場合分けする。
    • \( Y = 0 \) のとき、
      • \( \mathrm{init} ( X, Y ) \) の値は \( 0 \) である。
    • \( Y = Y _ v \oplus Y _ s \) のとき、
      • \( \mathrm{init} ( X, Y ) \) の値は \( X \oplus \mathrm{init} ( Y _ v, Y _ s ) \) である。

可算濃度の極限順序数に対する基本列は \( ( X, n ) \mapsto X [ n ] \) により定められる。元々の定義と比べて非常に長大であるが、「非標準形を同一視により処理するのではなくそもそも現れないようにする」「プライムで表されていた二つの異なる操作を明記する」などの作業を行っただけで、定義の意味合いは同じである。

\( ( X, n ) \mapsto X [ n ] _ \varphi \) を定義する。

• \( X \) の行の長さを \( m \) とする。
• \( X = \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 1 } \\ B _ 0 & B _ 1 & \cdots & B _ { m - 1 } \\ \end{matrix} \right) \) とする。
• \( m \) の値で場合分けする。
• \( m = 1 \) のとき、
  • \( j _ \oplus ( B _ { m - 1 } \) の値で場合分けする。
  • \( O \) のとき、
    • あり得ない状態である。
  • \( S \) のとき、
    • \( X [ n ] \) の値は \( f ^ n ( 0 ) \) に等しい。
      • ただし、 \( Y \mapsto f ( Y ) \) は以下のように定義される関数である。
      • \( f ( Y ) \) の値は \( \left( \begin{matrix} 0 \\ { B _ { m - 1 } } ^ - \\ \end{matrix} \right) \oplus Y \) である。
  • \( L \) のとき、
    • \( X [ n ] \) の値は \( f ^ n ( 0 ) \) に等しい。
      • ただし、 \( Y \mapsto f ( Y ) \) は以下のように定義される関数である。
      • \( f ( Y ) \) の値は \( \left( \begin{matrix} 0 \\ B _ { m - 1 } [ n ] \\ \end{matrix} \right) \oplus Y \) である。
• \( m > 1 \) のとき、
  • \( j _ \oplus ( A _ { m - 2 } ) \) の値で場合分けする。
  • \( O \) のとき、
    • あり得ない状態である。
  • \( S \) のとき、
    • \( { A _ { m - 2 } } ^ - \) の値で場合分けする。
    • \( { A _ { m - 2 } } ^ - = _ \oplus 0 \) のとき、
      • \( j _ \oplus ( B _ { m - 2 } ) \) の値で場合分けする。
      • \( O \) のとき、
        • あり得ない状態である。
      • \( S \) のとき、
        • \( { B _ { m - 2 } } ^ - \) の値で場合分けする。
        • \( { B _ { m - 2 } } ^ - = _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & 0 \\ B _ 0 & B _ 1 & \cdots & Y \\ \end{matrix} \right) \oplus 0 \) である。
        • \( { B _ { m - 2 } } ^ - > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 2 } & 0 \\ B _ 0 & B _ 1 & \cdots & { B _ { m - 2 } } ^ - & Y \\ \end{matrix} \right) \oplus 0 \) である。
      • \( L \) のとき、
        • \( B _ { m - 2 } [ n ] \) の値で場合分けする。
        • \( B _ { m - 2 } [ n ] = _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & 0 \\ B _ 0 & B _ 1 & \cdots & Y \\ \end{matrix} \right) \oplus 0 \) である。
        • \( B _ { m - 2 } [ n ] > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & 0 \\ B _ 0 & B _ 1 & \cdots & Y \\ \end{matrix} \right) \oplus 0 \) である。
    • \( { A _ { m - 2 } } ^ - > _ \oplus 0 \) のとき、
      • \( j _ \oplus ( B _ { m - 2 } ) \) の値で場合分けする。
      • \( O \) のとき、
        • あり得ない状態である。
      • \( S \) のとき、
        • \( { B _ { m - 2 } } ^ - \) の値で場合分けする。
        • \( { B _ { m - 2 } } ^ - > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & { A _ { m - 1 } } ^ - & 0 \\ B _ 0 & B _ 1 & \cdots & Y & 0 \\ \end{matrix} \right) \oplus 0 \) である。
        • \( { B _ { m - 2 } } ^ - > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 2 } & { A _ { m - 1 } } ^ - & 0 \\ B _ 0 & B _ 1 & \cdots & { B _ { m - 2 } } ^ - & Y & 0 \\ \end{matrix} \right) \oplus 0 \) である。
      • \( L \) のとき、
        • \( B _ { m - 2 } [ n ] \) の値で場合分けする。
        • \( B _ { m - 2 } [ n ] = _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & { A _ { m - 1 } } ^ - & 0 \\ B _ 0 & B _ 1 & \cdots & Y & 0 \\ \end{matrix} \right) \oplus 0 \) である。
        • \( B _ { m - 2 } [ n ] > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 2 } & { A _ { m - 1 } } ^ - & 0 \\ B _ 0 & B _ 1 & \cdots & B _ { m - 2 } [ n ] & Y & 0 \\ \end{matrix} \right) \oplus 0 \) である。
  • \( L \) のとき、
    • \( A _ { m - 1 } [ n ] \) の値で場合分けする。
    • \( A _ { m - 1 } [ n ] = _ \oplus 0 \) のとき、
      • \( j _ \oplus ( B _ { m - 2 } ) \) の値で場合分けする。
      • \( O \) のとき、
        • あり得ない状態である。
      • \( S \) のとき、
        • \( { B _ { m - 2 } } ^ - \) の値で場合分けする。
        • \( { B _ { m - 2 } } ^ - = _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 1 } [ n ] \\ B _ 0 & B _ 1 & \cdots & Y \\ \end{matrix} \right) \oplus 0 \) である。
        • \( { B _ { m - 2 } } ^ - > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 2 } & A _ { m - 1 } [ n ] \\ B _ 0 & B _ 1 & \cdots & { B _ { m - 2 } } ^ - & Y \\ \end{matrix} \right) \oplus 0 \) である。
      • \( L \) のとき、
        • \( B _ { m - 2 } [ n ] \) の値で場合分けする。
        • \( B _ { m - 2 } [ n ] = _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
          • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 1 } [ n ] \\ B _ 0 & B _ 1 & \cdots & Y \\ \end{matrix} \right) \oplus 0 \) である。
        • \( B _ { m - 2 } [ n ] > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
          • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 2 } & A _ { m - 1 } [ n ] \\ B _ 0 & B _ 1 & \cdots & B _ { m - 2 } [ n ] & Y \\ \end{matrix} \right) \oplus 0 \) である。
    • \( A _ { m - 1 } [ n ] > _ \oplus 0 \) のとき、
      • \( j _ \oplus ( B _ { m - 2 } ) \) の値で場合分けする。
      • \( O \) のとき、
        • あり得ない状態である。
      • \( S \) のとき、
        • \( { B _ { m - 2 } } ^ - \) の値で場合分けする。
        • \( { B _ { m - 2 } } ^ - = _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 1 } [ n ] & 0 \\ B _ 0 & B _ 1 & \cdots & Y & 0 \\ \end{matrix} \right) \oplus 0 \) である。
        • \( { B _ { m - 2 } } ^ - > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
            • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 2 } & A _ { m - 1 } [ n ] & 0 \\ B _ 0 & B _ 1 & \cdots & { B _ { m - 2 } } ^ - & Y & 0 \\ \end{matrix} \right) \oplus 0 \) である。
      • \( L \) のとき、
        • \( B _ { m - 2 } [ n ] \) の値で場合分けする。
        • \( B _ { m - 2 } [ n ] = _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
          • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 1 } [ n ] & 0 \\ B _ 0 & B _ 1 & \cdots & Y & 0 \\ \end{matrix} \right) \oplus 0 \) である。
        • \( B _ { m - 2 } [ n ] > _ \oplus 0 \) のとき、
          • \( X [ n ] \) の値は \( g ^ n ( B _ { m - 1 } ) \) に等しい。
            • ただし、 \( Y \mapsto g ( Y ) \) は以下のように定義される関数である。
          • \( g ( Y ) \) の値は \( \left( \begin{matrix} A _ 0 & A _ 1 & \cdots & A _ { m - 2 } & A _ { m - 1 } [ n ] & 0 \\ B _ 0 & B _ 1 & \cdots & B _ { m - 2 } [ n ] & Y & 0 \\ \end{matrix} \right) \oplus 0 \) である。

解析

...