一句话：区分递归的精简与完全同余，证明 bisimilarity 在 ntyft/ntyxt 下满足 lean 同余，在 tyft/tyxt 下满足 full 同余。
本文研究带递归构造的进程描述语言中语义等价与预序的同余性质。作者区分两种要求：lean 同余只允许将进程的封闭子表达式替换为等价项；full 同余还允许在递归规约内部替换可能含外部绑定递归变量的子表达式。通过结构操作语义（SOS）的 ntyft/ntyxt 与 tyft/tyxt 格式，论文证明 bisimilarity 对所有 ntyft/ntyxt 语言是递归的 lean（预）同余，并在更强的 tyft/tyxt 格式下成为 full 同余。结果明确了递归替换下的同余边界，为进程演算语义格式提供了统一定理。
In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions. I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.