Higman 引理

长度可以无限增长，字母组合也可以无限变化，但若只在乎某种较短模式能否通过删除符号得到，就无法永远制造两两避开的新模式。这个结论让无界消息队列也可能拥有有限阈值表示。

顺序选对很重要。FIFO 消息丢失可以发生在中间位置，因此删除式子词关系与模型一致；只比较队首前缀则没有相同的结构保证。

真正执行一次嵌入检查 ​

对 $u=aba$、$v=baabba$，从左到右扫描 $v$：第一个 $a$ 选位置 $2$，随后 $b$ 选位置 $4$，最后 $a$ 选位置 $6$，故 $u{⪯}_{\ast }v$。这三个位置不连续，所以不是子串匹配。

有限相等字母表下，始终选最早可匹配位置的贪心算法正确：若某个嵌入把当前字母放在更晚的位置，用更早位置替代只会给后续匹配留下更多余地。两指针实现用 $O(|u|+|v|)$ 时间、常数额外空间。

最小坏序列证明如何缩短反例 ​

先说明有限字母表情形。假设存在无限坏序列。依次选择 $w_0,w_1,\dots$，每步在仍能延续为无限坏序列的词中选最短词。坏序列不含空词，因为空词嵌入所有后继。

写 $w_i=v_i{a}_i$。有限字母表使某个末字母 $a$ 在下标 $i_0<i_1<\cdots$ 上反复出现。考察

若早期 $w_j$ 嵌入某个 $v_{i_k}$，它也嵌入 $w_{i_k}$，违反原序列坏性；若 $v_{i_k}$ 嵌入 $v_{i_{\ell }}$，在末尾同时加上 $a$ 就得 $w_{i_k}{⪯}_{\ast }{w}_{i_{\ell }}$，也矛盾。因此新列仍坏，却在第 $i_0$ 位用更短的词代替了最短选择，矛盾。

一般 wqo 字母表用末字母的无限非减子列代替相同末字母子列，其他论证不变。存在这种子列是 wqo 的标准等价性质；只有“字母表无限”而没有 wqo 并不足够。

前缀顺序为什么失败 ​

在二字母表上，$ab,aab,aaab,\dots$ 互不为前缀，因此前缀顺序有无限反链；它们却在子词顺序下依次嵌入。不能把 Higman 引理中的关系随意换成更严格的匹配关系。

若无限字母表取相等关系，各不同单字母词就已构成无限反链，违反字母层面的 wqo 前提。

有损信道系统公理库有损信道系统Lossy channel system用有限控制加无界 FIFO 字串建模有损通信，以子词顺序证明兼容性，并划清丢失、可靠性与概率保证。把消息队列按子词排序；有限控制状态要求相同，多条信道逐分量比较。Higman 引理加有限乘积封闭性给 wqo，消息可丢失则负责迁移兼容性。这两项证明义务不能互相替代。

引理保证没有无限坏序列，不保证它们都短。算法复杂度还依赖每一步允许增加多少消息；有损信道验证可以远远超出通常的指数时间尺度。