查看“︁变换映射”︁的源代码

变换映射方法是<code>P進大好きbot</code>发展的一个系统性地对记号进行分析和证明良序的方法。

分析一个符号时，需要将其与另一个符号进行比较。换句话说，需要明确“哪个项对应哪个项”。在传统的表格分析中，我们并非写出每个项对应的项，而是简单地选择有限个看起来美观的项，然后写出希望它们对应的项。而使用转换映射进行分析，则是一种通过将项的对应关系定义为全局映射来写出每个项对应的项的方法。

----------

带有基本列的符号指的是集合 <math>T</math> 中的一对 <math>(T,[]_{T})</math> 。

映射 <math>[]_{T} \colon T \times \mathbb {N} \to T \circ</math> 。实际中，我们经常在更抽象的场景中考虑四元组 <math>(T,[]_{T},\Gamma . 7,\mathrm {d o m}) .</math> 

1. 集合 <math>T</math> 。

2. 映射 <math>\mathbb {I}_{T} \colon T^{2} \to T</math> 。

3. 单射映射 ⌜·⌝ <math>\colon \mathbb {N} \hookrightarrow T</math> 。

4. 映射 dom: <math>T T</math> 。

以下讨论可以自然地扩展到这种情况，但为了避免复杂性，本文仅讨论前一种形式。

'''定理 1'''（与序数相关的基本列符号）

当给定可数序数 <math>\alpha</math> 和每个小于 <math>\alpha</math> 的极限序数 <math>\beta</math> 的基本列 <math>\beta[n]</math> 时，该基本列系统可以通过以下方式扩展到非极限序数：(1) 如果 <math>\beta=0</math> ，则 <math>\beta[n]= 0</math> ；(2) 如果 <math>\beta</math> 是后继序数<math>\beta^{\prime} + 1</math> ，则 <math>\beta[n]= \beta^{\prime}</math> 。如果我们将其扩展为 <math>[]_{\alpha} \colon \alpha \times {\mathbb {N}} \to \alpha</math> ，则 <math>\left(\alpha,\mathbb {I}_{\alpha} \right)</math> 成为基本列符号的最基本示例。

'''定理 2'''（基本列与序数符号关联）

设 <math>B T</math> 为与扩展的 Buchholz <math>\psi</math> 函数关联的适当符号， <math>[]_{B T} \colon B T \times B T \to B T</math> 为其标准基本列。通过将映射 <math>\left[\right]_{B T}^{\prime} \colon B T \times {\mathbb {N}} \to B T</math> 定义为 <math>t[n]_{B T}^{\prime}=t[\psi_{0}(0) + \cdot \cdot \cdot + \psi_{0}(0)]_{B T}</math> ，我们得到基本列为 <math>(B T,\left[\right]_{B T}^{\prime})</math> 的符号。

加法和 <math>\psi_{0}(0)</math> 的表达方式取决于 <math>B T</math> 的定义方式，但为了便于理解，这里我们将其表示为 <math>^ +</math> 和 <math>\psi_{0}(0)</math> 本身。这种构造不仅限于扩展的 Buchholz <math>\psi</math> 函数，对于其他具有适当定义的基础序列的 OCF 也类似。

'''定理 3'''（限制）

设 <math>(T,[]_{T})</math> 为基本列符号。如果子集 <math>T_{0} \subset T</math> 对于任意 <math>(t,n) \in T_{0} \times \mathbb {N}</math> 都满足 <math>t[n]\in T_{0}</math> ，则它就是 <math>(T,[]_{T})</math> 的限制。然后，通过将 <math>[]_{T_{0}} \colon T_{0} \times \mathbb {N} T_{0}</math> 定义为 <math>\left[\right]_{T}</math> 的限制，我们得到基本列符号 <math>(T_{0},[]_{T_{0}})</math> 。

限制的典型示例包括：所有通过适当条件化而被视为“标准形式”的项的子集，或将基本列反复应用于某个固定项而得到的所有项的子集。

可以为 <math>(T,[]_{T})</math> 定义一个类似于 Hardy 函数层次和快速增长函数层次的函数层次，因此我们将其表示为 <math>\mathrm {H H}_{T,[]_{T}}</math> 和 <math>\mathrm {F G H}_{T,[]_{T}}</math> 。 <math>\mathrm {H H}_{T,[]_{T}}</math> 和 <math>\mathrm {F G H}_{T,[]_{T}}</math> 是部分函数 <math>T \times \mathbb {N} \to \mathbb {N}</math> ，既不是全局函数也不是可计算函数。因此，如果我们想用它们来定义可计算大数，我们需要确定它们既是全局函数又是可计算函数的充分条件。此外，如果可能的话，它们不仅是全局函数、可计算函数，而且还是解析函数，也是理想的。为了实现这一点，我们引入了阶函数。

对于基本列符号 <math>(T,[]_{T})</math> ，我们定义 <math>T</math> 上的二元关系 <math>s \leq_{T,\mathbb {I}_{T}} ~ t</math> 为“存在 <math>k \in \mathbb N</math> 和<math>(n_{i})_{i=0}^{k-1} \in \mathbb {N}^{k}</math> 使得 <math>t[n_{0}]\cdot \cdot \cdot[n_{k-1}]= s^{;}</math> ”。这里，我们将 <math>k=0</math> 时左边的 <math>t[n_{0}]\cdots[n_{k-1}]</math> 定义为 <math>t</math> 。

<math>\leq_{T,\mathbb {I}_{T}}</math> 具有自反性和传递性，但通常不一定是偏序的。另一方面，示例 1 中用 <math>\left(\alpha,\big[\big]_{\alpha} \right)</math> 构造的 <math>\leq_{\alpha,\mathbb {I}_{\alpha}}</math> 和 <math>\leq_{B T,\mathbb {I}_{B T}^{\prime}}</math> 以及示例 2 中的 <math>(B T,[]_{B T}^{\prime})</math> 符合其通常的顺序，因此它们是良序的。

此外，即使 <math>(T,[]_{T})</math> 是递归的， <math>\leq_{T,\mathbb {I}_{T}}</math> 通常也不一定可计算，但示例 2 中用 <math>(B T,[]_{B T}^{\prime})</math> 构造的 <math>\leq_{B T,\mathbb {I}_{B T}^{\prime}}</math> 符合其通常的顺序，即字典序，因此它是可计算的。

通过研究 <math>\leq_{T,\mathbb {I}_{T}}</math> 的性质，我们可以推导出 <math>\mathrm {H H}_{T,[]_{T}}</math> 和 <math>\mathrm {F G H}_{T,[]_{T}}</math> 的各种性质：

'''定理 4'''（序的良基性与函数的停机性的关系）

（1）设 <math>\leq_{T,\mathbb {I}_{T}}</math> 为良基偏序，则 <math>(T,\leq_{T,\mathbb {I}_{T}})</math> 的每个全序子集的序类型的上界 <math>Lim_{T,\parallel_{T}}</math> 被确定为一个序数，且由于对 <math>\leq_{T,\mathbb {I}_{T}}</math> 的超限归纳是可证明的，故 <math>H H_{T,\parallel_{T}}</math> 和 <math>F G H_{T,\parallel_{T}}</math> 为全定义域。（因此，如果你不关心可计算性或大小，你可以用这种方式创建巨大的数字。）

（2）如果 <math>\leq_{T,\mathbb {I}_{T}}</math> 是良序序，那么 <math>\leq_{T,\mathbb {I}_{T}}</math> 的序类型是 <math>Lim_{T,\parallel_{T}}</math> ，我们可以为 <math>H H_{T,\parallel_{T}}</math> 和<math>F G H_{T,\parallel_{T}}</math> 定义极限函数，使得 <math>Lim_{T,\parallel_{T}}</math> 的序类型与递归结构相匹配。（ <math>\langle Lim_{T,\parallel_{T}}</math> 通常被称为<math>(T,[]_{T})</math> 的极限序数，虽然这本身并不能提供任何关于 <math>H H_{T,\parallel_{T}}</math> 或 <math>F G H_{T,\parallel_{T}}</math> 极限函数增长率的信息，但它常常能为分析提供线索。）

(3) 如果 <math>\leq_{T,\mathbb {I}_{T}}</math> 是递归良序，则 <math>H H_{T,\parallel_{T}} \setminus F G H_{T,\parallel_{T}}</math> 及其极限函数是全局可计算函数。（这为我们提供了一个具有保证停机性质的可计算函数，并为使用序数进行分析提供了一些线索。）

命题 4 (2) 定义了一个序数，该序数为对每个 <math>t \in T</math> 的 <math>(T,[]_{T})</math> 的限制 <math>\{t^{\prime} \in T \mid t^{\prime} \leq</math> <math>t \wedge t^{\prime} \neq t \}</math> 的极限，使得 <math>\leq_{T,\mathbb {I}_{T}}</math> 对 <math>\{t^{\prime} \in T \mid t^{\prime} \leq t \land t^{\prime} \neq t \}</math> 的限制为良序。设该序数为<math>o_{T,\parallel_{T}}(t)</math> ，并称其为 <math>t</math> 在 <math>(T,[]_{T})</math> 中的对应序数。

如果对于任意的 <math>t \in T</math> ， <math>\leq_{T,\mathbb {I}_{T}}</math> 到 <math>\{t^{\prime} \in T \mid t^{\prime} \leq t \land t^{\prime} \neq t \}</math> 的限制满足良序，则 <math>(T,[]_{T})</math> 为一棵树。根据 <math>{{\cal O}_{T,\prod_{T}}}</math> 的基本列直接定义，可知：

'''定理 5'''（树项对应序数的基本性质）

假设 <math>(T,[]_{T})</math> 是一棵树。则有：

(1) 对于任意 <math>(t,n) \in T \times \mathbb {N}</math> ， <math>o_{T,\parallel_{T}}(t)[n]\leq o_{T,\parallel_{T}}(t)_{\circ}</math> 。

(2) 对于任意 <math>t \in T</math> ，若不存在 <math>n \in \mathbb {N}</math> 使得 <math>t[n]= t</math> ，则 <math>o_{T,\parallel_{T}}(t)=\operatorname* {i n f} \{\alpha \in O n \mid \forall n \in</math> <math>\mathbb {N},o_{T,\mathbb {I}_{T}}(t[n]) \in \alpha \} .</math> 。

具体来说，在命题 5 中，如果树 <math>(T,[]_{T})</math> 满足附加条件：

1. 如果 <math>t[0]= t</math> ，则对于任意 <math>n \in \mathbb {N}</math> ， <math>t[n]= t</math> 。

2. 如果 <math>t[0]= t[1]\neq t</math> ，则对于任意 <math>n \in \mathbb {N}</math> ， <math>t[0]= t[n]</math> 。

这是一个易于分析的性质。

1. 如果 <math>t[0]= t</math> ，则 <math>o_{T,\parallel_{T}}(t)=0</math> 。

2. 如果 <math>t[0]= t[1]\neq t</math> ，则 <math>o_{T,\parallel_{T}}(t)=o_{T,\parallel_{T}}(t[0]) + 1</math> 。

3. 如果 <math>t[0]\neq t[1]</math> ，则 <math>\begin{array} {r} {o_{T,\parallel_{T}}(t)=\operatorname* {s u p}_{n \in \mathbb {N}} o_{T,\parallel_{T}}(t[n]) .} \end{array}</math> 。

现在，我们需要一种方法来研究 <math>\leq_{T,\mathbb {I}_{T}}</math> 的性质。为此，我们引入了基本列的良基性概念。

令 <math>(T,[]_{T})</math> 为具有基本列的符号。如果对于任意 <math>n \in \mathbb N</math> ， <math>t[n]= 0</math> ，则称 <math>t \in T</math> 为零项。如果对于任意 <math>t \in T</math> 且 <math>(n_{i})_{i=0}^{\infty} \in \mathbb {N}^{\omega}</math> ，存在某个 <math>k \in \mathbb N</math> 使得 <math>t[n_{0}]\cdots[n_{k-1}]</math> 为零项，则称<math>(T,[]_{T})</math> 为良基本列。

由于 <math>\leq_{T,\mathbb {I}_{T}}</math> 中严格单调递减的无限序列是通过重复应用基本列获得的序列的子序列，因此：

'''定理 6'''（基本列的良基性与序的良基性之间的关系）

<math>(T,[]_{T})</math> 的良基性等价于 <math>\leq_{T,\mathbb {I}_{T}}</math> 的良基性偏序性。特别地，如果 <math>(T,[]_{T})</math> 是一棵树，则它是良基的。

根据命题 4 和 6，为了证明由 <math>(T,[]_{T})</math> 构造的各种函数的总体，只需证明 <math>(T,[]_{T})</math> 的良基性即可。为此，引入了一个变换映射。

令 <math>(T_{1},R_{T_{1}})</math> 和 <math>(T_{2},R_{T_{2}})</math> 为严格（不相等）或（相等）偏序集，令 Trans 为 <math>T_{1} T_{2}</math> 的映射。

若“对于任意 <math>(s,t) \in T_{1} \times T_{1}</math> ，若 <math>s R_{T_{1}} t</math> ，则 <math>\mathrm {Trans}(s) R_{T_{2}} \mathrm {Trans}(t)^{,}</math> ”，则 Trans 为保序映射 <math>(T_{1},R_{T_{1}}) (T_{2},R_{T_{2}})^{\prime \prime}</math> 。如果 Trans 是双射保序映射 <math>(T_{1},R_{T_{1}}) (T_{2},R_{T_{2}})</math> ，且 Trans−1是保序映射 <math>(T_{2},R_{T_{2}}) (T_{1},R_{T_{1}})</math> ，则 Trans 是序同构 <math>(T_{1},R_{T_{1}}) (T_{2},R_{T_{2}})</math> 。注意，如果<math>R_{T_{1}}</math> 和 <math>R_{T_{2}}</math> 均为严格全序或均为全序，则 <math>\mathrm {Trans}^{-1}</math> 上的条件是自动满足的。

注意，即使将一个或两个有序集转换为更一般的二元相关集，部分有序集（无论是否相等）之间的映射的顺序保持和顺序同构的定义也相同。这种“保持某些元素的映射”通常称为同态，而“同态且逆也同态的映射”通常称为同构。

设 <math>(T_{1},\prod_{T_{1}})</math> 和 <math>(T_{2},[]_{T_{2}})</math> 为基列表示法，设 Trans 为 <math>T_{1} T_{2}</math> 的映射。

如果 Trans 是一个保序映射 <math>(T_{1},\Sigma_{T_{1},[]_{T_{1}}}) \to(T_{2},\Sigma_{T_{2},[]_{T_{2}}})</math> ，则 Trans 是一个保序映射<math>(T_{1},[]_{T_{1}}) (T_{2},[]_{T_{2}}),</math> 。

Trans 是一个序同构 (T1,[]T1) → (T2,[]T2)，这意味着 Trans 是一个序同构 (T1,≤T1,[]T <math>(T_{1},[]_{T_{1}}) (T_{2},[]_{T_{2}})</math> <math>(T_{1},\leq_{T_{1},\mathbb {I}_{T_{1}}}</math> <math>) (T_{2},\leq_{T_{2},[]_{T_{2}}}) \circ</math> 。

Trans 是一个保基本列映射 <math>(T_{1},[]_{T_{1}}) (T_{2},[]_{T_{2}})</math> ，这意味着“对于任何 <math>(t,n) \in T_{1} \times \mathbb {N}</math> <math>\operatorname {Trans}(t[n])=\operatorname {Trans}(t)[n]^ {\prime \prime}</math> 成立。

如果 Trans 是一个双射保基本列映射 <math>(T_{1},[]_{T_{1}}) (T_{2},[]_{T_{2}})</math> ，则 Trans 的基本列同构为<math>(T_{1},[l_{T_{1}}) (T_{2},[l_{T_{2}})</math> 。

注意，即使将一个或两个基本列符号转换为偏序集（包含或不包含相等性）（更一般地，具有 2 个元关系的集合），基本列符号之间的映射的保序性和保序性定义相同。例如，<math>(T_{1},[]_{T_{1}}) (T_{2},\pm_{T_{2}})</math> 的保序性是 <math>(T_{1},\Sigma_{T_{1},[]_{T_{1}}}) \to(T_{2},\Sigma_{T_{2}})</math> 的保序性。

根据定义，对于基本列符号之间的映射，保序性和保序性的定义如下：

'''定理 7'''（基本列保持性、序保持性和良基性之间的关系）

(1) 如果 Trans 是基本列同构，则 Trans 和 Trans−1 是基本列保持映射。

(2) 如果 Trans 是基本列保持映射，则 Trans 是序保持映射。

(3) 如果 Trans 是基本列同构，则 Trans 是序同构。

（4）若 Trans 为单射保序映射，且 <math>(T_{2},[]_{T_{2}})</math> 为良基映射（或树），则 <math>(T_{1},\prod_{T_{1}})</math> 为良基映射（或树），且 LimT1,[]T ≤ LimT2,[]T 。 <math>Lim_{T_{1},[]_{T_{1}}} \leq Lim_{T_{2},[]_{T_{2}}}</math> 

(5) 若 Trans 为序同构，且 <math>(T_{1},[]_{T_{1}})</math> 为良基集（或树），则 <math>(T_{2},\parallel_{T_{2}})</math> 为良基集（或树），且 <math>Lim_{T_{1},\parallel_{T_{1}}}=Lim_{T_{2},\parallel_{T_{2}}}</math> 。

此外，当将一个或两个基本列符号转换为偏序集，并将基本列符号的极限的良基性和序数替换为偏序集的良基性和部分良序集的序类型的上界时，命题 7 (4) 和 (5) 中关于极限的良基性和序数的断言仍然成立。

在实践中，很多情况下我们想要比较全序（例如字典序），而不是与基础序列相关的顺序。以下是一些在这种情况下有用的命题。对于集合 <math>T</math> 上的二元关系 <math>R_{1}</math> 和 <math>R_{2}</math> ，如果对于任何 <math>(s,t) \in T^{2}</math> ， <math>s R_{1} t</math> 成立，则 <math>R_{1}</math> 蕴涵 <math>R_{2}</math> ，并且 <math>s R_{2} t</math> 成立。

'''定理 8'''（全序没有非平凡蕴涵）

(1) 设 <math><_{1}</math> 和 <math><_{2}</math> 是集合 <math>T</math> 上的严格全序。如果 <math><_{1}</math> 蕴涵 <math><_{2}</math> ，则 <math><_{1}</math> 和 <math><_{2}</math> 相等。

(2) 设 <math>\leq_{1}</math> 和 <math>\leq_{2}</math> 是集合 <math>T</math> 上的全序。如果 <math>\leq_{1}</math> 蕴涵 <math>\leq_{2}</math> ，则 <math>\leq_{1}</math> 和 <math>\leq_{2}</math> 相等。

证明：

(2) 可直接从 (1) 推出，因此我们只需证明 (1)。假设 <math>(s,t) \in T^{2}</math> 满足 <math>s <_{2} t</math> 。只需证明 <math>s <_{1} t</math> 即可。假设情况并非如此，则会导致矛盾。由于 <math>s <_{1} \ t</math> 并非严格全序，因此 <math><_{1}</math> 是严格全序，所以 <math>s=t</math> 或 <math>t <_{1} s</math> 。

如果 <math>s=t</math> ，则 <math>s <_{2} t</math> 与 <math><_{2}</math> 是严格全序相矛盾。

如果 <math>t <_{1} s</math> ，则根据假设 <math>t <_{2} s</math> 成立，这与 <math>s <_{2} t</math> 和 <math><_{2}</math> 是严格全序相矛盾。

由于这两种情况相互矛盾，因此 <math>s <_{1} t</math> 成立。

证毕。

命题 8 本身并不常用，但以下命题（命题 8 的一个应用）可能相当容易使用。

'''定理 9'''（基本列与字典序的比较方法）

设 <math>(T_{1},\mathbb {I}_{T_{1}}</math> 为具有基本列的表示， <math>\le_{T_{1}}</math> 为 <math>T_{1}</math> 上的全序。若 Trans: <math>(T_{1},[]_{T_{1}}) </math> ，则<math>\leq_{T_{1},\parallel_{T_{1}}}</math> 蕴涵 <math>\leq_{T_{1}}</math> ，且与某个全序集 <math>(T_{2},{\leq}_{T_{2}})</math> 序同构。若 <math>(T_{2},{\leq}_{T_{2}})</math> 存在，则 <math>\leq_{T_{1},\parallel_{T_{1}}}</math> 与 <math>\leq_{T_{1}}</math> 相等。

证明：

由于 Trans 是序同构，且 <math>{\le}_{T_{2}}</math> 是全序， <math>\leq_{T_{1},[]_{T_{1}}}</math> 也是全序。由此可知，命题 8 成立。

证毕。

命题 9 主要用于证明具有基本列的符号通过变换映射是良基的，然后将该符号限制为“合适的”标准形式，使其成为关于另一个标准序的序数符号。然而，确定一个“合适的”标

准形式通常并不容易。这是因为，即使直接使用递归集的可计算基本列定义的范式是递归可枚举的，这一点显而易见，但它是递归的，这一点通常并非不证自明。有一种情况可以保证这样的范式是递归的，我们将在下文介绍。

'''定理 10'''（基本列递归枚举的基本性质）

设 <math>T</math> 为递归集， <math>[]_{T} \colon T \times \mathbb {N} \to \mathbb {N}</math> 为可计算映射， <math>\leq_{T}</math> 为 <math>T</math> 上的可计算全序，dom: <math>T </math> <math>\{0,1,2 \}</math> 为可计算映射， <math>T_{0} \subset T</math> 为有限子集，对于每个 <math>n \in \mathbb {N}</math> ，递归定义一个递归可枚举子集 <math>O T_{n} \subset T</math> ，如下所示：

(i) 若 <math>n=0</math> ，则 <math>O T_{n}:=T_{0}</math> 。

(ii) 若 <math>n \neq 0</math> ，则 <math>O T_{n}:=\{t[n]_{T} \mid(t,n) \in O T_{n-1} \times \mathbb {N} \}_{\mathsf {\Omega}} \mathrm {~,~}</math> 。

设 <math>O T</math> 是 <math>T</math> 的一个递归可枚举子集 <math>\textstyle \bigcup_{n \in \mathbb {N}} O T_{n}</math> 。若 <math>\leq_{T,\mathbb {I}_{T}}</math> 蕴涵 <math>\leq_{T}</math> ，且存在可数序数<math>\alpha</math> 和一个映射 Trans: <math>T \to \alpha</math> ，且满足：

(a) Trans 对 OT 的限制是 <math>O T \alpha</math> 双射。

(b) 对于任意 <math>(a,n) \in O T \times \mathbb {N}</math> 且 cof(<math>Trans(a))=0</math> ， <math>a[n]_{T}=a</math> 

(c) 对于任意 <math>(a,n) \in O T \times \mathbb {N}</math> 且 cof <math>Trans(a))=1</math> ， <math>Trans(a[n]_{T}) + 1=Trans(a) {\mathrm {{c}}}</math> 

(d) 对于任何 <math>a \in O T</math> 且 <math>c o f(Trans(a))=\omega</math> ， <math>(Trans(a[n]_{T}))_{n \in \mathbb {N}}</math> 是 <math>Trans(a)</math> 的基本列。

(e) 对于任何 <math>a \in O T</math> ， <math>dom(a)=\operatorname {m i n} \{c o f(Trans(a)),2 \}</math> 

证明：

我们使用一种类似于 Fish 算法（通常称为 rpakr 方法）的方法，该方法有望提供一种确定 Bashik 矩阵范式的算法。可计算子图

<math>\begin{array}{l} \downarrow \colon O T \times T \times \mathbb {N} \quad \rightarrow \quad \{0,1 \} \\ (s,a,n) \mapsto \downarrow_{s} (a,n) \\ \end{array}</math>

我们递归定义如下：

如果 <math>a=s</math> ，则 <math>\downarrow_{s}(a,n):=1</math> 。

令 <math>a \neq s</math> 

如果 <math>s \leq_{T} a</math> ，则 <math>\downarrow_{s}(a,n):=0</math> 。

令 <math>\begin{array} {r l} {s} & {{} \leq_{T} a} \end{array}</math> 

如果 <math>\mathrm {d o m}(s)=0</math> ，则 <math>\downarrow_{s}(a,n):=0</math> 。

令 <math>\mathrm {d o m}(s) \neq 0</math> 。

如果满足 <math>a \leq_{T} s[n]_{T}</math> ，则 <math>\downarrow_{s}(a,n):=\downarrow_{s[n]_{T}}(a,0)</math> 。令 <math>a \leq_{T} s[n]_{T}</math> 不满足。

如果 <math>\mathrm {d o m}(s)=1</math> ，则 <math>\downarrow_{s}(a,n):=0</math> 。

如果 <math>\mathrm {d o m}(s)=2</math> ，则 <math>\downarrow_{s}(a,n):=\downarrow_{s}(a,n + 1)</math> 。

由于条件 (a) 和 (d)，分支 22222 在有限次迭代后过渡到分支 2221。由于条件 (c) 和(d)，在分支 2221 处，

<math>\operatorname {Trans} (s[n]_{T})< \operatorname {Trans} (s)</math>

成立。因此，由于 <math>\alpha</math> 的良基性，分支 22222 和分支 2221 在有限次迭代后过渡到分支1、分支 21、分支 221 或分支 22221。由上式可知，↓ 是总定义域。

此处，令 <math>\big[\big]_{O T}</math> 为 <math>\left[\right]_{T}</math> 的定义域和陪域，分别限制为 <math>O T \times \mathbb {N}</math> 和 <math>O T</math> 。条件 (a)、(b)、(c) 和 (d) 表明，Trans 到 <math>O T</math> 的限制是 <math>(O T,\leq_{O T,\parallel_{O T}}) (\alpha,\subset)</math> 的序同构。命题 9 表明，<math>\leq_{O T,\mathbb {I}_{O T}}</math> 与 <math>\leq_{T}</math> 到 <math>O T</math> 的限制相一致，并且特别地， <math>\leq_{O T,\mathbb {I}_{O T}}</math> 是全序。

令 <math>\downarrow^{\prime}</math> 为将 ↓ 计算中所有条件分支中的 <math>\leq_{T}</math> 替换为 <math>\leq_{T,\mathbb {I}_{T}}</math> 后得到的子映射。因为 ↓ 是全定义域，且 <math>\leq_{O T,\mathbb {I}_{O T}}</math> 与 <math>\leq_{T}</math> 对 <math>O T</math> 的限制相同，所以 <math>\downarrow^{\prime}</math> 的定义域包含 <math>O T^{2} \times \mathbb {N}</math> ，且对于任何 <math>(s,a,n) \in O T^{2} \times \mathbb {N}</math> ，↓s <math>(a,n)=\downarrow_{s}^{\prime}(a,n)</math> 。因为 <math>\leq_{O T,\mathbb {I}_{O T}}</math> 是全序，所以对于任何<math>(a,s) \in O T^{2}</math> ，且 <math>a \neq s</math> ， <math>s \leq_{O T,\mathbb {I} o_{T}} a</math> 等价于 <math>a \leq_{O T,\mathbb {I} o r}</math> s。

下面我们证明，对于任意的 <math>(s,a) \in O T^{2}</math> ，若 <math>a \leq_{O T,\mathbb {I} o_{T}} s</math> 则 <math>\downarrow_{s}^{\prime}(a,0)=1</math> 。

Trans 对 <math>O T</math> 的限制是序同构 <math>(O T,\lnot o {\cal o T},\lfloor \ l o {\cal T} \rfloor \to(\alpha,\subset)</math> ，因此 <math>\mathrm {Trans}(a) \leq \mathrm {Trans}(s) .</math> 。<math>\downarrow_{s}^{\prime} ~(a,0)</math> 的递归公式只需将 <math>[]_{T}</math> 应用于 1 个参数或修改 3 个参数即可。只要 Trans 中 1 个参数的像基于条件 (c) 和 (d) 大于 Trans <math>(a)</math> ，那么在 Trans 的递归公式中，将 <math>[]_{T}</math> 应用于 1个参数的结果的像就等于或大于 Trans <math>(a)</math> 。因此，由于 <math>\alpha</math> 的良基性， <math>\downarrow_{s}^{\prime} ~(a,0)</math> 的计算最终到达分支 1。换句话说， <math>\downarrow_{s}^{\prime}(a,0)=1</math> 。

下面我们证明，对于任意 <math>(s,a) \in O T \times T</math> ， <math>a \leq_{T,\mathbb {I}_{T}} s</math> 等价于 <math>\downarrow_{s}(a,0)=1</math> 。

假设 <math>a \leq_{T,\mathbb {I}_{T}} s</math> 。在这种情况下， <math>a \in O T</math> 为真，因为 <math>s \in O T</math> 。因此， <math>a \leq_{O T,\parallel_{O T}} s</math> 为真，所以 <math>\downarrow_{s}</math> <math>{\bf \Pi}_{\cdot s} \left(a,0 \right)=\downarrow_{s}^{\prime}</math> <math>(a,0)=1</math> 。假设 <math>\downarrow_{s}</math> <math>\downarrow_{s} ~(a,0)=1</math> 。在这种情况下， <math>\downarrow</math> 的定义表明我们最终必须经过分支 1，但 <math>\downarrow</math> 的递归公式只需将 <math>\left[\right]_{T}</math> 应用于 1 个参数或更改 3 个参数，因此<math>a \leq_{T,\mathbb {I}_{T}} s</math> 。由上可知， <math>\begin{array} {r} {O T=\{a \in T \mid \sum_{s \in S_{0}} \downarrow_{s}(a,0) \neq 0 \}} \end{array}</math> ，因此 <math>O T</math> 是 <math>T</math> 的递归子集。

证毕。

请注意，命题 10 目前不适用于 Bashicu 矩阵。这是因为在 Bashicu 矩阵中尚不清楚如何获得 <math>\alpha</math> 和 Trans，即使成功获得它们，证明条件 (a) 也极其困难，尽管条件 (b)、(c) 和(d) 很容易证明。例如，单射性的常用方法是将其归结为序数的适当范式表示的唯一性。单射性通常很难。

'''定理 11'''（变换映射是否为全射的判定法）

设 <math>(T,[]_{T})</math> 为具有基本列的符号， <math>\alpha</math> 为可数序数。如果映射 Trans: <math>T \to \alpha</math> 满足以下条件，则 Trans 为全射：

(a) Trans 的像在 <math>\alpha</math> 中无界。

<math>(b)</math> 对于任意 <math>a \in T</math> ，且 <math>c o f(Trans(a))=1</math> ，则 <math>Trans(a[0]_{T}) + 1=Trans(a) {\mathrm {{\Omega}}}</math> 。

(c) 对于任何 <math>a \in T</math> 使得 <math>c o f(Trans(a))=\omega</math> ， <math>(Trans(a[n]_{T}))_{n \in \mathbb {N}}</math> 是 Trans(a) 的基本列。

证明：

根据条件 (b) 和 (c)，Trans 定义了一个保序映射 <math>(T,\leq_{T,\Vert_{T}}) \to(\alpha,\in)</math> 。因此，令 Trans的像为 <math>X</math> 。假设 <math>X \neq \alpha</math> 会导致矛盾。

根据假设， <math>\alpha \backslash X</math> 非空，因此根据 <math>\alpha</math> 的良基性，存在 <math>\alpha \setminus X</math> 的最小元素 <math>\beta</math> 。对于每个<math>i \in \mathbb N</math> ，递归定义 <math>s_{i} \in T</math> 如下：

如果 <math>i=0</math> ，则根据条件 (a)，存在 <math>s</math> 满足 <math>\beta \in \mathrm {Trans}(s)</math> ，因此定义 <math>s_{i}</math> 为这样的 <math>s</math> 之一。

如果 <math>i \neq 0</math> ，则条件 (b) 和 (c) 以及 <math>\beta \notin X</math> 意味着 <math>\{n \in \mathrm {c o f}(\mathrm {Trans}(s_{i})) ~ | ~ \beta \in s_{i-1}[n]_{T}</math> 非空，因此我们将 <math>n_{i}</math> 定义为其最小值，并设 <math>s_{i}:=s_{i-1}[n_{i}]_{T}</math> 。

然后，通过反复应用 <math>\left[\right]_{T}</math> 以及条件 (b) 和 (c) 构造 <math>(s_{i})_{i \in \mathbb {N}},(\mathrm {Trans}(s_{i}))_{i \in \mathbb {N}}</math> 可知 <math>(\mathrm {Trans}(s_{i}))_{i \in \mathbb {N}}</math> 变为 <math>\alpha</math> 的无限下降序列，这与 <math>\alpha</math> 的良基性相矛盾。从上面可知， <math>X=\alpha</math> 。

证毕。

现在，从命题 4 (1)、命题 6、命题 7 (3) 和命题 7 (5) 可知，如果我们能够得到一个基本列同构于序数的部分符号，或与序数相关的基本列的符号，那么我们就可以自动证明其良基性，证明各种函数的停机性，并立即确定该符号的序数极限。给定映射是否为基本列同构相对容易，因为只需根据基本列定义中出现的情况区分（如果可计算，则为有限多个）进行检查即可。这就是为什么证明 HPrSS 和 SAN 的停机性非常容易的原因。

另一方面，序同构不一定是基本列同构。证明非基本列同构的映射是序同构非常困难。这就是为什么对序列停机性的证明非常复杂的原因。