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系统中的非代数规则以求解单一不动点方程。鉴于过程语义的独有特性导致Salomaa证明策略失效，Milner将系统Mil的完备性列为开放问题。作为解决此问题的证明论方法，我们刻画了不动点规则为Mil的纯等式部分Mil$^-$所增添的推导能力。具体而言，我们通过一条余归纳规则实现此目标：该规则允许由具备空步的有限过程图（满足分层循环存在与消除性质LLEE）及其两个Mil$^{-}$可证解构成的循环推导。以此规则替代Mil中的不动点规则，我们定义了Mil$^{-}$的扩展系统——余归纳重构系统cMil。为证明cMil与Mil定理等价，我们建立了从Mil到cMil及其逆转换的有效证明变换。由于cMil位于互模拟关系与Milner系统Mil证明之间的中间地带，它或将成为证明Mil完备性的桥头堡。本文扩展了我们在CALCO 2022会议论文中的贡献，通过将证明变换重构为可推导规则与可采纳规则的消去过程，并将余归纳证明关联至过程图解的余代数表述。