一句话：证明 Milner 1984 年提出的正则表达式进程语义双相似性证明系统完备，并引入保持 LLEE 的结晶化程序处理空步图。
Milner（1984）为正则表达式的进程解释定义了双相似性，并给出了一个可靠证明系统，但其完备性长期未决。本文以概念性方式报告该证明系统完备性的证明，并对 Grabmayer 与 Fokkink（2020）关于“无 1”正则表达式限制的完备性证明作实质性精化。关键困难在于：含空步迁移且满足分层环路存在/消除性质（LLEE）的进程图，在双相似坍缩下不封闭，而仅有正常步迁移的 LLEE 图则封闭。为绕开这一障碍，作者定义了保持 LLEE 的“结晶化程序”，由此得到近坍缩的 LLEE 进程图，其强连通分量要么已坍缩，要么呈“双晶”形状。这类图可保证正则表达式进程解释的双相似坍缩存在可证明的解，从而完成完备性论证。
Milner (1984) defined a process semantics for regular expressions. He formulated a sound proof system for bisimilarity of process interpretations of regular expressions, and asked whether this system is complete. We report conceptually on a proof that shows that Milner’s system is complete, by motivating and describing all of its main steps. We substantially refine the completeness proof by Grabmayer and Fokkink (2020) for the restriction of Milner’s system to ‘1-free’ regular expressions. As a crucial complication we recognize that process graphs with empty-step transitions that satisfy the layered loop-existence/elimination property LLEE are not closed under bisimulation collapse (unlike process graphs with LLEE that only have proper-step transitions). We circumnavigate this obstacle by defining a LLEE-preserving ‘crystallization procedure’ for such process graphs. By that we obtain ‘near-collapsed’ process graphs with LLEE whose strongly connected components are either collapsed or of ‘twin-crystal’ shape. Such near-collapsed process graphs guarantee provable solutions for bisimulation collapses of process interpretations of regular expressions.