by Proposition 29.

For showing statement 33, let $e_{1},e_{2}\in{\textit{StExp}}({\mathit{A}})$
be such that there is a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ with
${\mathcal{C}}({e_{1}})\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}$\rightarrow$}}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}\underline{\mathcal{C}}\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{$\leftarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}{\mathcal{C}}({e_{2}})$. We have to show
$e_{1}\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}e_{2}$.

We first note that due to Lemma 25 the extraction function $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ of a (guarded) LLEE-witness $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ of the guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ yields a Mil--provable (and hence also a Mil-
provable) solution $s$ of $\underline{\mathcal{C}}$ whose principal value we
denote by $e$. Next we apply Theorem 4.3, (ii), to extend the assumed
functional
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
to $\underline{\mathcal{C}}$ above the chart interpretations
${\mathcal{C}}({e_{1}})$ and ${\mathcal{C}}({e_{2}})$ to start from the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretations ${\underline{\mathcal{C}}}({e_{1}})$ and
${\underline{\mathcal{C}}}({e_{2}})$: we obtain
${\underline{\mathcal{C}}}({e_{1}})\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}$\rightarrow$}}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}{\mathcal{C}}({e_{1}})\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}$\rightarrow$}}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}\underline{\mathcal{C}}\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{$\leftarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}{\mathcal{C}}({e_{2}})\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{$\leftarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}{\underline{\mathcal{C}}}({e_{2}})$. By Theorem 4.3, (i), we find
that ${\underline{\mathcal{C}}}({e_{1}})$ and
${\underline{\mathcal{C}}}({e_{2}})$ are guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts.
By transitivity of  $\rightarrow$ we obtain
${\underline{\mathcal{C}}}({e_{1}})\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}$\rightarrow$}}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}\underline{\mathcal{C}}\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{$\leftarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}{\underline{\mathcal{C}}}({e_{2}})$. Now we can apply Lemma 32 to
obtain, from the Mil-provable solution $s$ of $\underline{\mathcal{C}}$, a
Mil-provable solution $L_{e_{1},2}$ of ${\underline{\mathcal{C}}}({e_{1}})$
with principal value $e$, and $L_{e_{2},2}$ of
${\underline{\mathcal{C}}}({e_{2}})$ also with principal value $e$. By Lemma
17 we furthermore obtain Mil--provable (and hence Mil-provable) solutions
$L_{e_{1},1}$ of ${\underline{\mathcal{C}}}({e_{1}})$ with principal value
$e_{1}$, and $L_{e_{2},1}$ of ${\underline{\mathcal{C}}}({e_{2}})$ with
principal value $e_{2}$. The two Mil-provable solutions $L_{e_{1},1}$ and
$L_{e_{1},2}$ of the guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
${\underline{\mathcal{C}}}({e_{1}})$ can be combined to a LLEE-witnessed
coinductive proof $\langle{\underline{\mathcal{C}}}({e_{1}}),\hskip
0.5ptL_{e_{1}}\rangle$ of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e$
over Mil. Analogously, the two Mil-provable solutions $L_{e_{2},1}$ and
$L_{e_{2},2}$ of the guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
${\underline{\mathcal{C}}}({e_{2}})$ can be combined to a LLEE-witnessed
coinductive proof $\langle{\underline{\mathcal{C}}}({e_{2}}),\hskip
0.5ptL_{e_{2}}\rangle$ of
$e_{2}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e$
over Mil. Together we obtain:

$e_{1}\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{\text{\sf Mil}}}}e\;\;\text{ and
}\;\;e_{2}\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{\text{\sf Mil}}}}e\hskip 1.5pt{.}$

Now by an appeal to Proposition 29 we obtain $e_{1}\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}e$ and $e_{2}\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}e$.
Finally, by applying of symmetry and transitivity rules in Mil we obtain
$e_{1}\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}e_{2}$.

######  Remark 34.

While both of the statements 33 and 33 of Corollary 33 were important pieces
of the puzzle for constructing the completeness proof for Mil as sketched in
[Gra22a], neither of them yields such a proof directly. This is because of the
following two facts: First, two bisimilar chart interpretations do not always
have a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
as their joint expansion along  $\leftarrow$ . This can be demonstrated with
the counterexample of the charts in Example 4.1 of [GF20a]. As a consequence,
33 is sometimes not applicable. Second, two bisimilar chart interpretations do
not in general have a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
as their joint minimization along  $\rightarrow$ . This is an easy consequence
of the counterexample that is described in [Gra22a, Sect. 6]. Therefore direct
application of 33 is also excluded in some situations.

Yet more sophisticated applications of 33 and 33 can still turn out to be
expedient. Indeed, a strengthening of 33 has helped us settle a subcase, and a
refinement of 33 has led to completeness proof for Mil as sketched in
[Gra22a]. In [GF20a], Fokkink and I have employed the stronger and more
specific version of the joint minimization idea in Corollary 33, 33, for a
completeness proof of an adaptation BBP by Bergstra, Bethke, and Ponse of Mil
to ‘$1$-free star expressions’ (without $1$, and with binary iteration instead
of unary iteration). Concretely, we used that bisimilar chart interpretations
of $1$-free star expressions have LLEE-charts as their bisimulation collapses
(and thus have guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
as joint minimizations). The completeness proof for Mil as summarized in
[Gra22a] has been built around a more involved argument that employs
‘crystallized’ LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
approximations of the joint bisimulation collapse of bisimilar chart
interpretations.

##  7\. From Milner’s system to LLEE-witnessed coinductive proofs

In this section we develop a proof-theoretic interpretation of Mil in the
subsystem cMil1 of cMil, and hence also a proof-theoretic interpretation of
Mil in cMil. Since Mil and cMil1 differ only by the fixed-point rule
$\textrm{RSP}^{*}$ (which is part of Mil, but not of cMil) and the rule
LCoProof1 (which is part of cMil1, but not of Mil), the crucial step for this
proof transformation is to show that instances of $\textrm{RSP}^{*}$ can be
mimicked in cMil1.

We will do so by showing that instances of $\textrm{RSP}^{*}$ are derivable in
cMil1, and in particular, can be mimicked by instances of LCoProof1. More
precisely, we will show that every instance $\iota$ of the fixed-point rule
$\textrm{RSP}^{*}$ of Mil can be mimicked by an instance of LCoProof1 that has
the same premise and conclusion, and that uses as its side-condition a LLEE-
witnessed coinductive proof over Mil- in which the premise of $\iota$ may be
used. Still more explicitly, we show that every $\textrm{RSP}^{*}$-instance
with premise $e=f\,{{\cdot}}\,e+g$ such that ${f}{{\downarrow}}$ and with
conclusion $e=f^{*}\,{{\cdot}}\,g$ gives rise to a coinductive proof of
$e=f^{*}\,{{\cdot}}\,g$ over ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{e=f\,{{\cdot}}\,e+g}\right\\}}$ with
underlying
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
${\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})$ and guarded LLEE-witness
${\hskip 0.2pt\hat{\underline{\mathcal{C}}}}({f^{*}\,{{\cdot}}\,g})$.

We first illustrate this mimicking step by a concrete example (see Example 7),
in order to motivate and convey the idea of this proof transformation. It will
be built on three auxiliary statements (see after Example 7) two of which we
have shown already in Section 4. Subsequently we prove the remaining crucial
auxiliary statement (Lemma 35), and then establish the transformation by
showing that $\textrm{RSP}^{*}$ is a derivable rule in cMil1 (Lemma 37, using
Lemma 36). Finally we use derivability of $\textrm{RSP}^{*}$ in cMil1 in order
to obtain the proof transformation from Mil to cMil1 (see Theorem 38).

We consider an instance of $\textrm{RSP}^{*}$ that corresponds, up to an
application of ${\text{r-distr}}({+,{\cdot}})$, to the instance of
$\textrm{RSP}^{*}$ at the bottom in Figure 13:

$\mathord{\overbrace{(a+b)^{*}}^{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}\mathord{}$$\overbrace{((a\cdot
a^{*}+b)\cdot
b^{*})}^{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\cdot\overbrace{(a+b)^{*}}^{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}+\overbrace{1}^{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}$
$\textrm{RSP}^{*}$ (where
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}{\ndownarrow}$)
$\mathord{\underbrace{(a+b)^{*}}_{\smash{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}\mathord{}$$\underbrace{((a\cdot
a^{*}+b)\cdot
b^{*})^{*}}_{\smash{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}}}\cdot\underbrace{1}_{\smash{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}}$
(21)

We want to mimic this instance of $\textrm{RSP}^{*}$ by an instance of
LCoProof1 that uses a LLEE-witnessed coinductive proof of
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\cdot{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
over Mil- plus the premise of the $\textrm{RSP}^{*}$ instance (21). We first
obtain the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{f^{*}}}})$
of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{f^{*}}}$
according to Definition 4.2, see Figure 15, together with its LLEE-witness
${\hskip
0.2pt\hat{\underline{\mathcal{C}}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{f^{*}}}})\,$
that is guaranteed by Theorem 4.3.

$((1\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,a^{*})\,{\cdot}\,b^{*})\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$$((1\,{\cdot}\,a^{*})\,{\cdot}\,b^{*})\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$$a$$b$$(a^{*}\,{\cdot}\,b^{*})\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$$a$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[1]}}$$b$$(1\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,b^{*})\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$$(1\,{\cdot}\,b^{*})\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$$b$$b^{*}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$$b$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[1]}}$$\underbrace{{((a\,{\cdot}\,a^{*}+b)\,{\cdot}\,b^{*})^{*}}}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}}$$a$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[2]}}$$b$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[2]}}$
Figure 15. The
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}})$
for ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$
as in (21) in Example 7.

Due to Lemma 17 the iterated partial 1-derivatives as depicted define a Mil--
provable solution of
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{f^{*}}}})$
when stacked products
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$
are replaced by products ${\cdot}\,$. From this LLEE-witness that carries a
Mil-provable solution we now obtain a LLEE-witnessed coinductive proof of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
under the assumption of
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$,
as follows. By replacing parts
$({\ldots})\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$
by
${\pi}({({\ldots})})\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}$
in the Mil-provable solution of
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}})$,
and respectively, by replacing
$({\ldots})\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$
by
$({\pi}({({\ldots})})\,{{\cdot}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}})\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
we obtain the left- and the right-hand sides of the formal equations in the
cyclic derivation in Figure 16.

$((1\,{{\cdot}}\,a^{*})\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}(((1\,{{\cdot}}\,a^{*})\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}})\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$$((1\,{{\cdot}}\,a^{*})\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}(((1\,{{\cdot}}\,a^{*})\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}})\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$$a$$b$$(a^{*}\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}((a^{*}\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}})\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$$a$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[1]}}$$b$$(1\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}((1\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}})\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$$(1\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}((1\,{{\cdot}}\,b^{*})\,{{\cdot}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}})\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$$b$$b^{*}\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}(b^{*}\,{{\cdot}}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}})\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$$b$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[1]}}$$\underbrace{\underbrace{{((a\,{{\cdot}}\,a^{*}+b)\,{{\cdot}}\,b^{*})}\rule[-10.0pt]{0.0pt}{11.5pt}}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\,{{\cdot}}\,\underbrace{(a+b)^{*}\rule[-10.0pt]{0.0pt}{11.5pt}}_{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}+\underbrace{1\rule[-10.0pt]{0.0pt}{11.5pt}}_{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}}_{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}\>{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\;\;\text{\small(by
rule
assumption)}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}\underbrace{{(((a\,{{\cdot}}\,a^{*}+b)\,{{\cdot}}\,b^{*})^{*}\rule[-10.0pt]{0.0pt}{11.5pt}}}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}}\,{{\cdot}}\,\underbrace{1\rule[-10.0pt]{0.0pt}{11.5pt}}_{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}$$a$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[2]}}$$b$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[2]}}$
Figure 16. LLEE-witnessed coinductive proof of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\cdot{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
over ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\mathrel{{\cdot}}{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}}+{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}}\right\\}}\,$.

That derivation is a LLEE-witnessed coinductive proof $\mathcal{LCP}$ of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\cdot{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
over ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\mathrel{{\cdot}}{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}}+{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}}\right\\}}\,$:
The right-hand sides form a Mil-provable solution of
${\mathcal{C}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\cdot{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}})$
due to Lemma 17 (note that
${\mathcal{C}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\cdot{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}})$
is isomorphic to
${\mathcal{C}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}})$
due to
${\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}\mathrel{{\equiv}}1$).
The left-hand sides also form a solution of
${\mathcal{C}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\cdot{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}})$
(see Lemma 35 below), noting that for the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions
back to the conclusion the assumption
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
must be used in addition to Mil-. By using this assumption again, the result
$\mathcal{LCP^{\prime}}$ of replacing
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
in the conclusion of $\mathcal{LCP}$ by
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}$
is also a LLEE-witnessed coinductive proof over ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\mathrel{{\cdot}}{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}}+{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}}\right\\}}$.
Consequently:

${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\mathrel{{\cdot}}{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}}+{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}$
${\mathcal{LCP}_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\mathrel{{\cdot}}{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}}+{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}}\right\\}}}}({{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}^{*}}}\mathrel{{\cdot}}{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}})$
LCoProof1
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{f^{*}}}}\mathrel{{\cdot}}{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}$
(22)

is a rule instance of cMil and CLC by which we have mimicked the
$\textrm{RSP}^{*}$ instance in (21).

By examining the steps that we used in the example above, we find that three
main auxiliary statements were used for the construction of a LLEE-witnessed
coinductive proof that mimics an instance of the fixed-point rule
$\textrm{RSP}^{*}$ by an instance of LCoProof1. In relation to an instance of
$\textrm{RSP}^{*}$ of the generic form as in Definition 2.1, these are the
statements that, for all star expressions $e$, $f$, and $g$, it holds:

  1. (a)

The
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation ${\underline{\mathcal{C}}}({e})$ of a star expressions $e$ is a
guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart.

  2. (b)

$e$ is the principal value of a Mil--provable solution of the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation ${\underline{\mathcal{C}}}({e})$ of $e$.

  3. (c)

$e$ is the principal value of a $({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{e=f\,{{\cdot}}\,e+g}\right\\}})$-provable
solution of the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation ${\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})$ of
$f^{*}\,{{\cdot}}\,g$.

While (a) is guaranteed by Theorem 4.3, and (b) by Lemma 17, we are now going
to justify the central statement (c) by proving the following lemma.

######  Lemma 35.

Let $e,f,g\in{\textit{StExp}}({\mathit{A}})$ with
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{f}{\ndownarrow}}$,
and let
$\Gamma\mathrel{{:=}}\left\\{{e={{f}\mathrel{{\cdot}}{e}}+{g}}\right\\}$. Then
$e$ is the principal value of a $({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})$-provable solution of the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation ${\underline{\mathcal{C}}}({{{f^{*}}}\mathrel{{\cdot}}{g}})$ of
${f^{*}}{\,{{\cdot}}\,}{g}$.

######  Proof 7.1.

First, it can be verified that the vertices of
${\underline{\mathcal{C}}}({f^{*}\cdot g})$ are of either of three forms:

${V}({{\underline{\mathcal{C}}}({f^{*}\cdot g})})=\left\\{{f^{*}\cdot
g}\right\\}\cup\bigl{\\{}{(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\cdot
g}\mathrel{\big{|}}{F\in{{\underline{\partial}^{+}}}({f})}\bigr{\\}}\cup\left\\{{G}\mathrel{|}{G\in{{\underline{\partial}^{+}}}({g})}\right\\}\hskip
1.5pt{,}$ (23)

where ${{\underline{\partial}^{+}}}({f})$ means the set of iterated
1-derivatives of $f$ according to the TSS in Def. 4.2.

This facilitates to define a function
$s\mathrel{:}{V}({{\underline{\mathcal{C}}}({f^{*}\cdot
g})})\to{\textit{StExp}}({\mathit{A}})$ on
${\underline{\mathcal{C}}}({f^{*}\cdot g})$ by:

$\displaystyle{s}({f^{*}\,{{\cdot}}\,g})$
$\displaystyle{}\mathrel{{:=}}e\hskip 1.5pt{,}$
$\displaystyle{s}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})$
$\displaystyle{}\mathrel{{:=}}{\pi}({F})\,{{\cdot}}\,e\hskip 1.5pt{,}$ (for
$F\in{{\underline{\partial}^{+}}}({f})$), $\displaystyle{s}({G})$
$\displaystyle{}\mathrel{{:=}}{\pi}({G})$ (for
$G\in{{\underline{\partial}^{+}}}({g})$),

We will show that $s$ is a $({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})$-provable solution of
${\underline{\mathcal{C}}}({f^{*}\cdot g})$. Instead of verifying the
correctness conditions for $s$ for list representations of transitions, we
will argue more loosely with sums over action 1-derivatives sets
${\textit{\text@underline{A$\partial$}}}({H})$ of stacked star expressions $H$
where such sums are only well-defined up to ACI. Due to $\text{\sf
ACI}\mathrel{{\sqsubseteq}}\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}$ such an
argumentation is possible. Specifically we will demonstrate, for all
$E\in{V}({{\underline{\mathcal{C}}}({f^{*}\cdot g})})$, that $s$ is a
$({\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})$-provable solution
at $E$, that is, that it holds:

${s}({E})\mathrel{{=_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}\hskip
1.0pt}}{\tau_{{\underline{\mathcal{C}}}({E})}}({E})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptE^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({E})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({E^{\prime}})\hskip
1.5pt{,}$ (24)

where by the sum on the right-hand side we mean an arbitrary representative of
the ACI equivalence class of star expressions that is described by the sum
expression of this form.

For showing (24), we distinguish the three cases of vertices
$E\in{V}({{\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})})$ according to
(23), that is, $E\mathrel{{\equiv}}f^{*}\,{{\cdot}}\,g$,
$E\mathrel{{\equiv}}(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g$
for some $F\in{{\underline{\partial}^{+}}}({f})$, and $E\mathrel{{\equiv}}G$
for some $G\in{{\underline{\partial}^{+}}}({g})$. We will see that the
assumption $\Gamma$ will only be needed for the treatment of the first case.

In the first case, we consider $E\mathrel{{\equiv}}f^{*}\,{{\cdot}}\,g$. We
find by Lemma 14 (or by inspecting the TSS in Definition 4.2), and in view of
(23):

$\displaystyle{\textit{\text@underline{A$\partial$}}}({f^{*}\,{{\cdot}}\,g})$
$\displaystyle{}=\left\\{{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5pt(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g\rangle}\mathrel{|}{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF\rangle\in{\textit{\text@underline{A$\partial$}}}({f})}\right\\}\cup{\textit{\text@underline{A$\partial$}}}({g})\hskip
1.5pt{,}$ (25)
$\displaystyle\begin{split}{{\underline{\partial}}}({f^{*}\,{{\cdot}}\,g})&{}=\left\\{{(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g}\mathrel{|}{F\in{{\underline{\partial}}}({f})}\right\\}\cup{{\underline{\partial}}}({g})\\\
&{}\subseteq\left\\{{(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g}\mathrel{|}{F\in{{\underline{\partial}^{+}}}({f})}\right\\}\cup{{\underline{\partial}^{+}}}({g})\subseteq{V}({{\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})})\hskip
1.5pt{.}\end{split}$ (26)

Then (26) guarantees that $s$ is defined for all partial 1-derivatives of
$E\mathrel{{\equiv}}f^{*}\cdot g$. With this knowledge we can argue as
follows:

$\displaystyle{s}({E})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{s}({f^{*}\,{{\cdot}}\,g})\qquad\quad\text{(by
$E\mathrel{{\equiv}}f^{*}\,{{\cdot}}\,g$)}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>e\phantom{{}\cdot
e+g}\qquad\quad\text{(by the definition of $s$)}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}\hskip
1.0pt}}$}\>f\,{{\cdot}}\,e+g\qquad\quad\text{(since
$\Gamma=\left\\{{e=f\,{{\cdot}}\,e+g}\right\\}$)}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>\Big{(}{\tau_{{\underline{\mathcal{C}}}({f})}}({f})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF\rangle\in{\textit{\text@underline{A$\partial$}}}({f})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{\pi}({F})\Big{)}\,{{\cdot}}\,e+\Big{(}{\tau_{{\underline{\mathcal{C}}}({g})}}({g})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptG\rangle\in{\textit{\text@underline{A$\partial$}}}({g})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{\pi}({G})\Big{)}$
(by using Lemma 16)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>\Big{(}{\tau_{{\underline{\mathcal{C}}}({f})}}({f})\,{{\cdot}}\,e+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF\rangle\in{\textit{\text@underline{A$\partial$}}}({f})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,({\pi}({F})\,{{\cdot}}\,e)\Big{)}+\Big{(}{\tau_{{\underline{\mathcal{C}}}({g})}}({g})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptG\rangle\in{\textit{\text@underline{A$\partial$}}}({g})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{\pi}({G})\Big{)}$
(by using (${\text{r-distr}}({+,{\cdot}})$) and (${\text{assoc}}({{\cdot}})$))
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>\Big{(}\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF\rangle\in{\textit{\text@underline{A$\partial$}}}({f})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,({\pi}({F})\,{{\cdot}}\,e)\Big{)}+\Bigl{(}{\tau_{{\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})}}({f^{*}\,{{\cdot}}\,g})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptG\rangle\in{\textit{\text@underline{A$\partial$}}}({g})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{\pi}({G})\Bigr{)}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf ACI}}\hskip
1.0pt}}$}\>{\tau_{{\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})}}({f^{*}\,{{\cdot}}\,g})+\Big{(}\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF\rangle\in{\textit{\text@underline{A$\partial$}}}({f})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,({s}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\cdot
g}))\Big{)}+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptG\rangle\in{\textit{\text@underline{A$\partial$}}}({g})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({G})$
(by definition of $s$, axioms (${\text{comm}}({+})$))
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf ACI}}\hskip
1.0pt}}$}\>{\tau_{{\underline{\mathcal{C}}}({E})}}({E})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptE^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({f^{*}\cdot
g})={\textit{\text@underline{A$\partial$}}}({E})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({E^{\prime}})$
(by $E\mathrel{{\equiv}}f^{*}\,{{\cdot}}\,g$ and (25)).

Due to $\text{\sf ACI}\mathrel{{\sqsubseteq}}\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}\mathrel{{\sqsubseteq}}{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$ this chain of equalities is provable
in ${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$, which verifies
(24) for $E$ as considered here, or in other words, $s$ is a
$({\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})$-provable solution
of at $E$.

In the second case we consider
$E\mathrel{{\equiv}}(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g\in{V}({{\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})})$.
Then $F\in{{\underline{\partial}^{+}}}({f})$, and
${\tau_{{\underline{\mathcal{C}}}({E})}}({E})\mathrel{{\equiv}}{\tau_{{\underline{\mathcal{C}}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})\mathrel{{\equiv}}0$
holds, because expressions with stacked product occurring do not have
immediate termination by Definition 4.2. We distinguish the subcases
${F}{{\downarrow}}$ and ${F}{\ndownarrow}$.

For the first subcase we assume ${F}{\ndownarrow}$. Then
${\tau_{{\underline{\mathcal{C}}}({F})}}({F})\mathrel{{\equiv}}0$ holds, and
we find by Lemma 14 (or by inspecting the TSS in Definition 4.2), by
$F\in{{\underline{\partial}^{+}}}({f})$, and from (23):

$\displaystyle{\textit{\text@underline{A$\partial$}}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})$
$\displaystyle{}=\left\\{{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5pt(F^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g\rangle}\mathrel{|}{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({F})}\right\\}\hskip
1.5pt{,}$ (27)
$\displaystyle\begin{split}{{\underline{\partial}}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})&{}=\left\\{{(F^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g}\mathrel{|}{F^{\prime}\in{{\underline{\partial}}}({F})}\right\\}\\\
&{}\subseteq\left\\{{(F^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g}\mathrel{|}{F^{\prime}\in{{\underline{\partial}^{+}}}({f})}\right\\}\subseteq{V}({{\underline{\mathcal{C}}}({f^{*}\cdot
g})})\hskip 1.5pt{.}\end{split}$ (28)

Due to (28), $s$ is defined for all partial 1-derivatives of
$E\mathrel{{\equiv}}(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g$.
We argue as follows:

$\displaystyle{s}({E})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{s}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})$
(by
$E\mathrel{{\equiv}}(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\pi}({F})\,{{\cdot}}\,e$
(by the definition of $s$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>\Big{(}{\tau_{{\underline{\mathcal{C}}}({F})}}({F})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({F})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{\pi}({F^{\prime}})\Big{)}\,{{\cdot}}\,e$
(by using Lemma 16)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>0\,{{\cdot}}\,e+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({F})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,({\pi}({F^{\prime}})\,{{\cdot}}\,e)$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>0+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({F})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({(F^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})$
(by ax. (deadlock) and def. of $s$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf ACI}}\hskip
1.0pt}}$}\>{\tau_{{\underline{\mathcal{C}}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptE^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({E^{\prime}})$
(due to (27), and
${\tau_{{\underline{\mathcal{C}}}({E})}}({E})\mathrel{{\equiv}}0)$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\tau_{{\underline{\mathcal{C}}}({E})}}({E})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptE^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({E})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({E^{\prime}})$
(by
$E\mathrel{{\equiv}}(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g$).

For the second subcase we assume ${F}{{\downarrow}}$. Then
$F\in{\textit{StExp}}({\mathit{A}})$ (that is, $F$ does not contain a stacked
product symbol), and
${\tau_{{\underline{\mathcal{C}}}({F})}}({F})\mathrel{{\equiv}}1$ holds.
Furthermore, we find, again by inspecting the TSS in Definition 4.2, by
$F\in{{\underline{\partial}^{+}}}({f})$, and in view of (23):

$\displaystyle{\textit{\text@underline{A$\partial$}}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})$
$\displaystyle{}=\left\\{{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1},\hskip
0.5ptf^{*}\,{{\cdot}}\,g\rangle}\right\\}\cup\left\\{{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5pt(F^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g\rangle}\mathrel{|}{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({F})}\right\\}\hskip
1.5pt{.}$ (29)
$\displaystyle\begin{split}{{\underline{\partial}}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})&{}=\left\\{{f^{*}\,{{\cdot}}\,g}\right\\}\cup\left\\{{(F^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g}\mathrel{|}{F^{\prime}\in{{\underline{\partial}}}({F})}\right\\}\\\
&{}\subseteq\left\\{{f^{*}\,{{\cdot}}\,g}\right\\}\cup\left\\{{(F^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g}\mathrel{|}{F^{\prime}\in{{\underline{\partial}^{+}}}({f})}\right\\}\subseteq{V}({{\underline{\mathcal{C}}}({f^{*}\cdot
g})})\hskip 1.5pt{.}\end{split}$ (30)

Due to (30), $s$ is defined for all partial 1-derivatives of
$E\mathrel{{\equiv}}(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g$
also in this subcase. Then we can argue as follows:

$\displaystyle{s}({E})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{s}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,e})$
(by
$E\mathrel{{\equiv}}(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\pi}({F})\,{{\cdot}}\,e$
(by the definition of $s$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>\Big{(}{\tau_{{\underline{\mathcal{C}}}({F})}}({F})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({F})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{\pi}({F^{\prime}})\Big{)}\,{{\cdot}}\,e$
(by using Lemma 16)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>1\,{{\cdot}}\,e+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({f})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,({\pi}({F^{\prime}})\,{{\cdot}}\,e)$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>1\,{{\cdot}}\,{s}({f^{*}\,{{\cdot}}\,g})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptF^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({f})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({(F^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})$
(by the definition of $s$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf ACI}}\hskip
1.0pt}}$}\>0+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptE^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({E^{\prime}})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\tau_{{\underline{\mathcal{C}}}({E})}}({E})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptE^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({E})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({E^{\prime}})$
(by
$E\mathrel{{\equiv}}(F\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,f^{*})\,{{\cdot}}\,g$,
and ${\tau_{{\underline{\mathcal{C}}}({E})}}({E})\mathrel{{\equiv}}0$).

Due to $\text{\sf ACI}\mathrel{{\sqsubseteq}}\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}\mathrel{{\sqsubseteq}}{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$ the chains of equalities in both
subcases are provable in ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$, and therefore we have now verified
(24) also in the (entire) second case, that is, that $s$ is a
$({\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})$-provable solution
of ${\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})$ at $E$ as in this case.

In the final case, $E\mathrel{{\equiv}}G$ with
$G\in{{\underline{\partial}^{+}}}({g})$. Since then 1-derivatives of $G$ are
in ${{\underline{\partial}^{+}}}({g})$ as well, and hence by (23) also in
${V}({{\underline{\mathcal{C}}}({f^{*}\cdot g})})$, it follows that $s$ is
defined for all 1-derivatives of $G$ and $E$. With this knowledge we can argue
as follows:

$\displaystyle{s}({E})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{s}({G})$ (by
$E\mathrel{{\equiv}}G$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\pi}({G})$ (by the
definition of $s$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\tau_{{\underline{\mathcal{C}}}({G})}}({G})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptG^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({G})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{\pi}({G^{\prime}})$
(by using Lemma 16)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf ACI}}\hskip
1.0pt}}$}\>{\tau_{{\underline{\mathcal{C}}}({G})}}({G})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptG^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({G})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({G^{\prime}})$
(by the definition of $s$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf ACI}}\hskip
1.0pt}}$}\>{\tau_{{\underline{\mathcal{C}}}({E})}}({E})+\sum_{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}},\hskip
0.5ptE^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({E})}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\,{{\cdot}}\,{s}({E^{\prime}})$
(by $E\mathrel{{\equiv}}G$).

Due to $\text{\sf ACI}\mathrel{{\sqsubseteq}}\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}\mathrel{{\sqsubseteq}}{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$ this chain of equalities verifies (24)
also in this case.

By having established (24) for the, according to (23), three possible forms of
stacked star expressions that are vertices of
${\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})$, we have shown that $s$ is
indeed a $({\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})$-provable
solution of ${\underline{\mathcal{C}}}({f^{*}\,{{\cdot}}\,g})$.

After having proved statement (c), we can combine the statements (a), (b), and
(c) as above in order construct LLEE-witnessed coinductive proofs with which
instances of $\textrm{RSP}^{*}$ can be mimicked by instances of LCoProof1.
This leads us to Lemma 36 below, and, as it can show derivability of
$\textrm{RSP}^{*}$ in cMil1, to Lemma 37.

######  Lemma 36.

Let $e,f,g\in{\textit{StExp}}({\mathit{A}})$ with ${f}{\ndownarrow}$, and let
$\Gamma\mathrel{{:=}}\left\\{{e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{f}\mathrel{{\cdot}}{e}}+{g}}\right\\}$.
Then it holds that $e\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})}}}{{f^{*}}}\mathrel{{\cdot}}{g}$.

######  Proof 7.2.

First, there is a ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$-provable solution $s_{1}$ of
${\underline{\mathcal{C}}}({{{f^{*}}}\mathrel{{\cdot}}{g}})$ with
${s_{1}}({{{f^{*}}}\mathrel{{\cdot}}{g}})\mathrel{{\equiv}}e$, due to Lemma
35. Second, there is a Mil--provable solution $s_{2}$ of
${\underline{\mathcal{C}}}({{{f^{*}}}\mathrel{{\cdot}}{g}})$ with
${s_{2}}({{{f^{*}}}\mathrel{{\cdot}}{g}})\mathrel{{\equiv}}{{f^{*}}}\mathrel{{\cdot}}{g}$,
due to Lemma 17. Then
$\langle{\underline{\mathcal{C}}}({f^{*}{\,{{\cdot}}\,}g}),\hskip
0.5ptL\rangle$ with
${L}({v})\mathrel{{:=}}{s_{1}}({v})\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{s_{2}}({v})$
for all $v\in{V}({{\underline{\mathcal{C}}}({f^{*}{\,{{\cdot}}\,}g})})$ is a
LLEE-witnessed coinductive proof of
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f^{*}{\,{{\cdot}}\,}g$
over ${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$, because
${\underline{\mathcal{C}}}({{{f^{*}}}\mathrel{{\cdot}}{g}})$ has the guarded
LLEE-witness ${\hskip
0.2pt\hat{\underline{\mathcal{C}}}}({{{f^{*}}}\mathrel{{\cdot}}{g}})$ by
Theorem 4.3.

We note that the equation in the set $\Gamma$ in the assumption of Lemma 36
does not need to be sound semantically. Therefore it was crucial for the
formulation of this lemma that we did not require proof systems
${\mathcal{S}}$ to be sound with respect to
$\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}$ for the
definition of coinductive proofs in Definition 8. Indeed we have done so there
in order to be able to formulate this lemma, which states that also instances
of the fixed-point rule $\textrm{RSP}^{*}$ with premises that are not
semantically sound can be mimicked by appropriate coinductive proofs.

######  Lemma 37.

$\textrm{RSP}^{*}$ is a derivable rule in cMil.

######  Proof 7.3.

Every instance $\iota$ of $\textrm{RSP}^{*}$ can be replaced by a mimicking
derivation $\mathcal{D}_{\iota}$ in cMil1 according to the following step,
where ${f}{\ndownarrow}$ holds as the side-condition of the instance of
$\textrm{RSP}^{*}$ :

$\begin{aligned}
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
26.09583pt\hbox{\vbox{\hbox{\hskip 6.53937pt\hbox{\hskip
4.0pt\hbox{$\mathord{e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}\mathord{}$}\hbox{${{f}\mathrel{{\cdot}}{e}}+{g}$}\hskip
4.0pt}}\vskip-1.86806pt\nointerlineskip\hbox{\hskip 0.0pt\lower
1.95277pt\hbox{{$\iota$}\hskip 3.0pt}\hbox
to49.52435pt{\xleaders\hrule\hfill}\lower 3.86804pt\hbox{\hskip
3.0pt$\text{$\textrm{RSP}^{*}$}$}}\vskip-1.86804pt\nointerlineskip\hbox{\hskip
6.53937pt\hbox{\hskip 0.0pt\hbox{\hskip
4.0pt\hbox{$\mathord{e}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}\mathord{}$}\hbox{${{f^{*}}}\mathrel{{\cdot}}{g}\rule[-5.0pt]{0.0pt}{7.5pt}$}\hskip
4.0pt}}}}}\ignorespaces\end{aligned}\qquad\Longmapsto\qquad\begin{aligned}
\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
26.09583pt\hbox{\vbox{\hbox{\hskip
4.0pt\hbox{$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{f}\mathrel{{\cdot}}{e}}+{g}$}\hskip
4.0pt}\vskip-2.17445pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to49.52435pt{\xleaders\hrule\hfill}\lower
2.37pt\hbox{\hskip
3.0pt\text{LCoProof${}_{1}$}}}\vskip-2.17444pt\nointerlineskip\hbox{\hskip
4.81703pt\hbox{\hbox{\hskip
4.0pt\hbox{$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{f^{*}}}\mathrel{{\cdot}}{g}\rule[-5.0pt]{0.0pt}{7.5pt}$}\hskip
4.0pt}}}}}\ignorespaces\end{aligned}$ (31)

Here the side-condition $e\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{{f}\mathrel{{\cdot}}{e}}+{g}}\right\\}})}}}{{f^{*}}}\mathrel{{\cdot}}{g}$
of the instance of LCoProof1 in the derivation $\mathcal{D}_{\iota}$ on the
right is guaranteed by Lemma 36.

We now can show the main result of this section, the proof transformation from
Mil to cMil1. We obtain this transformation by using derivability of
$\textrm{RSP}^{*}$ in cMil1 as stated by this lemma, and by combining basic
proof-theoretic transformations that eliminate derivable, and hence correct
and admissible, rules from derivations as described in the proof of Lemma 1.

######  Theorem 38.

$\text{\sf Mil}\mathrel{{\precsim}}{\text{{\sf cMil}${}_{1}$}}$. What is more,
every derivation in Mil with conclusion
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
can be transformed effectively into a derivation with conclusion
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
in cMil1.

######  Proof 7.4.

Due to Lemma 37, $\textrm{RSP}^{*}$ is a derivable rule in cMil1. Then by
Lemma 1, (ii), $\textrm{RSP}^{*}$ is also an admissible rule in cMil1, and
hence ${{\text{{\sf
cMil}${}_{1}$}}}{+}{\text{$\textrm{RSP}^{*}$}}\mathrel{\sim}{\text{{\sf
cMil}${}_{1}$}}$ holds. With that we can now argue as follows:

$\displaystyle\text{\sf Mil}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{$\textrm{RSP}^{*}$}}$
$\displaystyle{}\mathrel{{\sqsubseteq}}{({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{$\textrm{RSP}^{*}$}})}{+}{\text{LCoProof${}_{1}$}}$
$\displaystyle{}={({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{LCoProof${}_{1}$}})}{+}{\text{$\textrm{RSP}^{*}$}}={{\text{{\sf
cMil}${}_{1}$}}}{+}{\text{$\textrm{RSP}^{*}$}}\mathrel{\sim}{\text{{\sf
cMil}${}_{1}$}}\hskip 1.5pt{.}$

From this we can infer $\text{\sf Mil}\mathrel{{\precsim}}{\text{{\sf
cMil}${}_{1}$}}$, because ${\sqsubseteq}$ implies ${\precsim}$, and
${{\precsim}}\cdot{{\sim}}\subseteq{\sim}$. That every derivation
$\mathcal{D}$ in Mil can be transformed effectively into a derivation
$\mathcal{D}^{\prime}$ in cMil with the same conclusion follows from
derivability of $\textrm{RSP}^{*}$ in cMil: then in $\mathcal{D}$ every
instance of $\textrm{RSP}^{*}$ can be replaced by a corresponding instance of
LCoProof1 as described in (31) of the proof of Lemma 37 with as result a
derivation $\mathcal{D}^{\prime}$ in cMil1 with the same conclusion as
$\mathcal{D}$. This argument instantiates the implication from rule
derivability to rule admissibility, and the transformations explained in the
proof of Lemma 1, (i) and (ii), specifically (1).

In Figure 2 we provided a first illustration for translating an instance of
the fixed-point rule into a coinductive proof in Figure 2 on page 2.
Specifically, we mimicked the instance $\iota$ (see below) of the fixed-point
rule $\textrm{RSP}^{*}$ in Milner’s system $\text{\sf Mil}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{$\textrm{RSP}^{*}$}}$ by a coinductive
proof over ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{premise of $\iota$}}\right\\}}$
with LLEE-witness ${\hskip
0.2pt\hat{\underline{\mathcal{C}}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\cdot{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}0}})$.

The correctness conditions that have to be satisfied for the right-hand sides
in order to recognize this prooftree as a LLEE-witnessed coinductive proof
${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{premise of
$\iota$}}\right\\}}$ are the same as those that we have verified for the
right-hand sides of the coinductive proof over Mil- with the same LLEE-witness
in Example 5. Note that the premise of $\iota$ is not used for the correctness
conditions of the right-hand sides. The correctness condition for the left-
hand side
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}$
at the bottom vertex of
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\cdot{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}0}})$
can be verified as follows, now making use of the premise of the considered
instance $\iota$ of $\textrm{RSP}^{*}$ :

$\displaystyle{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}$
$\displaystyle\;\;{\mathrel{{=_{\left\\{{\text{premise of
$\iota$}}\right\\}}\hskip
1.0pt}}}\;\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}0}$
$\displaystyle\;\;\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\;\;(a\,{{\cdot}}\,(a+b)+b)\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})$
$\displaystyle\;\;\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\;\;(a\,{{\cdot}}\,(a+b))\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})+b\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})$
$\displaystyle\;\;\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\;\;a\,{{\cdot}}\,((a+b)\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}))+b\,{{\cdot}}\,(1\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}))$
$\displaystyle\;\;\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\;\;a\,{{\cdot}}\,((1\,{{\cdot}}\,(a+b))\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}))+b\,{{\cdot}}\,(1\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}))$

Together this yields the provable equation:

$\displaystyle{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}$
$\displaystyle\;\;{\mathrel{{=_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{premise of
$\iota$}}\right\\}}}\hskip
1.0pt}}}\;\;a\,{{\cdot}}\,((1\,{{\cdot}}\,(a+b))\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}))+b\,{{\cdot}}\,(1\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}))\hskip
1.5pt{,}$

which demonstrates the correctness condition for the left-hand side
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}$
at the bottom vertex of
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\cdot{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}0}})$.
The correctness condition for the left-hand side
$a\,{{\cdot}}\,((1\,{{\cdot}}\,(a+b))$ at the top left vertex of
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\cdot{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}0}})$
can be verified without using the premise of $\iota$ as follows:

$\displaystyle((1\,{{\cdot}}\,(a+b))\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}}((a+b)\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})\mathrel{\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}}a\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})+b\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}}a\,{{\cdot}}\,(1\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}))+b\,{{\cdot}}\,(1\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0}))\hskip
1.5pt{.}$

Finally, the correctness condition of the left-hand side
$1\,{{\cdot}}\,({\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}{e_{0}^{*}}\,{{\cdot}}\,0})$
at the right upper vertex of
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}0}})$
can be obtained by an application of the axiom
(${\text{id}_{\text{l}}}({{\cdot}})$) only.

We close this section by giving an example that provides an additional sanity
check for the proof transformation from Mil to cMil that we developed above.
The example below shows that the construction of a LLEE-witnessed coinductive
proof fails for an inference that is not an instance of the fixed-point rule
$\textrm{RSP}^{*}$ because the side-condition is violated.

######  Non-Example 39.

We consider the following (not semantically valid) inference according to a
(semantically unsound) extension $\textrm{\sout{RSP}}^{*}$ of the fixed-point
rule $\textrm{RSP}^{*}$ that does not require the guardedness side-condition
${f}{\ndownarrow}$ (see Definition 2.1):

$\mathord{\overbrace{(a+c)^{*}}^{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}\mathord{}$$\overbrace{(a+1)}^{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\cdot\overbrace{(a+c)^{*}}^{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}+\overbrace{1}^{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}$
$\textrm{\sout{RSP}}^{*}$ (but not $\textrm{RSP}^{*}$ since
$f\mathrel{{\equiv}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(a+1)}}{{\downarrow}}}$)
$\mathord{(a+c)^{*}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}\mathord{}$$\underbrace{(a+1)^{*}}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}}\cdot\underbrace{1}_{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}$

The premise is semantically valid by Proposition 2.2 because it is provable in
Mil-:

$\displaystyle(a+c)^{*}$ $\displaystyle\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1+(a+c)\cdot(a+c)^{*}\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}1+a\cdot(a+c)^{*}+c\cdot(a+c)^{*}$
$\displaystyle\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1+a\cdot(a+c)^{*}+1+a\cdot(a+c)^{*}+c\cdot(a+c)^{*}$
$\displaystyle\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1+a\cdot(a+c)^{*}+(a+c)^{*}\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}1+a\cdot(a+c)^{*}+1\cdot(a+c)^{*}$
$\displaystyle\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1+(a+1)\cdot(a+c)^{*}\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}(a+1)\cdot(a+c)^{*}+1\hskip 1.5pt{.}$

But the conclusion of the inference is obviously not valid semantically,
because its left-hand side can iterate ${c}$-transitions, while its right-hand
side does not permit ${c}$-transitions.

${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}})$$1\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}$$\underbrace{(a+1)^{*}}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}}$$a$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[1]}}$$1\,{\cdot}\,\overbrace{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}^{(a+c)^{*}}$$\underbrace{\underbrace{(a+1)}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}}\,{\cdot}\,\underbrace{(a+c)^{*}}_{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}}+\underbrace{1}_{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}}_{\>=\>{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}\;\;\text{(by
rule
assumption)}}$$a$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[1]}}$$\boldsymbol{\times}$$(1\,{\cdot}\,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}})\,{\cdot}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$$\underbrace{(a+1)^{*}}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}}\,{\cdot}\,\underbrace{1}_{{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}$$a$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[1]}}$
Figure 17.  Failure of the construction a Mil--provable solution for a
coinductive proof that would mimic an instance of a fixed-point rule like
$\textrm{RSP}^{*}$ without side-condition.

Now by mechanically performing the same construction of a coinductive proof as
we illustrated it in Example 7 and in Example 7, we obtain the LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
${\underline{\mathcal{C}}}({f^{*}})$ and the star expression assignments to it
as in Figure 17. There we recognize that, while
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
is the principal value of a Mil--provable solution of
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}})$
(see on the right), we have not obtained a ${\text{\sf
Mil}}{+}{\left\\{{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}}\right\\}}$-provable
solution of
${\underline{\mathcal{C}}}({{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f^{*}}\,{{\cdot}}\,{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}})$
with principal value
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}f}\,{{\cdot}}\,{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}e}+{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}g}$
(see in the middle). This is because the correctness condition is violated at
the bottom vertex, because
$(a+1)\,{{\cdot}}\,(a+c)^{*}+1\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1+a\,{{\cdot}}\,(1\,{{\cdot}}\,(a+c)^{*})$ does not hold: otherwise it
would have to be semantically valid by Proposition 2.2, but it is not, because
only the left-hand side permits an initial ${c}$-transition.

Therefore the construction does not give rise to a LLEE-witnessed coinductive
proof of the (not semantically valid) formal equation
$(a+c)^{*}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}(a+1)\cdot(a+c)^{*}+1$.

Based on the proof transformations that we have developed in this section and
earlier in Section 6, we now obtain our main result. It justifies that we
called the proof system cMil a reformulation of Milner’s system Mil.

######  Theorem 40.

$\text{\sf Mil}\mathrel{\sim}{\text{{\sf
cMil}${}_{1}$}}\mathrel{\sim}\text{\sf cMil}\mathrel{\sim}\text{\sf CLC}$,
i.e. these proof systems are theorem-equivalent.

######  Proof 7.5.

By combining the statements of Theorem 38, Lemma 23, and Theorem 31 we obtain
the theorem-subsumption statements $\text{\sf
Mil}\mathrel{{\precsim}}{\text{{\sf
cMil}${}_{1}$}}\mathrel{{\precsim}}\text{\sf cMil}\>(\mathrel{\sim}\text{\sf
CLC})\mathrel{{\precsim}}\text{\sf Mil}$, which together justify the theorem-
equivalence of Mil with each of cMil1, cMil, and CLC.

##  8\. Summary and Conclusion

We set out on a proof-theoretic investigation of the problem of whether
Milner’s system Mil is complete for process-semantics equality
$\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}$ on regular
expressions (which Milner calls ‘star expressions’ for disambiguation when
interpreted according to the process semantics). Specifically we aimed at
characterizing the derivational power that the fixed-point rule
$\textrm{RSP}^{*}$ in Mil adds to its purely equational part Mil-.

In order to define a substitute for the rule $\textrm{RSP}^{*}$ we based ours
on two results that we have obtained earlier (the first in joint work with
Fokkink):

  1. (S/U)[SandU]

Linear specifications of the shape444The two examples on page 1 illustrate the
correspondence between a recursive specifications and its associated
transition graph. But note that these graphs do not satisfy LLEE (see Example
4). of transition graphs that satisfy the layered loop existence and
elimination property LLEE are:

     * (S)[S]

solvable by star expressions modulo provability in Mil- (and modulo
$\leftrightarrow$ ).

     * (U)[U]

uniquely solvable by star expressions modulo provability in Mil (and mod.
$\leftrightarrow$ ).

These statements were crucial steps in the completeness proof [GF20b, GF20a]
by Fokkink and myself for a tailored restriction BBP of Mil to ‘$1$-free’ star
expressions.

  2. (IV)1[IVone]

While the chart interpretation ${\mathcal{C}}({e})$ of a star expression $e$
does not always satisfy LLEE, there is a variant
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation ${\underline{\mathcal{C}}}({e})$ (typically with
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions)
that is
(${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-)bisimilar
to $e$, and satisfies LLEE, for all star expressions $e$. (See Definition 4.2,
and [Gra20, Gra21c]). Hereby
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions
are interpreted as empty-step processes.

Now in order to obtain results for
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
that are analogous to LABEL:S and LABEL:U, we have generalized these
statements to guarded
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
in Section 6. In doing so, we obtained:

  1. (S/U)1[SUone]

Guarded linear specifications of the shape of
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
that satisfy the loop existence and elimination property LLEE are:

     * (S)1[Sone]

solvable by star expressions modulo provability in Mil- (see LABEL:SE),

     * (U)1[Uone]

uniquely solvable by star expressions modulo provability in Mil (see
LABEL:SU).

These statements correspond to the statements LABEL:SE and LABEL:SU in Section
6 which we have proved as Lemma 26, and Lemma 28, respectively.

Milner’s system
and variants Coinductive reformulation of Milner’s system
and variant systems $\text{\sf Mil}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{$\textrm{RSP}^{*}$}}$$\text{\sf
cMil}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n}}$$\text{\sf
CLC}=\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n}$$\text{\text{\sf
Mil}${}^{\prime}$}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{$\textrm{USP}_{1}$}}$${\text{{\sf
cMil}${}_{1}$}}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{LCoProof${}_{1}$}}$$\text{$\overline{\sf
Mil}{}^{\prime}$}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\textrm{USP}}$$\text{$\overline{\text{\sf
cMil}}$}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{CoProof${}_{n}$}}\right\\}_{n}}$$\text{\sf
CC}=\left\\{{\text{CoProof${}_{n}$}}\right\\}_{n}$Thm. 38Thm. 38Lem. 2,(i)Thm.
31Lem. 23,(iii)Lem. 23,(i)Lem. 23,(iii)Lem. 23,(i)Lem. 2,(ii)Lem. 23,(ii)Lem.
23,(ii)Lem. 23,(iv)Rem. 24Lem. 23,(iv)

Figure 18. Web of proof transformations between Milner’s system Mil and
variants, and the coinductive reformulation cMil of Mil with kernel system CLC
and variants.

These statements motivated us to define ‘coinductive proofs’ as pairs of
solutions for guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts,
because every pair of Mil--provable, or Mil-provable solutions can be proved
equal in Mil. On the basis of this idea we developed the following concepts
and results (we emphasize earlier introduced terminology again here below):

  1. 1

_LLEE -witnessed coinductive proof over an equational proof system
${\mathcal{S}}$_ (Definition 8): We defined a coinductive proof as a weakly
guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ whose vertices are labeled by equations between the
values of two ${\mathcal{S}}$-provable solutions of $\underline{\mathcal{C}}$.

  2. 2

_Coinductive reformulation cMil_ of Milner’s system Mil (Definition 21): We
defined cMil as the result of replacing the fixed-point rule
$\textrm{RSP}^{*}$ in Mil with rules of the scheme
$\left\\{{\text{LCoProof${}_{i}$}}\right\\}_{i\in{\rm Nature}}$ that formalize
provability by LLEE-witnessed coinductive proofs.

     * $\triangleright$

As the ‘kernel’ of cMil we defined the system CLC (Definition 21) for
combining LLEE-witnessed coinductive proofs with only the rules of the scheme
$\left\\{{\text{LCoProof${}_{i}$}}\right\\}_{i\in{\rm Nature}}$.

  3. 3

_Proof transformations_ between cMil and Mil that show their theorem-
equivalence.

     * $\triangleright$

We showed that the rules of
$\left\\{{\text{LCoProof${}_{i}$}}\right\\}_{i\in{\rm Nature}}$ are correct
and admissible for Mil, and that this implies that every derivation in cMil
can be transformed into one in Mil with the same conclusion by eliminating
occurrences of these rules. (See Section 6.)

     * $\triangleright$

We showed that the fixed-point rule $\textrm{RSP}^{*}$ of Mil is derivable in
cMil, because every instance $\iota$ can be mimicked by an instance of
LCoProof1 that uses the premise of $\iota$, and, as a side-condition, a LLEE-
witnessed coinductive proof over Mil-. As a consequence we showed that every
derivation in Mil can be transformed into one in cMil with the same conclusion
by eliminating occurrences of $\textrm{RSP}^{*}$. (See Section 7.)

  4. 4

_Coinductive reformulation $\overline{\text{\sf cMil}}$_ of the variant
$\overline{\sf Mil}{}^{\prime}$ (with the powerful rule USP, see Definition
2.1) of Mil: We formulated systems $\overline{\text{\sf cMil}}$ (Definition
21) and CC (Definition 21) based on coinductive proofs without LLEE-witnesses.
The systems $\overline{\text{\sf cMil}}$ and CC can be recognized as complete
variants of cMil and CLC. We have, however, only argued that in Remark 24 (on
the basis of earlier work [Gra06]), but not proved it in detail here.

  5. 5

_Proof transformations_ between cMil and CLC, and $\overline{\text{\sf cMil}}$
and CC that show their theorem-equivalence. Here the idea of the non-trivial
transformations from cMil to CLC was to ‘hide’ all derivation parts that
consist of axioms or rules of the purely equational part Mil- of Mil into the
correctness conditions of solutions in LLEE-witnessed coinductive proofs,
which occur as side-conditions of instances of rules of
$\left\\{{\text{LCoProof${}_{i}$}}\right\\}_{i\in{\rm Nature}}$ in CLC. The
transformation from $\overline{\text{\sf cMil}}$ to CC operates analogously.
(See Lemma 23, (iii), and (iv).)

In Figure 18 we have illustrated the web of proof transformations between, on
the one hand, Milner’s systems and its variants as defined in Definition 2.1,
and, on the other hand, the coinductive reformulations cMil and cMil1 of Mil,
and $\overline{\text{\sf cMil}}$ of $\overline{\sf Mil}{}^{\prime}$ in
Definition 21, as well as the coinductive kernel systems CLC of cMil, and CC
of $\overline{\text{\sf cMil}}$ in Definition 21.

$e_{1}\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}e_{2}$$e_{1}\mathrel{{=_{\text{\sf cMil}}\hskip
1.0pt}}e_{2}$$e_{1}\mathrel{{=_{\text{\sf CLC}}\hskip 1.0pt}}e_{2}$
${\mathcal{C}}({e_{1}})\mathrel{\hbox{\kern 0.43057pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{$\leftrightarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}\hskip 1.0pt}{\mathcal{C}}({e_{2}})$
$e_{1}\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}e_{2}$
Thm. 38Thm. 31Lem. 23,(iii)Lem. 23,(iii)due to Prop. 2.2? Figure 19. The
coinductive proof system CLC (next to cMil) as potential beachhead for a
completeness proof of Mil. We label with a question mark the transformation
that is not defined here (it can be extracted from the completeness proof of
Mil).

The coinductive reformulation cMil of Mil, and its coinductive kernel CLC, can
be looked upon as being situated roughly half-way in between Mil and
bisimulations between chart interpretations of star expressions. We illustrate
this in Figure 19. This picture arises from the highest level in Figure 18,
when instantiated for specified conclusions $e_{1}\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}e_{2}$, $e_{1}\mathrel{{=_{\text{\sf cMil}}\hskip
1.0pt}}e_{2}$, and $e_{1}\mathrel{{=_{\text{\sf CLC}}\hskip 1.0pt}}e_{2}$, and
by extending it further to ${\mathcal{C}}({e_{1}})\mathrel{\hbox{\kern
0.43057pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{$\leftrightarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}\hskip 1.0pt}{\mathcal{C}}({e_{2}})$, and hence to
$e_{1}\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}e_{2}$.
For the last step we use soundness of CLC, which follows from soundness of Mil
with respect to
$\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}$, see
Proposition 2.2, in view of the proof transformations that link CLC via cMil
to Mil. Now we note that derivations of CLC represent proof-trees of
coinductive proofs each of which defines a bisimulation up to provability by
Proposition 20, and Remark 21. Therefore we can argue that prooftrees in CLC,
and by proof-theoretic association also prooftrees in cMil, are situated
roughly half-way in between prooftrees in Mil and bisimulations between chart
interpretation of star expressions. We think that Figure 19 provides a
reasonable suggestion of the proof-theoretic closeness of these systems.

The proof-theoretic connections of CLC with cMil and Mil guarantee that
completeness of Mil (with respect to
$\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}$) is
equivalent to completeness of cMil, and also to completeness of CLC. Stronger
still, the proof transformations between CLC, cMil, and Mil guarantee that
every completeness proof of Mil can be ‘routed through’ CLC (and also through
cMil). Such a ‘rerouting’ through CLC of a completeness proof of Mil does,
however, not need to be equally natural as a ‘direct’ completeness proof of
Mil. But since CLC is intuitively much closer to
$\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}$ than Mil
(as suggested by Figure 19), much hope was warranted to obtain a completeness
proof for Mil by finding a completeness proof for CLC first, or to at least to
use concepts that we have introduced here. (The latter hope turned out to be
justified.)

Indeed, since the proof systems cMil and CLC are tied to process graphs via
the circular deductions they permit and to bisimulations up to provability,
and since cMil and CLC are theorem-equivalent with Mil, they were conceived as
(and still can be) natural beachheads for a completeness proof of Milner’s
system. In Figure 19 we have indicated the step to CLC that is missing _here_
for a completeness proof of Mil with a question mark: a completeness proof of
CLC, and that is, an argument that, for every bisimulation between
${\mathcal{C}}({e_{1}})$ and ${\mathcal{C}}({e_{2}})$ where $e_{1}$ and
$e_{2}$ are given star expressions, yields a prooftree in CLC with conclusion
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$.

Due to their feature of permitting derivations that can be construed as
combinations of
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
(up to provability), we were confident that the proof system cMil and its
coinductive kernel CLC substantially increase the space for graph-based
approaches to finding a completeness proof of Mil. A concrete indication for
this expectation was the following. By closely analyzing the completeness
proof in [GF20b, GF20a] for the tailored restriction BBP of Mil to ‘$1$-free’
star expressions we find:

$\left.\;\parbox{368.57964pt}{Valid equations between $1$-free\ star
expressions admit derivations in \text{\sf CLC}\ of depth less than or equal
to 2.}\;\>\right\\}$ (32)

This fact suggests the following research question:

$\left.\;\parbox{368.57964pt}{Can derivations in \text{\sf CLC}\ (derivations
in $\text{\sf cMil}$) always be simplified to some kind of normal form that is
of bounded depth (respectively, of bounded nesting depth of
{LLEE}-wit\\-nessed\ coinductive proofs)?}\;\>\right\\}$ (33)

Despite of the fact that this question admits a trivial answer in view of the
completeness proof of Mil in [Gra22a], see (C2) and (C3) below, it can be
desirable to also find an answer that is based on a proof-theoretic analysis,
and that leads to a workable concept of ‘normal form’ for derivations in CLC
or in cMil. Intuitions for finding such a concept may be found in developing
simplification steps of
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
with LLEE under
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimilarity,
as those are used in the completeness proofs for BBP with respect to
‘$1$-free’ star expressions in [GF20b, GF20a], and for Mil with respect to all
star expressions in [Gra22a, Gra22b]. We close by listing consequences of the
latter (one is direct, the other two are a bit technical).

#### Consequences of the completeness proof of Mil in [Gra22a].

Below we list the most important consequences that the completeness proof of
Mil as summarized in [Gra22a] has for the line of investigation on coinductive
versions of Mil as reported here:

  1. (C1)

The coinductive versions cMil and CLC of Milner’s system Mil are (just like
Mil) complete with respect to process semantics equality
$\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}$ of star
expressions. (This follows directly from Theorem 5.1 in [Gra22a] in view of
Theorem 40 here.)

  2. (C2)

Valid equations between star expressions admit derivations in CLC of depth
less than or equal to $2$. (This generalization of (32) can be shown by a
close analysis of the structure of the completeness proof of Mil in Section 5
of [Gra22a]. The proof is similar to that of Corollary 33, 33, and also
similar to the argumentation for the analogous statement concerning ‘$1$-free’
star expressions and the system BBP as reported above.)

  3. (C3)

As a consequence of (C2) the research question (33) admits the trivial answer
“yes”, albeit one that avoids a close proof-theoretic analysis. (Yet we still
think that an answer that is based on a fine-grained proof-theoretic analysis
would be more desirable).

### Acknowledgement

First I want to thank the editors Alexandra Silva and Fabio Gadducci very
much: without their leniency with the deadline I would not have been able to
finish this extended article version of my CALCO paper [Gra21b]. Second, I am
greatly indebted to the reviewers of this article for reading it carefully,
spotting distracting problems, asking spot-on questions, and suggesting
changes and additions. To mention two important examples: an acute pointer to
a shortcoming of the more informal definition of LLEE-witness in terms of
recordings of loop elimination steps (now rectified by using multi-step loop
elimination steps, see Definition 5) and a perceptive question of whether the
proof system Mil is complete with respect to bisimulations that are witnessed
by guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
(it is indeed, and the question has led me to formulating and proving
Corollary 33).

I am very thankful to Luca Aceto for giving me the chance to continue my work
on Milner’s problems on the process interpretation of regular expressions in
the PRIN project _IT MATTERS \- Methods and Tools for Trustworthy Smart
Systems_ (ID: 2017FTXR7S_005).

## References

  * [AC93] Roberto M. Amadio and Luca Cardelli.  Subtyping Recursive Types.  ACM Transactions on Programming Languages and Systems, 15(4):575–631, Sept. 1993.  doi:10.1145/155183.155231.
  * [AK96] Zena M. Ariola and Jan Willem Klop.  Equational Term Graph Rewriting.  Fundamenta Informaticae, 26(3,4):207–240, Dec 1996.  doi:10.3233/FI-1996-263401.
  * [Ant96] Valentin Antimirov.  Partial Derivatives of Regular Expressions and Finite Automaton Constructions.  Theoretical Computer Science, 155(2):291–319, 1996.  doi:10.1016/0304-3975(95)00182-4.
  * [BH98] Michael Brandt and Fritz Henglein.  Coinductive Axiomatization of Recursive Type Equality and Subtyping.  Fundamenta Informaticae, 33(4):309–338, Dec 1998.  doi:10.1007/3-540-62688-3_29.
  * [Blo01] Stefan Blom.  Term Graph Rewriting – Syntax and Semantics.  PhD thesis, Vrije Universiteit Amsterdam, 2001.
  * [Bos97] Doeko Bosscher.  Grammars Modulo Bisimulation.  PhD thesis, University of Amsterdam, 1997.
  * [GF20a] Clemens Grabmayer and Wan Fokkink.  A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity.  In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20, page 465–478, New York, NY, USA, 2020. Association for Computing Machinery.  Extended report [GF20b].  doi:10.1145/3373718.3394744.
  * [GF20b] Clemens Grabmayer and Wan Fokkink.  A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity.  Technical Report 2004.12740, arxiv.org, April 2020.  Extends [GF20a].
  * [Gra04] Clemens Grabmayer.  Derivability and Admissibility of Inference Rules in Abstract Hilbert Systems.  In Matthias Baaz, Johann A. Makowsky, and Andrei Voronkov, editors, Collegium Logicum, volume VIII of Collegium Logicum, pages 91–97. Kurt Gödel Society, Wien, 2004.  Available at clegra.github.io/lf/collegiumlogicum.pdf.
  * [Gra05a] Clemens Grabmayer.  Relating Proof Systems for Recursive Types.  PhD thesis, Vrije Universiteit Amsterdam, March 2005.  clegra.github.io/lf/proefschrift.pdf.
  * [Gra05b] Clemens Grabmayer.  Using Proofs by Coinduction to Find “Traditional” Proofs.  In José Luiz Fiadeiro, Neal Harman, Markus Roggenbach, and Jan Rutten, editors, Proceedings of CALCO 2005, volume 3629 of LNCS, pages 175–193. Springer, 2005.  doi:10.1007/11548133_12.
  * [Gra06] Clemens Grabmayer.  A Coinductive Axiomatisation of Regular Expressions under Bisimulation.  Technical report, University of Nottingham, 2006.  Short Contribution to CMCS 2006, March 25-27, 2006, Vienna Institute of Technology, Austria (slides at clegra.github.io/lf/cmcs06.pdf, extended abstract at clegra.github.io/lf/sc.pdf).
  * [Gra20] Clemens Grabmayer.  Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions.  Technical Report 2012.10869, arxiv.org, December 2020.  Extends [Gra21c].
  * [Gra21a] Clemens Grabmayer.  A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity.  Technical Report 2108.13104, arxiv.org, August 2021.  Extends [Gra21b].
  * [Gra21b] Clemens Grabmayer.  A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity.  In Fabio Gadducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021), volume 211 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1–16:23, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  Extended report [Gra21a].  doi:10.4230/LIPIcs.CALCO.2021.16.
  * [Gra21c] Clemens Grabmayer.  Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions.  In Patrick Bahr, editor, Proceedings 11th International Workshop on Computing with Terms and Graphs, Online, 5th July 2020, volume 334 of Electronic Proceedings in Theoretical Computer Science, pages 29–45. Open Publishing Association, 2021.  doi:10.4204/EPTCS.334.3.
  * [Gra22a] Clemens Grabmayer.  Milner’s Proof System for Regular Expressions Modulo Bisimilarity is Complete (Crystallization: Near-Collapsing Process Graph Interpretations of Regular Expressions).  In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22, New York, NY, USA, 2022. Association for Computing Machinery.  Extended report [Gra22b].  doi:10.1145/3531130.3532430.
  * [Gra22b] Clemens Grabmayer.  Milner’s Proof System for Regular Expressions Modulo Bisimilarity is Complete (Crystallization: Near-Collapsing Process Graph Interpretations of Regular Expressions).  Technical Report 2209.12188, arxiv.org, September 2022.  Extends [Gra22a].
  * [HN11] Fritz Henglein and Lasse Nielsen.  Regular Expression Containment: Coinductive Axiomatization and Computational Interpretation.  In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’11, page 385–398, New York, NY, USA, 2011. Association for Computing Machinery.  doi:10.1145/1926385.1926429.
  * [HS91] Hans Hüttel and Colin Stirling.  Actions Speak Louder Than Words: Proving Bisimilarity for Context-Free Processes.  In Proceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science, pages 376–386, Los Alamitos, CA, USA, jul 1991. IEEE Computer Society.  doi:10.1109/LICS.1991.151661.
  * [HS98] Hans Hüttel and Colin Stirling.  Actions Speak Louder Than Words: Proving Bisimilarity for Context-Free Processes.  J. Log. Comput., 8(4):485–509, 1998.  doi:10.1093/logcom/8.4.485.
  * [JR97] Bart Jacobs and Jan Rutten.  A Tutorial on (Co)Algebras and (Co)Induction.  Bulletin-European Association for Theoretical Computer Science, 62:222–259, 1997.  URL: http://www.cs.ru.nl/B.Jacobs/PAPERS/JR.ps.
  * [Mil84] Robin Milner.  A Complete Inference System for a Class of Regular Behaviours.  Journal of Computer and System Sciences, 28(3):439–466, 1984.  doi:10.1016/0022-0000(84)90023-0.
  * [Rut98] J. J. M. M. Rutten.  Automata and Coinduction (an Exercise in Coalgebra).  In Davide Sangiorgi and Robert de Simone, editors, CONCUR’98 Concurrency Theory, pages 194–218, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.  doi:10.1007/BFb0055624.
  * [Sal66] Arto Salomaa.  Two Complete Axiom Systems for the Algebra of Regular Events.  Journal of the ACM, 13(1):158–169, 1966.  doi:10.1145/321312.321326.
  * [Sho67] Joseph R. Shoenfield.  Mathematical Logic.  Addison-Wesely Publishing Company, 1967.
  * [SRS21] Todd Schmid, Jurriaan Rot, and Alexandra Silva.  On Star Expressions and Coalgebraic Completeness Theorems.  Technical Report 2106.08074, arxiv.org, 2021.  Presented at MFPS XXXVII, Aug 30–Sep 3, Salzburg, Austria.
  * [Tar72] Robert Tarjan.  Depth-First Search and Linear Graph Algorithms.  SIAM Journal on Computing, 1(2):146–160, 1972.  doi:10.1137/0201010.