Milner (1984) defined an operational semantics for regular expressions as finite-state processes. In order to axiomatize bisimilarity of regular expressions under this process semantics, he adapted Salomaa's proof system that is complete for equality of regular expressions under the language semantics. Apart from most equational axioms, Milner's system Mil inherits from Salomaa's system a non-algebraic rule for solving single fixed-point equations. Recognizing distinctive properties of the process semantics that render Salomaa's proof strategy inapplicable, Milner posed completeness of the system Mil as an open question. As a proof-theoretic approach to this problem we characterize the derivational power that the fixed-point rule adds to the purely equational part Mil$^-$ of Mil. We do so by means of a coinductive rule that permits cyclic derivations that consist of a finite process graph with empty steps that satisfies the layered loop existence and elimination property LLEE, and two of its Mil$^{-}$-provable solutions. With this rule as replacement for the fixed-point rule in Mil, we define the coinductive reformulation cMil as an extension of Mil$^{-}$. In order to show that cMil and Mil are theorem equivalent we develop effective proof transformations from Mil to cMil, and vice versa. Since it is located half-way in between bisimulations and proofs in Milner's system Mil, cMil may become a beachhead for a completeness proof of Mil. This article extends our contribution to the CALCO 2022 proceedings. Here we refine the proof transformations by framing them as eliminations of derivable and admissible rules, and we link coinductive proofs to a coalgebraic formulation of solutions of process graphs.

翻译：Milner（1984）将正则表达式的操作语义定义为有限状态过程。为了在此过程语义下公理化正则表达式的双相似性，他改编了Salomaa在语言语义下对正则表达式相等性完备的证明系统。除大多数等式公理外，Milner系统Mil继承了Salomaa系统用于求解单个不动点方程的非代数规则。Milner认识到过程语义的特殊性导致Salomaa证明策略无法适用，遂将系统Mil的完备性作为一个开放问题。作为对此问题的证明论研究方法，本文刻画了不动点规则为Mil的纯等式部分Mil$^-$增加的推导能力。我们通过一种余归纳规则实现这一点，该规则允许由具有空步的有限过程图（满足分层循环存在与消除性质LLEE）及其两个Mil$^{-}$可解的解组成的循环推导。以此规则替换Mil中的不动点规则，我们定义了Mil$^-$的扩展——余归纳重构cMil。为证明cMil与Mil定理等价，我们开发了从Mil到cMil及反向的有效证明变换。由于cMil介于双模拟与Milner系统Mil的证明之间，它可能成为证明Mil完备性的桥头堡。本文扩展了我们在CALCO 2022会议论文中的贡献。此处我们通过将证明变换框架化为可导出规则与可容许规则的消除来加以精炼，并将余归纳证明与过程图解向余代数表述联系起来。