亜原始数列とペア数列システム

未完成

日本時間2021/05/23、Discordサーバーグーゴロジストの社交場のボイスチャンネルにおいて、亜原始数列の極限\((0,\omega)\)はペア数列システムに簡潔に対応するだろうと話題に上がった。ここでは、そこで定めた写像を改めてオープンな場に書く。

背景

亜原始数列とはYukito氏が考案した表記で、極限\((0,\omega)\)はヴェブレンの\(\varphi\)関数で\(\varphi(\omega,0)\)に対応すると信じられてきたが、その証明は2022/05/17現在存在しない。過去にヴェブレンの\(\varphi\)関数への対応写像を公開したが、非常に乱雑かつ複雑であり、証明は難航していた。日本時間2021/05/23、グーゴロジストの社交場のボイスチャンネルにおいて亜原始数列を順序数表記に対応させる話題が上がり、そして上記の複雑さからより簡単に対応させることができる表記がないか探すことになり、ペア数列が選ばれた。そこでは亜原始数列をペア数列システムへ変換する写像\(\textrm{S2P}\)を定めた。これは確かに従来のものと比べ遥かに簡潔であった。なお、当時のログからYukito氏とKoteitan氏の助けがあったようであり、この場を借りて感謝する。また、\(\textrm{P2S}\)は対応が完全に一致するよう一部修正されており、\(\textrm{S2P}\)の逆写像\(\textrm{P2S}\)はそこでは与えられておらず、新規のものである。

ペア数列システムとはBashicu氏が考案した表記である。ペア数列システムはp進大好きbot氏によって停止性が証明されているため、厳密な停止性の証明には適切である。亜原始数列の極限と考えられている\(\varphi(\omega,0)\)はペア数列システムにおいて\((0,0)(1,1)(2,1)(3,0)\)である([[#亜原始数列の順序型)。

また、p進大好きbot氏によって定義されたペア数列システムからブーフホルツの表記系、ひいては順序数への対応は全単射であることが証明されている。よって、ここでは亜原始数列とペア数列システムが変換写像を通して互いの基本列を表現できることを示し、亜原始数列の停止性及び\((0,\omega)\)に対応する順序数を求める。

p進大好きbot氏のヴェブレン関数に写すことによる停止性の証明も参照。

表記の定義

配列

亜原始数列は要素を\(1\)から数え、ペア数列システムは\(0\)から数えるため、まず長い記法で任意の配列をインデックスし、それぞれに対して短い記法を定める。

有限列\(a\)に対して\(\textrm{Length}(a)\)を\(a\)の長さとする。

任意の有限列\(a\)と非負整数\(0\leq i<\textrm{Length}(a)\)に対して\(\textrm{Get}(a,i)\)を\(a\)の\(0\)番目から数えたときの\(i\)番目の成分とする。

任意の有限列\(a\)と整数\(i,j\)に対して\(\textrm{Slice}(a,i,j)\)を次のように定める。

1. \(0\leq i\leq\textrm{Length}(a)\)かつ\(0\leq j\leq\textrm{Length}(a)\)かつ\(i< j\)ならば\(\textrm{Slice}(a,i,j)=(\textrm{Get}(a,k))_{k=i}^{j-1}\)とする。
2. \(0\leq i\leq\textrm{Length}(a)\)かつ\(0\leq j\leq\textrm{Length}(a)\)かつ\(i\geq j\)ならば\(\textrm{Slice}(a,i,j)=()\)とする。
3. \(0\leq i\leq\textrm{Length}(a)\)かつ\(j>\textrm{Length}(a)\)ならば\(\textrm{Slice}(a,i,j)=\textrm{Slice}(a,i,\textrm{Length}(a))\)とする。
4. \(0\leq i\leq\textrm{Length}(a)\)かつ\(0>j\)ならば\(\textrm{Slice}(a,i,j)=\textrm{Slice}(a,i,\textrm{Length}(a)+j)\)とする。
5. \(i>\textrm{Length}(a)\)ならば\(\textrm{Slice}(a,i,j)=\textrm{Slice}(a,\textrm{Length}(a),j)\)とする。
6. \(0>i\)ならば\(\textrm{Slice}(a,i,j)=\textrm{Slice}(a,\textrm{Length}(a)+i,j)\)とする。

2つの有限列\(a,b\)に対して\(a\frown b\)を\(a\)と\(b\)の結合とする。

有限列の有限列\(a\)に対して\(\bowtie a\)を\(a\)の要素の結合とする。

任意の\(v\)と非負整数\(n\)に対して、\(v\ast n=(v)_{i=0}^{n-1}\)とする。

\(\{\bowtie,\}>\{ast,\oplus,\boxplus\}>\{\frown\}\)の順で結合が強いとする。

亜原始数列

の定義と同等であることを想定している。

\(\mathbb{S}\subset\mathbb{N}_{\geq0}^{<\omega}\cup\{(0,\omega)\}\)を空配列\(()\)と最も左の要素が\(0\)である非負整数の配列\(S\)と\((0,\omega)\)の集合とする。ただし、計算可能性のため、亜原始数列の文脈では\(\omega\)を文字として扱う。

任意の\(S\in\mathbb{N}_{\geq0}^{<\omega}\cup\{(0,\omega)\}\)に対して\(l_S=\textrm{Length}(S)\)とする。

任意の\(S\in\mathbb{N}_{\geq0}^{<\omega}\cup\{(0,\omega)\}\)と正整数\(1\leq i\leq l_S\)に対して、\(S_i=\textrm{Get}(S,i-1)\)とする。

任意の\(S\in\mathbb{N}_{\geq0}^{<\omega}\cup\{(0,\omega)\}\)と整数\((i,j)\in\mathbb{Z}^2\)に対して、\(S_{[i\colon j]}=\textrm{Slice}(S,i-1,j)\)、\(S_{[i\colon]}=S_{[i\colon l_S]}\)とする。

\((\mathbb{N}_{\geq0}^{<\omega}\cup\{(0,\omega)\})^2\)上の関係\(<_\mathbb{P}\)を数列の辞書式順序として定める。ただし、\(S<_\mathbb{S}(0,\omega)\)は\(S\neq(0,\omega)\)と同値であり、\((0,\omega)<_\mathbb{S}S\)は偽であるとする。

任意の\((S,T)\in\mathbb{S}^2\)に対して\(S\leq_\mathbb{S}T\)を\(S=T\lor S<_\mathbb{S}T\)の略記とする。

任意の数列\(S\in\mathbb{N}_{\geq0}^{<\omega}\)と整数\(n\in\mathbb{Z}\)に対して、\(S\oplus n=(\max(S_i+n,0))_{i=1}^{l_S}\)とする。

写像

\begin{eqnarray*} r\colon\mathbb{S}&\to&\mathbb{N}_{>0}\\ S&\mapsto&r_S\\ \end{eqnarray*}

を次のように定義する。

\(S\in\{(),(0,\omega)\}\)または\(S_{l_S}=0\)ならば\(r_S=l_S\)とする。

\(S\not\in\{(),(0,\omega)\}\)かつ\(S_{l_S}>0\)ならば\(r_S=\min\{i\mid i\in\mathbb{N}_{>0}\land1\leq i< l_S\land S_i< S_{l_S}\}\)とする。

任意の数列\(S\in\mathbb{S}\)に対して\(G_S=S_{[1\colon r_S-1]},B_S=S_{[r_S\colon-1]},\Delta_S=S_{l_S}-S_{r_S}-1\)とする。

任意の非負整数\(n\)に対して\(B_S(0)=B_S,B_S(n+1)=B_S(n)\oplus\Delta_S\)とする。

写像

\begin{eqnarray*} \textrm{ExpandS}\colon\mathbb{S}\times\mathbb{N}_{\geq0}&\to&\mathbb{S}\\ (S,n)&\mapsto&\textrm{ExpandS}(S,n)\\ \end{eqnarray*}

を次のように定義する。

\(S=()\)ならば\(\textrm{ExpandS}(S,n)=()\)とする。

\(S=(0,\omega)\)ならば\(\textrm{ExpandS}(S,n)=(0,n)\)とする。

\(S\not\in\{(),(0,\omega)\}\)かつ\(S_{l_S}=0\)ならば\(\textrm{ExpandS}(S,n)=S_{[1\colon-1]}\)とする。

\(S\not\in\{(),(0,\omega)\}\)かつ\(S_{l_S}\neq0\)ならば\(\textrm{ExpandS}(S,n)=G_S\frown\bowtie(B_S(k))_{k=0}^n\)とする。

写像

\begin{eqnarray*} []\colon\mathbb{S}\times\mathbb{N}_{\geq0}&\to&\mathbb{N}_{\geq0}\\ (S,n)&\mapsto&S[n]\\ \end{eqnarray*}

を次のように定義する。

\(S=()\)ならば\(S[n]=n\)とする。

\(S=(0,\omega)\)ならば\(S[n]=(0,n)[n]\)とする。

\(S\not\in\{(),(0,\omega)\}\)ならば\(S[n]=\textrm{ExpandS}(S,n)[n+1]\)とする。

写像

\begin{eqnarray*} f\colon\mathbb{N}_{\geq0}&\to&\mathbb{N}_{\geq0}\\ n&\mapsto&f(n)\\ \end{eqnarray*}

を\(f(n)=(0,\omega)[n]\)と定義する。

写像

\begin{eqnarray*} \textrm{ExpandSMulti}\colon\mathbb{S}\times\mathbb{N}_{\geq0}^{<\omega}&\to&\mathbb{S}\\ (S,a)&\mapsto&\textrm{ExpandSMulti}(S,a)\\ \end{eqnarray*}

を次のように定義する。

1. \(a=()\)ならば、\(\textrm{ExpandSMulti}(S,a)=S\)とする。
2. \(a\neq()\)ならば、\(\textrm{ExpandSMulti}(S,a)=\textrm{ExpandSMulti}(\textrm{ExpandS}(S,a_1),a_{[2\colon]})\)とする。

\(S\in\mathbb{S}\)が標準形であるとは、ある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}((0,\omega),a)=S\)であることである。\(\mathbb{OS}\)を標準形である\(\mathbb{S}\)の要素全体の集合とする。

ペア数列システム

より次の記法を用いる。

• \(M_j,M_{i,j}\mid M\in T_{\textrm{PS}}\) - 2次元配列の要素。\(M_j=\textrm{Get}(M,j)\)、\(M_{i,j}=\textrm{Get}(\textrm{Get}(M,j),i)\)である。
• \(\textrm{Pred}(M)\) - ペア数列の前者
• \(<_M^{\textrm{Next}}\)
• \(\leq_M\)
• \(P(M)\mid M\in T_{\textrm{PS}}\) - ペア数列の単項成分
• \(\textrm{Trans}\)

また次の記法を使う。

• 2つの配列の結合\(a\oplus_Ab\)は\(a\frown b\)を用いる
• ペア数列全体の集合\(T_{\textrm{PS}}\)は\(\mathbb{P}\)と書く
• 単項なペア数列全体の集合\(PT_{\textrm{PS}}\)は\(\mathbb{PP}\)と書く
• 複項なペア数列全体の集合\(MT_{\textrm{PS}}\)は\(\mathbb{MP}\)と書く
• 広い意味で標準形なペア数列全体の集合\(ST_{\textrm{PS}}\)は\(\mathbb{SP}\)と書く
• 列数\(\textrm{Lng}(M)\mid M\in T_{\textrm{PS}}\)は\(X^M=\textrm{Length}(M)\)と書く
• ペア数列の基本列\(M[n]\mid M\in T_{\textrm{PS}}\)は\(\textrm{ExpandP}(M,n)\)と書く

の\(<_{\textrm{PS}},\leq_{\textrm{PS}}\)を\(<_\mathbb{P},\leq_\mathbb{P}\)、\(CT_{\textrm{PS}}\)を\(\mathbb{OP}\)と書く。

及びも参照。

より次の記法を用いる。

• \(\psi_ua\)
• \(D_ua\)
• \(G_ua\)
• \(o\)

任意の\(M\in\mathbb{P}\)と整数\((i,j)\in\mathbb{Z}^2\)に対して、\(M_{[i\colon j)}=\textrm{Slice}(M,i,j)\)、\(m_{[i\colon)}=M_{[i\colon X^M]}\)とする。

\(Q\in\mathbb{P}^{<\omega}\)が降順であるとは、任意の非負整数\(0\leq i\leq j<\textrm{Length}(Q)\)に対して\(\textrm{Get}(Q,j)\leq_\mathbb{P}\textrm{Get}(Q,i)\)であることと同値である。

任意の非負整数\(m\)に対して、任意の\(M\in(\mathbb{N}^m)^{<\omega}\)と\(v\in\mathbb{Z}^m\)に対して、\(M\boxplus v=((\max(M_{i,j}+\textrm{Get}(v,i),0))_{i=0}^{m-1})_{j=0}^{\textrm{Length}(M)-1}\)とする。

任意の\(M\in\mathbb{P}\)に対して、\(t^M=\max\{-1\}\cup\{i\mid i\in\{0,1\}\land M_{i,X^M-1}>0\}\)とする。\(\textrm{operation}[]\)の定義中の\(i_1\)に相当する。

任意の\(M\in\mathbb{P}\)と非負整数\(0\leq x< X^M\)と非負整数\(y\in\{0,1\}\)に対して、\(P^M_y(x)=\max\{-1\}\cup\{p\mid p\in\mathbb{N}_{\geq0}\land(i,p)<_M^{\textrm{Next}}(i,x)\}\)とする。

任意の\(M\in\mathbb{P}\)に対して、\(r^M=\begin{cases}P^M_{t^M}(X^M-1)&t^M\in\{0,1\}\\X^M-1&\textrm{otherwise}\end{cases}\)とする。\(\textrm{operation}[]\)の定義中の\(j_0\)に相当する。

任意の\(M\in\mathbb{P}\)に対して\(\boldsymbol{G}^M=M_{[0\colon r^M)}\)、\(\boldsymbol{B}^M=M_{[r^M\colon-1)}\)、\(\Delta^M_0=\begin{cases}M_{0,X^M-1}-M_{0,r^M}&t^M=1\\0&\textrm{otherwise}\end{cases}\)とする。それぞれ\(\textrm{operation}[]\)の定義中の\(G\)、\(\textrm{Get}(B,0)\)、\(\delta_0\)に相当する。

任意の\(M\in\mathbb{P}\)と非負整数\(n\)に対して\(\boldsymbol{B}^{M(0)}=\boldsymbol{B}^M,\boldsymbol{B}^{M(n+1)}=\boldsymbol{B}^{M(n)}\boxplus(\Delta^M_0,0)\)とする。\(\textrm{operation}[]\)の定義中の\(\textrm{Get}(B,n)\)に相当する。

写像

\begin{eqnarray*} \textrm{ExpandPMulti}\colon\mathbb{P}\times\mathbb{N}_{>0}^{<\omega}&\to&\mathbb{P}\\ (M,a)&\mapsto&\textrm{ExpandPMulti}(M,a)\\ \end{eqnarray*}

を次のように定義する。

1. \(a=()\)ならば、\(\textrm{ExpandPMulti}(M,a)=M\)とする。
2. \(a\neq()\)ならば、\(\textrm{ExpandPMulti}(M,a)=\textrm{ExpandPMulti}(\textrm{ExpandP}(M,a_1),a_{[2\colon]})\)とする。

任意の\((M,N)\in\mathbb{P}\)に対して、\(M\leq_{\textrm{PS}[]}N\)はある非負整数列\(a\)が存在して\(M=\textrm{ExpandPMulti}(N,a)\)であることと同値である。

変換写像

\(\mathbb{NS}=\{0\ast n\mid n\in\mathbb{N}_{\geq0}\}\)、\(\mathbb{NP}=\{(0,0)\ast n\mid n\in\mathbb{N}_{>0}\}\)、\($=((0,0),(1,1),(2,1),(3,0))\)、\(\mathbb{P}\downarrow=\{M\mid M\in\mathbb{P}\land M\leq_\mathbb{P}$\}\)、\(\mathbb{SP}\downarrow=\mathbb{P}\downarrow\cap\mathbb{SP}\)とする。

計算可能全域写像

\begin{eqnarray*} \exp_\omega\colon\mathbb{S}&\to&\mathbb{S}\\ S&\mapsto&\exp_\omega{S}\\ \end{eqnarray*}

を以下のように再帰的に定める。

1. \(S=(0,\omega)\)ならば、\(\exp_\omega{S}=(0,\omega)\)とする。
2. \(S\neq(0,\omega)\)であり、かつ\(l_S<2\)または\(S_2<2\)ならば、\(\exp_\omega{S}=(0)\frown S\oplus1\)とする。
3. \(S\neq(0,\omega)\)かつ\(l_S\geq2\)かつ\(S_2\geq2\)ならば、ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、かつ\(k=l_S\)または\(S_{k+1}<2\)である。
   1. \(k=l_S\)または\(S_{k+1}=0\)ならば、\(\exp_\omega{S}=S_{[1\colon k]}\frown S_{[k+1\colon]}\oplus1\)とする。
   2. \(k< l_S\)かつ\(S_{k+1}=1\)ならば、\(\exp_\omega{S}=S_{[1\colon k]}\frown S\oplus1\)とする。

計算可能全域写像

\begin{eqnarray*} \log_\omega\colon\mathbb{S}&\to&\mathbb{S}\\ S&\mapsto&\log_\omega{S}\\ \end{eqnarray*}

を以下のように再帰的に定める。

1. \(l_S<2\)ならば、\(\log_\omega{S}=()\)とする。
2. \(S=(0,\omega)\)ならば、\(\log_\omega{S}=(0,\omega)\)とする。
3. \(l_S\geq2\)かつ\(S\neq(0,\omega)\)かつある正整数\(2\leq k\leq l_S\)が存在して\(S_k=0\)ならば、そのような\(k\)で最小のものを\(k_0\)として、\(\log_\omega{S}=\log_\omega(S_{[1\colon k_0-1]})\)とする。
4. \(l_S\geq2\)かつ\(S\neq(0,\omega)\)かつ任意の正整数\(2\leq k\leq l_S\)に対して\(S_k>0\)であるとする。
   1. \(S_2<2\)ならば、\(\log_\omega{S}=S_{[2\colon]}\oplus-1\)とする。
   2. \(S_2\geq2\)ならば、ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、かつ\(k=l_S\)または\(S_{k+1}<2\)である。
      1. \(S<_\mathbb{S}S_{[1\colon k]}\frown S_{[1\colon k]}\oplus1\frown(2)\)ならば、\(\log_\omega{S}=S_{[1\colon k]}\frown S_{[k+1\colon]}\oplus-1\)とする。
      2. \(S_{[1\colon k]}\frown S_{[1\colon k]}\oplus1\frown(2)\leq_\mathbb{S}S\)ならば、\(\log_\omega{S}=S_{[k+1\colon]}\oplus-1\)とする。

計算可能全域写像

\begin{eqnarray*} \textrm{S2P}_0\colon\mathbb{S}&\to&\mathbb{P}\cup\{()\}\\ S&\mapsto&\textrm{S2P}_0(S)\\ \end{eqnarray*}

を以下のように再帰的に定める。

1. \(S=()\)ならば、\(\textrm{S2P}_0(S)=()\)とする。
2. \(S=(0)\)ならば、\(\textrm{S2P}_0(S)=((0,0))\)とする。
3. \(S=(0,\omega)\)ならば、\(\textrm{S2P}_0(S)=$\)とする。
4. \(S\not\in\{(),(0),(0,\omega)\}\)ならば、ある正整数\(k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)と\(k< j\leq l_S\)に対して\(S_k\leq S_i\)かつ\(S_k< S_j\)である。そのような\(k\)で最大のものを\(k_0\)とする。
   1. \(S_{k_0}=0\)ならば、\(\textrm{S2P}_0(S)=\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown\textrm{S2P}_0(S_{[k_0\colon]})\)とする。
   2. \(S_{k_0}=1\)ならば、\(\textrm{S2P}_0(S)=\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown\textrm{S2P}_0(S_{[k_0\colon]}\oplus-1)\boxplus(1,0)\)とする。
   3. \(S_{k_0}\geq2\)ならば、\(\textrm{S2P}_0(S)=\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1))\frown(2,1)\ast S_{k_0}-2\frown\textrm{S2P}_0(\log_\omega(S_{[k_0\colon]}\oplus-S_{k_0}))\boxplus(2,0)\)とする。

計算可能全域写像

\begin{eqnarray*} \textrm{S2P}\colon\mathbb{S}&\to&\mathbb{P}\cup\{()\}\\ S&\mapsto&\textrm{S2P}(S)\\ \end{eqnarray*}

を以下のように定める。

1. \(S\in\mathbb{NS}\)ならば、\(\textrm{S2P}(S)=(0,0)\ast l_S+1\)とする。
2. \(S\not\in\mathbb{NS}\)ならば、\(\textrm{S2P}(S)=\textrm{S2P}_0(S)\)とする。

\(\textrm{undefined}\not\in\mathbb{S}\)として、\(\mathbb{S}?=\mathbb{S}\cup\{\textrm{undefined}\}\)とする。

全域写像

\begin{eqnarray*} \gg=\colon\mathbb{S}?\times(\mathbb{S}\setminus\{(0,\omega)\}\to\mathbb{S}?\setminus\{(0,\omega)\})&\to&\mathbb{S}?\setminus\{(0,\omega)\}\\ (S,f)&\mapsto&S\gg=f\\ \end{eqnarray*}

を以下のように定める。

1. \(S\in\{(0,\omega),\textrm{undefined}\}\)ならば、\(S\gg=f=\textrm{undefined}\)とする。
2. \(S\not\in\{(0,\omega),\textrm{undefined}\}\)ならば、\(S\gg=f=f(S)\)とする。

計算可能全域写像

\begin{eqnarray*} \textrm{P2S}_0\colon\mathbb{P}\cup\{()\}&\to&\mathbb{S}?\\ M&\mapsto&\textrm{P2S}(M)\\ \end{eqnarray*}

を以下のように再帰的に定める。

1. \(M=()\)ならば、\(\textrm{P2S}_0(M)=()\)とする。
2. \(M=((0,0))\)ならば、\(\textrm{P2S}_0(M)=(0)\)とする。
3. \(M=$\)ならば、\(\textrm{P2S}_0(M)=(0,\omega)\)とする。
4. \(M\neq()\)かつ\(M_0\neq(0,0)\)ならば、\(\textrm{P2S}_0(M)=\textrm{undefined}\)とする。
5. \(M\not\in\{(),((0,0)),$\}\)かつ\(M_0=(0,0)\)ならば、ある非負整数\(x< X^M\)が存在して、任意の非負整数\(1\leq v\leq x\)と\(x< w< X^M\)に対して\(M_x\leq_\mathbb{S}M_v\)かつ\(M_x<_\mathbb{S}M_w\)である。そのような\(x\)で最大のものを\(x_0\)とする。
   1. \(M_{x_0}=(0,0)\)ならば、\(\textrm{P2S}_0(M)=\textrm{P2S}_0(M_{[0\colon x_0)})\gg=S\mapsto\textrm{P2S}_0(M_{[x_0\colon)})\gg=T\mapsto S\frown T\)とする。
   2. \(M_{x_0}=(1,0)\)ならば、\(\textrm{P2S}_0(M)=\textrm{P2S}_0(M_{[0\colon x_0)})\gg=S\mapsto\textrm{P2S}_0(M_{[x_0\colon)}\boxplus(-1,0))\gg=T\mapsto S\frown T\oplus1\)とする。
   3. \(M_{x_0}=(1,1)\)ならば、ただ一つの非負整数\(x_0\leq z< X^M\)が存在して、任意の非負整数\(x_0< w\leq z\)に対して\(M_w=(2,1)\)であり、かつ\(z=X^M-1\)または\(M_{z+1}\neq(2,1)\)である。このとき、\(\textrm{P2S}_0(M)=\textrm{P2S}_0(M_{[0\colon x_0)})\gg=S\mapsto\textrm{P2S}_0(M_{[z+1\colon)}\boxplus(-2,0))\gg=T\mapsto S\frown\exp_\omega{T}\oplus z-x_0+1\)とする。
   4. \(M_{x_0}\not\in\{(0,0),(1,0),(1,1)\}\)ならば、\(\textrm{P2S}_0(M)=\textrm{undefined}\)とする。

計算可能全域写像

\begin{eqnarray*} \textrm{P2S}\colon\mathbb{P}&\to&\mathbb{S}?\\ M&\mapsto&\textrm{P2S}(M)\\ \end{eqnarray*}

を以下のように定める。

1. \(M\in\mathbb{NP}\)ならば、\(\textrm{P2S}(M)=(0,0)\ast X^M-1\)とする。
2. \(M\not\in\mathbb{NP}\)ならば、\(\textrm{P2S}(M)=\textrm{P2S}_0(M)\)とする。

証明

命題 (展開のデクリメント性)
(1) 任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)と非負整数\(n\)に対して、\(l_{\textrm{ExpandS}(S,n)}\geq l_S-1\)かつ\(\textrm{ExpandS}(S,n)_{[1\colon l_S-1]}=S_{[1\colon-1]}\)である。
(2) 任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)と正整数\(n\)に対して、\(S_{l_S}\neq0\)ならば\(l_{\textrm{ExpandS}(S,n)}\geq l_S\)かつ\(\textrm{ExpandS}(S,n)_{l_S}=S_{l_S}-1\)である。
(3) 任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)に対して\(\textrm{ExpandS}(S,0)=S_{[1\colon-1]}\)である。
(4) 任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)と非負整数\(n\)に対して、\(S_{l_S}=0\)ならば\(\textrm{ExpandS}(S,n)=S_{[1\colon-1]}\)である。

証明

(1) \(S=G_S\frown B_S\frown(S_{l_S})\)である。

\(S_{l_S}=0\)ならば、\(\textrm{ExpandS}(S,n)=S_{[1\colon-1]}\)であるから\(l_{\textrm{ExpandS}(S,n)}\geq l_S-1\)かつ\(\textrm{ExpandS}(S,n)_{[1\colon l_S-1]}=S_{[1\colon-1]}\)である。

\(S_{l_S}\neq0\)ならば、$$\begin{align}\textrm{ExpandS}(S,n)&=G_S\frown\bowtie(B_S(k))_{k=0}^n\\&=G_S\frown B_S(0)\frown\bowtie(B_S(k))_{k=1}^n\\&=G_S\frown B_S\frown\bowtie(B_S(k))_{k=1}^n\\&=S_{[1\colon-1]}\frown\bowtie(B_S(k))_{k=1}^n\end{align}$$であるから\(l_{\textrm{ExpandS}(S,n)}\geq l_S-1\)かつ\(\textrm{ExpandS}(S,n)_{[1\colon l_S-1]}=S_{[1\colon-1]}\)である。

よっていずれの場合でも\(l_{\textrm{ExpandS}(S,n)}\geq l_S-1\)かつ\(\textrm{ExpandS}(S,n)_{[1\colon l_S-1]}=S_{[1\colon-1]}\)である。□

(2) $$\begin{align}\textrm{ExpandS}(S,n)_{l_S}&=(G_S\frown\bowtie(B_S(k))_{k=0}^n)_{l_S}\\&=(G_S\frown B_S(0)\frown B_S(1)\frown\bowtie(B_S(k))_{k=2}^n)_{l_S}\\&=(S_{[1\colon-1]}\frown B_S(1)\frown\bowtie(B_S(k))_{k=2}^n)_{l_S}\\&={B_S(1)}_1\\&={B_S(0)}_1+\Delta_S\\&=S_{r_S}+S_{l_S}-S_{r_S}-1\\&=S_{l_S}-1\end{align}$$である。□

(3) \(S=G_S\frown B_S\frown(S_{l_S})\)である

\(S_{l_S}=0\)ならば、\(\textrm{ExpandS}(S,0)=S_{[1\colon-1]}\)である。

\(S_{l_S}\neq0\)ならば、$$\begin{align}\textrm{ExpandS}(S,0)&=G_S\frown\bowtie(B_S(k))_{k=0}^0\\&=G_S\frown B_S(0)\\&=G_S\frown B_S\\&=S_{[1\colon-1]}\end{align}$$である。

よっていずれの場合でも\(\textrm{ExpandS}(S,0)=S_{[1\colon-1]}\)である。□

(4) \(\textrm{ExpandS}\)の定義より即座に従う。□

命題 (展開の辞書式縮小性)
任意の\(S\in\mathbb{S}\setminus\{()\}\)と非負整数\(n\)に対して\(\textrm{ExpandS}(S,n)<_\mathbb{S}S\)である。

証明

展開のデクリメント性(1)、(2)及び\(<_\mathbb{S}\)の定義より即座に従う。□

命題 (展開の切片の不変性)
任意の\(S\in\mathbb{S}\setminus\{(0,\omega)\}\)と非負整数\(i,j,m,n\)に対して、\(1\leq i\leq j\)かつ\(j\leq l_{\textrm{ExpandS}(S,m)}\)かつ\(j\leq l_{\textrm{ExpandS}(S,n)}\)ならば\(\textrm{ExpandS}(S,m)_{[i\colon j]}=\textrm{ExpandS}(S,n)_{[i\colon j]}\)である。

証明

\(\textrm{ExpandS}(S,m)=\textrm{ExpandS}(S,n)\)ならば\(\textrm{ExpandS}(S,m)_{[i\colon j]}=\textrm{ExpandS}(S,n)_{[i\colon j]}\)である。

よって\(m\neq n\)かつ\(S\neq()\)かつ\(S_{l_S}\neq0\)とする。

命題が\(m\)と\(n\)に対して対称であることから\(m< n\)である場合のみ考えればいい。

$$\begin{align}\textrm{ExpandS}(S,n)_{[1\colon l_{\textrm{ExpandS}(S,m)}]}&=(G_S\frown\bowtie(B_S(k))_{k=0}^n)_{[1\colon l_{\textrm{ExpandS}(S,m)}]}\\&=(G_S\frown\bowtie(B_S(k))_{k=0}^m\frown\bowtie(B_S(k))_{k=m}^n)_{[1\colon l_{\textrm{ExpandS}(S,m)}]}\\&=(\textrm{ExpandS}(S,m)\frown\bowtie(B_S(k))_{k=m}^n)_{[1\colon l_{\textrm{ExpandS}(S,m)}]}\\&=\textrm{ExpandS}(S,m)\end{align}$$である。

\(i\leq j\leq l_{\textrm{ExpandS}(S,m)}\)であるから、上より\(\textrm{ExpandS}(S,n)_{[i\colon j]}=(\textrm{ExpandS}(S,n)_{[1\colon l_{\textrm{ExpandS}(S,m)}]})_{[i\colon j]}=\textrm{ExpandS}(S,m)_{[i\colon j]}\)である。

よっていずれの場合でも\(\textrm{ExpandS}(S,m)_{[i\colon j]}=\textrm{ExpandS}(S,n)_{[i\colon j]}\)である。□

命題 (悪い部分の展開)
任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)と非負整数\(n\)に対して、\(S_{l_S}\neq0\)ならば\(\textrm{ExpandS}(S,n)=G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S})\)である。

証明

\(B_S\)及び\(\oplus\)の定義より\(l_{B_S\oplus-S_{r_S}}=l_{B_S}=l_S-r_S+1\)である。

\(r_S\)の定義より任意の正整数\(r_S< i\leq l_S\)に対して\(S_{r_S}< S_i\leq S_{l_S}\)であるから、任意の正整数\(r_S< i\leq l_S\)に対して\((B_S\oplus-S_{r_S})_{i-r_S+1}=S_i-S_{r_S}\)である。

上より任意の正整数\(1\leq i\leq l_{B_S}\)に対して\((B_S\oplus-S_{r_S})_i<(B_S\oplus-S_{r_S})_{l_{B_S}}\)は\(S_{i+r_S-1}< S_{l_S}\)と同値であるから、\(r_S\)の定義より\(r_{B_S\oplus-S_{r_S}}=1\)である。

よって\(G_{B_S\oplus-S_{r_S}}=(),B_{B_S\oplus-S_{r_S}}=(B_S\oplus-S_{r_S})_{[1\colon-1]},\Delta_{B_S\oplus-S_{r_S}}=\Delta_S\)であり、よって\(B_S(n),\textrm{ExpandS}\)の定義より\(l_{\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S})}=(l_{B_S}-1)(n+1)\)かつ任意の非負整数\(m\leq n\)と正整数\(1\leq i\leq l_{B_S}-1\)に対して\(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S})_{(l_{B_S}-1)m+i}=B_{B_S\oplus-S_{r_S}}(m)_i=S_{r_S+i}-S_{r_S}+\Delta_Sm\)である。

従って\(l_{G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S})}=r_S-1+(l_S-r_S)(n+1)\)であり、かつ任意の正整数\(1\leq i< r_S\)に対して\((G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S}))_i=(G_S)_i=S_i\)であり、かつ非負整数\(m\leq n\)と正整数\(1\leq i\leq l_{B_S}-1\)に対して\((G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S}))_{r_S–1+(l_S-r_S)m+i}=(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S})_{(l_S-r_S)m+i}=S_{r_S+i}+\Delta_Sm\)である。

\(B_S(n),\textrm{ExpandS}\)の定義より\(l_{\textrm{ExpandS}(S,n)}=l_{G_S}+l_{B_S}(n+1)=r_S-1+(l_S-r_S)(n+1)\)であり、かつ任意の正整数\(1\leq i< r_S\)に対して\(\textrm{ExpandS}(S,n)_i=(G_S)_i=S_i\)であり、かつ非負整数\(m\leq n\)と正整数\(1\leq i\leq l_{B_S}-1\)に対して\(\textrm{ExpandS}(S,n)_{r_S–1+(l_S-r_S)m+i}=B_S(m)_i=S_{r_S+i}+\Delta_Sm\)である。

従って\(l_{\textrm{ExpandS}(S,n)}=l_{G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S}))}\)かつ任意の正整数\(1\leq i\leq l_{\textrm{ExpandS}(S,n)}\)に対して\(\textrm{ExpandS}(S,n)_i=(G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S}))_i\)であるから、\(\textrm{ExpandS}(S,n)=G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S})\)である。□

任意の\(S\in\mathbb{OS}\setminus\{(0,\omega)\}\)に対して、\(\textrm{LastChildNode}(S)=\max\{1\}\cup\{i\mid i\in[2..l_S]\forall j\in[2..i-1]S_i< S_j\}\)とする。

命題 (末子列の基本性質)
(1) 任意の\(S\in\mathbb{S}\setminus\{(0,\omega)\}\)に対して、\(S\in\{(),(0)\}\)ならば\(\textrm{LastChildNode}(S)=1\)であり、。\(S\not\in\{(),(0)\}\)ならば\(\textrm{LastChildNode}(S)\geq2\)である。
(2) 任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)に対して、\(m=\textrm{LastChildNode}(S)\)としたとき任意の正整数\(m\leq i\leq l_S\)に対して\(S_m\leq S_i\)である。
(3) 任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)に対して、\(m=\textrm{LastChildNode}(S)\)、\(R=S_{[m\colon]}\)としたとき\(R\oplus-S_m=(S_i-S_m)_{i=m}^{l_S}\)かつ\(R\oplus-S_m\oplus S_m=R\)である。

証明

(1) \(S\in\{(),(0)\}\)ならば、\(l_S<2\)より\(\textrm{LastChildNode}(S)=1\)である。

\(S\not\in\{(),(0)\}\)ならば、\(i=2\)とすると\(i-1<2\)より条件を満たすから\(\textrm{LastChildNode}(S)\geq2\)である。□

(2) \(S\in\{(),(0)\}\)ならば(1)より即座に従う。

よって\(S\not\in\{(),(0)\}\)とする。

定義より\(S_m=\min\{S_j\mid j\in[2..m]\}である。

任意の\(m\leq i< l_S\)をとり、\(\min\{S_j\mid j\in[2..i]\}=S_m\)と仮定すると、条件よりある正整数\(2\leq j< i+1\)が存在して\(S_{i+1}\geq S_j\)であるから、\(S_{i+1}\geq\min\{S_j\mid j\in[2..i]\}\)であり、従って\(\min\{S_j\mid j\in[2..i+1]\}=\min\{S_j\mid j\in[2..i]\}=S_m\)である。

帰納法により任意の\(m\leq i\leq l_S\)に対して\(\min\{S_j\mid j\in[2..i]\}=S_m\)である。

よって任意の正整数\(m\leq i\leq l_S\)に対して\(S_m\leq S_i\)である。□

(3) (2)より即座に従う。□

命題 (末子列の展開)
任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)と非負整数\(n\)に対して、\(S_{l_S}\neq0\)かつ\(m=\textrm{LastChildNode}(S)\)、\(L=S_{[1\colon m-1]}\)、\(R=S_{[m\colon]}\)としたとき\(S_{l_S}\neq S_m\)ならば\(\textrm{ExpandS}(S,n)=L\frown(\textrm{ExpandS}(R\oplus-S_m,n)\oplus S_m)\)である。

証明

\(m\)の定義より任意の正整数\(m\leq i\leq l_S\)に対して\(S_i\geq S_m\)である。

上より任意の正整数\(m\leq i\leq l_S\)に対して\((R\oplus-S_m)_{i-m+1}=S_i-S_m\)である。

上より任意の正整数\(1\leq i\leq l_{R\oplus-S_m}\)と\(1\leq j\leq l_{R\oplus-S_m}\)に対して\((R\oplus-S_m)_i<(R\oplus-S_m)_j\)は\(S_{i-m+1}< S_{j-m+1}\)と同値である。

\(S_{l_S}\geq S_m\)であるから仮定より\(S_{l_S}>S_m\)である。

上よりある正整数\(m\leq i< l_S\)が存在して\(S_i< S_{l_S}\)である。

よって\(r_S\)の定義より\(m\leq r_S\)である。

従って\(r_{R\oplus-S_m}=r_S-m+1\)、\(G_{R\oplus-S_m}=(G_S)_{[m\colon]}\oplus-S_m\)、\(B_{R\oplus-S_m}=B_S\oplus-S_m\)である。

悪い部分の展開より\(\textrm{ExpandS}(S,n)=G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S}))\)かつ\(\textrm{ExpandS}(R\oplus-S_m)=G_{R\oplus-S_m}\frown(\textrm{ExpandS}(B_{R\oplus-S_m}\oplus-(R\oplus-S_m)_{r_{R\oplus-S_m}},n)\oplus(R\oplus-S_m)_{r_{R\oplus-S_m}}))\)である。

よって$$\begin{array}{l}L\frown(\textrm{ExpandS}(R\oplus-S_m,n)\oplus S_m))\\=L\frown(\textrm{ExpandS}(R\oplus-S_m,n)\oplus S_m))\\=L\frown((G_{R\oplus-S_m}\frown(\textrm{ExpandS}(B_{R\oplus-S_m}\oplus-(R\oplus-S_m)_{r_{R\oplus-S_m}},n)\oplus(R\oplus-S_m)_{r_{R\oplus-S_m}}))\oplus S_m)\\=L\frown((((G_S)_{[m\colon]}\oplus-S_m)\frown(\textrm{ExpandS}(B_S\oplus-S_m\oplus-(R\oplus-S_m)_{r_S-m+1},n)\oplus(R\oplus-S_m)_{r_S-m+1}))\oplus S_m)\\=L\frown((((G_S)_{[m\colon]}\oplus-S_m)\frown(\textrm{ExpandS}(B_S\oplus-S_m\oplus-(S_{r_S}-S_m),n)\oplus(S_{r_S}-S_m)))\oplus S_m)\\=L\frown((((G_S)_{[m\colon]}\oplus-S_m)\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus(S_{r_S}-S_m)))\oplus S_m)\\=L\frown((G_S)_{[m\colon]}\oplus-S_m\oplus S_m)\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus(S_{r_S}-S_m)\oplus S_m)\\=(G_S)_{[1\colon m-1]}\frown(G_S)_{[m\colon]}\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S})\\=G_S\frown(\textrm{ExpandS}(B_S\oplus-S_{r_S},n)\oplus S_{r_S})\\=\textrm{ExpandS}(S,n)\end{array}$$である。

従って\(\textrm{ExpandS}(S,n)=L\frown(\textrm{ExpandS}(R\oplus-S_m,n)\oplus S_m)\)である。□

命題 (標準形を短縮すれば標準形)
任意の\(S\in\mathbb{OS}\)に対して、任意の正整数\(1\leq l\leq l_S\)に対して\(S_{[1\colon l]}\in\mathbb{OS}\)であり、特にある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon l]}\)である。

証明

\(S=(0,\omega)\)とする。

仮定より\(l=1\)または\(l=2\)である。

\(l=1\)ならば、\(\textrm{ExpandSMulti}(S,(0,0))=\textrm{ExpandSMulti}((0,\omega),(0,0))=(0)=S_{[1\colon l]}\)である。

\(l=2\)ならば、\(\textrm{ExpandSMulti}(S,())=\textrm{ExpandSMulti}((0,\omega),())=(0,\omega)=S_{[1\colon l]}\)である。

よっていずれの場合でもある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon l]}\)である。

\(\mathbb{OS}\)の定義より\(S_{[1\colon l]}\in\mathbb{OS}\)である。

\(S\neq(0,\omega)\)とする。

\(\textrm{ExpandSMulti}(S,())=S=S_{[1\colon l_S]}\)である。

任意の正整数\(1< l\leq l_S\)をとり、ある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon l]}\)であると仮定すると、展開のデクリメント性(3)より\(\textrm{ExpandSMulti}(S,a\frown(0))=(S_{[1\colon l]})_{[1\colon-1]}=S_{[1\colon l-1]}\)である。

帰納法により任意の正整数\(1\leq l\leq l_S\)に対してある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon l]}\)である。

\(\textrm{OS}\)の定義よりある非負整数列\(a^0\)が存在して\(\textrm{ExpandSMulti}((0,\omega),a^0)=S\)である。

任意の正整数\(1\leq l\leq l_S\)に対して、ある非負整数列\(a^1\)が存在して\(\textrm{ExpandSMulti}(S,a^1)=S_{[1\colon l]}\)であり、このとき\(\textrm{ExpandSMulti}((0,\omega),a^0\frown a^1)=\textrm{ExpandSMulti}(S,a^1)=S_{[1\colon l]}\)であるから\(\mathbb{OS}\)の定義より\(S_{[1\colon l]}\in\mathbb{OS}\)である。

よっていずれの場合でも任意の正整数\(1\leq l\leq l_S\)に対して\(S_{[1\colon l]}\in\mathbb{OS}\)であり、かつある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon l]}\)である。□

命題 (標準形を減少させれば標準形)
任意の\(S\in\mathbb{OS}\setminus\{(0,\omega)\}\)に対して、任意の非負整数\(0\leq n\leq S_{l_S}\)に対して\(S_{[1\colon-1]}\frown(n)\in\mathbb{OS}\)であり、特にある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon-1]}\frown(n)\)である。

証明

\(\textrm{ExpandSMulti}(S,())=S=S_{[1\colon-1]}\frown(S_{l_S})\)である。

任意の非負整数\(0< n\leq S_{l_S}\)をとり、ある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon-1]}\frown(n)\)であると仮定する。

\(T=\textrm{ExpandS}(S_{[1\colon-1]}\frown(n),1)\)とする。

\((S_{[1\colon-1]}\frown(n))_{l_{S_{[1\colon-1]}\frown(n)}}=n>0\)であるから、展開のデクリメント性(1)及び(2)より\(l_T\geq l_S\)かつ\(T_{[1\colon l_S]}=S_{[1\colon-1]}\frown(n-1)\)である。

標準形を短縮すれば標準形よりある非負整数列\(a^0\)が存在して\(\textrm{ExpandSMulti}(T,a^0)=T_{[1\colon l_S]}=S_{[1\colon-1]}\frown(n-1)\)である。

$$\begin{array}{l}\textrm{ExpandSMulti}(S,a\frown(1)\frown a^0)\\=\textrm{ExpandSMulti}(S_{[1\colon-1]}\frown(n),(1)\frown a^0)\\=\textrm{ExpandSMulti}(T,a^0)\\=S_{[1\colon-1]}\frown(n-1)\end{array}$$である。

帰納法により任意の非負整数\(0\leq n\leq S_{l_S}\)に対して、ある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon-1]}\frown(n)\)である。

\(\textrm{OS}\)の定義よりある非負整数列\(a^0\)が存在して\(\textrm{ExpandSMulti}((0,\omega),a^0)=S\)である。

任意の非負整数\(0\leq n\leq S_{l_S}\)に対して、ある非負整数列\(a^1\)が存在して\(\textrm{ExpandSMulti}(S,a^1)=S_{[1\colon l]}\)であり、このとき\(\textrm{ExpandSMulti}((0,\omega),a^0\frown a^1)=\textrm{ExpandSMulti}(S,a^1)=S_{[1\colon-1]}\frown(n)\)であるから\(\mathbb{OS}\)の定義より\(S_{[1\colon-1]}\frown(n)\in\mathbb{OS}\)である。

よって任意の非負整数\(0\leq n\leq S_{l_S}\)に対して\(S_{[1\colon-1]}\frown(n)\in\mathbb{OS}\)であり、かつある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(S,a)=S_{[1\colon-1]}\frown(n)\)である。□

命題 (展開の上昇性)
(1) 任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)と非負整数\(n\)に対して、任意の正整数\(l_S\leq i\leq l_{\textrm{ExpandS}(S,n)}\)に対して\(S_{l_S}-1\leq\textrm{ExpandS}(S,n)_i\)である。
(2) 任意の\(S\in\mathbb{S}\setminus\{(),(0,\omega)\}\)と非負整数\(n\)に対して、\(S_{l_S}-S_{r_S}\geq2\)ならば任意の正整数\(l_S< i\leq l_{\textrm{ExpandS}(S,n)}\)に対して\(S_{l_S}\leq\textrm{ExpandS}(S,n)_i\)である。

証明

\(\textrm{ExpandS}(S,n)\)の定義より\(\textrm{ExpandS}(S,n)_{[l_S\colon]}=(G_S\frown B_S\frown\bowtie(B_S(k))_{k=1}^n)_{[l_S\colon]}=\bowtie(B_S(k))_{k=1}^n\)である。

(1) 任意の正整数\(l_S\leq i\leq l_{\textrm{ExpandS}(S,n)}\)に対してある非負整数\(1\leq m\leq n\)と正整数\(1\leq j\leq l_S-r_S\)が存在して\(\textrm{ExpandS}(S,n)_i=B_S(m)_j\)である。

\(r_S\)の定義より任意の正整数\(r_S< i\leq l_S\)に対して\(S_{r_S}< S_i\)である。

\(\Delta_S\)の定義より\(\Delta_S\geq0\)である。

\(B_S(n)\)の定義より任意の非負整数\(1\leq m\leq n\)と正整数\(1\leq i\leq l_S-r_S\)に対して\(B_S(m)_i=S_{i+r_S—1}+\Delta_Sm\geq S_{r_S}+\Delta_S=S_{l_S}-1\)である。

従って任意の正整数\(l_S\leq i\leq l_{\textrm{ExpandS}(S,n)}\)に対して\(S_{l_S}-1\leq\textrm{ExpandS}(S,n)_i\)である。□

(2) 任意の正整数\(l_S+1\leq i\leq l_{\textrm{ExpandS}(S,n)}\)に対してある非負整数\(1\leq m\leq n\)と正整数\(1\leq j\leq l_S-r_S\)が存在して\(m\neq1\)または\(j\neq1\)であり、かつ\(\textrm{ExpandS}(S,n)_i=B_S(m)_j\)である。

\(r_S\)の定義より任意の正整数\(r_S< i\leq l_S\)に対して\(S_{r_S}< S_i\)である。

\(\Delta_S\)の定義と仮定より\(\Delta_S>0\)である。

\(B_S(n)\)の定義より任意の非負整数\(2\leq m\leq n\)と正整数\(1\leq i\leq l_S-r_S\)に対して\(B_S(m)_i=S_{i+r_S—1}+\Delta_Sm\geq S_{r_S}+2\Delta_S=S_{l_S}-1+\Delta_S\geq S_{l_S}\)である。

従って任意の正整数\(l_S< i\leq l_{\textrm{ExpandS}(S,n)}\)に対して\(S_{l_S}\leq\textrm{ExpandS}(S,n)_i\)である。□

命題 (標準形の末子列の生成)
任意の\(S\in\mathbb{OS}\setminus\{(),(0),(0,\omega)\}\)に対して、\(m=\textrm{LastChildNode}(S)\)、\(L=S_{[1\colon m-1]}\)としたとき\(L\frown(S_m+1)\in\mathbb{OS}\)であり、かつある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a)=S\)である。

証明

\(m=2\)とする。

\(\textrm{ExpandSMulti}((0,\omega),(S_2+1))=(0,S_2+1)=L\frown(S_m+1)\)であるから\(L\frown(S_m+1)\in\mathbb{OS}\)である。

\(r_{(0,S_2+1)}=1,G_{(0,S_2+1)}=(),B_{(0,S_2+1)}=(0),\Delta_{(0,S_2+1)}=S_2,\textrm{ExpandS}((0,S_2+1),1)=(0,S_2)\)である。

よって\(a=(1)\)とすると\(\textrm{ExpandSMulti}(L\frown(S_m+1),a)=S\)である。

\(m>2\)とする。

\(\mathbb{OS}\)の定義よりある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}((0,\omega),a)=S\)である。

ある正整数\(1\leq g< l_a\)が存在して\(l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g]})}< l_S\)または\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g]})_{[1\colon l_S]}\neq S\)であり、そのような\(g\)で最大のものを\(g_0\)とする。

\(g_0\)の定義より任意の正整数\(1\leq i< m\)に対して\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0+1]})_i=S_i\)である。

\(m\)の定義より任意の正整数\(2\leq i< m\)に対して\(S_m< S_i\)である。

よって\(0\leq S_m< S_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}=\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}\)である。

\(l_S\geq l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}\)であるから、展開のデクリメント性(4)より\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}\neq0\)である。

上より展開のデクリメント性(1)より任意の正整数\(1\leq i< l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}\)に対して\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_i=\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0+1]})_i=S_i\)かつ\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}=\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0+1]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}+1=S_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}+1\)である。

よって任意の正整数\(2\leq i< m\)に対して\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}\leq S_i\)である。

\(r_S\)の定義より\(r_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}=1\)である。

\(S_m=0\)とする。

展開の上昇性(1)より\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}-1\leq\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0+2]})_m=S_m=0\)であり、また\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}>S_m=0\)であるから、\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}=1\)である。

よって\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0+1]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}=0\)である。

\(l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}< m\)とすると、\(S_m< S_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}=\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0+1]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}\)と矛盾するため、\(l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}=m\)である。

\(S_m>0\)とする。

仮定より\(S_m+1\leq2\leq \textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}\)であるから、\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}-\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{r_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}\geq2\)である。

\(l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}< m\)とすると、展開の上昇性(2)より\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}\leq\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0+1]})_m\)であるが、これは\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0+1]})_m=S_m< \textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})_{l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}}\)と矛盾するため、\(l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}=m\)である。

いずれの場合でも\(l_{\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})}=m\)であるから、\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]})=L\frown(S_m+1)\)である。

よって\(L\frown(S_m+1)\in\mathbb{OS}\)である。

\(a\)と\(\textrm{ExpandSMulti}\)の定義より、\(a'=a_{[g_0+1\colon]}\)とすると\(\textrm{ExpandSMulti}(L\frown(S_m+1),a')=\textrm{ExpandSMulti}(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon g_0]}),a')=\textrm{ExpandSMulti}(L\frown(S_m+1),a)=S\)である。

よっていずれの場合でも\(L\frown(S_m+1)\in\mathbb{OS}\)であり、かつある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a)=S\)である。□

命題 (標準形の末子列の上界)
任意の\(S\in\mathbb{OS}\setminus\{(),(0),(0,\omega)\}\)に対して、\(m=\textrm{LastChildNode}(S)\)、\(L=S_{[1\colon m-1]}\)としたときある非負整数\(n\)が存在して\(S<_\mathbb{S}\textrm{ExpandS}(L\frown(S_m+1),n)\)である。

証明

標準形の末子列の生成より、ある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a)=S\)である。

展開の辞書式縮小性より\(S=\textrm{ExpandSMulti}(L\frown(S_m+1),a)\leq_\mathbb{S}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon-1]})\)である。

\(S_m+1>0\)であるから、\(B_{L\frown(S_m+1)}\neq()\)であり、\(\textrm{ExpandS}\)の定義より$$\begin{align}S&\leq_\mathbb{S}\textrm{ExpandS}(L\frown(S_m+1),a_0)\\&=G_{L\frown(S_m+1)}\frown\bowtie(B_{L\frown(S_m+1)}(k)_{k=0}^{a_0}\\&<_\mathbb{S}G_{L\frown(S_m+1)}\frown\bowtie(B_{L\frown(S_m+1)}(k)_{k=0}^{a_0}\frown B_{L\frown(S_m+1)}(a_0+1)\\&=G_{L\frown(S_m+1)}\frown\bowtie(B_{L\frown(S_m+1)}(k)_{k=0}^{a_0+1}\\&=\textrm{ExpandS}(L\frown(S_m+1),a_0+1)\end{align}$$である。□

命題 (標準形の末子列の辞書式縮小性)
任意の\(S\in\mathbb{OS}\setminus\{(),(0),(0,\omega)\}\)に対して、\(m=\textrm{LastChildNode}(S)\)、\(R=S_{[m\colon]}\)としたとき\(R\oplus-S_m<_\mathbb{S}S\)である。

証明

\(L=S_{[1\colon m-1]}\)とする。

標準形の末子列の上界よりある非負整数\(n\)が存在して\(S<_\mathbb{S}\textrm{ExpandS}(L\frown(S_m+1),n)\)である。そのような\(n\)で最小のものを\(n_0\)とする。

\(m\)の定義より任意の正整数\(2\leq i< m\)に対して\(S_m< S_i\)である。

\(r_S\)の定義より\(r_{L\frown(S_m+1)}=1\)である。

\(G_S\)の定義より\(G_{L\frown(S_m+1)}=()\)であるから、\(\textrm{ExpandS}\)の定義より\(\textrm{ExpandS}(L\frown(S_m+1),n_0)=\bowtie(B_{L\frown(S_m+1)}(k))_{k=0}^{n_0}\)である。

\(\Delta_S\)の定義より\(\Delta_{L\frown(S_m+1)}=S_m\)であるから、上より任意の正整数\(1\leq i\leq l_S-m+1\)に対して\(\textrm{ExpandS}((L\frown(S_m+1))_{i+m-1}=\textrm{ExpandS}((L\frown(S_m+1))_i+S_m\)である。

上より\(\textrm{ExpandS}(L\frown(S_m+1),n_0)_{[m\colon-1]}\oplus-S_m=\bowtie(B_{L\frown(S_m+1)}(k))_{k=0}^{n_0-1}\)である。

よって任意の正整数\(1\leq i\leq l_{\textrm{ExpandS}(L\frown(S_m+1),n_0)}-m+1\)に対して\(\textrm{ExpandS}(L\frown(S_m+1),n_0)_i=\textrm{ExpandS}(L\frown(S_m+1),n_0)_i\)である。

\(S<_\mathbb{S}\textrm{ExpandS}(L\frown(S_m+1),n_0)\)であるから、ただ一つの正整数\(1\leq k\leq l_S\)が存在して、任意の正整数\(1\leq i\leq k\)に対して\(S_i=\textrm{ExpandS}(L\frown(S_m+1),n_0)_i\)であり、かつ\(k=l_S\)または\(S_{k+1}<\textrm{ExpandS}(L\frown(S_m+1),n_0)_{k+1}\)である。

\(k\)の定義より任意の正整数\(1\leq i\leq k-m+1\)に対して$$\begin{align}S_i&=\textrm{ExpandS}(L\frown(S_m+1),n_0)_i\\&=(\textrm{ExpandS}(L\frown(S_m+1),n_0)_{[m\colon-1]}\oplus-S_m)_i\\&=(R\oplus-S_m)_i\end{align}$$である。

\(k=l_S\)ならば、任意の正整数\(1\leq i\leq l_{R\oplus-S_m}=l_S-m+1=k-m+1\)に対して\(S_i=(R\oplus-S_m)_i\)であり、かつ\(l_{R\oplus-S_m}< l_S\)であるから、\(R\oplus-S_m<_\mathbb{S}S\)である。

\(k< l_S\)ならば、任意の正整数\(1\leq i\leq k-m+1\)に対して\(S_i=(R\oplus-S_m)_i\)であり、かつ\((R\oplus-S_m)_{k-m+2}=S_{k+1}-S_m<\textrm{ExpandS}(L\frown(S_m+1),n_0)_{k+1}-S_m=\textrm{ExpandS}(L\frown(S_m+1),n_0)_{k-m+2}=S_{k-m+2}\)であるから、\(R\oplus-S_m<_\mathbb{S}S\)である。

従って\(R\oplus-S_m<_\mathbb{S}S\)である。□

命題 (標準形の末子列は標準形)
任意の\(S\in\mathbb{OS}\setminus\{(),(0),(0,\omega)\}\)に対して、\(m=\textrm{LastChildNode}(S)\)、\(R=S_{[m\colon]}\)としたとき\(R\oplus-S_m\in\mathbb{OS}\)である。

証明

\(L=S_{[1\colon m-1]}\)とする。

標準形の末子列の生成より、\(L\frown(S_m+1)\in\mathbb{OS}\)かつある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a)=S\)である。

展開の辞書式縮小性より任意の正整数\(1\leq i\leq l_a\)に対して\(S\leq_\mathbb{S}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon i]})<_\mathbb{S}L\frown(S_m+1)\)である。

上より任意の正整数\(1\leq i\leq l_a\)に対して、\(l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon i]})}\geq l_S\)かつ任意の正整数\(1\leq i\leq m\)に対して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon i]})_j=S_j\)である。

非負整数列\(t\)を、正整数\(1\leq i\leq l_a\)のうち、任意の正整数\(2\leq j\leq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon i]})}\)に対して\(S_m\leq\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon i]})_j\)を満たす\(i\)を小さい順に並べたものとする。

非負整数列\(a'\in\mathbb{N}_{\geq0}^{l_t}\)が任意の正整数\(1\leq i\leq l_t\)に対して\(a'_i=a_{t_i}\)を満たすとする。

展開の上昇性(1)より任意の正整数\(l_{L\frown(S_m+1)}=m\leq i\leq l_{\textrm{ExpandS}(L\frown(S_m+1),a_1)}\)に対して\(\textrm{ExpandS}(L\frown(S_m+1),a_1)_i\geq (L\frown(S_m+1))_{l_{L\frown(S_m+1)}}-1=S_m\)である。

\(m\)の定義より任意の正整数\(2\leq i< m\)に対して\(S_m< S_i=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon i]})_i\)である。

任意の正整数\(2\leq i\leq l_{\textrm{ExpandS}(L\frown(S_m+1),a_1)}\)に対して\(S_m\leq\textrm{ExpandS}(L\frown(S_m+1),a_1)_i\)であるから\(t_1=1\)である。

\(S\leq_\mathbb{S}\textrm{ExpandS}(L\frown(S_m+1),a_1)\)より\(\textrm{ExpandS}(L\frown(S_m+1),a_1)\neq L=\textrm{ExpandS}(L\frown(S_m+1),0)\)であるから\(a_1>0\)である。

\(r_S\)の定義より\(r_{L\frown(S_m+1)}=1\)である。

\(G_S\)の定義より\(G_{L\frown(S_m+1)}=()\)であるから、\(\textrm{ExpandS}\)の定義より\(\textrm{ExpandS}(L\frown(S_m+1),a_1)=\bowtie(B_{L\frown(S_m+1)}(k)_{k=0}^{a_1}\)である。

\(\Delta_S\)の定義より\(\Delta_{L\frown(S_m+1)}=S_m\)であるから、上より任意の正整数\(1\leq i\leq l_S-m+1\)に対して\(\textrm{ExpandS}((L\frown(S_m+1))_{i+m-1}=\textrm{ExpandS}((L\frown(S_m+1))_i+S_m\)である。

上より$$\begin{array}{l}\textrm{ExpandS}(L\frown(S_m+1),a_1)_{[m\colon]}\oplus-S_m\\=\bowtie(B_{L\frown(S_m+1)}(k))_{k=0}^{a_1-1}\\=\textrm{ExpandS}(L\frown(S_m+1),a_1-1)\end{array}$$である。

よって$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_1]})_{[m\colon]}\oplus–S_m\\=\textrm{ExpandSMulti}(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_1]})_{[m\colon]}\oplus–S_m,())\\=\textrm{ExpandSMulti}(\textrm{ExpandS}(L\frown(S_m+1),a_1)_{[m\colon]}\oplus–S_m,())\\=\textrm{ExpandSMulti}(\textrm{ExpandS}(L\frown(S_m+1),a_1-1),())\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1))\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon1]})\end{array}$$である。

任意の正整数\(1\leq k< l_t\)をとり、$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[m\colon]}\oplus–S_m\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k]})\end{array}$$であると仮定する。

\(t\)の定義より任意の正整数\(2\leq i\leq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)に対して\(S_m\leq\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_i\)である。

上より任意の正整数\(m\leq i\leq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)に対して$$\begin{array}{l}(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[m\colon]}\oplus–S_m)_{i-m+1}\\=(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[m\colon]})_{i–m+1}–S_m\end{array}$$である。

\(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}=S_m\)とする。

\(S_m=0\)または\(a_{t_{k+1}}=0\)ならば\(\textrm{ExpandS}\)の定義より$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_{k+1}]})\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[1\colon-1]}\end{array}$$である。

\(S_m>0\)かつ\(a_{t_{k+1}}>0\)とする。

展開のデクリメント性(1)及び(2)より\(l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k+1]})}\geq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)かつ任意の正整数\(1\leq i< l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)に対して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k+1]})_i=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_i\)でありかつ$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k+1]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}-1\end{array}$$である。

任意の正整数\(t_k+1\leq p< t_{k+1}\)をとり、\(l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p]})}\geq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)かつ任意の正整数\(1\leq i< l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)に対して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]}\frown(a_p))_i=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_i\)でありかつ$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}\\<\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}\end{array}$$であると仮定する。

展開のデクリメント性(1)より\(l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p+1]})}\geq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p]})}-1\geq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}-1\)かつ任意の正整数\(1\leq i< l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)に対して$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]}\frown(a_{p+1}))_i\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]}\frown(a_p))_i\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_i\end{array}$$である。

\(p< t_{k+1}-1\)ならば、\(t_k< p+1< t_{k+1}\)であるから\(t\)の定義より\(l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p+1]})}\geq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)であり、展開の辞書式縮小性より$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p+1]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}\\\leq\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}\\<\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}\end{array}$$である。

帰納法により任意の正整数\(t_k+1\leq p\leq t_{k+1}\)に対して\(l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p]})}\geq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}-1\)かつ任意の正整数\(1\leq i< l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)に対して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]}\frown(a_p))_i=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_i\)である。

よって任意の正整数\(1\leq i< l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)に対して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_{k+1}]})_i=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_i\)である。

展開の辞書式縮小性及び\(t\)の定義より\(l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon p]})}\neq l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}\)である。

従って$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_{k+1}]})\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[1\colon-1]}\end{array}$$である。

よっていずれの場合でも$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_{k+1}]})\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[1\colon-1]}\end{array}$$である。

仮定より$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k]})}}\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}-S_m\\=0\end{array}$$であるから、\(\textrm{ExpandS}\)の定義より$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k+1]})\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k]})_{[1\colon-1]}\end{array}$$である。

従って$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_{k+1}]})_{[m\colon]}\oplus–S_m\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[m\colon-1]}\oplus-S_m\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k]})_{[1\colon-1]}\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k+1]})\end{array}$$である。

\(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{l_{\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})}}>S_m\)とする。

任意の正整数\(1\leq i< m\)に対して\(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_m=S_m< S_i=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_i\)であるから、末子列の展開より$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_{k+1}]})\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[1\colon m-1]}\frown(\textrm{ExpandS}(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[m\colon]}\oplus-\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_m,a_{t+1})\oplus\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_m)\end{array}$$である。

従って$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_{k+1}]})_{[m\colon]}\oplus–S_m\\=\textrm{ExpandS}(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[m\colon]}\oplus-\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_m,a_{t+1})\oplus\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_m\oplus-S_m\\=\textrm{ExpandS}(\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[m\colon]}\oplus-S_m,a_{t+1})\oplus S_m\oplus-S_m\\=\textrm{ExpandS}(\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k]}),a_{t+1})\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k+1]})\end{array}$$である。

よっていずれの場合でも$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_{k+1}]})_{[m\colon]}\oplus–S_m\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k+1]})\end{array}$$である。

帰納法により任意の正整数\(1\leq k\leq l_t\)に対して$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a_{[1\colon t_k]})_{[m\colon]}\oplus–S_m\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k]})\end{array}$$である。

上より$$\begin{array}{l}\textrm{ExpandSMulti}(L\frown(S_m+1),a)_{[m\colon]}\oplus–S_m\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon]})\end{array}$$である。

\(\mathbb{OS}\)の定義よりある非負整数列\(a^0\)が存在して\(\textrm{ExpandSMulti}((0,\omega),a^0)=L\frown(S_m+1)\)である。

従って$$\begin{array}{l}R\oplus-S_m\\=\textrm{ExpandSMulti}(L\frown(S_m+1),a)_{[m\colon]}\oplus–S_m\\=\textrm{ExpandSMulti}(L\frown(S_m+1),(a_1-1)\frown a'_{[2\colon k]})\\=\textrm{ExpandSMulti}(\textrm{ExpandSMulti}((0,\omega),a^0),(a_1-1)\frown a'_{[2\colon k]})\\=\textrm{ExpandSMulti}((0,\omega),a^0\frown(a_1-1)\frown a'_{[2\colon k]})\end{array}$$である。

よって\(R\oplus-S_m\in\mathbb{OS}\)である。□

命題 (標準形の子孫列は標準形)
任意の\(S\in\mathbb{OS}\setminus\{(),(0),(0,\omega)\}\)と正整数\(1\leq m\leq l_S\)に対して、任意の正整数\(m\leq i\leq l_S\)に対して\(S_m\leq S_i\)ならば\(S_{[m\colon]}\oplus-S_m\in\mathbb{OS}\)である。

証明

任意の非負整数\(t\)に対して、\(S^t\in\mathbb{S}\)と\(m^t\in\mathbb{N}_{>0}\)と以下のように定める。

\(S^0=S\)とする。

\(m^t=\max\{i\mid i\in\mathbb{N}_{>0}\land2\leq i\leq l_{S^t}\land\forall j\in\mathbb{N}_{>0}[2\leq j< i\Rightarrow S^t_i< S^t_j]\}\)とする。

\(l_S-l_{S^t}+1=m\)ならば\(S^{t+1}=S^t\)とする。

\(l_S-l_{S^t}+1\neq m\)ならば\(S^{t+1}=S^t_{[m^t\colon]}\oplus-S^t_{m^r}\)とする。

\(S^0\)の定義より\(S^0=S\in\mathbb{OS}\)かつ\(l_S-l_{S^0}+1=1\)かつ任意の正整数\(1\leq i\leq l_{S^0}\)に対して\(S^0_i=S_i=S_i-S_1=S_{i+l_S-l_{S^0}}-S_{l_S-l_{S^0}+1}\)である。

任意の非負整数\(t\)をとり、\(S^t\in\mathbb{OS}\)かつ\(l_S-l_{S^t}+1\leq m\)かつ任意の正整数\(1\leq i\leq l_{S^t}\)に対して\(S^t_i=S_{i+l_S-l_{S^t}}-S_{l_S-l_{S^t}+1}\)であると仮定する。

\(l_S-l_{S^t}+1=m\)ならば\(S^{t+1}=S^t\in\mathbb{OS}\)かつ\(l_S-l_{S^{t+1}}+1=l_S-l_{S^t}+1=m\)かつ\(S^{t+1}_{l_{S^{t+1}}}=S^t_{l_{S^t}}\neq0\)かつ任意の正整数\(1\leq i\leq l_{S^{t+1}}\)に対して\(S^{t+1}_i=S^t_i=S_{i+l_S-l_{S^t}}-S_{l_S-l_{S^t}+1}=S_{i+l_S-l_{S^{t+1}}}-S_{l_S-l_{S^{t+1}}+1}\)である。

\(l_S-l_{S^t}+1\neq m\)とする。

仮定より\(l_S-l_{S^t}+1< m\)である。

標準形の末子列は標準形より\(S^{t+1}=S^t_{[m^t\colon]}\in\mathbb{OS}\)である。

\(m^t\)の定義より任意の正整数\(m^t\leq i\leq l_S^t\)に対して\(S^t_i\geq S^t_m\)である。

上より任意の正整数\(m^t\leq i\leq l_{S^t}\)に対して\((S^t_{[m^t\colon]}\oplus-S_{m^t})_{i-m^t+1}=S^t_i-S^t_{m^t}\)である。

\(m\)の定義及び仮定より任意の正整数\(m\leq i\leq l_S\)に対して\(S^t_{m-l_S+l_{S^t}}=S_{m-l_S+l_{S^t}+l_S-l_{S^t}}-S_{l_S-l_{S^t}+1}=S_m-S_{l_S-l_{S^t}+1}\leq S_i-S_{l_S-l_{S^t}+1}=S_{i-l_S+l_{S^t}+l_S-l_{S^t}}-S_{l_S-l_{S^t}+1}=S^t_{i-l_S+l_{S^t}}\)である。

上より\(m^t+l_S-l_{S^t}>m\)とすると\(S^t_{m^t}=S^t_{m^t+l_S-l_{S^t}-l_S+l_{S^t}}\geq S^t_{m-l_S+l_{S^t}}\)であるが、仮定より\(m-l_S+l_{S^t}< m^t\)であるから\(m\)の定義より\(S^t_{m^t}< S^t_{m-l_S+l_{S^t}}\)であり矛盾するため、\(m^t+l_S-l_{S^t}\leq m\)である。

従って\(l_{S^{t+1}}\leq m\)である。

任意の正整数\(1\leq i\leq l_{S^t}-m^t+1=l_{S^{t+1}}\)に対して$$\begin{align}S^{t+1}_i&=(S^t_{[m^t\colon]}\oplus-S_{m^t})_i\\&=S^t_{i+m^t-1}-S^t_{m^t}\\&=S_{i+m^t-1+l_S-l_{S^t}}-S_{l_S-l_{S^t}+1}-S_{m^t+l_S-l_{S^t}}+S_{l_S-l_{S^t}+1}\\&=S_{i+m^t-1+l_S-l_{S^t}}-S_{m^t+l_S-l_{S^t}}\\&=S_{i+l_S-l_{S^{t+1}}}-S_{l_S-l_{S^{t+1}}+1}\end{align}$$である。

よっていずれの場合でも\(S^{t+1}\in\mathbb{OS}\)かつ\(l_S-l_{S^{t+1}}+1\leq m\)かつ任意の正整数\(1\leq i\leq l_{S^{t+1}}\)に対して\(S^{t+1}_i=S_{i+l_S-l_{S^{t+1}}}-S_{l_S-l_{S^{t+1}}+1}\)である。

帰納法により任意の非負整数\(t\)に対して\(S^t\in\mathbb{OS}\)かつ\(l_S-l_{S^t}+1\leq m\)かつ任意の正整数\(1\leq i\leq l_{S^t}\)に対して\(S^t_i=S_{i+l_S-l_{S^to}}-S_{l_S-l_{S^t}+1}\)である。

任意の非負整数\(t\)に対して\(1\leq l_S-l_{S^t}+1\leq m\)であり、かつ\(l_S-l_{S^t}+1< m\)ならば\(l_S-l_{S^t}+1< l_S-l_{S^{t+1}}+1\)であるから、ある非負整数\(t\)が存在して\(l_S-l_{S^t}+1=m\)であり、そのような\(t\)で最小のものを\(t_0\)とする。

\(l_{S^{t_0}}=l_S-m+1=l_{S_{[m\colon]}}\)である。

\(m\)の定義より任意の正整数\(m\leq i\leq l_S\)に対して\(S_m\leq S_i\)である。

上より任意の正整数\(1\leq i\leq l_S-m+1=l_{S_{[m\colon]}}\)に対して\((S_{[m\colon]}\oplus-S_m)_i=S_{i+m-1}-S_m\)である。

任意の正整数\(1\leq i\leq l_{S^{t_0}}\)に対して\(S^{t_0}_i=S_{i+l_S-l_{S^{t_0}}}-S_{l_S-l_{S^{t_0}}+1}=S_{i+m-1}-S_m\)である。

従って\(S_{[m\colon]}\oplus-S_m=S^{t_0}\)である。

よって\(S_{[m\colon]}\oplus-S_m=S^{t_0}\in\mathbb{OS}\)である。□

命題 (標準形の悪い部分は標準形)
任意の\(S\in\mathbb{OS}\setminus\{(),(0),(0,\omega)\}\)に対して、\(S_{l_S}\neq0\)ならば\(B_S\oplus-S_{r_S}\in\mathbb{OS}\)である。

証明

\(B_S\)の定義より\(B_S=S_{[r_S\colon-1]}\)である。

\(r_S\)の定義より任意の正整数\(r_S\leq i\leq l_S\)に対して\(S_{r_S}\leq S_i\)である。

標準形の子孫列は標準形より\(S_{[r_S\colon]}\oplus-S_{r_S}\in\mathbb{OS}\)である。

標準形を短縮すれば標準形より\(S_{[r_S\colon-1]}\oplus-S_{r_S}\in\mathbb{OS}\)である。

よって\(B_S\oplus-S_{r_S}\in\mathbb{OS}\)である。□

命題 (小さな標準形への経路)
任意の\((S,T)\in\mathbb{OS}^2\)に対して、\(S\leq_\mathbb{S}T\)ならばある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=S\)である。

証明

\(S=T\)ならば\(\textrm{ExpandSMulti}(T,())=T=S\)である。

\(T=(0,\omega)\)ならば、\(\mathbb{OS}\)の定義よりある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=\textrm{ExpandSMulti}((0,\omega),a)=S\)である。

\(S<_\mathbb{S}T\)かつ\(T\neq(0,\omega)\)とする。

仮定より\(S\neq(0,\omega)\)である。

\(l_S\leq2\)とする。

\(S\in\{(),(0)\}\)である。

\(\mathbb{S}\)の定義より\(S=(0)_{[1\colon l_S]}=T_{[1\colon l_S]}\)である。

標準形を短縮すれば標準形よりある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=S\)である。

\(l_S>2\)ならば、任意の\((S',T')\in\mathbb{OS}^2\)に対して、\(l_{S'}< l_S\)かつ\(S'<_\mathbb{S}T'\)ならばある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T',a)=S'\)であると仮定する。

\(f=\min\{\min(l_S,l_T)+1\}\cup\{i\mid i\in\mathbb{N}_{>0}\land1\leq i\leq\min(l_S,l_T)\land S_i\neq T_i\}\)とする。

\(f=l_S+1\)ならば、\(S=T_{[1\colon l_S]}\)であるから標準形を短縮すれば標準形よりある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=S\)である。

\(f\leq l_S\)とする。

\(S<_\mathbb{S}T\)であるから\(S_f< T_f\)である。

\(f\)の定義より\(f< l_T+1\)である。

\(f=l_T\)かつ\(S_f=T_f-1\)とする。

仮定より\(T=S_{[1\colon l_T-1]}\frown(S_{l_T}+1)\)である。

\(f\)の定義より\(l_T< l_S\)である。

\(\mathbb{OS}\)の定義よりある非負整数列\(a^0\)が存在して\(\textrm{ExpandSMulti}((0,\omega),a^0)=S\)である。

展開の辞書式縮小性及び展開のデクリメント性(1)よりある非負整数\(1\leq g\leq l_{a^0}\)が存在して\(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g]})_{[1\colon l_T]}=S_{[1\colon l_T]}\)であり、そのような\(g\)で最小のものを\(g_0\)とする。

\(S<_\mathbb{S}T\)かつ\(l_S>2\)であるから\(l_T\geq2\)である。

\(l_S>l_T\geq2\)かつ任意の非負整数\(n\)に対して\(l_{\textrm{ExpandS}((0,\omega),n)}=l_{(0,n)}=2\)であるから\(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]})\neq(0,\omega)\)である。

展開のデクリメント性(1)より\(l_{\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]})}\leq l_T\)である。

展開の切片の不変性より任意の非負整数\(n\)に対して\(\textrm{ExpandS}(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]}),n)_{[1\colon\min\{l_{\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]})},l_T\}]}=S_{[1\colon\min\{l_{\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]})},l_T\}]}\)である。

任意の非負整数列\(u\)に対して、\(u<_\mathbb{S}v<_\mathbb{S}u_{[1\colon l_u-1]}\frown(u_{l_u}+1)\)かつ\(l_v\leq l_u\)であるような非負整数列\(v\)は存在しないから、\(T\leq_\mathbb{S}\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]})\)である。

\(T<_\mathbb{S}\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]})\)とする。

仮定よりある非負整数列\(a^1\)が存在して\(\textrm{ExpandSMulti}(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]}),a^1)=T\)である。

展開の辞書式縮小性より\(\textrm{ExpandS}(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]}),a^1_1)\leq_\mathbb{S}T\)である。

\(\textrm{ExpandS}(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]}),a^1_1)_{[1\colon\min\{l_T,l_{\textrm{ExpandS}(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]}),a^1_1)}]}=S_{[1\colon\min\{l_T,l_{\textrm{ExpandS}(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]}),a^1_1)}]}\)であるから\(\textrm{ExpandS}(\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]}),a^1_1)<_\mathbb{S}T\)であるが、これは上と矛盾する。

従って\(T=\textrm{ExpandSMulti}((0,\omega),a^0_{[1\colon g_0-1]})\)である。

よって\(\textrm{ExpandSMulti}(T,a^0_{[g_0\colon]})=S\)である。

従って任意の\((S,T)\in\mathbb{OS}^2\)に対して、\(S<_\mathbb{S}T\)かつ\(f=\min\{\min(l_S,l_T)+1\}\cup\{i\mid i\in\mathbb{N}_{>0}\land1\leq i\leq\min(l_S,l_T)\land S_i\neq T_i\}\)としたとき\(f=l_T\)かつ\(S_f=T_f-1\)ならばある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=S\)である。

\(f=l_T\)かつ\(S_f< T_f-1\)とする。

標準形を減少させれば標準形よりある非負整数列\(a^0\)が存在して\(\textrm{ExpandSMulti}(T,a^0)=T_{[1\colon f-1]}\frown(S_f+1)\)である。

ある非負整数列\(a^1\)が存在して\(\textrm{ExpandSMulti}(S_{[1\colon f-1]}\frown(S_f+1),a^1)=S\)である。

\(f\)の定義より\(S_{[1\colon f-1]}=T_{[1\colon f-1]}\)である。

よって\(\textrm{ExpandSMulti}(T,a^0\frown a^1)=S\)である。

従って任意の\((S,T)\in\mathbb{OS}^2\)に対して、\(S<_\mathbb{S}T\)かつ\(f=\min\{\min(l_S,l_T)+1\}\cup\{i\mid i\in\mathbb{N}_{>0}\land1\leq i\leq\min(l_S,l_T)\land S_i\neq T_i\}\)としたとき\(f=l_T\)ならばある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=S\)である。

\(f< l_T\)とする。

標準形を短縮すれば標準形よりある非負整数列\(a^0\)が存在して\(\textrm{ExpandSMulti}(T,a^0)=T_{[1\colon f]}\)である。

ある非負整数列\(a^1\)が存在して\(\textrm{ExpandSMulti}(T_{[1\colon f]},a^1)=S\)である。

\(\textrm{ExpandSMulti}(T,a^0\frown a^1)=S\)である。

よっていずれの場合でもある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=S\)である。

帰納法により任意の\((S,T)\in\mathbb{OS}^2\)に対して、\(S<_\mathbb{S}T\)ならばある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=S\)である。

よっていずれの場合でもある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}(T,a)=S\)である。□

補題 (ω対数の長さ)
任意の\(S\in\mathbb{S}\)に対して\(l_{\log_\omega{S}}\leq l_S\)である。

証明

\(\log_\omega\)の定義中の記号を\(S\)に対して定義する。

\(l_S<2\)ならば、\(l_{\log_\omega{S}}=l_{()}=0\leq l_S\)である。

\(S=(0,\omega)\)ならば、\(l_{\log_\omega{S}}=l_{(0,\omega)}=2=l_S\)である。

\(l_S\geq2\)かつ\(S\neq(0,\omega)\)かつある正整数\(2\leq k\leq l_S\)が存在して\(S_k=0\)ならば、\(\log_\omega{S}=\log_\omega(S_{[1\colon k_0-1]})\)であり、\(k_0\)の定義より任意の正整数\(2\leq k\leq k_0-1\)に対して\((S_{[1\colon k_0-1]})_k=S_k>0\)であり、\(l_{\log_\omega(S_{[1\colon k_0-1]})}\leq l_{S_{[1\colon k_0-1]}}\)ならば\(l_{\log_\omega{S}}=l_{\log_\omega(S_{[1\colon k_0-1]})}\leq k_0-1<l_S\)であるから、\(l_S\geq2\)かつ\(S\neq(0,\omega)\)ならば任意の正整数\(2\leq k\leq l_S\)に対して\(S_k>0\)である場合のみ考えればいい。

\(l_S\geq2\)かつ\(S\neq(0,\omega)\)かつ任意の正整数\(2\leq k\leq l_S\)に対して\(S_k>0\)であるとする。

\(S_2<2\)ならば、\(l_{\log_\omega{S}}=l_{S_{[2\colon]}\oplus-1}=l_S-1< l_S\)である。

\(S_2\geq2\)とする。

\(S<_\mathbb{S}S_{[1\colon k]}\frown S_{[1\colon k]}\oplus1\frown(2)\)ならば、\(l_{\log_\omega{S}}=l_{S_{[1\colon k]}\frown S_{[k+1\colon]}\oplus-1}=k+l_S-k=l_S\)である。

\(S_{[1\colon k]}\frown S_{[1\colon k]}\oplus1\frown(2)\leq_\mathbb{S}S\)ならば、\(l_{\log_\omega{S}}=l_{S_{[k+1\colon]}\oplus-1}=l_S-k< l_S\)である。

よっていずれの場合でも\(l_{\log_\omega{S}}\leq l_S\)である。□

補題 (亜原始数列の粗い像が空列を保存すること)
任意の\(S\in\mathbb{S}\)に対して\(\textrm{S2P}_0(S)=()\)と\(S=()\)は同値である。

証明

場合分け及び帰納法により即座に従う。□

補題 (亜原始数列の像が空列でないこと)
任意の\(S\in\mathbb{S}\)に対して\(\textrm{S2P}(S)\in\mathbb{P}\)である。

証明

場合分け及び亜原始数列の粗い像が空列を保存することより即座に従う。□

補題 (自然数項が上限以下であること)
任意の正整数\(n\)に対して\((0,0)\ast n<_\mathbb{P}$\)である。

証明

\(<_\mathbb{P}\)の定義より即座に従う。□

補題 (亜原始数列の粗い像が上限以下であること)
(1) 任意の\(S\in\mathbb{S}\setminus\{(0,\omega)\}\)に対して\(\textrm{S2P}_0(S)=()\)または\(\textrm{S2P}_0(S)<_\mathbb{P}$\)である。
(2) 任意の\(S\in\mathbb{S}\)に対して\(\textrm{S2P}_0(S)=()\)または\(\textrm{S2P}_0(S)\leq_\mathbb{P}$\)である。

証明

(1) \(\textrm{S2P}_0(())=()\)である。

\(\textrm{S2P}_0((0))=((0,0))<_\mathbb{P}$\)である。

任意の非負整数\(l\geq1\)をとり、任意の\(S'\in\mathbb{S}\setminus\{(0,\omega)\}\)に対して、\(l_{S'}< l\)ならば\(\textrm{S2P}_0(S')=()\)または\(\textrm{S2P}_0(S')<_\mathbb{P}$\)であると仮定し、任意の\(S\in\mathbb{S}\setminus\{(0,\omega)\}\)をとり\(l_S=l+1\)とする。

\(\textrm{S2P}_0\)の定義中の記号を\(S\)に対して定義する。

\(l_S\geq2\)である。

\(k_0\geq2\)より\(S_{[1\colon k_0-1]}\neq()\)であるから、亜原始数列の粗い像が空列を保存することより\(\textrm{S2P}_0(S_{[1\colon k_0-1]})\neq()\)かつ\(\textrm{S2P}_0(S_{[k_0\colon]}\oplus-S_{k_0})\neq()\)である。

ω対数の長さ及び仮定より\(\textrm{S2P}_0(S_{[1\colon k_0-1]})<_\mathbb{P}$\)かつ\(\textrm{S2P}_0(S_{[k_0\colon]}\oplus-S_{k_0})<_\mathbb{P}$\)かつ、\(\textrm{S2P}_0(\log_\omega(S_{[k_0\colon]}\oplus-S_{k_0}))=()\)または\(\textrm{S2P}_0(\log_\omega(S_{[k_0\colon]}\oplus-S_{k_0}))<_\mathbb{P}$\)である。

\(S_{k_0}=0\)ならば、\(\textrm{S2P}_0(S)=\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown\textrm{S2P}_0(S_{[k_0\colon]})<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown$<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))\)である。

\(S_{k_0}=1\)ならば、\(\textrm{S2P}_0(S)=\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown\textrm{S2P}_0(S_{[k_0\colon]}\oplus-1)\boxplus(1,0)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown$\boxplus(1,0)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))\)である。

\(S_{k_0}=2\)ならば、\(\textrm{S2P}_0(S)=\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1))\frown(2,1)\ast0\frown\textrm{S2P}_0(\log_\omega(S_{[k_0\colon]}\oplus-S_{k_0})\boxplus(2,0)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1))\frown$\boxplus(2,0)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))\)である。

\(S_{k_0}=3\)ならば、\(\textrm{S2P}_0(S)=\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1))\frown(2,1)\ast1\frown\textrm{S2P}_0(\log_\omega(S_{[k_0\colon]}\oplus-S_{k_0})\boxplus(2,0)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1))\frown$\boxplus(2,0)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))\)である。

\(S_{k_0}\geq4\)ならば、\(\textrm{S2P}_0(S)=\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1))\frown(2,1)\ast S_{k_0}-2\frown\textrm{S2P}_0(\log_\omega(S_{[k_0\colon]}\oplus-S_{k_0})\boxplus(2,0)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(2,1))\frown(2,1)\ast S_{k_0}-4\frown$\boxplus(2,0)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))\)である。

よっていずれの場合でも\(\textrm{S2P}_0(S)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))\)である。

\(<_\mathbb{P}\)の定義より任意の正整数\(1\leq j\leq\min(X^{\textrm{S2P}_0(S_{[1\colon k_0-1]})},X^$)\)に対して\(\textrm{S2P}_0(S_{[1\colon k_0-1]})_{[0\colon j)}\leq_\mathbb{P}$_{[0\colon j)}\)である。

\(<_\mathbb{P}\)の定義よりある正整数\(1\leq j\leq\min(X^{\textrm{S2P}_0(S_{[1\colon k_0-1]})},X^$)\)が存在して\(\textrm{S2P}_0(S_{[1\colon k_0-1]})_{[0\colon j)}<_\mathbb{P}$_{[0\colon j)}\)であるとすると、任意の\(T\in\mathbb{P}\cup\{()\}\)に対して\(\textrm{S2P}_0(S_{[1\colon k_0-1]})_{[0\colon j)}\frown T<_\mathbb{P}$_{[0\colon j)}\)であるから、\(\textrm{S2P}_0(S_{[1\colon k_0-1]})_{[0\colon j)}=$_{[0\colon j)}\)とする。

\(X^{\textrm{S2P}_0(S_{[1\colon k_0-1]})}\geq X^$\)とすると、\(\textrm{S2P}_0(S_{[k_0\colon]}\oplus-S_{k_0})<_\mathbb{P}$\)より\(\textrm{S2P}_0(S_{[k_0\colon]}\oplus-S_{k_0})_{[0\colon X^$)}\neq$_{[0\colon X^$)}\)であり、上の条件と反するから\(X^{\textrm{S2P}_0(S_{[1\colon k_0-1]})}< X^$=4\)とする。

上の条件より\(\textrm{S2P}_0(S_{[1\colon k_0-1]})=$_{[0\colon X^{\textrm{S2P}_0(S_{[1\colon k_0-1]})})}\)である。

\(X^{\textrm{S2P}_0(S_{[1\colon k_0-1]})}=1\)ならば、\(\textrm{S2P}_0(S)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))=$_{[0\colon1)}\frown((1,1),(2,1),(3,0))=((0,0),(1,1),(2,1),(3,0))=$\)である。

\(X^{\textrm{S2P}_0(S_{[1\colon k_0-1]})}=2\)ならば、\(\textrm{S2P}_0(S)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))=$_{[0\colon2)}\frown((1,1),(2,1),(3,0))=((0,0),(1,1),(1,1),(2,1),(3,0))<_\mathbb{P}$\)である。

\(X^{\textrm{S2P}_0(S_{[1\colon k_0-1]})}=3\)ならば、\(\textrm{S2P}_0(S)<_\mathbb{P}\textrm{S2P}_0(S_{[1\colon k_0-1]})\frown((1,1),(2,1),(3,0))=$_{[0\colon3)}\frown((1,1),(2,1),(3,0))=((0,0),(1,1),(2,1),(1,1),(2,1),(3,0))<_\mathbb{P}$\)である。

よっていずれの場合でも\(\textrm{S2P}_0(S)<_\mathbb{P}$\)である。

帰納法により任意の\(S\in\mathbb{S}\setminus\{(0,\omega)\}\)に対して\(\textrm{S2P}_0(S)=()\)または\(\textrm{S2P}_0(S)<_\mathbb{P}$\)である。□

(2) (1)及び\(\textrm{S2P}((0,\omega))=$\)から即座に従う。□

系 (亜原始数列の像が上限以下であること)
任意の\(S\in\mathbb{S}\)に対して\(\textrm{S2P}(S)\leq_\mathbb{P}$\)である。

証明

亜原始数列の像が空列でないこと、自然数項が上限以下であること及び亜原始数列の粗い像が上限以下であること及びより即座に従う。□

命題 (\(\textrm{P2S}\)の上限以下の標準形上での全域性)
任意の\(M\in\mathbb{SP}\downarrow\)に対して\(\textrm{P2S}(M)\in\mathbb{S}\)である。

証明

sorry。□

命題 (\(\textrm{P2S}\)が順序を保つこと)
任意の\((M,N)\in\mathbb{SP}\downarrow^2\)に対して、\(\textrm{P2S}(M)\in\mathbb{S}\)かつ\(\textrm{P2S}(N)\in\mathbb{S}\)かつ\(M<_\mathbb{P}N\)ならば\(\textrm{P2S}(M)<_\mathbb{S}\textrm{P2S}(N)\)である。

証明

sorry。□

命題 (標準形にω対数がうまく適用できること)

任意の\(S\in\mathbb{OS}\setminus\{(0,\omega)\}\)に対して、\(l_S\geq2\)かつ任意の正整数\(2\leq k\leq l_S\)に対して\(S_k>0\)であるならば、「\(S_2<2\)ならば\(l_S<3\)または\(S_3<3\)である」かつ「\(S_2\leq2\)ならば、ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、\(S<_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\)または「\(l_S\geq2k+1\)かつ\(S_{[k+1\colon2k]}=S_{[1\colon k]}\oplus1\)かつ\(S_{2k+1}<3\)」」である。

証明

sorry。□

命題 (上限以下の標準形の変換にω冪がうまく適用できること)

任意の\(M\in\mathbb{SP}\downarrow\)に対して、\(\textrm{P2S}(M)\in\mathbb{S}\setminus\{(0,\omega)\}\)かつ\(l_{\textrm{P2S}(M)}\geq2\)かつ\(\textrm{P2S}(M)_2\geq2\)ならば、ただ一つの正整数\(2\leq k\leq l_{\textrm{P2S}(M)}\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(\textrm{P2S}(M)_i\geq2\)であり、\(k< l_{\textrm{P2S}(M)}\)かつ\(\textrm{P2S}(M)_{k+1}=0\)ならば\(\textrm{P2S}(M)_{[k+1\colon]}<_\mathbb{S}\textrm{P2S}(M)_{[1\colon k]}\frown(1)\)である。

証明

sorry。□

命題 (ω冪とω対数が互いに逆関数であること)
(1) 任意の\(S\in\mathbb{S}\setminus\{()\}\)に対して、\(l_S<2\)または\(S=(0,\omega)\)または「任意の正整数\(2\leq k\leq l_S\)に対して\(S_k>0\)であり、かつ「\(S_2<2\)ならば\(l_S<3\)または\(S_3<3\)である」かつ「\(S_2\leq2\)ならば、ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、\(S<_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\)または「\(l_S\geq2k+1\)かつ\(S_{[k+1\colon2k]}=S_{[1\colon k]}\oplus1\)かつ\(S_{2k+1}<3\)である」」」ならば、\(\exp_\omega{\log_\omega{S}}=S\)である。
(2) 任意の\(S\in\mathbb{S}\)に対して、\(S=(0,\omega)\)または\(l_S<2\)または\(S_2<2\)または「ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、\(k< l_S\)かつ\(S_{k+1}=0\)ならば\(S_{[k+1\colon]}< S_{[1\colon k]}\frown(1)\)である」ならば、\(\log_\omega{\exp_\omega{S}}=S\)である。

証明

(1) \(l_S<2\)ならば、\(S\neq()\)であるから\(S=(0)\)であるため、\(\exp_\omega{\log_\omega{S}}=\exp_\omega{()}=(0)=S\)である。

\(S=(0,\omega)\)ならば、\(\exp_\omega{\log_\omega{S}}=\exp_\omega{(0,\omega)}=(0,\omega)=S\)である。

\(l_S\geq2\)かつ\(S\neq(0,\omega)\)かつ任意の正整数\(2\leq k\leq l_S\)に対して\(S_k>0\)であるとする。

仮定より任意の正整数\(2\leq k\leq l_S\)に対して\(S_k\leq1\)であるから、任意の正整数\(2\leq k\leq l_S\)に対して\((S_{[2\colon]}\oplus-1)_{k-1}=S_k-1\)である。

上より任意の正整数\(2\leq k\leq l_S\)に対して\(S_{[k\colon]}\oplus-1\oplus1=S_{[k\colon]}\)である。

\(S_2<2\)であり、かつ\(l_S<3\)または\(S_3<3\)であるとする。

\(\log_\omega{S}=S_{[2\colon]}\oplus-1\)である。

仮定より\(l_{\log_\omega{S}}=l_S-1<2\)または\((\log_\omega{S})_2=S_3-1<2\)である。

\(\mathbb{S}\)の定義より\(S_1=0\)である。

よって$$\begin{align}\exp_\omega{\log_\omega{S}}&=(0)\frown(\log_\omega{S}\oplus-1\oplus1)\\&=(0)\frown(S_{[2\colon]}\oplus-1\oplus1)\\&=(S_1)\frown S_{[2\colon]}\\&=S\end{align}$$である。

\(S_2\geq2\)ならば、ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、かつ\(k=l_S\)または\(S_{k+1}<2\)である。

\(S<_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\)とする。

\(\log_\omega{S}=S_{[1\colon k]}\frown(S_{[k+1\colon]}\oplus-1)\)である。

仮定より任意の正整数\(2\leq i\leq k\)に対して\({\log_\omega{S}}_i=S_i\geq2\)であり、かつ\(k=l_{\log_\omega{S}}=l_S\)または\((\log_\omega{S})_{k+1}=S_{k+1}-1<2\)である。

よって$$\begin{align}\exp_\omega{\log_\omega{S}}&=(\log_\omega{S})_{[1\colon k]}\frown((\log_\omega{S})_{[k+1\colon]}\oplus-1)\\&=S_{[1\colon k]}\frown(S_{[k+1\colon]}\oplus-1\oplus-1)\\&=S_{[1\colon k]}\frown S_{[k+1\colon]}\\&=S\end{align}$$である。

\(S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\leq_\mathbb{S}S\)かつ\(l_S\geq2k+1\)かつ\(S_{[k+1\colon2k]}=S_{[1\colon k]}\oplus1\)かつ\(S_{2k+1}<3\)とする。

\(\log_\omega{S}=S_{[k+1\colon]}\oplus-1\)である。

仮定より\(S_{2k+1}=2\)かつ任意の正整数\(2\leq i\leq k\)に対して\((\log_\omega{S})_i=S_{k+i}-1=S_i+k-1=S_i\leq 2\)である。

上より\(l_{\log_\omega{S}}=l_S-k\geq k+1>k\)かつ\((\log_\omega{S})_{k+1}=S_{2k+1}-1=1<2\)である。

よって$$\begin{align}\exp_\omega{\log_\omega{S}}&=(\log_\omega{S})_{[1\colon k]}\frown(\log_\omega{S}\oplus1)\\&=(S_{[k+1\colon]}\oplus-1)_{[1\colon k]}\frown(S_{[k+1\colon]}\oplus-1\oplus1)\\&=(S_{[k+1\colon2k]}\oplus-1)\frown S_{[k+1\colon]}\\&=(S_{[1\colon k]}\oplus1\oplus-1)\frown S_{[k+1\colon]}\\&=S_{[1\colon k]}\frown S_{[k+1\colon]}\\&=S\end{align}$$である。

よって\(l_S<2\)または\(S=(0,\omega)\)または「任意の正整数\(2\leq k\leq l_S\)に対して\(S_k>0\)であり、かつ「\(S_2<2\)ならば\(l_S<3\)または\(S_3<3\)である」かつ「\(S_2\leq2\)ならば、ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、\(S<_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\)または「\(l_S\geq2k+1\)かつ\(S_{[k+1\colon2k]}=S_{[1\colon k]}\oplus1\)かつ\(S_{2k+1}<3\)である」」」ならば、\(\exp_\omega{\log_\omega{S}}=S\)である。□

(2) \(S=(0,\omega)\)ならば、\(\log_\omega{\exp_\omega{S}}=\log_\omega{(0,\omega)}=(0,\omega)=S\)である。

\(S\neq(0,\omega)\)であり、かつ\(l_S<2\)または\(S_2<2\)とする。

\(S=()\)ならば、\(\log_\omega{\exp_\omega{S}}=\log_\omega{(0)}=()=S\)である。

\(S\neq()\)ならば、仮定より\(S=(0)\)であるため、\(\log_\omega{\exp_\omega{S}}=\log_\omega{(0,1)}=(0)=S\)である。

\(S\neq(0,\omega)\)かつ\(l_S\geq2\)かつ\(S_2\geq2\)ならば、ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、かつ\(k=l_S\)または\(S_{k+1}<2\)である。

\(k=l_S\)、または\(S_{k+1}=0\)かつ\(S_{[k+1\colon]}< S_{[1\colon k]}\frown(1)\)とする。

\(\exp_\omega{S}=S_{[1\colon k]}\frown(S_{[k+1\colon]}\oplus1)\)である。

仮定より任意の正整数\(2\leq i\leq k\)に対して\({\exp_\omega{S}}_i=S_i\geq2\)であり、かつ\(k=l_S\)ならば\(k=l_{\exp_\omega{S}}=l_S\)、\(S_{k+1}=0\)ならば\((\exp_\omega{S})_{k+1}=S_{k+1}+1=1<2\)である。

\(k=l_S\)ならば、\(\exp_\omega{S}=S_{[1\colon k]}<_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\)である。

\(k\neq l_S\)かつ\(S_{k+1}=0\)かつ\(S_{[k+1\colon]}< S_{[1\colon k]}\frown(1)\)ならば、\(\exp_\omega{S}=S_{[1\colon k]}\frown(S_{[k+1\colon]}\oplus1)<_\mathbb{S}S_{[1\colon k]}\frown((S_{[1\colon k]}\frown(1))\oplus1)<_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\)である。

よっていずれの場合でも\(\exp_\omega{S}<_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)=(\exp_\omega{S})_{[1\colon k]}\frown((\exp_\omega{S})_{[1\colon k]}\oplus1)\frown(2)\)である。

よって$$\begin{align}\log_\omega{\exp_\omega{S}}&=(\exp_\omega{S})_{[1\colon k]}\frown((\exp_\omega{S})_{[k+1\colon]}\oplus-1)\\&=S_{[1\colon k]}\frown(S_{[k+1\colon]}\oplus1\oplus-1)\\&=S_{[1\colon k]}\frown S_{[k+1\colon]}\\&=S\end{align}$$である。

\(k< l_S\)かつ\(S_{k+1}=1\)とする。

\(\exp_\omega{S}=S_{[1\colon k]}\frown(S\oplus1)\)である。

仮定より\(l_{\exp_\omega{S}}=l_S+k>k\)かつ\((\exp_\omega{S})_{k+1}=S_1+1=1<2\)かつ任意の正整数\(2\leq i\leq k\)に対して\({\exp_\omega{S}}_i=S_i\geq2\)である。

\((\exp_\omega{S})_{[1\colon k]}\frown((\exp_\omega{S})_{[1\colon k]}\oplus1)\frown(2)=S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\)である。

\(\exp_\omega{S}=S_{[1\colon k]}\frown(S\oplus1)=S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(S_{k+1}+1)\frown(S_{[k+2\colon]}\oplus1)=S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\frown(S_{[k+2\colon]}\oplus1)\)である。

従って\((\exp_\omega{S})_{[1\colon k]}\frown((\exp_\omega{S})_{[1\colon k]}\oplus1)\frown(2)=S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\leq_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\frown(S_{[k+2\colon]}\oplus1)=\exp_\omega{S}\)である。

よって$$\begin{align}\log_\omega{\exp_\omega{S}}&=(\exp_\omega{S})_{[k+1\colon]}\oplus-1\\&=S\oplus1\oplus-1\\&=S\end{align}$$である。

よって\(S=(0,\omega)\)または\(l_S<2\)または\(S_2<2\)または「ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、\(k< l_S\)かつ\(S_{k+1}=0\)ならば\(S_{[k+1\colon]}< S_{[1\colon k]}\frown(1)\)である」ならば、\(\log_\omega{\exp_\omega{S}}=S\)である。□

命題 (変換写像が互いに逆関数であること)
(1) 任意の\(S\in\mathbb{OS}\)に対して\(\textrm{P2S}(\textrm{S2P}(S))=S\)である。
(2) 任意の\(M\in\mathbb{SP}\downarrow\)に対して\(\textrm{S2P}(\textrm{P2S}(M))=M\)である。

証明

sorry。□

命題 (変換写像とω冪とω対数と展開写像の合成に対しての可換性)
(1) 任意の\(S\in\mathbb{S}\setminus\{()\}\)と非負整数\(n\)に対して、\(l_S<2\)または\(S=(0,\omega)\)または「任意の正整数\(2\leq k\leq l_S\)に対して\(S_k>0\)であり、かつ「\(S_2<2\)ならば\(l_S<3\)または\(S_3<3\)である」かつ「\(S_2\leq2\)ならば、ただ一つの正整数\(2\leq k\leq l_S\)が存在して、任意の正整数\(2\leq i\leq k\)に対して\(S_i\geq2\)であり、\(S<_\mathbb{S}S_{[1\colon k]}\frown(S_{[1\colon k]}\oplus1)\frown(2)\)または「\(l_S\geq2k+1\)かつ\(S_{[k+1\colon2k]}=S_{[1\colon k]}\oplus1\)かつ\(S_{2k+1}<3\)である」」」ならば、\(\textrm{S2P}(\log_\omega(\textrm{ExpandS}(S,n)))=\textrm{ExpandP}(\textrm{S2P}(\log_\omega{S}),n)\)である。
(2) 任意の\(M\in\mathbb{SP}\downarrow\)と非負整数\(n\)に対して\(\exp_\omega(\textrm{P2S}(\textrm{ExpandP}(M,n)))=\textrm{ExpandS}(\exp_\omega(\textrm{P2S}(M)),n))\)である。

証明

sorry。□

命題 (基本列が互いに表現可能であること)
(1) 任意の\(S\in\mathbb{OS}\)と非負整数\(n\)に対して、ある正整数列\(a\)が存在して\(\textrm{S2P}(\textrm{ExpandS}(S,n))=\textrm{ExpandPMulti}(\textrm{S2P}(S),a)\)である。
(2) 任意の\(M\in\mathbb{SP}\downarrow\)と正整数\(n\)に対して、ある非負整数列\(a\)が存在して\(\textrm{P2S}(\textrm{ExpandP}(M,n))=\textrm{ExpandSMulti}(\textrm{P2S}(M),a)\)である。

証明

sorry。□

命題 (上限以下のペア数列が可算であること)
\(\mathbb{SP}\downarrow\subset\mathbb{OP}\)である。

証明

\(\mathbb{SP}\downarrow\)の定義より任意の\(M\in\mathbb{SP}\downarrow\)に対して\(M\in\mathbb{SP}\)かつ\(M<_\mathbb{P}$\)である。

　\($_0=(0,0)\)であるから\(<_\mathbb{P}\)の定義より\(M_0=(0,0)\)である。

よって定義より\(M\in\mathbb{OP}\)である。□

命題 (ペア数列システムに課された上限が標準形であること)
\($\in\mathbb{OP}\)である。

証明

\(\textrm{ExpandPMulti}(((j,j))_{j=0}^2,(3,2,1,1))=$\)であるから、の可算な標準形の起源より\($\in\mathbb{OP}\)である。□

命題 (ペア数列システムの標準形が上限以下であることの判定法)
任意の\(M\in\mathbb{P}\)に対して、\(M\in\mathbb{SP}\downarrow\)とある非負整数列\(a\)が存在して\(\textrm{ExpandPMulti}($,a)=M\)であることは同値である。

証明

ペア数列システムに課された上限が標準形であることより\($\in\mathbb{OP}\)である。

\(M\not\in\mathbb{OP}\)ならば、上限以下のペア数列が可算であることより\(M\not\in\mathbb{SP}\downarrow\)であり、の順序の線形性より任意の非負整数列\(a\)に対して\(\textrm{ExpandPMulti}($,a)\neq M\)である。

\(M\in\mathbb{OP}\)ならば、の順序の等価性より従う。□

命題 (変換写像が標準形を保存すること)
(1) 任意の\(S\in\mathbb{OS}\)に対して\(\textrm{S2P}(S)\in\mathbb{SP}\downarrow\)である。	(2) 任意の\(M\in\mathbb{SP}\downarrow\)に対して\(\textrm{P2S}(M)\in\mathbb{OS}\)である。

証明

(1) \(\mathbb{OS}\)の定義よりある非負整数列\(a\)が存在して\(\textrm{ExpandSMulti}((0,\omega),a)=S\)である。

\(\textrm{S2P}((0,\omega))=$\)である。

任意の非負整数\(k< l_a\)をとり、ある非負整数列\(a^0\)が存在して\(\textrm{S2P}(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon k]}))=\textrm{ExpandPMulti}($,a^0)\)であると仮定すると、\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon k]})\in\mathbb{OS}\)であるから基本列が互いに表現可能であること(1)よりある非負整数列\(a^1\)が存在して$$\begin{array}{l}\textrm{S2P}(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon k+1]}))\\=\textrm{S2P}(\textrm{ExpandS}(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon k]}),a_{k+1}))=\\\textrm{ExpandPMulti}(\textrm{S2P}(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon k]})),a^1)\\=\textrm{ExpandPMulti}(\textrm{ExpandPMulti}($,a^0),a^1)\\=\textrm{ExpandPMulti}($,a^0\frown a^1)\end{array}$$である。

帰納法により任意の非負整数\(k\leq l_a\)に対して、ある非負整数列\(a^0\)が存在して\(\textrm{S2P}(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon k]}))=\textrm{ExpandPMulti}($,a^0)\)である。

したがってある非負整数列\(a'\)が存在して\(\textrm{S2P}(S)=\textrm{S2P}(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon l_a]}))=\textrm{ExpandPMulti}($,a')\)である。

ペア数列システムの標準形が上限以下であることの判定法より\(\textrm{S2P}(S)\in\mathbb{SP}\downarrow\)である。□

(2) ペア数列システムの標準形が上限以下であることの判定法よりある非負整数列\(a\)が存在して\(\textrm{ExpandPMulti}($,a)=M\)である。

\(\textrm{P2S}($)=(0,\omega)\)である。

任意の非負整数\(k< l_a\)をとり、ある非負整数列\(a^0\)が存在して\(\textrm{P2S}(\textrm{ExpandPMulti}($,a_{[1\colon k]}))=\textrm{ExpandSMulti}((0,\omega),a^0)\)であると仮定すると、\(\textrm{ExpandSMulti}((0,\omega),a_{[1\colon k]})\in\mathbb{OS}\)であるから基本列が互いに表現可能であること(2)よりある非負整数列\(a^1\)が存在して$$\begin{array}{l}\textrm{P2S}(\textrm{ExpandPMulti}($,a_{[1\colon k+1]}))\\=\textrm{P2S}(\textrm{ExpandP}(\textrm{P2S}(\textrm{ExpandPMulti}($,a_{[1\colon k]})),a_{k+1}))=\\\textrm{ExpandSMulti}(\textrm{P2S}(\textrm{ExpandPMulti}($,a_{[1\colon k]})),a^1)\\=\textrm{ExpandSMulti}(\textrm{ExpandSMulti}((0,\omega),a^0),a^1)\\=\textrm{ExpandSMulti}((0,\omega),a^0\frown a^1)\end{array}$$である。

帰納法により任意の非負整数\(k\leq l_a\)に対して、ある非負整数列\(a^0\)が存在して\(\textrm{P2S}(\textrm{ExpandPMulti}($,a_{[1\colon k]}))=\textrm{ExpandSMulti}((0,\omega),a^0)\)である。

したがってある非負整数列\(a'\)が存在して\(\textrm{P2S}(M)=\textrm{P2S}(\textrm{ExpandPMulti}($,a_{[1\colon l_a]}))=\textrm{ExpandSMulti}((0,\omega),a')\)である。

\(\mathbb{OS}\)の定義より\(\textrm{P2S}(M)\in\mathbb{OS}\)である。□

命題 (変換写像の全単射性)
\(\textrm{S2P}\)は\(\mathbb{OS}\to\mathbb{SP}\downarrow\)上で全域な全単射である。

証明

sorry。□

命題 (変換写像が順序同型であること)
\(\textrm{S2P}\)が順序同型\((\mathbb{OS},\textrm{ExpandS})\to(\mathbb{SP}\downarrow,\textrm{ExpandP})\)である。

証明

sorry。□

命題 (亜原始数列の停止性)
\(f\)は全域である。

証明

変換写像が順序同型であること、の標準形ペア数列システムの停止性及びの基本列保存性と順序保存性と整礎性の関係(5)より\((\mathbb{OS},\textrm{ExpandS})\)は整礎である。

従って任意の\(S\in\mathbb{OS}\)と非負整数\(i\)に対して、\(\textrm{ExpandSMulti}(S,a_{[1\colon i]})\neq()\)であるような無限非負整数列\(a\)は存在しないから、\(\mathbb{OS}\times\mathbb{N}_{\geq0}\subset\textrm{dom}([])\)である。

\((0,\omega)\in\mathbb{OS}\)であるから\(f\)は全域である。□

命題 (亜原始数列の大きさの上界)
\((\mathbb{OS}\setminus\{(0,\omega)\},\leq_\mathbb{S})\)の順序型は\(\varphi(\omega,0)\)である。

証明

sorry。□

謝辞

• p進大好きbot氏 - このブログを書くにあたり構文を参考にいたしました。また、解析の肝であるペア数列システムからブーフホルツの表記系への変換写像の定義者であり、その全単射性を示すヒントをいただきました。
• Koteitan氏 - ボイスチャンネルにてこの写像のアイデアや指摘をいただきました。
• Yukito氏 - 亜原始数列の作者です。
• Bashicu氏 - ペア数列システムの作者です。