良拟序

顺序表示“至少包含同样多的资源或结构”。向上闭坏状态意味着：一旦资源配置已经坏，再添加资源也坏。有限基把无限多个坏状态压缩为有限个最小阈值。

良拟序不保证状态空间有限。它保证一直寻找“完全新的、不能由先前阈值代表的形状”不可能无限成功。这才是许多无限状态搜索能够停止的原因。

一张有限阈值清单 ​

在 ${\mathbb{N}}^2$ 的逐坐标顺序下，令

有限基为 $B=\{(3,0),(1,2)\}$。$(4,1)$ 被第一点覆盖，$(1,5)$ 被第二点覆盖，$(2,1)$ 则不在 $U$。两个基点不可比，所以不能只保留一个“最小状态”。此顺序的良拟序性由 Dickson 引理公理库Dickson 引理Dickson lemma自然数向量的逐坐标序为良拟序；用逐坐标抽取证明，并手算二维最小基和维数变化的边界。保证。

有限基的一般证明可以反证：若有限点始终覆盖不了 $U$，先取 $x_0\in U$，再取 $x_n\in U\setminus \uparrow \{x_0,\dots ,x_{n-1}\}$，便构造出无限坏序列。有限基存在来自 wqo，如何算出它则是另一项有效性要求。

良基关系仍可能有无限反链 ​

自然数上的相等关系没有严格下降链，但序列 $0,1,2,\dots$ 没有不同位置的可比对，故不是 wqo。正整数按整除排序也有无限反链：不同素数互不整除。实数通常大小顺序有无限严格下降列 $1,1/2,1/3,\dots$，同样不满足 wqo。

相反，$\mathbb{N}$ 通常顺序是 wqo，虽然有无限上升列。禁止的是无限坏序列，不是禁止所有无限变化。

向上闭集的严格增长链

在 wqo 上不可能无限持续。若每步取 $x_n\in U_{n+1}\setminus U_n$，wqo 给 $i<j$ 且 $x_i⪯x_j$。因为 $x_i\in U_{i+1}\subseteq U_j$ 且 $U_j$ 向上闭，就有 $x_j\in U_j$，矛盾。

这项增长链性质用于 后向覆盖算法公理库覆盖性的后向基算法Backward coverability algorithm从向上闭坏状态反向扩展有限基，给出 Petri 网前驱公式、完整小例运行与终止和安全不动点证明。。方向不能颠倒：$\uparrow 0⊋\uparrow 1⊋\uparrow 2⊋\cdots$ 是自然数上合法的无限递减链。

有限基和最终稳定都不是复杂度界。若每轮出现的数字或字符串长度越来越大，稳定之前仍可能经历极长计算；还需分析状态增长速率和表示成本。