  By adapting Salomaa's complete proof system for equality of regular
expressions under the language semantics, Milner (1984) formulated a sound
proof system for bisimilarity of regular expressions under the process
interpretation he introduced. He asked whether this system is complete.
Proof-theoretic arguments attempting to show completeness of this equational
system are complicated by the presence of a non-algebraic rule for solving
fixed-point equations by using star iteration.
  We characterize the derivational power that the fixed-point rule adds to the
purely equational part $\text{Mil$^{\boldsymbol{-}}$}$ of Milner's system
$\text{$\text{Mil}$}$: it corresponds to the power of coinductive proofs over
$\text{Mil$^{\boldsymbol{-}}$}$ that have the form of finite process graphs
with the loop existence and elimination property $\text{LEE}$. We define a
variant system $\text{cMil}$ by replacing the fixed-point rule in $\text{Mil}$
with a rule that permits $\text{LEE}$-shaped circular derivations in
$\text{Mil$^{\boldsymbol{-}}$}$ from previously derived equations as a premise.
With this rule alone we also define the variant system $\text{CLC}$ for merely
combining $\text{LEE}$-shaped coinductive proofs over
$\text{Mil$^{\boldsymbol{-}}$}$. We show that both $\text{cMil}$ and
$\text{CLC}$ have proof interpretations in $\text{Mil}$, and vice versa. As
this correspondence links, in both directions, derivability in $\text{Mil}$
with derivation trees of process graphs, it widens the space for graph-based
approaches to finding a completeness proof of Milner's system.
  This report is the extended version of a paper with the same title presented
at CALCO 2021.
