sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
with sets $U,U_{1},\ldots,U_{n}$ of loop-entry transitions from their start
vertices $v,v_{1},\ldots,v_{n}\in V$, respectively, for $n\in{\rm
Nature}\setminus\left\\{{0}\right\\}$.

The
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}^{\prime}$ that results by the _elimination of (the
loop sub-
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart)
$\underline{\mathcal{L}}$ from $\underline{\mathcal{C}}$_ arises by removing
all loop-entry transitions in $U$ of $\underline{\mathcal{L}}$ from
$\underline{\mathcal{C}}$, and then also removing all vertices and transitions
that become unreachable; in this case we write
$\underline{\mathcal{C}}\mathrel{\Rightarrow_{\text{{elim}}}}\underline{\mathcal{C}}^{\prime}$,
and also say that $\underline{\mathcal{C}}^{\prime}$ results by a _single-step
loop elimination_ from $\underline{\mathcal{C}}$.

Suppose that the loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
$\underline{\mathcal{L}}_{1}$, …, $\underline{\mathcal{L}}_{n}$ satisfy the
following two conditions:

  1. (ms-1)

their sets $U_{1},\ldots,U_{n}$ of loop-entry transitions are disjoint (that
is, $U_{i}\cap U_{j}\neq\varnothing$ for all
$i,j\in\left\\{{1,\ldots,n}\right\\}$ with $i\neq j$),

  2. (ms-2)

no start vertex of a loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{L}}_{i}$ is in the body of another one
$\underline{\mathcal{L}}_{j}$, for all $i,j\in\left\\{{1,\ldots,n}\right\\}$
with $i\neq j$.

Then we say that a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}^{\prime}$ results by the _multi-step loop elimination
of $\underline{\mathcal{L}}_{1}$, …, $\underline{\mathcal{L}}_{n}$ from
$\underline{\mathcal{C}}$_ if $\underline{\mathcal{C}}^{\prime}$ arises from
$\underline{\mathcal{C}}$ by removing all loop-entry transitions in
$U_{1},\ldots,U_{n}$ of $\underline{\mathcal{L}}_{1}$, …,
$\underline{\mathcal{L}}_{n}$ from $\underline{\mathcal{C}}$, and then also
removing all vertices and transitions that become unreachable; in this case we
write
$\underline{\mathcal{C}}\mathrel{\mbox{$\Longrightarrow$\raisebox{-0.275pt}{
\leavevmode\hbox to5.52pt{\vbox to5.52pt{\pgfpicture\makeatletter\hbox{\hskip
2.76074pt\lower-2.76074pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.56075pt}{0.0pt}\pgfsys@curveto{2.56075pt}{1.41428pt}{1.41428pt}{2.56075pt}{0.0pt}{2.56075pt}\pgfsys@curveto{-1.41428pt}{2.56075pt}{-2.56075pt}{1.41428pt}{-2.56075pt}{0.0pt}\pgfsys@curveto{-2.56075pt}{-1.41428pt}{-1.41428pt}{-2.56075pt}{0.0pt}{-2.56075pt}\pgfsys@curveto{1.41428pt}{-2.56075pt}{2.56075pt}{-1.41428pt}{2.56075pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\hskip
7.39755pt}_{\text{{elim}}}}\underline{\mathcal{C}}^{\prime}$, and say that
$\underline{\mathcal{C}}^{\prime}$ results by a _multi-step loop elimination_
from $\underline{\mathcal{C}}$.

######  Lemma 11.

${\Rightarrow_{\text{{elim}}}}\,\subseteq\,{\mbox{$\Longrightarrow$\raisebox{-0.275pt}{
\leavevmode\hbox to5.52pt{\vbox to5.52pt{\pgfpicture\makeatletter\hbox{\hskip
2.76074pt\lower-2.76074pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.56075pt}{0.0pt}\pgfsys@curveto{2.56075pt}{1.41428pt}{1.41428pt}{2.56075pt}{0.0pt}{2.56075pt}\pgfsys@curveto{-1.41428pt}{2.56075pt}{-2.56075pt}{1.41428pt}{-2.56075pt}{0.0pt}\pgfsys@curveto{-2.56075pt}{-1.41428pt}{-1.41428pt}{-2.56075pt}{0.0pt}{-2.56075pt}\pgfsys@curveto{1.41428pt}{-2.56075pt}{2.56075pt}{-1.41428pt}{2.56075pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\hskip
7.39755pt}_{\text{{elim}}}}\,\subseteq\,{\Rightarrow_{\text{{elim}}}^{+}}$,
and consequently
${\Rightarrow_{\text{{elim}}}^{*}}={\mbox{$\Longrightarrow$\raisebox{-0.275pt}{
\leavevmode\hbox to5.52pt{\vbox to5.52pt{\pgfpicture\makeatletter\hbox{\hskip
2.76074pt\lower-2.76074pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.56075pt}{0.0pt}\pgfsys@curveto{2.56075pt}{1.41428pt}{1.41428pt}{2.56075pt}{0.0pt}{2.56075pt}\pgfsys@curveto{-1.41428pt}{2.56075pt}{-2.56075pt}{1.41428pt}{-2.56075pt}{0.0pt}\pgfsys@curveto{-2.56075pt}{-1.41428pt}{-1.41428pt}{-2.56075pt}{0.0pt}{-2.56075pt}\pgfsys@curveto{1.41428pt}{-2.56075pt}{2.56075pt}{-1.41428pt}{2.56075pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\hskip
7.39755pt}_{\text{{elim}}}^{*}}$.

######  Proof 4.1.

First,
${\Rightarrow_{\text{{elim}}}}\subseteq{\mbox{$\Longrightarrow$\raisebox{-0.275pt}{
\leavevmode\hbox to5.52pt{\vbox to5.52pt{\pgfpicture\makeatletter\hbox{\hskip
2.76074pt\lower-2.76074pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.56075pt}{0.0pt}\pgfsys@curveto{2.56075pt}{1.41428pt}{1.41428pt}{2.56075pt}{0.0pt}{2.56075pt}\pgfsys@curveto{-1.41428pt}{2.56075pt}{-2.56075pt}{1.41428pt}{-2.56075pt}{0.0pt}\pgfsys@curveto{-2.56075pt}{-1.41428pt}{-1.41428pt}{-2.56075pt}{0.0pt}{-2.56075pt}\pgfsys@curveto{1.41428pt}{-2.56075pt}{2.56075pt}{-1.41428pt}{2.56075pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\hskip
7.39755pt}_{\text{{elim}}}}$ holds because every single-step loop elimination
is also a multi-step loop elimination. Crucially,
${\mbox{$\Longrightarrow$\raisebox{-0.275pt}{ \leavevmode\hbox to5.52pt{\vbox
to5.52pt{\pgfpicture\makeatletter\hbox{\hskip 2.76074pt\lower-2.76074pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.56075pt}{0.0pt}\pgfsys@curveto{2.56075pt}{1.41428pt}{1.41428pt}{2.56075pt}{0.0pt}{2.56075pt}\pgfsys@curveto{-1.41428pt}{2.56075pt}{-2.56075pt}{1.41428pt}{-2.56075pt}{0.0pt}\pgfsys@curveto{-2.56075pt}{-1.41428pt}{-1.41428pt}{-2.56075pt}{0.0pt}{-2.56075pt}\pgfsys@curveto{1.41428pt}{-2.56075pt}{2.56075pt}{-1.41428pt}{2.56075pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\hskip
7.39755pt}_{\text{{elim}}}}\subseteq{\Rightarrow_{\text{{elim}}}^{+}}$ holds,
because every multi-step loop elimination of loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
$\underline{\mathcal{L}}_{1},\ldots,\underline{\mathcal{L}}_{n}$ in a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ with loop-entry transitions $U_{1},\ldots,U_{n}$ can
be implemented as a sequence of single-step loop eliminations of
$\underline{\mathcal{L}}_{1},\ldots,\underline{\mathcal{L}}_{n}$ irrespective
of the chosen order: hereby (ms-1) guarantees that every loop-entry transition
belongs uniquely to one of
$\underline{\mathcal{L}}_{1},\ldots,\underline{\mathcal{L}}_{n}$ and thus is
removed in precisely one step; and (ms-2) ensures that, after the elimination
of a loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{L}}_{i}$, another one $\underline{\mathcal{L}}_{j}$ with
$j\neq i$ that has not yet been eliminated is still a loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart.
Finally these statements imply that the many-step versions of single-step and
multi-step loop elimination coincide.

[LEE and LLEE] Let $\underline{\mathcal{C}}=\langle
V,\mathit{A},{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1},v_{\text{s}},{{\to}},{{\downarrow}}\rangle$
be a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart.

We say that $\underline{\mathcal{C}}$ has the _loop existence and elimination
property_ (LEE) if repeated loop elimination started on
$\underline{\mathcal{C}}$ leads to a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
without an infinite path, that is, if there is multi-step loop elimination
reduction sequence
$\underline{\mathcal{C}}\mathrel{\mbox{$\Longrightarrow$\raisebox{-0.275pt}{
\leavevmode\hbox to5.52pt{\vbox to5.52pt{\pgfpicture\makeatletter\hbox{\hskip
2.76074pt\lower-2.76074pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.56075pt}{0.0pt}\pgfsys@curveto{2.56075pt}{1.41428pt}{1.41428pt}{2.56075pt}{0.0pt}{2.56075pt}\pgfsys@curveto{-1.41428pt}{2.56075pt}{-2.56075pt}{1.41428pt}{-2.56075pt}{0.0pt}\pgfsys@curveto{-2.56075pt}{-1.41428pt}{-1.41428pt}{-2.56075pt}{0.0pt}{-2.56075pt}\pgfsys@curveto{1.41428pt}{-2.56075pt}{2.56075pt}{-1.41428pt}{2.56075pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\hskip
7.39755pt}_{\text{{elim}}}^{*}}\underline{\mathcal{C}}^{\prime}$ (or by Lemma
11 equivalently, a single-step loop elimination reduction sequence
$\underline{\mathcal{C}}\mathrel{\Rightarrow_{\text{{elim}}}^{*}}\underline{\mathcal{C}}^{\prime}$)
that leads to a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}^{\prime}$ without an infinite path.

If, in a successful elimination sequence from a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$, loop-entry transitions are never removed that
depart from a vertex in the body of a previously eliminated loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart,
then we say that $\underline{\mathcal{C}}$ satisfies _layered LEE_ (LLEE), and
that $\underline{\mathcal{C}}$ is a _LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart_.

$\underline{\mathcal{C}}$$v$$v_{1}$$v_{11}$$v_{2}$$v_{21}$$v$$v_{1}$$v_{11}$$v_{2}$$v_{21}$step
1elim$v$$v_{1}$$v_{11}$$v_{2}$$v_{21}$step 2elimmulti-step 1

$\boldsymbol{\bigcirc}$

elim$v$$v_{1}$$v_{11}$$v_{2}$$v_{21}$removeloop
entries$\underline{\mathcal{C}}^{\prime\prime\prime}$$v$ garbage
collect step 3 / (multi-)step 2

$\boldsymbol{\bigcirc}$

elim Figure 4. Example of a loop elimination process that witnesses LEE/LLEE
for the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$. Three single-step loop eliminations from
$\underline{\mathcal{C}}$ reach the same result
$\underline{\mathcal{C}}^{\prime\prime\prime}$ as two multi-step loop
eliminations (where the second multi-step is also a single step).
$v$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$\hskip
0.2pt\widehat{\underline{\mathcal{E}}}^{\scriptscriptstyle(1)}$$u$$w_{1}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$$w_{2}$$v$$u$$w_{1}$$v$$u$$w_{1}$$w_{2}$step
2elim$v$$\underline{\mathcal{E}}$$u$$w_{1}$$w_{2}$step
1elim$v$$u$$w_{1}$$w_{2}$step
1elim$v$$\underline{\mathcal{E}}$$u$$w_{1}$$w_{2}$step
2elim$v$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[2]}}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$\hskip
0.2pt\widehat{\underline{\mathcal{E}}}^{\scriptscriptstyle(2)}$$u$$w_{1}$$w_{2}$
Figure 5. Two runs of the loop elimination procedure on the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{E}}$ in the middle: the one to the left witnesses LEE
(but not LLEE, due to the removal of the red loop-entry transition from the
body of the green loop subchart removed earlier), its recording is the (not
layered) LEE-witness $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}^{\scriptscriptstyle(1)}$ of
$\underline{\mathcal{E}}$; the one to the right witnesses layered LEE (LLEE),
its recording is the LLEE-witness (layered LEE-witn.) $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}^{\scriptscriptstyle(2)}$ of
$\underline{\mathcal{E}}$.

In Figure 4 we have illustrated a successful run of the loop elimination
procedure for the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ there. The loop-entry transitions of loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
that are eliminated in the next step, respectively, are marked in bold. We
have neglected action labels there, except for indicating
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions
by dotted arrows. Since the graph
$\underline{\mathcal{C}}^{\prime\prime\prime}$ that is reached by three loop-
subgraph elimination steps
$\underline{\mathcal{C}}\mathrel{\Rightarrow_{\text{{elim}}}^{+}}\underline{\mathcal{C}}^{\prime\prime\prime}$
from the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ does not have an infinite path, and since no loop-
entry transitions have been removed from a previously eliminated loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart,
we conclude that $\underline{\mathcal{C}}$ satisfies LEE and LLEE.

In Figure 5 we illustrate two runs of the loop elimination procedure from a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{E}}$: The one from $\underline{\mathcal{E}}$ to the left
only witnesses LEE but not LLEE, since in the second elimination step a loop-
entry transition (drawn red) is removed from the body of the loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
that is eliminated in the first step (drawn in green). The one from
$\underline{\mathcal{E}}$ to the right witnesses LLEE, because transitions are
only removed sequentially at the same vertex, and hence no loop-entry
transition is removed from the body of a loop
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
that was eliminated before.

The two process graphs $G_{1}$ and $G_{2}$ on page 1, which are not
expressible by star expressions modulo bisimilarity, do not satisfy LLEE nor
LEE: neither of them has a loop subchart (as argued in Example 4), yet both of
them facilitate infinite paths.

[LLEE-witness] Let $\underline{\mathcal{C}}=\langle
V,\mathit{A},{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1},v_{\text{s}},{{\to}},{{\downarrow}}\rangle$
be a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart.

By an _entry/body-labeling_ of $\underline{\mathcal{C}}$ we mean a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\hskip 0.2pt\hat{\underline{\mathcal{C}}}=\langle V,\mathit{A}\times{\rm
Nature},{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1},v_{\text{s}},\hat{{{\to}}},{{\downarrow}}\rangle$
with actions in $\mathit{A}\times{\rm Nature}$ that results from
$\underline{\mathcal{C}}$ by attaching to every transition of
$\underline{\mathcal{C}}$ an additional _marking label_ in ${\rm Nature}$ (the
transitions in $\hat{{{\to}}}$ are marking-labeled versions of the transitions
in ${{\to}}$).

A _LLEE -witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ of_ a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ is an entry/body-labeling of
$\underline{\mathcal{C}}$ that is the recording of a LLEE-guaranteeing,
successful run
$\underline{\mathcal{C}}\mathrel{\mbox{$\Longrightarrow$\raisebox{-0.275pt}{
\leavevmode\hbox to5.52pt{\vbox to5.52pt{\pgfpicture\makeatletter\hbox{\hskip
2.76074pt\lower-2.76074pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.56075pt}{0.0pt}\pgfsys@curveto{2.56075pt}{1.41428pt}{1.41428pt}{2.56075pt}{0.0pt}{2.56075pt}\pgfsys@curveto{-1.41428pt}{2.56075pt}{-2.56075pt}{1.41428pt}{-2.56075pt}{0.0pt}\pgfsys@curveto{-2.56075pt}{-1.41428pt}{-1.41428pt}{-2.56075pt}{0.0pt}{-2.56075pt}\pgfsys@curveto{1.41428pt}{-2.56075pt}{2.56075pt}{-1.41428pt}{2.56075pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} } \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\hskip
7.39755pt}_{\text{{elim}}}^{*}}\underline{\mathcal{C}}^{\prime}$ of the multi-
step loop elimination procedure on $\underline{\mathcal{C}}$ that results by
attaching to a transition $\tau$ of $\underline{\mathcal{C}}$ the marking
label $n$ for $n\in{\rm Nature}^{+}$ (in pictures indicated as
${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[n]}}$,
in steps as
${{\to}_{{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[n]}}}}$)
forming a _loop-entry transition_ if $\tau$ is eliminated in the $n$-th multi-
step, and by attaching marking label $0$ to all other transitions of
$\underline{\mathcal{C}}$ (in pictures neglected, in steps indicated as
${{\to}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}$)
forming a _body transition_.

We say that a LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ of a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ _is guarded_ if the action labels of the loop-entry
transitions of $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ are proper
(different from
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$).
We say that a LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ is _guarded_ if $\underline{\mathcal{C}}$ has a
guarded LLEE-witness.

The definition above of guardedness for LLEE-witnesses is justified in view of
the fact that loop-entry transitions divide infinite paths in LLEE-witnesses
into finite segments that consist only of body transitions with perhaps a
leading loop-entry transition. This is a consequence of the fact that LLEE-
witnesses do not permit infinite paths of body transitions (see Lemma 13, 2).
Therefore guarded LLEE-witnesses, in which loop-entry transitions must be
proper, do not permit infinite paths of
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions.
It also follows that the underlying
(LLEE-)${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
of a guarded LLEE-witness is weakly guarded.

$\hskip
0.2pt\widehat{\underline{\mathcal{C}}}^{\scriptscriptstyle(1)}$$v$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{3}]}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{3}]}$$v_{1}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$v_{11}$$v_{2}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$$v_{21}$$\hskip
0.2pt\widehat{\underline{\mathcal{C}}}^{\scriptscriptstyle(2)}$$v$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{4}]}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{3}]}$$v_{1}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$$v_{11}$$v_{2}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$v_{21}$$\hskip
0.2pt\widehat{\underline{\mathcal{C}}}^{\scriptscriptstyle(3)}$$v$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$$v_{1}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$v_{11}$$v_{2}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$v_{21}$
Figure 6.  Three LLEE-witnesses of the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ in Figure 4, of which $\hskip
0.2pt\widehat{\underline{\mathcal{C}}}^{\scriptscriptstyle(1)}$ and $\hskip
0.2pt\widehat{\underline{\mathcal{C}}}^{\scriptscriptstyle(3)}$ are the
recordings of the successful single-step and multi-step runs of the loop
elimination procedure in Figure 4, respectively.

$v$$\underline{\mathcal{E}}_{1}$$u$$w_{1}$$w_{2}$$v$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$\hskip
0.2pt\widehat{\underline{\mathcal{E}}}_{1}^{\scriptscriptstyle(1)}$$u$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$$w_{1}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{3}]}$$w_{2}$$v$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[3]}}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$\hskip
0.2pt\widehat{\underline{\mathcal{E}}}_{1}^{\scriptscriptstyle(2)}$$u$${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[2]}}$$w_{1}$$w_{2}$

Figure 7.  A LEE-witness that is not layered (in the middle), and a LLEE-
witness (right) for a variation $\underline{\mathcal{E}}_{1}$ of the LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{E}}$ in Figure 5.

The entry/body-labelings $\hskip 0.2pt\hat{\underline{\mathcal{C}}}_{1}$ and
$\hskip 0.2pt\hat{\underline{\mathcal{C}}}_{3}$ in Figure 6 of the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ from Figure 4 are LLEE-witnesses that arise from the
successful runs of the loop elimination procedure in Example 5: $\hskip
0.2pt\hat{\underline{\mathcal{C}}}_{1}$ is the recording on
$\underline{\mathcal{C}}$ of the three single-step loop eliminations (viewed
as trivial multi-steps in order to apply the clause for a LLEE-witness in
Definition 5) that lead to $\underline{\mathcal{C}}^{\prime\prime\prime}$, and
$\hskip 0.2pt\hat{\underline{\mathcal{C}}}_{3}$ is the recording on
$\underline{\mathcal{C}}$ of the two multi-step loop eliminations from
$\underline{\mathcal{C}}$ to $\hskip
0.2pt\hat{\underline{\mathcal{C}}}^{\prime\prime\prime}$. The entry/body-
labeling $\hskip 0.2pt\hat{\underline{\mathcal{C}}}_{2}$ in Figure 6 is
another LLEE-witness of $\underline{\mathcal{C}}$ that records the successful
process of four elimination steps of four loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
each of which is induced by only a single loop-entry transition. The
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ in Figure 4 has a property that does not hold in
general: $\underline{\mathcal{C}}$ only admits layered LEE -witnesses.

Indeed, this does not hold for the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{E}}$ in Figure 5: the entry/body-labeling $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}^{\scriptscriptstyle(1)}$ is not a
layered LLEE-witness, because it arises from a run of the loop elimination
process in which in the second step a loop-entry transition is eliminated from
the body of a loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
that was eliminated in the first step. But the entry/body-labeling $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}^{\scriptscriptstyle(2)}$ there is a
layered LLEE-witness of $\underline{\mathcal{E}}$. The situation is analogous
for the two entry/body-labelings $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}_{1}^{\scriptscriptstyle(1)}$ and
$\hskip 0.2pt\widehat{\underline{\mathcal{E}}}_{1}^{\scriptscriptstyle(2)}$ of
the slightly more involved LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{E}}_{1}$ in Figure 7, where $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}_{1}^{\scriptscriptstyle(2)}$ is a
layered LLEE-witness of $\underline{\mathcal{E}}_{1}$, but $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}_{1}^{\scriptscriptstyle(1)}$ is a LEE-
witness of $\underline{\mathcal{E}}$ that is not layered.

######  Remark 12 (from LEE-witnesses to LLEE-witnesses).

It can be shown that every LEE-witness that is not layered can be transformed
into a layered LEE-witness (LLEE-witness) of the same underlying
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart.
Indeed, the step from the (not layered) LEE-witness $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}_{1}^{\scriptscriptstyle(1)}$ to the
LLEE-witness $\hskip
0.2pt\widehat{\underline{\mathcal{E}}}_{1}^{\scriptscriptstyle(2)}$ in the
example in Figure 7, which transfers the loop-entry transition marking label
${{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[3]}}$
from the transition from $w_{1}$ to $w_{2}$ over to the transition from $v$ to
$u$, hints at the proof of this statement. However, we do not need this
result, because we will be able to use the guaranteed existence of LLEE-
witnesses (see Theorem 4.3) for the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation below (see Definition 4.2).

For the proofs in Section 6 we will need the ‘descends-in-loop-to’ relation
${\curvearrowright}$ as defined below, and the fact that it constitutes a
‘descent’ in a LLEE-witness. The latter is expressed by the subsequent lemma
together with termination of the body-step relation
${{\to}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}$.
Both of these properties can be established by arguing with the successful
runs of the loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
elimination procedure that underlies a LLEE-witness.

Let $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ be a LLEE-witness of a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}=\langle
V,\mathit{A},{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1},v_{\text{s}},{{\to}},{{\downarrow}}\rangle$.

Let $v,w\in V$. We denote by $v\mathrel{{\curvearrowright}}w$, and by
$w\mathrel{{\curvearrowleft}}v$, and say that $v$ _descends in a loop to_ $w$,
if $w$ is in the body of the loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
at $v$, which means that there is a path
$v\mathrel{{{\to}_{{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[n]}}}}}v^{\prime}\mathrel{{{\to}^{*}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}}w$
from $v$ via a loop-entry transition and subsequent body transitions without
encountering $v$ again.

######  Lemma 13.

The relations ${\curvearrowright}$ and
${{\to}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}$
defined by a LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ of a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ satisfy:

  1. (1)

${{\curvearrowleft}^{+}}$ is a well-founded, strict partial order on $V$.

  2. (2)

${\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}$
is a well-founded strict partial order on $V$.

######  Proof 4.2.

Well-foundedness and irreflexivity of each of ${{\curvearrowleft}^{+}}$ and
${\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}$
follows from termination of ${\curvearrowright}$ and
${{\to}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}$,
respectively. These termination properties can be established in the same way
as for LLEE-charts without
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions,
for which they follow immediately from Lemma 5.2 in [GF20a, GF20b]. Since
${{\curvearrowleft}^{+}}$ and
${\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}$
are transitive by definition, it follows that both relations are well-founded
strict partial orders.

While chart interpretations of ‘$1$-free’ star expressions always satisfy LEE,
see [GF20b]), we observed in [Gra21c] that this is not true for the chart
interpretations of star expressions in general. As a remedy for this failure
of LEE for chart interpretations, we introduced
‘${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretations’ of star expressions [Gra21c]. For such
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretations we showed that LEE is guaranteed, and that they refine chart
interpretations in the sense that there always is a functional
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulation
from the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation of a star expression to its chart interpretation (see Theorem
4.3 below). For the definition of
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretations we extended the syntax of star expressions to obtain ‘stacked
star expressions’, see the definition below. The intuition behind the use of
the ‘stack product’ symbol
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$
is to keep track of when a transition has descended into the body of an
iteration expression such that the iteration can be interpreted as a loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
or a tower of nested (and possibly partially overlapping) loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts.
This feature of
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$
makes a transition system specification possible (see Definition 4.2) which
introduces
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions
only as ‘backlinks’ that lead from the body (the internal vertices) of some
loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{L}}$ of a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation back to the start vertex of $\underline{\mathcal{L}}$.

[stacked star expressions] Let $\mathit{A}$ be a set whose members we call
_actions_. The set
${\mathit{StExp}^{{\scriptscriptstyle(}{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}{\scriptscriptstyle)}}}({\mathit{A}})$
of _stacked star expressions over (actions in) $\mathit{A}$_ is defined by the
grammar:

$E\;\;\>{::=}\>\;\;e\>\mid\>{E}\mathrel{{\cdot}}{e}\>\mid\>{E}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e^{*}}}\qquad\text{(where
$e\in{\textit{StExp}}({\mathit{A}})$)}\hskip 1.5pt{.}$

Note that the set ${\textit{StExp}}({\mathit{A}})$ of star expressions would
arise if the clause
${E}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e^{*}}}$
were dropped.

The _star height_ $|{E}|_{\scalebox{0.8}{$*$}}$ of stacked star expressions
$E$ is defined by adding the two clauses
$|{{E}\mathrel{{\cdot}}{e}}|_{\scalebox{0.8}{$*$}}\mathrel{{:=}}\max\left\\{{|{E}|_{\scalebox{0.8}{$*$}},\,|{e}|_{\scalebox{0.8}{$*$}}}\right\\}$,
and
$|{{E}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e^{*}}}}|_{\scalebox{0.8}{$*$}}\mathrel{{:=}}\max\left\\{{|{E}|_{\scalebox{0.8}{$*$}},\,|{{e^{*}}}|_{\scalebox{0.8}{$*$}}}\right\\}$
to the definition of the star height of star expressions.

The _projection function_
$\pi\mathrel{:}{\mathit{StExp}^{{\scriptscriptstyle(}{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}{\scriptscriptstyle)}}}({\mathit{A}})\to{\textit{StExp}}({\mathit{A}})$
is defined by interpreting
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$
as ${\cdot}$ by the clauses:
${\pi}({{E}\mathrel{{\cdot}}{e}})\mathrel{{:=}}{{\pi}({E})}\mathrel{{\cdot}}{e}$,
${\pi}({{E}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e^{*}}}})\mathrel{{:=}}{{\pi}({E})}\mathrel{{\cdot}}{{e^{*}}}$,
and ${\pi}({e})\mathrel{{:=}}e$, for all stacked star expressions
$E\in{\mathit{StExp}^{{\scriptscriptstyle(}{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}{\scriptscriptstyle)}}}({\mathit{A}})$,
and star expressions $e\in{\textit{StExp}}({\mathit{A}})$.

In line with [Gra21c] we introduce the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation of a star expression $e$ with notation
${\underline{\mathcal{C}}}({e})$ as ‘the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
induced by (the process interpretation of) $e$’. For understanding the TSS in
its definition below it is key to note that, by the rules for iterations, the
stacked product operation
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$
helps to record that an expression has descended from the iteration expression
on the right-hand side of
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$.
This feature is used by the rule for stacked product to introduce
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions
only as backlinks to expressions from which they have descended. The rules for
iteration expressions define loop-entry transitions and body transitions,
respectively, dependent on whether $e$ is ‘strongly normed’ (symbolically
denoted by ${{\textit{nd}^{+}}}({e})$) in the sense of facilitating a process
trace to termination, and hence dependent on whether an iteration induces a
loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
(outside of inner loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts).

[${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation of star expressions] By 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 expression
$e$ we mean the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
that arises together with the entry/body-labeling ${\hskip
0.2pt\hat{\underline{\mathcal{C}}}}({e})$ as the $e$-rooted labeled transition
system with
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transitions
(${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-LTS)
generated by $\left\\{{e}\right\\}$ according to the following TSS on the set
$\mathit{StExp}^{{\scriptscriptstyle(}{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}{\scriptscriptstyle)}}$
of stacked star expressions, where
${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}\in\left\\{{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}\right\\}\cup\left\\{{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{n}]}}}\mathrel{|}{n\in{\rm
Nature}^{+}}\right\\}$ are marking labels:

$\begin{gathered}\begin{aligned} &\ignorespaces\ignorespaces\leavevmode\lower
25.54443pt\hbox{\vbox{\hbox{\hskip
4.0pt\hbox{$\phantom{a_{i}\>\mathrel{{\xrightarrow{a_{i}}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}}}\>1}$}\hskip
4.0pt}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to42.94138pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 1.92928pt\hbox{\hbox{\hskip
4.0pt\hbox{$a\>\mathrel{{\xrightarrow{a}}{{}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}}\>1$}\hskip
4.0pt}}}}}\ignorespaces&&\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
26.16666pt\hbox{\vbox{\hbox{\hbox{\hskip
4.0pt\hbox{$e_{i}\>\mathrel{{\xrightarrow{a}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}}}}\>E^{\prime}_{i}$}\hskip
4.0pt}\hbox{}\hbox{\hskip
4.0pt\hbox{\scriptsize($i\in\left\\{{1,2}\right\\}$)}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to84.50673pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 11.76057pt\hbox{\hbox{\hskip
4.0pt\hbox{${e_{1}}+{e_{2}}\>\mathrel{{\xrightarrow{a}}{{}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}}\>E^{\prime}_{i}$}\hskip
4.0pt}}}}}\ignorespaces&&\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
26.94443pt\hbox{\vbox{\hbox{\hbox{\hskip
4.0pt\hbox{$\phantom{e_{1}}e\>\mathrel{{\xrightarrow{a}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}}}}\>E^{\prime}\phantom{E^{\prime}_{1}}$}\hskip
4.0pt}\hbox{}\hbox{\hskip 4.0pt\hbox{\scriptsize(if
${\textit{nd${}^{+}$}}({e})$)}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to95.01216pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 13.21959pt\hbox{\hbox{\hskip
4.0pt\hbox{${e^{*}}\>\mathrel{{\xrightarrow{a}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{|{{e^{*}}}|_{\scalebox{0.8}{$*$}}}]}}}}}\>{E^{\prime}}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e^{*}}}$}\hskip
4.0pt}}}}}\ignorespaces&&\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
26.19443pt\hbox{\vbox{\hbox{\hbox{\hskip
4.0pt\hbox{$\phantom{e_{1}}e\>\mathrel{{\xrightarrow{a}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}}}}\>E^{\prime}\phantom{e^{\prime}_{1}}$}\hskip
4.0pt}\hbox{}\hbox{\hskip 4.0pt\hbox{\scriptsize(if
$\neg{{\textit{nd${}^{+}$}}({e})}$)}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to96.37679pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 16.72342pt\hbox{\hbox{\hskip
4.0pt\hbox{${e^{*}}\>\mathrel{{\xrightarrow{a}}{{}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}}\>{E^{\prime}}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e^{*}}}$}\hskip
4.0pt}}}}}\ignorespaces\end{aligned}\\\ \begin{aligned}
&\ignorespaces\ignorespaces\leavevmode\lower
26.16666pt\hbox{\vbox{\hbox{\hskip 10.23405pt\hbox{\hskip
4.0pt\hbox{$E_{1}\>\mathrel{{\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}}}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}}}}\>E^{\prime}_{1}$}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to64.95021pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{${E_{1}}\mathrel{{\cdot}}{e_{2}}\>\mathrel{{\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}}}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}}}}\>{E^{\prime}_{1}}\mathrel{{\cdot}}{e_{2}}$}\hskip
4.0pt}}}}\ignorespaces&&\ignorespaces\ignorespaces\leavevmode\lower
26.19443pt\hbox{\vbox{\hbox{\hskip 17.17844pt\hbox{\hskip
4.0pt\hbox{$E_{1}\>\mathrel{{\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}}}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}}}}\>E^{\prime}_{1}$}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to78.83897pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{${E_{1}}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e_{2}^{*}}}\>\mathrel{{\xrightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}}}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}}}}\>{E^{\prime}_{1}}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e_{2}^{*}}}$}\hskip
4.0pt}}}}\ignorespaces&&\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
26.16666pt\hbox{\vbox{\hbox{\hbox{\hskip
4.0pt\hbox{${e_{1}}{{\downarrow}}$}\hskip 4.0pt}\hbox{\hskip
14.45377pt}\hbox{\hskip
4.0pt\hbox{$e_{2}\>\mathrel{{\xrightarrow{a}}{{}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}}}}}\>E^{\prime}_{2}$}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to76.37598pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 10.19522pt\hbox{\hbox{\hskip
4.0pt\hbox{${e_{1}}\mathrel{{\cdot}}{e_{2}}\>\mathrel{{\xrightarrow{a}}{{}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}}\>E^{\prime}_{2}$}\hskip
4.0pt}}}}}\ignorespaces&&\ignorespaces\ignorespaces\leavevmode\lower
27.54443pt\hbox{\vbox{\hbox{\hskip 4.0pt\hbox{$\hskip
21.52771pt{e_{1}}{{\downarrow}}\rule{0.0pt}{13.0pt}\hskip 21.52771pt$}\hskip
4.0pt}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to63.5117pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 1.45483pt\hbox{\hbox{\hskip
4.0pt\hbox{${e_{1}}\mathrel{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}{{e_{2}^{*}}}\>\mathrel{{\xrightarrow{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}}}{{}_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}}\>{e_{2}^{*}}$}\hskip
4.0pt}}}}}\ignorespaces\end{aligned}\end{gathered}$

The condition ${{\textit{nd}^{+}}}({e})$ means a strengthening of normedness,
namely, that $e$ permits a positive length path to an expression $f$ with
${f}{{\downarrow}}\,$; it is definable by induction. Immediate termination for
expressions of ${\underline{\mathcal{C}}}({e})$ is defined by the same rules
as in Definition 2 (for star expressions only, preventing immediate
termination for expressions with stacked product
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$).
We note that finiteness of ${\underline{\mathcal{C}}}({e})$ as a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
is guaranteed by Theorem 4.3, (ii), below.

We also extend the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation of star expressions in the obvious way to all stacked star
expressions
$E\in\mathit{StExp}^{{\scriptscriptstyle(}{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}{\scriptscriptstyle)}}$:
by ${\underline{\mathcal{C}}}({E})$ we mean the $E$-rooted
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-LTS
generated by $\left\\{{E}\right\\}$ in the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-LTS
generated by the TSS above.

For every stacked star expression
$E\in{\mathit{StExp}^{{\scriptscriptstyle(}{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}{\scriptscriptstyle)}}}({\mathit{A}})$,
we define the set ${\textit{\text@underline{A$\partial$}}}({E})$ of _action
(partial) 1-derivatives of_ $E$, and the set ${{\underline{\partial}}}({E})$
of _(partial) 1-derivatives of_ $E$ by:

$\displaystyle{\textit{\text@underline{A$\partial$}}}({E})$
$\displaystyle{}\mathrel{{:=}}\bigl{\\{}{\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}\mathrel{\big{|}}{E\mathrel{{\xrightarrow{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}}}}E^{\prime}}\bigr{\\}}\subseteq{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{\mathit{A}}}\times{\mathit{StExp}^{{\scriptscriptstyle(}{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}{\scriptscriptstyle)}}}({\mathit{A}})\hskip
1.5pt{,}$ $\displaystyle{{\underline{\partial}}}({E})$
$\displaystyle{}\mathrel{{:=}}\bigl{\\{}{E^{\prime}}\mathrel{\big{|}}{E\mathrel{{\xrightarrow{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}}}}E^{\prime}\text{
for some
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}\in{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{\mathit{A}}}$}}\bigr{\\}}\subseteq{\mathit{StExp}^{{\scriptscriptstyle(}{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}{\scriptscriptstyle)}}}({\mathit{A}})\hskip
1.5pt{,}$

where the transitions are defined by the TSS in Definition 4.2.

######  Lemma 14.

The action 1-derivatives ${\textit{\text@underline{A$\partial$}}}({E})$ of a
stacked star expression $E$ over actions in $\mathit{A}$ satisfy the following
recursive equations, for all $a\in\mathit{A}$,
$e,e_{1},e_{2}\in{\textit{StExp}}({\mathit{A}})$, and stacked star expressions
$E_{1}$ over actions in $\mathit{A}$:

$\displaystyle{\textit{\text@underline{A$\partial$}}}({0})$
$\displaystyle{}\mathrel{{:=}}{\textit{\text@underline{A$\partial$}}}({1})\mathrel{{:=}}\varnothing\hskip
1.5pt{,}$ $\displaystyle{\textit{\text@underline{A$\partial$}}}({a})$
$\displaystyle{}\mathrel{{:=}}\left\\{{\langle a,\hskip
0.5pt1\rangle}\right\\}\hskip 1.5pt{,}$
$\displaystyle{\textit{\text@underline{A$\partial$}}}({e_{1}+e_{2}})$
$\displaystyle{}\mathrel{{:=}}{\textit{\text@underline{A$\partial$}}}({e_{1}})\cup{\textit{\text@underline{A$\partial$}}}({e_{2}})\hskip
1.5pt{,}$
$\displaystyle{\textit{\text@underline{A$\partial$}}}({E_{1}\,{{\cdot}}\,e_{2}})$
$\displaystyle{}\mathrel{{:=}}\begin{cases}\bigl{\\{}{\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}_{1}\,{{\cdot}}\,e_{2}\rangle}\mathrel{\big{|}}{\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}_{1}\rangle\in{\textit{\text@underline{A$\partial$}}}({E_{1}})}\bigr{\\}}&\text{if
${E_{1}}{\ndownarrow}$,}\\\
\bigl{\\{}{\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}_{1}\,{{\cdot}}\,e_{2}\rangle}\mathrel{\big{|}}{\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}_{1}\rangle\in{\textit{\text@underline{A$\partial$}}}({E_{1}})}\bigr{\\}}\cup{\textit{\text@underline{A$\partial$}}}({E_{2}})&\text{if
${E_{1}}{{\downarrow}}$,}\end{cases}$
$\displaystyle{\textit{\text@underline{A$\partial$}}}({E_{1}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,e^{*}_{2}})$
$\displaystyle{}\mathrel{{:=}}\begin{cases}\bigl{\\{}{\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}_{1}\,{{\cdot}}\,e^{*}_{2}\rangle}\mathrel{\big{|}}{\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}_{1}\rangle\in{\textit{\text@underline{A$\partial$}}}({E_{1}})}\bigr{\\}}&\text{if
${E_{1}}{\ndownarrow}$,}\\\
\bigl{\\{}{\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}_{1}\,{{\cdot}}\,e^{*}_{2}\rangle}\mathrel{\big{|}}{\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}_{1}\rangle\in{\textit{\text@underline{A$\partial$}}}({E_{1}})}\bigr{\\}}\cup\left\\{{\langle{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1},\hskip
0.5pte^{*}_{2}\rangle}\right\\}&\text{if ${E_{1}}{{\downarrow}}$,}\end{cases}$
$\displaystyle{\textit{\text@underline{A$\partial$}}}({e^{*}})$
$\displaystyle{}\mathrel{{:=}}\bigl{\\{}{\langle a,\hskip
0.5ptE^{\prime}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,e^{*}\rangle}\mathrel{\big{|}}{\langle
a,\hskip
0.5ptE^{\prime}\rangle\in{\textit{\text@underline{A$\partial$}}}({e})}\bigr{\\}}\hskip
1.5pt{.}$

######  Proof 4.3.

By case-wise inspection of the definition of the TSS in Def. 4.2.

[[Gra20, Gra21c]] For every $e\in{\textit{StExp}}({\mathit{A}})$, the
following statements hold for the concepts as introduced in Definition 4.2:

  1. (i)

The entry/body-labeling ${\hskip 0.2pt\hat{\underline{\mathcal{C}}}}({e})$ of
${\underline{\mathcal{C}}}({e})$ is a guarded LLEE-witness of
${\underline{\mathcal{C}}}({e})$.

  2. (ii)

The projection function $\pi$ defines a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulation
from 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$ to the chart
interpretation ${\mathcal{C}}({e})$ of $e$, that is symbolically,
${\underline{\mathcal{C}}}({e})\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{$\rightarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}_{\pi}}}{\mathcal{C}}({e})$, and hence also
${\underline{\mathcal{C}}}({e})\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})$. Since the set of stacked star expressions
that form the pre-image of a star expression under the projection function is
always finite, it follows that
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretations of star expressions are always finite as well.

For the proof of Lemma 17 below we will need the second of the two subsequent
lemmas, Lemma 16. Its proof uses the first lemma, which crucially states that
every star expression $e$ with immediate termination can Mil--provably be
written as a star expression $1+f$ where $f$ does not permit immediate
termination.

######  Lemma 15.

If ${e}{{\downarrow}}$ for a star expression
$e\in{\textit{StExp}}({\mathit{A}})$, then there is a star expression
$f\in{\textit{StExp}}({\mathit{A}})$ with ${f}{\ndownarrow}$,
$e\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}1+f$,
$|{f}|_{\scalebox{0.8}{$*$}}=|{e}|_{\scalebox{0.8}{$*$}}$, and
${{((\textrm{id}\times\pi)}\circ{\textit{\text@underline{A$\partial$}})}}({f})={{((\textrm{id}\times\pi)}\circ{\textit{\text@underline{A$\partial$}})}}({e})$.

######  Proof 4.4.

By a proof by induction on structure of $e$, in which all axioms of Mil- are
used.

######  Lemma 16.

${\pi}({E})\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}{\tau_{{\underline{\mathcal{C}}}({E})}}({E})+\sum_{i=1}^{n}{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}_{i}}}\mathrel{{\cdot}}{{\pi}({E^{\prime}_{i}})}$,
given a list representation
${T_{{\underline{\mathcal{C}}}({E})}}({w})=\bigl{\\{}{E\mathrel{{\xrightarrow{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}_{i}}}}}E^{\prime}_{i}}\mathrel{\big{|}}{i\in\left\\{{1,\ldots,n}\right\\}}\bigr{\\}}$
of the transitions from $E$ in ${\underline{\mathcal{C}}}({E})$.

######  Proof 4.5.

We establish the lemma by induction on the star height
$|{E}|_{\scalebox{0.8}{$*$}}$ of $E$ with a subinduction on the syntactical
structure of $E$. All cases of stacked star expressions can be dealt with in a
quite straightforward manner, except for the case of star expressions with an
outermost iteration. There, an appeal to Lemma 15 is crucial. We treat this
case in detail below.

Suppose that $E\mathrel{{\equiv}}e^{*}$ for some star expression
$e\in{\textit{StExp}}({\mathit{A}})$ (without occurrences of stacked product
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$).
For showing the representation of ${\pi}({E})$ as stated by the lemma, we
assume that the transitions from $e$ in ${\underline{\mathcal{C}}}({e})$ as
defined in Definition 4.2 are as follows:

${T_{{\underline{\mathcal{C}}}({e})}}({e})=\bigl{\\{}{e\mathrel{{\xrightarrow{a_{i}}}}E^{\prime}_{i}}\mathrel{\big{|}}{i=1,\ldots
n}\bigr{\\}}\hskip 1.5pt{,}$ (4)

for some stacked star expression $E^{\prime}_{1},\ldots,E^{\prime}_{n}$, which
are 1-derivatives of $e$. Note that according to the TSS in Definition 4.2
only proper transitions (those with proper action labels in $\mathit{A}$) can
depart from the star expression $e$ (which does not contain stacked products
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$).
Then it follows, again from the TSS in Definition 4.2 that:

${T_{{\underline{\mathcal{C}}}({E})}}({E})={T_{{\underline{\mathcal{C}}}({e^{*}})}}({e^{*}})=\bigl{\\{}{e^{*}\mathrel{{\xrightarrow{a_{i}}}}E^{\prime}_{i}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,e^{*}}\mathrel{\big{|}}{i=1,\ldots
n}\bigr{\\}}\hskip 1.5pt{.}$ (5)

We assume now that ${e}{{\downarrow}}$ holds. (We will see that if
${e}{\ndownarrow}$ holds, the argumentation below becomes easier). Then by
Lemma 15 there is a star expression $f\in{\textit{StExp}}({\mathit{A}})$ with
${f}{\ndownarrow}$, and such that $1+f\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}e$,
$|{f}|_{\scalebox{0.8}{$*$}}=|{e}|_{\scalebox{0.8}{$*$}}$, and
${{((\textrm{id}\times\pi)}\circ{\textit{\text@underline{A$\partial$}})}}({f})={{((\textrm{id}\times\pi)}\circ{\textit{\text@underline{A$\partial$}})}}({e})$
hold. From the latter it follows with (4):

$\displaystyle{T_{{\underline{\mathcal{C}}}({f})}}({f})$
$\displaystyle{}=\bigl{\\{}{f\mathrel{{\xrightarrow{a_{i}}}}F^{\prime}_{i}}\mathrel{\big{|}}{i=1,\ldots
n}\bigr{\\}}\hskip 1.5pt{,}$ (6) $\displaystyle{\pi}({F^{\prime}_{i}})$
$\displaystyle{}={\pi}({E^{\prime}_{i}})\qquad\text{(for all $i=1,\ldots
n$)}\hskip 1.5pt{,}$ (7)

for some stacked star expression $F^{\prime}_{1},\ldots,F^{\prime}_{n}$, which
are 1-derivatives of $f$. Note again that only proper transitions can depart
from the star expression $f$ according to Definition 4.2. On the basis of
these assumptions we can now argue as follows:

$\displaystyle{\pi}({E})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\pi}({e^{*}})$
(due to $E\mathrel{{\equiv}}e^{*}$ in this case)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>e^{*}$ (since
$e^{*}$ does not contain
${\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}$}\>(1+f)^{*}$ (by the choice of $f$
with $1+f\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}e$) $\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}$}\>f^{*}$ (by axiom (${\text{trm-
body}}({{}^{*}})$))
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}$}\>1+f\,{{\cdot}}\,f^{*}$ (by axiom
(${\text{rec}}({{}^{*}})$))
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}$}\>1+f\,{{\cdot}}\,(1+f)^{*}$ (by
axiom (${\text{trm-body}}({{}^{*}})$))
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}$}\>1+f\,{{\cdot}}\,e^{*}$ (by the
choice of $f$ with $1+f\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}e$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>1+\bigl{(}{\tau_{{\underline{\mathcal{C}}}({f})}}({f})+\sum_{i=1}^{n}a_{i}\,{{\cdot}}\,{\pi}({F^{\prime}_{i}})\bigr{)}\,{{\cdot}}\,e^{*}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>1+\bigl{(}0+\sum_{i=1}^{n}a_{i}\,{{\cdot}}\,{\pi}({E^{\prime}_{i}})\bigr{)}\,{{\cdot}}\,e^{*}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\tau_{{\underline{\mathcal{C}}}({e^{*}})}}({e^{*}})+\sum_{i=1}^{n}a_{i}\,{{\cdot}}\,({\pi}({E^{\prime}_{i}})\,{{\cdot}}\,e^{*})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\tau_{{\underline{\mathcal{C}}}({E})}}({E})+\sum_{i=1}^{n}a_{i}\,{{\cdot}}\,{\pi}({E^{\prime}_{i}\,{{\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\varstar}}\,e^{*}})$
(by the definition of the projection $\pi$).

In view of (5), this chain of Mil--provable equalities verifies the statement
in the lemma in this case $E=e^{*}$ with ${e}{{\downarrow}}$. If
${e}{\ndownarrow}$ holds, then the detour via $f$ is not necessary, and the
argument is much simpler. The statement of the lemma holds true then as well.

######  Lemma 17.

For every star expression $e\in{\textit{StExp}}({\mathit{A}})$ with
${\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})=\langle{V}({e}),\mathit{A},{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1},e,{{\to}},{{\downarrow}}\rangle$
the star-expression function
$s\mathrel{:}{V}({e})\to{\textit{StExp}}({\mathit{A}})$, $E\mapsto{\pi}({E})$
is a Mil--provable solution of ${\underline{\mathcal{C}}}({e})$ with principal
value $e$.

######  Proof 4.6.

The statement of the lemma is an immediate consequence of Lemma 16.

##  5\. Coinductive version of Milner’s proof system

In this section we motivate and define ‘coinductive proofs’, introduce
coinductive versions of Milner’s system Mil, and establish first
interconnections between these proof systems.

$\underline{\mathcal{C}}$${{{\mathcal{C}}({e_{1}})}/_{{=_{\text{\sf
Mil}}\hskip 1.0pt}}}$${{{\mathcal{C}}({e_{2}})}/_{{=_{\text{\sf Mil}}\hskip
1.0pt}}}$LLEE, guarded$\left[{L_{1}}\right]_{{=_{\text{\sf Mil}}\hskip
1.0pt}}$$\left[{L_{2}}\right]_{{=_{\text{\sf Mil}}\hskip 1.0pt}}$ Figure 8.  A
coinductive proof $\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ over
Mil of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$
gives rise to functional
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
to factor charts of ${\mathcal{C}}({e_{1}})$ and ${\mathcal{C}}({e_{2}})$ with
respect to provability in Mil.

As the central concept we now introduce ‘coinductive proofs’ over
$\mathcal{EL}$-based proof systems ${\mathcal{S}}$. We have seen examples for
such circular deductions earlier in Figure 1 and Figure 2. We define a
coinductive proof over ${\mathcal{S}}$ as a weakly guarded
${\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 star
expressions such that the left-, and the right-hand sides of the equations
form ${\mathcal{S}}$-provable solutions of $\underline{\mathcal{C}}$. The
conclusion of such a proof is the equation that labels the start vertex of
$\underline{\mathcal{C}}$. If ${\mathcal{S}}$ is theorem-subsumed by Mil
(formally, ${\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$ holds), then a
coinductive proof with
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$, conclusion
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$,
and left- and right-hand side labeling functions $L_{1}$ and $L_{2}$ can be
viewed, due to Proposition 10, as a pair of
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
defined by $\left[{L_{1}}\right]_{{=_{\text{\sf Mil}}\hskip 1.0pt}}$ and by
$\left[{L_{2}}\right]_{{=_{\text{\sf Mil}}\hskip 1.0pt}}$ from
$\underline{\mathcal{C}}$ to ${{{\mathcal{C}}({e_{1}})}/_{{=_{\text{\sf
Mil}}\hskip 1.0pt}}}$, and to ${{{\mathcal{C}}({e_{2}})}/_{{=_{\text{\sf
Mil}}\hskip 1.0pt}}}$ (see Figure 8). In this case we can show that the
conclusion
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$
of the coinductive proof is semantically sound (see Proposition 20). Indeed a
stronger statement holds, and its proof will form the central part of Section
6: if ${\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$ holds, and the
underlying chart of the coinductive proof of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$
over ${\mathcal{S}}$ is a LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart,
then that proof can be transformed into a proof of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$
in Milner’s system Mil (see Proposition 29 in the next section).

In order to guarantee that coinductive proofs over a proof system
${\mathcal{S}}$ can only derive semantically valid equations, it is necessary
to demand that ${\mathcal{S}}$ is sound for process-semantics equality
${=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}$ (for example if
${\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$, using Proposition 2.2).
This notwithstanding, we do not include this requirement in the definition
below, but add it later to statements when it is needed. The reason is that in
Section 7 we want to be able to show (see Lemma 36) that even instances of the
fixed-point rule $\textrm{RSP}^{*}$ with premises that are not semantically
valid can be mimicked by coinductive proofs over appropriate proof systems
that are unsound.

[(LLEE-witnessed) coinductive proofs] Let $\mathit{A}$ be a set of actions.
Let ${\mathcal{S}}$ be an ${\text{$\mathcal{EL}$}}({\mathit{A}})$-based proof
system with $\text{\sf ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}$. Let
$e_{1},e_{2}\in{\textit{StExp}}({\mathit{A}})$ be star expressions.

By a _coinductive proof over ${\mathcal{S}}$ of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$_
we mean a pair $\mathcal{CP}=\langle\underline{\mathcal{C}},\hskip
0.5ptL\rangle$ that consists of a weakly guarded
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}=\langle
V,\mathit{A},{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1},v_{\text{s}},{{\to}},{{\downarrow}}\rangle$,
and a labeling function $L\mathrel{:}V\to{\textit{Eq}}({\mathit{A}})$ of
vertices of $\underline{\mathcal{C}}$ by formal equations over $\mathit{A}$
such that for the functions
$L_{1},L_{2}\mathrel{:}V\to{\textit{StExp}}({\mathit{A}})$ that denote the
star expressions ${L_{1}}({v})$, and ${L_{2}}({v})$, on the left-, and on the
right-hand side of the equation ${L}({v})$, respectively, the following
conditions hold:

  1. (cp1)

$L_{1}$ and $L_{2}$ are ${\mathcal{S}}$-provable solutions of
$\underline{\mathcal{C}}$,

  2. (cp2)

$e_{1}\mathrel{{\equiv}}{L_{1}}({v_{\text{s}}})$ and
$e_{2}\mathrel{{\equiv}}{L_{2}}({v_{\text{s}}})$ ($e_{1}$ and $e_{2}$ are
principal values of $L_{1}$ and $L_{2}$, respectively).

We denote by
$e_{1}\mathrel{{\overset{\text{coind}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}}}e_{2}$
that there is a coinductive proof over ${\mathcal{S}}$ of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$.

By a _LLEE -witnessed coinductive proof_ over ${\mathcal{S}}$ we mean a
coinductive proof $\mathcal{CP}=\langle\underline{\mathcal{C}},\hskip
0.5ptL\rangle$ where $\underline{\mathcal{C}}$ is a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart.
We denote by $e_{1}\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}}}e_{2}$ that there is a LLEE-
witnessed coinductive proof over ${\mathcal{S}}$ of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$.

While the restriction to guardedness of the LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
underlying LLEE-witnessed coinductive proofs could be relaxed to weak
guardedness, we have required guardedness in this definition in order to
(somewhat) reduce technicalities in the proofs in Section 6.

We provide two examples of LLEE-witnessed coinductive proofs. First we develop
a new one, and then we revisit and justify the example in Figure 1 from the
introduction.

In Figure 9 we have illustrated a LLEE-witnessed coinductive proof over Mil-
of the statement
${({{a^{*}}}\mathrel{{\cdot}}{{b^{*}}})^{*}}\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}}}{({a}+{b})^{*}}$. Formally this proof is of the
form $\mathcal{CP}=\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ where
$\underline{\mathcal{C}}={\underline{\mathcal{C}}}({(a^{*}\,{{\cdot}}\,b^{*})^{*}})$
has the guarded LLEE-witness ${\hskip
0.2pt\hat{\underline{\mathcal{C}}}}({(a^{*}\,{{\cdot}}\,b^{*})^{*}})$ (see
Theorem 4.3) as indicated in Figure 9 where framed boxes contain vertex names.

In this illustration we have drawn the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ that carries the equations with its start vertex
below in order to adhere to the prooftree intuition for the represented
derivation, namely with the conclusion at the bottom. We will do so repeatedly
also below. Solution correctness for the left-hand sides $L_{1}$ of the
equations $L$ on $\underline{\mathcal{C}}$ in Figure 9 follow from Lemma 17,
because
$\underline{\mathcal{C}}={\underline{\mathcal{C}}}({(a^{*}\,{{\cdot}}\,b^{*})^{*}})$
where $(a^{*}\,{{\cdot}}\,b^{*})^{*}$ is the left-hand side of the conclusion.
This notwithstanding, below we verify the correctness conditions in
$\underline{\mathcal{C}}$ for the left-hand side $L_{1}$ and the right-hand
side $L_{2}$ of the equation labeling function $L$ for the (most involved)
case of vertex $v_{1}$ as follows (we neglect some associative brackets, and
combine some applications of axioms in Mil-):

${({({1}\hskip 1.0pt{{\cdot}}\hskip 1.0pt{{a^{*}}})}\hskip
1.0pt{{\cdot}}\hskip 1.0pt{{b^{*}}})}\hskip 1.0pt{{\cdot}}\hskip
1.0pt{{({{a^{*}}}\hskip 1.0pt{{\cdot}}\hskip
1.0pt{{b^{*}}})^{*}}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{1}\hskip
1.0pt{{\cdot}}\hskip 1.0pt{{({a}+{b})^{*}}}$${({1}\hskip 1.0pt{{\cdot}}\hskip
1.0pt{{b^{*}}})}\hskip 1.0pt{{\cdot}}\hskip 1.0pt{{({{a^{*}}}\hskip
1.0pt{{\cdot}}\hskip
1.0pt{{b^{*}}})^{*}}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{1}\hskip
1.0pt{{\cdot}}\hskip 1.0pt{{({a}+{b})^{*}}}$${({{a^{*}}}\hskip
1.0pt{{\cdot}}\hskip 1.0pt{{b^{*}}})}\hskip 1.0pt{{\cdot}}\hskip
1.0pt{{({{a^{*}}}\hskip 1.0pt{{\cdot}}\hskip
1.0pt{{b^{*}}})^{*}}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{({a}+{b})^{*}}$${{b^{*}}}\hskip
1.0pt{{\cdot}}\hskip 1.0pt{{({{a^{*}}}\hskip 1.0pt{{\cdot}}\hskip
1.0pt{{b^{*}}})^{*}}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{({a}+{b})^{*}}$${({{a^{*}}}\hskip
1.0pt{{\cdot}}\hskip
1.0pt{{b^{*}}})^{*}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{({a}+{b})^{*}}$$v_{11}$$v_{1}$${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}a}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$b$$v_{21}$$v_{2}$${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}b}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$$v_{\text{s}}$${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}a}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}b}$${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$
Figure 9. LLEE-witnessed coinductive proof of
${({{a^{*}}}\mathrel{{\cdot}}{{b^{*}}})^{*}}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{({a}+{b})^{*}}$
over Mil- (see Ex. 5).

$\displaystyle{L_{1}}({v_{1}})$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{\equiv}}$}}(a^{*}\cdot
b^{*})\cdot(a^{*}\cdot b^{*})^{*}$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}((1+a\cdot a^{*})\cdot(1+b\cdot b^{*}))\cdot(a^{*}\cdot b^{*})^{*}$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(1\cdot 1+a\cdot a^{*}\cdot 1+1\cdot b\cdot b^{*}+a\cdot a^{*}\cdot
b\cdot b^{*})\cdot(a^{*}\cdot b^{*})^{*}$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(1+a\cdot a^{*}+a\cdot a^{*}\cdot b\cdot b^{*}+b\cdot
b^{*})\cdot(a^{*}\cdot b^{*})^{*}$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(1+a\cdot a^{*}\cdot(1+b\cdot b^{*})+b\cdot b^{*})\cdot(a^{*}\cdot
b^{*})^{*}$ $\displaystyle{}\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}(1+a\cdot a^{*}\cdot b^{*}+b\cdot
b^{*})\cdot(a^{*}\cdot b^{*})^{*}$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1\cdot(a^{*}\cdot b^{*})^{*}+a\cdot(((1\cdot a^{*})\cdot
b^{*})\cdot(a^{*}\cdot b^{*})^{*})+b\cdot((1\cdot b^{*})\cdot(a^{*}\cdot
b^{*})^{*})$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{\equiv}}$}}1\cdot{L_{1}}({v_{\text{s}}})+a\cdot{L_{1}}({v_{11}})+b\cdot{L_{1}}({v_{21}})$
$\displaystyle{L_{2}}({v_{1}})$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{\equiv}}$}}(a+b)^{*}$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(a+b)^{*}+(a+b)^{*}\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1+(a+b)\cdot(a+b)^{*}+1+(a+b)\cdot(a+b)^{*}$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1+1+(a+b)\cdot(a+b)^{*}+a\cdot(a+b)^{*}+b\cdot(a+b)^{*}$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1+(a+b)\cdot(a+b)^{*}+a\cdot(1\cdot(a+b)^{*})+b\cdot(1\cdot(a+b)^{*})$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1\cdot(a+b)^{*}+a\cdot(1\cdot(a+b)^{*})+b\cdot(1\cdot(a+b)^{*})$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{\equiv}}$}}1\cdot{L_{2}}({v_{\text{s}}})+a\cdot{L_{2}}({v_{11}})+b\cdot{L_{2}}({v_{21}})$

Note that the form of these two correctness conditions at $v_{1}$ arise from
the outgoing transitions from $v_{1}$ in $\underline{\mathcal{C}}$ in Figure
9: the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-transition
from $v_{1}$ to $v_{\text{s}}$, the ${a}$-transition from $v_{1}$ to $v_{11}$,
and the ${b}$-transition from $v_{1}$ to $v_{21}$.

The solution conditions for $L=\langle L_{1},\hskip 0.5ptL_{2}\rangle$ at the
vertices $v$ and $v_{2}$ can be verified analogously. At $v_{11}$ and at
$v_{21}$ the solution conditions follow by using the axiom
${\text{id}_{\text{l}}}({{\cdot}})$ of Mil-.

For the statement
$g^{*}\,{{\cdot}}\,0\mathrel{{\equiv}}(a+b)^{*}\,{{\cdot}}\,0\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}}}(a\,{{\cdot}}\,(a+b)+b)^{*}\,{{\cdot}}\,0\mathrel{{\equiv}}h^{*}\,{{\cdot}}\,0$,
we illustrated in Figure 2 the coinductive proof
$\mathcal{CP}=\langle{\underline{\mathcal{C}}}({h^{*}\,{{\cdot}}\,0}),\hskip
0.5ptL\rangle$ over Mil- with underlying guarded LLEE-witness ${\hskip
0.2pt\hat{\underline{\mathcal{C}}}}({h^{*}\,{{\cdot}}\,0})$, where
${\underline{\mathcal{C}}}({h^{*}\,{{\cdot}}\,0})$ and ${\hskip
0.2pt\hat{\underline{\mathcal{C}}}}({h^{*}\,{{\cdot}}\,0})$ is the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation as defined according to Definition 4.2, and the equation-
labeling function $L$ on ${\underline{\mathcal{C}}}({h^{*}\,{{\cdot}}\,0})$ is
defined as in the figure.

The correctness conditions at the start vertex (at the bottom) can be verified
as follows:

$\displaystyle g^{*}\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{\equiv}}$}}(a+b)^{*}\,{{\cdot}}\,0\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(1+(a+b)\,{{\cdot}}\,(a+b)^{*})\,{{\cdot}}\,0\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1\,{{\cdot}}\,0+((a+b)\,{{\cdot}}\,g^{*})\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}0+(a\,{{\cdot}}\,g^{*}+b\,{{\cdot}}\,g^{*})\,{{\cdot}}\,0\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(a\,{{\cdot}}\,g^{*}+b\,{{\cdot}}\,g^{*})\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(a\,{{\cdot}}\,g^{*})\,{{\cdot}}\,0+(b\,{{\cdot}}\,g^{*})\,{{\cdot}}\,0\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}a\,{{\cdot}}\,(g^{*}\,{{\cdot}}\,0)+b\,{{\cdot}}\,(g^{*}\,{{\cdot}}\,0)$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}a\,{{\cdot}}\,((1\,{{\cdot}}\,g^{*})\,{{\cdot}}\,0)+b\,{{\cdot}}\,((1\,{{\cdot}}\,g^{*})\,{{\cdot}}\,0)\hskip
1.5pt{,}$ $\displaystyle h^{*}\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{\equiv}}$}}(a\,{{\cdot}}\,(a+b)+b)^{*}\,{{\cdot}}\,0\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(1+(a\,{{\cdot}}\,(a+b)+b)\,{{\cdot}}\,(a\,{{\cdot}}\,(a+b)+b)^{*})\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}1\,{{\cdot}}\,0+((a\,{{\cdot}}\,(a+b)+b)\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}0+((a\,{{\cdot}}\,(a+b))\,{{\cdot}}\,h^{*}+b\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}(a\,{{\cdot}}\,((a+b)\,{{\cdot}}\,h^{*})+b\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}((a\,{{\cdot}}\,((a+b)\,{{\cdot}}\,h^{*}))\,{{\cdot}}\,0+(b\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}a\,{{\cdot}}\,((a+b)\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0)+b\,{{\cdot}}\,(h^{*}\,{{\cdot}}\,0)$
$\displaystyle{}\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}a\,{{\cdot}}\,((1\,{{\cdot}}\,(a+b))\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0)+b\,{{\cdot}}\,((1\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0)\hskip
1.5pt{.}$

From the provable equality for $g^{*}\,{{\cdot}}\,0$ the correctness condition
for $(1\,{{\cdot}}\,g^{*})\,{{\cdot}}\,0$ at the left upper vertex of
${\underline{\mathcal{C}}}({h^{*}\,{{\cdot}}\,0})$ can be obtained by
additional uses of the axiom (${\text{id}_{\text{l}}}({{\cdot}})$). The
correctness condition for
$((1\,{{\cdot}}\,(a+b))\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0$ at the left upper
vertex of ${\underline{\mathcal{C}}}({h^{*}\,{{\cdot}}\,0})$ can be verified
as follows:

$\displaystyle((1\,{{\cdot}}\,(a+b))\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}}((a+b)\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0\mathrel{\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}}(a\,{{\cdot}}\,h^{*}+b\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}}(a\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0+(b\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0\mathrel{\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}}a\,{{\cdot}}\,(h^{*}\,{{\cdot}}\,0)+b\,{{\cdot}}\,(h^{*}\,{{\cdot}}\,0)$
$\displaystyle{}\mathrel{\parbox{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}}a\,{{\cdot}}\,((1\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0)+b\,{{\cdot}}\,((1\,{{\cdot}}\,h^{*})\,{{\cdot}}\,0)\hskip
1.5pt{.}$

Finally, the correctness conditions at the right upper vertex of
${\underline{\mathcal{C}}}({h^{*}\,{{\cdot}}\,0})$ can be obtained by
applications of the axiom (${\text{id}_{\text{l}}}({{\cdot}})$) only.

As a direct consequence of Definition 8, the following lemma states that LLEE-
witnessed coinductive provability of an equation implies its coinductive
provability. The subsequent lemma states easy observations about the
composition of coinductive provability over a proof system ${\mathcal{S}}$
with provability ${=_{{\mathcal{S}}}\hskip 1.0pt}$ in ${\mathcal{S}}$.

######  Lemma 18.

$e_{1}\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}}}e_{2}$ implies
$e_{1}\mathrel{{\overset{\text{coind}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}}}e_{2}$,
for all $e_{1},e_{2}\in{\textit{StExp}}({\mathit{A}})$, where ${\mathcal{S}}$
is an $\mathcal{EL}$-based proof system over ${\textit{StExp}}({\mathit{A}})$
with $\text{\sf ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}$ that is sound with
respect to
$\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}$.

######  Lemma 19.

Let
${R}\in\bigl{\\{}{{\overset{\text{coind}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}},{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}}}\bigr{\\}}$ for some
$\mathcal{EL}$-based proof system ${\mathcal{S}}$ with $\text{\sf
ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}$. Then $\mathrel{{R}}$ is reflexive,
symmetric, and satisfies ${=_{{\mathcal{S}}}\hskip
1.0pt}\circ{R}\subseteq{R}$, ${R}\circ{=_{{\mathcal{S}}}\hskip
1.0pt}\subseteq{R}$, and ${=_{{\mathcal{S}}}\hskip 1.0pt}\subseteq{R}$.

The proposition below, and the subsequent remark are evidence for the fact,
mentioned at the start of this section, that coinductive proofs over proof
systems that are sound with respect to
${=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}$ derive semantically
valid conclusions themselves. Rather than formulating their statements for all
semantically sound proof systems, we restrict our attention to systems that
are theorem-subsumed by Mil.

######  Proposition 20.

Let ${\mathcal{S}}$ be an $\mathcal{EL}$-based proof system over
${\textit{StExp}}({\mathit{A}})$ with $\text{\sf
ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$.
Then for all $e_{1},e_{2}\in{\textit{StExp}}({\mathit{A}})$ it holds:

$e_{1}\mathrel{{\overset{\text{coind}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}}}e_{2}\;\;\Longrightarrow\;\;{\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}})\hskip 1.5pt{,}$ (8)

That is, if there is a coinductive proof over ${\mathcal{S}}$ of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$,
then the chart interpretations of $e_{1}$ and $e_{2}$ are bisimilar.

$\underline{\mathcal{C}}$${\mathcal{C}}({e_{1}})$${{{\mathcal{C}}({e_{1}})}/_{\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}}}$${{{\mathcal{C}}({e_{2}})}/_{\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}}}$${\mathcal{C}}({e_{2}})$LLEE, guarded(by Lem.
7)$\left[{L_{1}}\right]_{{=_{\text{\sf Mil}}\hskip
1.0pt}}$$\left[{L_{2}}\right]_{{=_{\text{\sf Mil}}\hskip 1.0pt}}$(by Lem.
7)$\left.\parbox{0.0pt}{{\large$\langle\underline{\mathcal{C}},\hskip
0.5ptL\rangle$\mbox{}} \\\ coinductive proof\mbox{} \\\ of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$\mbox{}
\\\ over ${\mathcal{S}}\mathrel{{\precsim}}\text{\sf
Mil}$\mbox{}}\right\\}$$\left\\{\;\begin{gathered}{\mathcal{C}}({e_{1}})\mathrel{\hbox{\kern
0.5167pt\vbox{\hbox{\raise
0.5167pt\hbox{\kern-0.5167pt{$\leftrightarrow$}\kern-0.5167pt}}\hrule}\kern
0.5167pt}\hskip 1.0pt}{\mathcal{C}}({e_{2}})\\\
e_{1}\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}e_{2}\end{gathered}\;\right.$(Prop.
10) Figure 10. Coinductive proofs over
${\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$ guarantee equality of
process semantics.

######  Proof 5.1.

We have illustrated the proof of this proposition in Figure 10: In every
coinductive proof $\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ over
${\mathcal{S}}$ with ${\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$ of an
equation
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$,
the star-expression functions $L_{1}$ and $L_{2}$ are Mil-provable solutions
of $\underline{\mathcal{C}}$. Then by using Proposition 10 and Lemma 7 we get
the link of functional
(${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-)bisimulations
between ${\mathcal{C}}({e_{1}})$ and ${\mathcal{C}}({e_{2}})$ as drawn in that
picture. Since (functional) bisimulations compose with (functional)
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
to
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations,
and
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
between charts are bisimulations, we obtain that
${\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}})$ holds, and consequently, that
$e_{1}\mathrel{{=_{\scriptscriptstyle\llbracket{\cdot}\rrbracket_{P}}}}e_{2}$
holds.

######  Remark 21.

For every coinductive proof
$\mathcal{CP}=\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$, whether
$\mathcal{CP}$ is LLEE-witnessed or not, over an $\mathcal{EL}$-based proof
system ${\mathcal{S}}$ with $\text{\sf
ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$
the finite relation defined by:

$B\,\mathrel{{:=}}\,\Bigl{\\{}{\displaystyle\Big{\langle}{\tau_{\underline{\mathcal{C}}}}({v})+\sum_{i=1}^{n}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}_{i}}\,{{\cdot}}\,{L_{1}}({v_{i}}),\,{\tau_{\underline{\mathcal{C}}}}({v})+\sum_{i=1}^{n}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}_{i}}\,{{\cdot}}\,{L_{2}}({v_{i}})\Big{\rangle}}\mathrel{\Big{|}}{\begin{gathered}{T_{\underline{\mathcal{C}}}}({v})=\bigl{\\{}{v\mathrel{{\xrightarrow{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\underline{a}}_{i}}}}}v_{i}}\mathrel{\big{|}}{i\in\left\\{{1,\ldots,n}\right\\}}\bigr{\\}},\\\\[-3.22916pt]
v\in{V}({\underline{\mathcal{C}}}),\,\text{the set of vertices of
$\underline{\mathcal{C}}$}\end{gathered}}\Bigr{\\}}$

is a
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulation
up to ${=_{{\mathcal{S}}}\hskip 1.0pt}$ with respect to the labeled transition
system on all star expressions that is defined by the TSS in Definition 2.
This can be shown by using that the left-hand sides ${L_{1}}({v})$, and
respectively the right-hand sides ${L_{2}}({v})$, of the equations ${L}({v})$
in $\mathcal{CP}$, for $v\in{V}({\underline{\mathcal{C}}})$, form
${\mathcal{S}}$-provable solutions of the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ that underlies $\mathcal{CP}$.

We now define two proof systems CLC and CC for combining LLEE-witnessed
coinductive provability. Each of these systems consists of a single rule
scheme, a more specific one for CLC, and a more liberal one for CC. Instances
of rules of these two schemes formalize LLEE-witnessed coinductive provability
in CLC, and respectively coinductive provability in CC, of equations between
star expressions from assumed equations. Different from the exposition in
[Gra21a, Gra21b], where we permitted entire coinductive proofs as formulas and
as premises of rules, we here keep the proof systems
${\textit{Eq}}({\mathit{A}})$-based by externalizing coinductive proofs from
the rules by ‘hiding’ them in side-conditions.222Keeping the systems equation-
based (by avoiding coinductive proofs as formulas as in [Gra21a, Gra21b])
permits us to then compare the coinductive proof systems CLC, CC, and later
cMil, and $\overline{\text{\sf cMil}}$ via rule derivability and admissibility
to Milner’s system Mil and its variants Mil′, and $\overline{\sf
Mil}{}^{\prime}$. The more restricted proof system CLC will form the core of
our coinductive reformulation of Milner’s system.

[proof systems CLC, CC for combining (LLEE-witn.) coinductive provability] Let
$\mathit{A}$ be a set of actions. We define
${\textit{Eq}}({\mathit{A}})$-based proof systems ${\text{\sf
CLC}}({\mathit{A}})$ and ${\text{\sf CC}}({\mathit{A}})$.

The _proof system ${\text{\sf CLC}}({\mathit{A}})$ for combining LLEE-
witnessed coinductive provability (over extensions of ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}({\mathit{A}})$) of equations between star
expressions over $\mathit{A}$_ is an ${\textit{Eq}}({\mathit{A}})$-based proof
system without _axioms_ , but with the _rules_ of the scheme:

$g_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1}$
…
$g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}$
LCoProofn (if (10) holds)
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
(9) $e\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}}}f$ for
$\Gamma=\left\\{{g_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1},\ldots,g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}}\right\\}$
with $n\in{\rm Nature}$ (including $n=0$). (10)

The _proof system ${\text{\sf CC}}({\mathit{A}})$ for combining coinductive
provability (over extensions of ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}({\mathit{A}})$)_ is an
${\textit{Eq}}({\mathit{A}})$-based proof system without _axioms_ , but with
the _rules_ of the scheme:

$g_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1}$
…
$g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}$
CoProofn (if (11) holds)
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
$e\mathrel{{\overset{\text{coind}}{=\joinrel=\joinrel=}_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}}}f$ for
$\Gamma=\left\\{{g_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1},\ldots,g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}}\right\\}$
with $n\in{\rm Nature}$ (including $n=0$). (11)

We will keep the set $\mathit{A}$ implicit, and write CLC and CC for
${\text{\sf CLC}}({\mathit{A}})$ and ${\text{\sf CC}}({\mathit{A}})$,
respectively.

Note that the systems CLC and CC do not contain the rules of $\mathcal{EL}$
nor any axioms. Instead, derivations in these systems have to start with
0-premise instances of LCoProof0 or CoProof0. Due to Lemma 18 every instance
of the rule LCoProofn of CLC for some $n\in{\rm Nature}$ is also an instance
of the rule CoProofn of CC. It follows that derivability of an equation
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
in CLC implies derivability of
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
in CC, that is, $\text{\sf CLC}\mathrel{{\precsim}}\text{\sf CC}$ holds, see
Lemma 23, (i), below.

Based on CLC, we now define the system that we call the coinductive variant
cMil of Milner’s proof system Mil. For this, we replace the fixed-point rule
in Mil by the rule scheme of CLC, or equivalently, by adding this rule scheme
to the purely equational part Mil- of Mil. By adding the rule scheme of CC to
Mil-, we also define an extension $\overline{\text{\sf cMil}}$ of cMil.

[proof systems cMil, cMil1, and $\overline{\text{\sf cMil}}$] Let $\mathit{A}$
be a set of actions.

The proof system ${\text{\sf cMil}}({\mathit{A}})$, the _coinductive variant
of ${\text{\sf Mil}}({\mathit{A}})$_, is an $\mathcal{EL}$-based proof system
whose _axioms_ are those of ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}({\mathit{A}})$, and whose _rules_ are those of
${\text{$\mathcal{EL}$}}({\mathit{A}})$, plus the _rule scheme_
$\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm Nature}}$ from
${\text{\sf CLC}}({\mathit{A}})$. By ${{\text{{\sf
cMil}${}_{1}$}}}({\mathit{A}})$ we mean _the simple coinductive variant of
${\text{\sf Mil}}({\mathit{A}})$_, an $\mathcal{EL}$-based proof system that
arises by only adding the rule LCoProof1 of ${\text{\sf CLC}}({\mathit{A}})$
to the rules and axioms of ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}({\mathit{A}})$.

By ${\text{$\overline{\text{\sf cMil}}$}}({\mathit{A}})$ we mean the variant
of ${\text{\sf cMil}}({\mathit{A}})$ in which the more general _rule scheme_
$\left\\{{\text{CoProof${}_{n}$}}\right\\}_{n\in{\rm Nature}}$ from
${\text{\sf CC}}({\mathit{A}})$ is used (instead of
$\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm Nature}}$ from
${\text{\sf CLC}}({\mathit{A}})$).

We again permit to write cMil, cMil1, $\overline{\text{\sf cMil}}$ for
${\text{\sf cMil}}({\mathit{A}})$, ${{\text{{\sf
cMil}${}_{1}$}}}({\mathit{A}})$, and ${\text{$\overline{\text{\sf
cMil}}$}}({\mathit{A}})$, respectively.

We now prove a lemma (Lemma 23 below) that gathers elementary theorem
equivalence and theorem subsumption statements between the coinductive
variants of Milner’s system defined above. For its proof we argue with
subsystem relationships as gathered by Lemma 22 below, and we explain basic
proof transformations between these systems.

######  Lemma 22.

The following subsystem relationships hold between the coinductive proof
systems defined above: [label=()]

$\text{\sf CLC}\mathrel{{\sqsubseteq}}\text{\sf cMil}$,

${\text{{\sf cMil}${}_{1}$}}\mathrel{{\sqsubseteq}}\text{\sf cMil}$,

$\text{\sf CC}\mathrel{{\sqsubseteq}}\text{$\overline{\text{\sf cMil}}$}$.

######  Lemma 23.

The following theorem subsumption and theorem equivalence statements hold:

  1. (i)

$\text{\sf CLC}\mathrel{{\precsim}}\text{\sf CC}$,

  2. (ii)

${\text{{\sf cMil}${}_{1}$}}\mathrel{{\precsim}}\text{\sf
cMil}\mathrel{{\precsim}}\text{$\overline{\text{\sf cMil}}$}$,

  3. (iii)

$\text{\sf CLC}\mathrel{\sim}\text{\sf cMil}$,

  4. (iv)

$\text{\sf CC}\mathrel{\sim}\text{$\overline{\text{\sf cMil}}$}$.

######  Proof 5.2.

We have argued for statement (i) above, below Definition 21: every instance of
the rule LCoProofn of CLC, for $n\in{\rm Nature}$, is also an instance of the
rule CoProofn of CC. This also implies the part $\text{\sf
cMil}\mathrel{{\precsim}}\text{$\overline{\text{\sf cMil}}$}$ of statement
(ii), because it shows in every derivation $\mathcal{D}$ of an equation
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
in cMil every instance of LCoProofn, for $n\in{\rm Nature}$, can be replaced
by an instance of CoProofn with as result a derivation $\mathcal{D}^{\prime}$
of
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
in $\overline{\text{\sf cMil}}$. The part ${\text{{\sf
cMil}${}_{1}$}}\mathrel{{\precsim}}\text{\sf cMil}$ of statement (ii) follows
from the fact that cMil1 is a subsystem of cMil by Lemma 22, 22.

For statement (iii), the theorem-subsumption part $\text{\sf
CLC}\mathrel{{\precsim}}\text{\sf cMil}$ follows from $\text{\sf
CLC}\mathrel{{\sqsubseteq}}\text{\sf cMil}$, see Lemma 22, 22. For showing the
converse implication, $\text{\sf CLC}\mathrel{{\succsim}}\text{\sf cMil}$, we
will demonstrate the proof-transformation statement (12) below by first
showing its special case (13):

$\displaystyle\left.\;\parbox{357.73517pt}{Every derivation $\mathcal{D}$ in
\text{\sf cMil}\ can be transformed into a derivation $\mathcal{D}^{\prime}$
in \text{\sf CLC}\ \\\ with the same conclusion.}\;\right\\}$ (12)
$\displaystyle\left.\;\parbox{357.73517pt}{The transformation statement
\eqref{eq:1:prf:it:3:lem:thmsubsumption:rels:coindproofsystems} holds for
every derivation $\mathcal{D}$ in \text{\sf cMil}\ with an instance of
$\text{LCoProof${}_{n}$}$, for some $n\in{\rm Nature}$, at the
bottom.}\;\right\\}$ (13)

The idea for both of these proof transformation statements is to ‘hide’
derivation parts that consist of axioms and rules in Mil- into the correctness
statements of coinductive proofs that appear as side-conditions in instances
of the coinductive rule in CLC. More precisely, the idea is to replace
derivation parts $\mathcal{D}_{0}$ in Mil- of a derivation $\mathcal{D}$ in
cMil, where $\mathcal{D}_{0}$ consists of the inference in Mil- of an equation
$g\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h$
from a set $\Gamma$ of $m$ assumption equations, by an instance of the
coinductive rule LCoProofm that has the $m$ assumptions of $\mathcal{D}_{0}$
in $\Gamma$ as its premises. Then whenever
$g\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h$
is needed to justify a correctness conditions it can be reconstructed from the
premises, provably in Mil-, on the basis of the derivation $\mathcal{D}_{0}$
in Mil-.

We start by showing (13), and proceed for this purpose by induction on the
depth $0pt{\mathcal{D}}$ of $\mathcal{D}$. Suppose that $\mathcal{D}$ is a
derivation in cMil with an occurrence of an instance $\iota$ of LCoProofn at
the bottom. To perform the induction step for $\mathcal{D}$, we need to
transform $\mathcal{D}$ into a derivation $\mathcal{D}^{\prime}$ in CLC with
the same conclusion. We may assume that the immediate subderivations
$\mathcal{D}_{1}$, …, $\mathcal{D}_{n}$ of $\mathcal{D}$ (just above the
instance $\iota$) contain axioms and/or rules of Mil-, because otherwise
$\mathcal{D}$ is already a derivation in CLC. To keep the illustration of the
transformation step simple, we assume that only the $i$-th subderivation
$\mathcal{D}_{i}$ contains axioms and/or rules of Mil; the general case will
become clear through this example. We assume that $\mathcal{D}$ is of the
form:

$\mathcal{D}_{1}$
$g_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1}$
$\mathcal{D}_{i1}$
$(g_{i1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i1})$
$\;\cdots\;$ $\mathcal{D}_{im}$
$(g_{im}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{im})$
$\mathcal{D}_{i0}$ $\ldots\hskip
12.91663ptg_{i}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i}\hskip
12.91663pt\ldots$ $\mathcal{D}_{n}$
$g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}$
LCoProofn
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
(14) $\displaystyle\text{with side-
con\\-di\\-tion}\;\;e\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}}}f\;\;\text{for
$\Gamma=\left\\{{g_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1},\ldots
g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}}\right\\}$$\hskip
1.5pt{,}$}$ (15)

where
$\mathcal{D}_{1},\ldots,\mathcal{D}_{i-1},\mathcal{D}_{i+1},\ldots\mathcal{D}_{n}$
are already derivations in CLC (with bottommost instances of
LCoProof${}_{n_{i}}$ that are suggested by dashed lines), but
$\mathcal{D}_{i}$ contains axioms and/or rule instances of Mil-, and can be
construed with a bottom part $\mathcal{D}_{i0}$ in Mil- below $m$ conclusions
$g_{i1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i1}$,
…,
$g_{im}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{im}$
of instances of coinductive rules from
$\left\\{{\text{LCoProof${}_{j}$}}\right\\}_{j\in{\rm Nature}}$.

Then we apply the induction hypothesis to the subderivations
$\mathcal{D}_{i1},\ldots,\mathcal{D}_{im}$ of $\mathcal{D}_{0}$, which is
possible due to
$0pt{\mathcal{D}_{i1}},\ldots,0pt{\mathcal{D}_{im}}<0pt{\mathcal{D}_{i}}<0pt{\mathcal{D}}$,
to obtain derivations
$\mathcal{D}^{\prime}_{i1},\ldots,\mathcal{D}^{\prime}_{im}$ in CLC with the
same conclusions
$g_{i1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i1}$,
…,
$g_{im}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{im}$,
respectively. Then we transform $\mathcal{D}$ by replacing the instance of
LCoProofn at the bottom by an instance of LCoProofn+m-1, keeping the first
$i-1$ and the last $n+1-i$ premises and their subderivations, but replacing
the $i$-th premise and its immediate subderivation $\mathcal{D}_{i}$ by $m$
additional premises with immediate subderivations $\mathcal{D}^{\prime}_{i1}$,
…, $\mathcal{D}^{\prime}_{im}$, thereby obtaining:

$\mathcal{D}_{1}$
$g_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1}$
$\;\;\ldots\;\;$ $\mathcal{D}^{\prime}_{i1}$
$\mathord{g_{i1}}\mathord{}$${}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i1}$
$\;\;\ldots\;\;$ $\mathcal{D}^{\prime}_{im}$
$\mathord{g_{im}}\mathord{}$${}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{im}$
$\;\;\ldots\;\;$ $\mathcal{D}_{n}$
$g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}$
LCoProofn+m-1
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
(16)

However, we need to show the side-condition for the displayed instance of
LCoProofn+m-1:

$e\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma^{\prime}}}}}f\;\;\text{with
}\begin{aligned}
&\Gamma^{\prime}=\bigl{\\{}g_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1},\ldots
g_{i-1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i-1},g_{i+1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i+1},\ldots,g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}\bigr{\\}}\cup\Delta\hskip
1.5pt{,}\\\ &\text{ where: }\Delta\mathrel{{:=}}\begin{aligned}
&\bigl{\\{}g_{i1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i1},\ldots
g_{im}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{im}\bigr{\\}}\\\\[-2.15277pt]
&\text{ the set of conclusions of
$\mathcal{D}^{\prime}_{i1},\ldots,\mathcal{D}^{\prime}_{im}$.}\end{aligned}\end{aligned}$
(17)

Now due to (15) there is a LLEE-witnessed coinductive proof $\mathcal{LCP}$ of
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
over ${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$. But now
$\mathcal{LCP}$ is also 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$
over ${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma^{\prime}}$, and
thus over a different set of premises, which we recognize as follows. The
equations in $\Delta$, which have been added to $\Gamma$ in order to get
$\Gamma^{\prime}$ after removing
$g_{i}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{i}$,
are derivable in ${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$ by
means for the derivation $\mathcal{D}_{0}$. Therefore the correctness
conditions for $\mathcal{LCP}$ as a LLEE-witnessed coinductive proof over
${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$ imply the
correctness conditions for $\mathcal{LCP}$ as a LLEE-witnessed coinductive
proof over ${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma^{\prime}}$.
This shows (17). Therefore the resulting derivation $\mathcal{D}^{\prime}$ in
(16) is a derivation in CLC with the same conclusion as $\mathcal{D}$. (This
transformation step can obviously be generalized to the situation in which not
just $\mathcal{D}_{i}$, but also others among the immediate subderivations
$\mathcal{D}_{1},\ldots,\mathcal{D}_{n}$ of $\mathcal{D}$ contain axioms
and/or rules of Mil-.) In this way we have performed the induction step.

Finally we establish (12) in full generality. For this we consider the
remaining situation in which the derivation $\mathcal{D}$ in cMil does not
terminate with an instance of a coinductive rule. Then $\mathcal{D}$ can be
construed with a part derivation $\mathcal{D}_{0}$ in Mil- above its
conclusion, and below $m\in{\rm Nature}$ subderivations $\mathcal{D}_{1}$, …,
$\mathcal{D}_{m}$, each of which terminates with a coinductive rule (see below
on the left). Note that $m=0$ is possible if $\mathcal{D}$ is a derivation in
Mil-. By applying (13) to $\mathcal{D}_{1},\ldots,\mathcal{D}_{m}$ we obtain
derivations $\mathcal{D}^{\prime}_{1},\ldots,\mathcal{D}^{\prime}_{m}$ in CLC
with the same conclusions, respectively. By combining these derivations in CLC
with an instance of LCoProofm we can perform the following transformation step
in order to obtain a derivation $\mathcal{D}^{\prime}$ in CLC :

$\displaystyle\mbox{ \ignorespaces\ignorespaces \ignorespaces
\ignorespaces\ignorespaces
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces
\ignorespaces\leavevmode\lower
72.76332pt\hbox{\vbox{\vbox{\hbox{\vbox{\hbox{\hskip 12.06146pt\hbox{\hskip
4.0pt\hbox{$\mathcal{D}_{1}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to42.56184pt{\xleaders\hbox to7.96677pt{\hss\vrule
width=3.98337pt,height=0.4pt,depth=0.0pt\hss}\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$(e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f_{1})$}\hskip
4.0pt}}}\hbox{$\ldots$}\vbox{\hbox{\hskip 13.1199pt\hbox{\hskip
4.0pt\hbox{$\mathcal{D}_{m}$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to46.79558pt{\xleaders\hbox to7.96677pt{\hss\vrule
width=3.98337pt,height=0.4pt,depth=0.0pt\hss}\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$(e_{m}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f_{m})$}\hskip
4.0pt}}}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip 1.0pt}}\lower-0.5pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 39.20926pt\hbox{\hbox{\hskip
4.0pt\hbox{$\mathcal{D}_{0}$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip
33.8367pt\lower-0.5pt\hbox{}\hbox{\vbox{\vskip
1.0pt}}\lower-0.5pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hskip
33.8367pt\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$}\hskip
4.0pt}}}}} \ignorespaces}\;\;\Longrightarrow\;\;\mbox{
\ignorespaces\ignorespaces\ignorespaces
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
49.38889pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 7.45627pt\hbox{\hskip
4.0pt\hbox{$\mathord{}\mathord{}$}\hbox{$\mathcal{D}^{\prime}_{1}$}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to34.78404pt{\xleaders\hbox to7.96677pt{\hss\vrule
width=3.98337pt,height=0.4pt,depth=0.0pt\hss}\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip
4.0pt\hbox{$\mathord{e_{1}}\mathord{}$}\hbox{${}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f_{1}$}\hskip
4.0pt}}\hbox{\hskip 4.30554pt}\hbox{\hskip 4.0pt\hbox{\ldots}\hskip
4.0pt}\hbox{\hskip 4.30554pt}\vbox{\hbox{\hskip 9.57314pt\hbox{\hskip
4.0pt\hbox{$\mathord{}\mathord{}$}\hbox{$\mathcal{D}^{\prime}_{m}$}\hskip
4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to39.01778pt{\xleaders\hbox to7.96677pt{\hss\vrule
width=3.98337pt,height=0.4pt,depth=0.0pt\hss}\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip
4.0pt\hbox{$\mathord{e_{m}}\mathord{}$}\hbox{${}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f_{m}$}\hskip
4.0pt}}}\vskip-1.875pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to97.9129pt{\xleaders\hrule\hfill}\lower
2.66945pt\hbox{\hskip
3.0pt$\text{LCoProof${}_{m}$}$}}\vskip-1.875pt\nointerlineskip\hbox{\hskip
34.36444pt\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$}\hskip
4.0pt}}}}} \ignorespaces}$ (18)

Here we need to establish the following side-condition for the instance of
LCoProofm at the bottom of $\mathcal{D}^{\prime}$:

$e\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}}}f\quad\text{where
}\Gamma\mathrel{{:=}}\left\\{{e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f_{1},\ldots,e_{m}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f_{m}}\right\\}\hskip
1.5pt{.}$ (19)

We can establish this coinductive-provability statement by recognizing that
$\langle{\underline{\mathcal{C}}}({e}),\hskip 0.5ptL\rangle$ with
${\underline{\mathcal{C}}}({e})$ the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
interpretation of $e$, and with equation labeling function:

$L\mathrel{:}{V}({{\underline{\mathcal{C}}}({e})})\to{\textit{StExp}}({\mathit{A}})\hskip
1.5pt{,}\;\;G\mapsto\begin{cases}G\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}G&\text{if
$G\mathrel{{\not\equiv}}e$}\\\\[-2.15277pt]
e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f&\text{if
$G\mathrel{{\equiv}}e$}\end{cases}$

is a LLEE-witnessed coinductive proof over ${\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$ of
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$.
To verify this statement, we use that ${\underline{\mathcal{C}}}({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
by Theorem 4.3, (i), and we have to check the correctness conditions for
$L_{1}$ and $L_{2}$ with $L=\langle L_{1},\hskip 0.5ptL_{2}\rangle$ to be
${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$-provable solutions
of ${\underline{\mathcal{C}}}({e})$. We first note that
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
is provable in ${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$ (i.e.
$e\mathrel{{=_{{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}\hskip
1.0pt}}f$) since $\mathcal{D}_{0}$ is a derivation of
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
in Mil- from the assumptions in $\Gamma$. Then we argue as follows:

  * •

The correctness conditions for $L_{1}$ to be a $({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})$-provable solution of
${\underline{\mathcal{C}}}({e})$ follow from the fact that $L_{1}$ is a Mil--
provable solution of ${\underline{\mathcal{C}}}({e})$ due to Lemma 17.

  * •

$L_{2}$ differs from $L_{1}$ only in the value for the start vertex $e$, where
${L_{2}}({e})\mathrel{{\equiv}}f$, but ${L_{1}}({e})\mathrel{{\equiv}}e$. From
this it follows, in view of $e\mathrel{{=_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}\hskip 1.0pt}}f$, that the correctness
conditions for $L_{1}$ imply the correctness conditions for $L_{2}$, because
they differ only up to expressions that are provably equal in
${\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}$ and also need to
hold up to $({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma})$-provability.

This argument shows (19), which justifies the side-condition of the instance
of LCoProofm at the bottom of the derivation $\mathcal{D}^{\prime}$ on the
right in (18). Therefore we have indeed obtained from $\mathcal{D}$ a
derivation in CLC with the same conclusion as $\mathcal{D}$. In this way we
have completed the proof of $\text{\sf cMil}\mathrel{{\precsim}}\text{\sf
CLC}$, the remaining part of (iii).

Statement (iv) can be shown entirely analogously as statement (iii).

######  Remark 24 (completeness of CC, $\overline{\text{\sf cMil}}$,
$\overline{\sf Mil}{}^{\prime}$).

The proof systems CC and $\overline{\text{\sf cMil}}$, as well as the variant
$\overline{\sf Mil}{}^{\prime}$ of Milner’s system with the general unique
solvability principle USP are complete for bisimilarity of star expressions.
This can be established along Salomaa’s completeness proof for his inference
system for language equality of regular expressions [Sal66], by an argument
that we can outline as follows. Given star expressions $e$ and $f$ with
${\mathcal{C}}({e})\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}}({f})$, $e$ and $f$ can be shown to be
principal values of Mil--provable solutions of ${\mathcal{C}}({e})$ and
${\mathcal{C}}({f})$, respectively (by a lemma for the chart interpretation
similar to Lemma 17). These solutions can be transferred to the
(${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-free)
product chart $\mathcal{C}$ of ${\mathcal{C}}({e})$ and ${\mathcal{C}}({f})$,
with $e$ and $f$ as principal values of Mil--provable solutions $L_{1}$ and
$L_{2}$ of $\mathcal{C}$, respectively. From this we obtain a (not necessarily
LLEE-witnessed) coinductive proof $\langle\mathcal{C},\hskip 0.5ptL\rangle$ of
$e=f$ over Mil-. It follows that $e=f$ is provable in CC, and in
$\overline{\text{\sf cMil}}$. Now since the correctness conditions for the Mil
--provable solutions $L_{1}$ and $L_{2}$ of $\mathcal{C}$ at each of the
vertices of $\mathcal{C}$ together form a guarded system of linear equations
to which the rule USP can be applied (as $\mathcal{C}$ is
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-free),
we obtain that
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
is also provable in $\overline{\sf Mil}{}^{\prime}$.

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

In this Section we develop a proof-theoretic interpretation of the coinductive
variant system cMil of Mil in Milner’s original system Mil. Since cMil and Mil
differ only by the coinductive rule scheme
$\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm Nature}}$ (which is part
of cMil, but not of Mil), and by the fixed-point rule $\textrm{RSP}^{*}$
(which is part of Mil, but not of cMil), the crucial step for this proof
transformation is to show that instances of LCoProofn, for $n\in{\rm Nature}$,
can be mimicked in Mil if their premise equations are derivable in Mil. We
will do so by showing that the rules LCoProofn, for $n\in{\rm Nature}$, are
correct for Mil. This implies that these rules are admissible in Mil (by Lemma
1), and also, that they can be eliminated from derivations in ${\text{\sf
Mil}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm Nature}}}$,
which is an extension of cMil. In this way we obtain the proof-theoretic
interpretation of cMil in Mil.

$\underline{\mathcal{C}}$${\mathcal{C}}({e_{1}})$${{{\mathcal{C}}({e_{1}})}/_{\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}}}$${{{\mathcal{C}}({e_{2}})}/_{\mathrel{{=_{\text{\sf
Mil}}\hskip
1.0pt}}}}$${\mathcal{C}}({e_{2}})$$\left[{L_{1}}\right]_{{=_{\text{\sf
Mil}}\hskip 1.0pt}}$$\left[{L_{2}}\right]_{{=_{\text{\sf Mil}}\hskip
1.0pt}}$$\left.\parbox{0.0pt}{{\large$\langle\underline{\mathcal{C}},\hskip
0.5ptL\rangle$\mbox{}} \\\
{\color[rgb]{0.13,0.55,0.13}\definecolor[named]{pgfstrokecolor}{rgb}{0.13,0.55,0.13}\text{LLEE}}-witnessed\mbox{}
\\\ coinductive proof\mbox{} \\\ of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$\mbox{}
\\\ over ${\mathcal{S}}\mathrel{{\precsim}}\text{\sf
Mil}$\mbox{}}\right\\}$LLEE, guarded$e_{1}\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}e_{2}$(Prop. 10) (Prop. 29, together
(with “$\Leftarrow$” in Prop. 10
(for ${\mathcal{S}}=\text{\sf Mil}$) Figure 11. Statement underlying the proof
transformation from cMil to Mil.

For proving correctness of LCoProofn for Mil, where $n\in{\rm Nature}$, we
will show that every LLEE-witnessed coinductive proof
$\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ over a proof system
${\mathcal{S}}$ that is theorem-subsumed by Mil of an equation
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$
can also be established by a proof of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$
in Milner’s system Mil. Informally, this statement is illustrated in Figure 11
by informally employing the characterization in Proposition 10 of the provable
solutions in such LLEE-witnessed coinductive proofs. We establish the
indicated informal second step in this section, where it will be guaranteed by