Proposition 29. In particular, our proof of this step will use the following
two statements:

  1. (SE)[SE]

_(solution extraction)_ from a LLEE-witness $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ of $\underline{\mathcal{C}}$ a Mil-
provable solution $s_{\underline{\mathcal{C}}}$ of $\underline{\mathcal{C}}$
can be extracted (Lemma 26), and

  2. (SU)[SU]

_(solution uniqueness)_ every Mil-provable solution 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{C}}$ (such as $L_{1}$ and $L_{2}$) is Mil-provably equal
to the solution $s_{\underline{\mathcal{C}}}$ extracted from $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ (Lemma 28).

By these statements we will obtain for every LLEE-witnessed coinductive proof
$\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ of
$e_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}e_{2}$,
assuming that $v_{\text{s}}$ is the star vertex of $\underline{\mathcal{C}}$
and hence ${L_{1}}({v_{\text{s}}})\mathrel{{\equiv}}e_{1}$ as well as
${L_{2}}({v_{\text{s}}})\mathrel{{\equiv}}e_{2}$ hold, that
$e_{1}\mathrel{{\equiv}}{L_{1}}({v_{\text{s}}})\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{\text{s}}})\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}{L_{2}}({v_{\text{s}}})\mathrel{{\equiv}}e_{2}$ holds, and
therefore $e_{1}\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}e_{2}$.

The proofs of the statements LABEL:SE and LABEL:SU below are adaptations to
LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
of proofs of analogous statements for LLEE-charts in Section 5 of [GF20a,
GF20b]. We have to, at places substantially, refine the extraction technique
of star expressions from process graphs with LLEE that was first described in
[GF20a, GF20b]. However, we will use the simplification to only reason about
guarded LLEE-witnesses, in which loop-entry transition are proper transitions.
We can do so because 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$ is
guaranteed to have a guarded LLEE-witness ${\hskip
0.2pt\hat{\underline{\mathcal{C}}}}({e})$ by Theorem 4.3.

For developing and proving the extraction statement LABEL:SE we use that the
hierarchical loop structure 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}}$ with LLEE-witness $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ facilitates the extraction of a Mil--
provable solution of $\underline{\mathcal{C}}$ (see Lemma 26). The reason is
as follows. The process behavior at every vertex $w$ in
$\underline{\mathcal{C}}$ can be split into an iteration part that is induced
via the loop-entry transitions from $w$ in $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ (which induce loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
with inner loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
whose behavior can be synthesized recursively), and an exit part that is
induced via the body transitions from $w$ in $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$. This intuition leads us to the definition
below. We define the ‘extraction function’ $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ from a ‘relative extraction function’
$t_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$, whose values ${t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip 0.5pt{v})$ capture the
behavior at $w$ in a loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
at $v$ until $v$ is reached.

[(relative) extraction function] 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 (guarded) LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
with guarded LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$.

The _extraction function $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}\mathrel{:}V\to{\textit{StExp}}({\mathit{A}})$
of $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$_ is defined from the _relative
extraction function $t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}\mathrel{:}\left\\{{\langle w,\hskip
0.5ptv\rangle}\mathrel{|}{w,v\in{V}({\underline{\mathcal{C}}}),\,w\mathrel{{{\curvearrowleft}^{=}}}v}\right\\}\to{\textit{StExp}}({\mathit{A}})$
of $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$_ for $w,v\in V$:

$\displaystyle{t_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})$ $\displaystyle{}\mathrel{{:=}}\begin{cases}1&\text{if
$w=v$,}\\\\[-2.15277pt]
{\displaystyle{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}}\mathrel{{\cdot}}{\displaystyle\Bigl{(}{\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}}\Bigr{)}}&\text{if $w\mathrel{{\curvearrowleft}}v$,}\end{cases}$
$\displaystyle{s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})$
$\displaystyle{}\mathrel{{:=}}{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}}\mathrel{{\cdot}}{\Bigl{(}{{\tau_{\underline{\mathcal{C}}}}({w})}+{\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}}\Bigr{)}}\hskip 1.5pt{,}$
$\displaystyle\text{provided: }{T_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})=\begin{aligned}
&\bigl{\\{}{w\mathrel{{\xrightarrow{a_{i}}}{{}_{{{\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}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}i}}]}}}}}w_{i}}\mathrel{\big{|}}{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}l}_{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}i}}\in{\rm
Nature}^{+},\,i\in\left\\{{1,\ldots,n}\right\\}}\bigr{\\}}{\cup}\bigl{\\{}{w\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{b}}_{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}}]}}}}}u_{i}}\mathrel{\big{|}}{i\in\left\\{{1,\ldots,m}\right\\}}\bigr{\\}}\text{,}\end{aligned}$
$\displaystyle\text{induction for $t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ on: }\begin{aligned} \langle w_{1},\hskip
0.5ptv_{1}\rangle\mathrel{{<}_{\text{lex}}}\langle w_{2},\hskip
0.5ptv_{2}\rangle\;\mathrel{:}\>\Longleftrightarrow\>v_{1}\mathrel{{{\curvearrowleft}^{+}}}v_{2}\mathrel{\vee}(\,v_{1}=v_{2}\mathrel{\wedge}w_{1}\mathrel{{\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}}w_{2}\,)\hskip
1.5pt{,}\end{aligned}$ $\displaystyle\text{induction for $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ on the strict partial order
${\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}$
(see Lemma\leavevmode\nobreak\ \ref{lem:descsteps:bodysteps:wf})}\hskip
1.5pt{,}$

where ${<}_{\text{lex}}$ is a well-founded strict partial order due to Lemma
13. The choice of the list representations of action-target sets of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ changes the definitions of these functions
only up to provability in ACI.

We exemplify the extraction process defined above by a concrete example.

$\begin{aligned} \scalebox{1.25}{ \leavevmode\hbox to100.06pt{\vbox
to114.3pt{\pgfpicture\makeatletter\hbox{\hskip 50.02911pt\lower-70.7996pt\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{ }
\par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.88954pt}{-34.00273pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
1.84999pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.25pt}{0.0pt}\pgfsys@curveto{1.25pt}{0.69035pt}{0.69035pt}{1.25pt}{0.0pt}{1.25pt}\pgfsys@curveto{-0.69035pt}{1.25pt}{-1.25pt}{0.69035pt}{-1.25pt}{0.0pt}\pgfsys@curveto{-1.25pt}{-0.69035pt}{-0.69035pt}{-1.25pt}{0.0pt}{-1.25pt}\pgfsys@curveto{0.69035pt}{-1.25pt}{1.25pt}{-0.69035pt}{1.25pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
1.84999pt\hfil&\hfil\hskip 21.33957pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 23.18956pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.25pt}{0.0pt}\pgfsys@curveto{1.25pt}{0.69035pt}{0.69035pt}{1.25pt}{0.0pt}{1.25pt}\pgfsys@curveto{-0.69035pt}{1.25pt}{-1.25pt}{0.69035pt}{-1.25pt}{0.0pt}\pgfsys@curveto{-1.25pt}{-0.69035pt}{-0.69035pt}{-1.25pt}{0.0pt}{-1.25pt}\pgfsys@curveto{0.69035pt}{-1.25pt}{1.25pt}{-0.69035pt}{1.25pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
1.84999pt\hfil\cr\vskip 28.45276pt\cr\hfil\hskip
1.84999pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.25pt}{0.0pt}\pgfsys@curveto{1.25pt}{0.69035pt}{0.69035pt}{1.25pt}{0.0pt}{1.25pt}\pgfsys@curveto{-0.69035pt}{1.25pt}{-1.25pt}{0.69035pt}{-1.25pt}{0.0pt}\pgfsys@curveto{-1.25pt}{-0.69035pt}{-0.69035pt}{-1.25pt}{0.0pt}{-1.25pt}\pgfsys@curveto{0.69035pt}{-1.25pt}{1.25pt}{-0.69035pt}{1.25pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
1.84999pt\hfil&\hfil\hskip 21.33957pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 23.18956pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.25pt}{0.0pt}\pgfsys@curveto{1.25pt}{0.69035pt}{0.69035pt}{1.25pt}{0.0pt}{1.25pt}\pgfsys@curveto{-0.69035pt}{1.25pt}{-1.25pt}{0.69035pt}{-1.25pt}{0.0pt}\pgfsys@curveto{-1.25pt}{-0.69035pt}{-0.69035pt}{-1.25pt}{0.0pt}{-1.25pt}\pgfsys@curveto{0.69035pt}{-1.25pt}{1.25pt}{-0.69035pt}{1.25pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
1.84999pt\hfil\cr\vskip 28.45276pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 23.18956pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\pgfsys@color@rgb@stroke{0.82}{0.41}{0.12}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.82}{0.41}{0.12}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.82,0.41,0.12}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\pgfsys@color@rgb@stroke{0.82}{0.41}{0.12}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.82}{0.41}{0.12}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.82,0.41,0.12}{}\pgfsys@moveto{1.25pt}{0.0pt}\pgfsys@curveto{1.25pt}{0.69035pt}{0.69035pt}{1.25pt}{0.0pt}{1.25pt}\pgfsys@curveto{-0.69035pt}{1.25pt}{-1.25pt}{0.69035pt}{-1.25pt}{0.0pt}\pgfsys@curveto{-1.25pt}{-0.69035pt}{-0.69035pt}{-1.25pt}{0.0pt}{-1.25pt}\pgfsys@curveto{0.69035pt}{-1.25pt}{1.25pt}{-0.69035pt}{1.25pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\pgfsys@color@rgb@stroke{0.82}{0.41}{0.12}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.82}{0.41}{0.12}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
1.84999pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}{{}{}}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.77779pt}{-64.66661pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\Large$\underline{\mathcal{C}}$, $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\par\par{{}}{}{{}{}}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-29.90225pt}{36.29045pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$v_{11}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}
{{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,1.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{-28.28955pt}{30.30275pt}\pgfsys@curveto{-49.62912pt}{30.30275pt}{-49.62912pt}{-1.84999pt}{-29.08954pt}{-1.84999pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-28.68954pt}{-1.84999pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par{{}}{}{{}{}}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-35.04413pt}{-10.08867pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$v_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.5,0,1}{}{}{}{}{{}}\pgfsys@moveto{-25.03955pt}{1.40001pt}\pgfsys@lineto{-25.03955pt}{26.25276pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-25.03955pt}{26.65276pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.39589pt}{5.8757pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}a}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-36.1386pt}{14.54181pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}
{{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,1.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{-25.03955pt}{-5.09999pt}\pgfsys@curveto{-25.03955pt}{-19.32637pt}{-17.47638pt}{-34.00273pt}{-6.04999pt}{-34.00273pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.65pt}{-34.00273pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{-22.3047pt}{-0.09413pt}\pgfsys@lineto{21.96812pt}{28.3308pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.84149}{0.54027}{-0.54027}{0.84149}{22.13641pt}{28.43884pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14583pt}{17.75938pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\par{{}}{}{{}{}}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.17685pt}{36.29045pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$v_{21}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}
{{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,1.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{28.28955pt}{30.30275pt}\pgfsys@curveto{49.62912pt}{30.30275pt}{49.62912pt}{-1.84999pt}{29.08954pt}{-1.84999pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{28.68954pt}{-1.84999pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par{{}}{}{{}{}}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.55003pt}{-10.08867pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$v_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.5,0,1}{}{}{}{}{{}}\pgfsys@moveto{25.03955pt}{1.40001pt}\pgfsys@lineto{25.03955pt}{26.25276pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{25.03955pt}{26.65276pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{26.6386pt}{4.68819pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}b}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{26.6386pt}{14.54181pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}
{{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,1.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{25.03955pt}{-5.09999pt}\pgfsys@curveto{25.03955pt}{-19.32637pt}{17.47638pt}{-34.00273pt}{6.04999pt}{-34.00273pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{5.65pt}{-34.00273pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par\par{{}}{}
{{}{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\pgfsys@color@rgb@stroke{0.82}{0.41}{0.12}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.82}{0.41}{0.12}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.82,0.41,0.12}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-45.01273pt}\pgfsys@lineto{0.0pt}{-49.65175pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{0.0pt}{-45.01273pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\pgfsys@color@rgb@stroke{0.82}{0.41}{0.12}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.82}{0.41}{0.12}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.82,0.41,0.12}{}\pgfsys@moveto{0.0pt}{-34.00273pt}\pgfsys@moveto{3.41434pt}{-34.00273pt}\pgfsys@curveto{3.41434pt}{-32.11703pt}{1.8857pt}{-30.5884pt}{0.0pt}{-30.5884pt}\pgfsys@curveto{-1.8857pt}{-30.5884pt}{-3.41434pt}{-32.11703pt}{-3.41434pt}{-34.00273pt}\pgfsys@curveto{-3.41434pt}{-35.88843pt}{-1.8857pt}{-37.41707pt}{0.0pt}{-37.41707pt}\pgfsys@curveto{1.8857pt}{-37.41707pt}{3.41434pt}{-35.88843pt}{3.41434pt}{-34.00273pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-34.00273pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}{}}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.77649pt}{-43.93355pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small$v_{\text{s}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{{{}{}}}{{}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.5,0,1}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-1.90498pt}{-29.1105pt}\pgfsys@lineto{-21.76328pt}{21.88884pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.36285}{0.93185}{-0.93185}{-0.36285}{-21.9084pt}{22.26157pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-15.70078pt}{-11.94223pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}a}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.65248pt}{-8.9252pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{{{}{}}}{{}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.5,0,1}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{1.90498pt}{-29.1105pt}\pgfsys@lineto{21.76328pt}{21.88884pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.36285}{0.93185}{-0.93185}{0.36285}{21.9084pt}{22.26157pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.6548pt}{-13.12975pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}b}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.68896pt}{2.7252pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\par
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\end{aligned}\hskip
4.30554pt\begin{aligned} {t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{21}},\hskip
0.5pt{v_{2}})&\;\parbox[t]{0.0pt}{$\mathrel{{:=}}$}\,{{0^{*}}}\mathrel{{\cdot}}{({1}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{2}},\hskip
0.5pt{v_{2}})})}\,\mathrel{{\equiv}}\,{{0^{*}}}\mathrel{{\cdot}}{({1}\mathrel{{\cdot}}{1})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}\,1\\\\[-0.43057pt] {t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{2}},\hskip
0.5pt{v_{\text{s}}})&\;\parbox[t]{0.0pt}{$\mathrel{{:=}}$}\,{{({b}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{21}},\hskip
0.5pt{v_{2}})})^{*}}}\mathrel{{\cdot}}{({1}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{\text{s}}},\hskip
0.5pt{v_{\text{s}}})})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}\,{b^{*}}\\\\[-0.43057pt] {t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{21}},\hskip
0.5pt{v_{\text{s}}})&\;\parbox[t]{0.0pt}{$\mathrel{{:=}}$}\,{{0^{*}}}\mathrel{{\cdot}}{({1}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{2}},\hskip
0.5pt{v_{\text{s}}})})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}\,{1}\mathrel{{\cdot}}{{b^{*}}}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}\,{b^{*}}\\\\[-0.43057pt] {t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{11}},\hskip
0.5pt{v_{1}})&\;\parbox[t]{0.0pt}{$\mathrel{{:=}}$}\,{{0^{*}}}\mathrel{{\cdot}}{({1}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{1}},\hskip
0.5pt{v_{1}})})}\,\mathrel{{\equiv}}\,{{0^{*}}}\mathrel{{\cdot}}{({1}\mathrel{{\cdot}}{1})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}\,1\\\\[-0.43057pt] {t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{1}},\hskip
0.5pt{v_{\text{s}}})&\;\parbox[t]{0.0pt}{$\mathrel{{:=}}$}\,{{({a}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{11}},\hskip
0.5pt{v_{\text{s}}})})^{*}}}\mathrel{{\cdot}}{({{b}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{21}},\hskip
0.5pt{v_{\text{s}}})}}+{{1}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{\text{s}}},\hskip
0.5pt{v_{\text{s}}})}})}\\\\[-2.15277pt]
&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\,{{a^{*}}}\mathrel{{\cdot}}{({{b}\mathrel{{\cdot}}{{b^{*}}}}+{1})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}\,{{a^{*}}}\mathrel{{\cdot}}{{b^{*}}}\\\\[-0.43057pt] {t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{11}},\hskip
0.5pt{v_{\text{s}}})&\;\parbox[t]{0.0pt}{$\mathrel{{:=}}$}\,{{0^{*}}}\mathrel{{\cdot}}{({1}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{1}},\hskip
0.5pt{v_{\text{s}}})})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}\,{{a^{*}}}\mathrel{{\cdot}}{{b^{*}}}\\\\[-0.43057pt] {s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{\text{s}}})&\;\parbox[t]{0.0pt}{$\mathrel{{:=}}$}\,{{({{a}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{11}},\hskip
0.5pt{v_{\text{s}}})}}+{{b}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{21}},\hskip
0.5pt{v_{\text{s}}})}})^{*}}}\mathrel{{\cdot}}{1}\\\\[-2.15277pt]
&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\,{({{a}\mathrel{{\cdot}}{({{a^{*}}}\mathrel{{\cdot}}{{b^{*}}})}}+{{b}\mathrel{{\cdot}}{{b^{*}}}})^{*}}\end{aligned}$
Figure 12. Extraction of the principal value of a Mil--provable solution
$s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ from the LLEE-witness $\hskip
0.75pt\hat{\mathcal{C}}$ in the coinductive proof in Example 5, with Mil--
provable simplifications.

We consider the
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$, and the LLEE-witness $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ of $\underline{\mathcal{C}}$, in the LLEE-
witnessed coinductive proof
$\mathcal{CP}=\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ 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})^{*}}$
in Example 5. We detail in Figure 12 the process of computing the principal
value ${s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({v_{\text{s}}})$ of the
extraction function $s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$. The statement of Lemma 26 below will
guarantee that $s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ is a Mil--
provable solution of $\underline{\mathcal{C}}$.

In order to show that the extraction function of a guarded 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}}$ defines a Mil--provable solution of
$\underline{\mathcal{C}}$, see Lemma 26 and its proof later, we first have to
establish a Mil--provable connection between the relative extraction function
and the extraction function of a guarded LLEE-witness. For this we prove the
following lemma.

######  Lemma 25.

Let $\underline{\mathcal{C}}$ be a (guarded) LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
with guarded LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$. Then
${s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v})}$ holds for all vertices
$w,v\in{V}({\underline{\mathcal{C}}})$ such that
$w\mathrel{{{\curvearrowleft}^{=}}}v$.

######  Proof 6.1.

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 LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
with guarded LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$.

We have to show that  ${s}({w})\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ holds for all $w,v\in V$ with
$w\mathrel{{{\curvearrowleft}^{=}}}v$. We first notice that this statement
holds obviously for $w=v$, due ${t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})\mathrel{{\equiv}}{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v},\hskip 0.5pt{v})\mathrel{{\equiv}}1$,
and the presence of the axiom $({\text{id}_{\text{l}}}({{\cdot}}))$ in Mil-.
Therefore it suffices to show, by also using this fact, that
${s}({w})\mathrel{{=_{\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}{{t_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ holds for all $w,v\in V$ with
$w\mathrel{{\curvearrowleft}}v$. We will show this by using the same induction
as for the definition of the relative extraction function $t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ in Definition 11, that is, by complete
induction on the (converse) lexicographic partial order ${<}_{\text{lex}}$ of
${{\curvearrowleft}^{+}}$ and
${\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}$
on $V\times V$ defined by: $\langle w_{1},\hskip
0.5ptv_{1}\rangle\mathrel{{<}_{\text{lex}}}\langle w_{2},\hskip
0.5ptv_{2}\rangle\;\mathrel{:}\>\Longleftrightarrow\>v_{1}\mathrel{{{\curvearrowleft}^{+}}}v_{2}\mathrel{\vee}(\,v_{1}=v_{2}\mathrel{\wedge}w_{1}\mathrel{{\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}}w_{2}\,)$,
which is well-founded by Lemma 13. For our argument we assume to have given,
underlying the definition of the relative extraction function $t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ and the extraction function $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$, list representations ${T_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ of the transitions from $w$ in
$\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ as in Definition 11, for all $w\in
V$.

In order to carry out the induction step, we let $w,v\in V$ be arbitrary, but
such that $w\mathrel{{\curvearrowleft}}v$. On the basis of the form of
${T_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ as in Definition 11 we
argue as follows, starting with a step in which we use the definition of
$s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$, and followed by a second step
in which we use that
${\tau_{\underline{\mathcal{C}}}}({w})\mathrel{{\equiv}}0$ holds, because $w$
cannot have immediate termination as due to $w\mathrel{{\curvearrowleft}}v$ it
is in the body of the loop at $v$ (cf. condition (L3) for loop
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
in Section 4):

$\displaystyle{s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}\mathrel{{\cdot}}{\Bigr{(}{\Bigr{(}\displaystyle\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigl{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigl{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}\mathrel{{\cdot}}{\Bigr{(}{\Bigr{(}\displaystyle\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigl{)}}+{0}\Bigl{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\>\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}\mathrel{{\cdot}}{\Bigr{(}\displaystyle\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigl{)}}$ (by axiom
$({\text{neutr}}({+}))$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}\mathrel{{\cdot}}{\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{({t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v}))}}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\Bigl{(}\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}\mathrel{{\cdot}}{{\Bigr{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\Bigl{)}\Bigr{)}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v})}}$ (by axioms
$({\text{r-distr}}({+,{\cdot}}))$, and $({\text{assoc}}({{\cdot}}))$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v})}$ (by
$w\mathrel{{\curvearrowleft}}v$, and the definition of ${t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip 0.5pt{v})$ in Def. 11)

We note that this reasoning also applies for the special cases $n=0$, and with
a slight change also for $m=0$, where
$\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\mathrel{{\equiv}}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{({t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v}))}}\mathrel{{\equiv}}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\mathrel{{\equiv}}0$, and then an axiom (deadlock) has to be used.
In this way we have shown, due to $\text{\sf
ACI}\mathrel{{\sqsubseteq}}\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}$, the
desired Mil--provable equality ${s}({w})\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ for the vertices $v$ and $w$ that we
picked with the property $w\mathrel{{\curvearrowleft}}v$.

Since $w,v\in V$ with $w\mathrel{{\curvearrowleft}}v$ were arbitrary above, we
have successfully carried out the proof by induction that  ${s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s_{\underline{\mathcal{C}}}}({v})}$ holds for all
$w,v\in V$ with $w\mathrel{{\curvearrowleft}}v$. As we have argued that the
statement also holds for $w=v$, we have proved the lemma.

######  Lemma 26 (extracted function is provable solution).

Let $\underline{\mathcal{C}}$ be a LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
with guarded LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$. Then
the extraction function $s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ of
$\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ is a Mil--provable solution of
$\underline{\mathcal{C}}$.

######  Proof 6.2.

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 (guarded) LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
with guarded LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$.

We show that the extraction function $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ is a Mil--provable solution of
$\underline{\mathcal{C}}$ by verifying the Mil--provable correctness
conditions for $s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ at every vertex
$w\in V$. For the argument we assume to have given, underlying the definition
of the relative extraction function $t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ and the extraction function $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$, list representations ${T_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ of the transitions from $w$ in
$\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ as written in Definition 11, for
all vertices $w\in V$.

We let $w\in V$ be arbitrary. Starting from the definition of $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ in Definition 11 on the basis of the form
of ${T_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})$, we argue by the
following steps:

$\displaystyle{s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\>\mathrel{{\equiv}}\>$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}\mathrel{{\cdot}}{\>\Bigr{(}\displaystyle{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigl{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\Bigl{(}{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}}+{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}}\mathrel{{\cdot}}{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}}\Bigr{)}}\mathrel{{\cdot}}{\Bigr{(}\displaystyle{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigl{)}}$
(by axiom $({\text{rec}}({{}^{*}}))$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}$}\>\begin{aligned}
&\Bigr{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigl{)}\\\\[-4.30554pt]
&{}+{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}}\mathrel{{\cdot}}{{\Bigl{(}\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{*}}\mathrel{{\cdot}}{\Bigl{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigr{)}}\Bigr{)}}}\end{aligned}$
(by axioms $({\text{r-distr}}({+,{\cdot}}))$,
$({\text{id}_{\text{l}}}({{\cdot}}))$, and $({\text{assoc}}({{\cdot}}))$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{\Bigr{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigl{)}}+{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})}}$ (by definition of ${s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ in Def. 11)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{\bigl{(}{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})\bigr{)}}}\Bigr{)}}+{\Bigr{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigl{)}}$
(by axioms $({\text{comm}}({+}))$, $({\text{r-distr}}({+,{\cdot}}))$, and
$({\text{assoc}}({{\cdot}}))$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}})}\Bigr{)}}+{{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf ACI}}\hskip
1.0pt}}$}\>{{\tau_{\underline{\mathcal{C}}}}({w})}+{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}})}\Bigr{)}}+{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}}\hskip 1.5pt{.}$

Since $\text{\sf ACI}\mathrel{{\sqsubseteq}}\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}$, this chain of equalities yields a Mil--provable
equality that establishes, in view of ${T_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ as in Definition 11, the
correctness condition for $s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ to
be a Mil--provable solution at the vertex $w$ that we picked.

Since $w\in V$ was arbitrary, we have established that the extraction function
$s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ is a Mil--provable solution of
$\underline{\mathcal{C}}$.

For showing the solution uniqueness statement LABEL:SU we can also use the
hierarchical loop structure 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}}$ with LLEE-witness $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ for carrying out proofs by induction. We
repurpose the two-step approach of the proof of Lemma 26 that used the Mil-
provable relationship between the extraction function $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ and the relative extraction function
$t_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ in Lemma 25. In doing so we first
establish, for every Mil-provable solution $s$ of $\underline{\mathcal{C}}$, a
connection with the relative extraction function $t_{\underline{\mathcal{C}}}$
of $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$, see Lemma 27 below. The proof
of this lemma proceeds by an induction that starts at innermost loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
of the given LLEE-witness, and then progresses to outer loop
sub-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts.
Different from Lemma 25, it will be crucial here to employ the fixed-point
rule $\textrm{RSP}^{*}$ of Mil in the proof.

######  Lemma 27.

Let $\underline{\mathcal{C}}$ be a LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
with guarded LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$.
Furthermore, let ${\mathcal{S}}$ be an
${\text{$\mathcal{EL}$}}({\mathit{A}})$-based proof system such that
$\text{\sf
ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$.

Let
$s\mathrel{:}{V}({\underline{\mathcal{C}}})\to{\textit{StExp}}({\mathit{A}})$
be an ${\mathcal{S}}$-provable solution of $\underline{\mathcal{C}}$. Then
${s}({w})\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ holds for all vertices
$w,v\in{V}({\underline{\mathcal{C}}})$ with
$w\mathrel{{{\curvearrowleft}^{=}}}v$.

######  Proof 6.3.

Let $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ be a guarded LLEE-witness of a
(guarded) LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}=\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 $s\mathrel{:}V\to{\textit{StExp}}({\mathit{A}})$ be an
${\mathcal{S}}$-provable solution of $\underline{\mathcal{C}}$.

We have to show that  ${s}({w})\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}{{t_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ holds for all $w,v\in V$ with
$w\mathrel{{{\curvearrowleft}^{=}}}v$. We first notice that this statement
holds obviously for $w=v$, due ${t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})\mathrel{{\equiv}}{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v},\hskip 0.5pt{v})\mathrel{{\equiv}}1$.
Therefore it suffices to show, by also using this fact, that
${s}({w})\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ holds for all $w,v\in V$ with
$w\mathrel{{\curvearrowleft}}v$. We will show this by using the same induction
as for the definition of the relative extraction function in Definition 11,
that is, by complete induction on the (converse) lexicographic partial order
${<}_{\text{lex}}$ of ${{\curvearrowleft}^{+}}$ and
${\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}$
on $V\times V$ defined by: $\langle w_{1},\hskip
0.5ptv_{1}\rangle\mathrel{{<}_{\text{lex}}}\langle w_{2},\hskip
0.5ptv_{2}\rangle\;\mathrel{:}\>\Longleftrightarrow\>v_{1}\mathrel{{{\curvearrowleft}^{+}}}v_{2}\mathrel{\vee}(\,v_{1}=v_{2}\mathrel{\wedge}w_{1}\mathrel{{\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}}w_{2}\,)$,
which is well-founded due to Lemma 13. For our argument we suppose to have
given, underlying the definition of the relative extraction function
$t_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ and the extraction function
$s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$, list representations
${T_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ of the transitions from
$w$ in $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ as written in Definition
11, for all $w\in V$.

In order to carry out the induction step, we let $w,v\in V$ be arbitrary such
that $w\mathrel{{\curvearrowleft}}v$. On the basis of the form of ${T_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ as in Definition 11 we argue as
follows, starting with a step in which we use that $s$ is an
${\mathcal{S}}$-provable solution of $\underline{\mathcal{C}}$, and followed
by a second step in which we use that
${\tau_{\underline{\mathcal{C}}}}({w})\mathrel{{\equiv}}0$ holds, because $w$
cannot have immediate termination as due to $w\mathrel{{\curvearrowleft}}v$ it
is in the body of the loop at $v$ (see condition (L3) for loop
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
in Section 4):

$\displaystyle{s}({w})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{{\mathcal{S}}}\hskip
1.0pt}}$}\>{{\tau_{\underline{\mathcal{C}}}}({w})}+{{\Bigl{(}\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{s}({w_{i}})}\Bigr{)}}+{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s}({u_{i}})}\Bigr{)}\Bigr{)}}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{s}({w_{i}})}\Bigr{)}}+{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s}({u_{i}})}\Bigr{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{\bigl{(}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\mathrel{{\cdot}}{{s}({w})}\bigr{)}}\Bigr{)}}+{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s}({u_{i}})}\Bigr{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{\bigl{(}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\mathrel{{\cdot}}{{s}({w})}\bigr{)}}\Bigr{)}}+{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{\bigl{(}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}\bigr{)}}\Bigr{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}}\mathrel{{\cdot}}{{s}({w})}}+{{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\Bigr{)}}\mathrel{{\cdot}}{{s}({v})}}$ (by axioms
$({\text{assoc}}({{\cdot}}))$, and $({\text{r-distr}}({+,{\cdot}}))$).

We note that these equalities also hold for the special cases in which $n=0$
or/and $m=0$, where in the case $m=0$ an axiom (deadlock) needs to be used in
the last step. Since $\text{\sf
ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$,
and $\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}\mathrel{{\sqsubseteq}}\text{\sf Mil}$, we have
obtained the following provable equality:

$\displaystyle{s}({w})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\>{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}}\mathrel{{\cdot}}{{s}({w})}}+{{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\Bigr{)}}\mathrel{{\cdot}}{{s}({v})}}\hskip 1.5pt{,}$

Since ${\bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\bigr{)}}{\ndownarrow}$ holds, we can apply $\textrm{RSP}^{*}$ in
order to obtain, and reason further:

$\displaystyle{s}({w})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\>{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{\\!*}\\!}}\mathrel{{\cdot}}{\\!\Bigl{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\Bigr{)}}\mathrel{{\cdot}}{{s}({v})}\Bigr{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{\Bigl{(}{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{\\!*}\\!}\mathrel{{\cdot}}{\\!\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}},\hskip
0.5pt{v})}\Bigr{)}}\Bigr{)}}\mathrel{{\cdot}}{{s}({v})}$ (by axiom
$({\text{assoc}}({{\cdot}}))$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ (by $w\mathrel{{\curvearrowleft}}v$,
and the definition of ${t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip 0.5pt{v})$ in Def. 11)

In this way we have shown, due to $\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}\mathrel{{\sqsubseteq}}\text{\sf Mil}$, the desired
Mil-provable equality ${s}({w})\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}{{t_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ for the vertices $v$ and $w$ that we
picked with the property $w\mathrel{{\curvearrowleft}}v$.

Since $w,v\in V$ with $w\mathrel{{\curvearrowleft}}v$ were arbitrary for this
argument, we have successfully carried out the proof by induction
${s}({w})\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w},\hskip
0.5pt{v})}\mathrel{{\cdot}}{{s}({v})}$ holds for all $w,v\in V$ with
$w\mathrel{{\curvearrowleft}}v$. As we have argued that the statement also
holds for $w=v$, we have proved the lemma.

For an ${\textit{Eq}}({\mathit{A}})$-based proof system ${\mathcal{S}}$ we say
that two star expression functions
$s_{1},s_{2}\mathrel{:}V\to{\textit{StExp}}({\mathit{A}})$ are
_${\mathcal{S}}$ -provably equal_ if
${s_{1}}({v})\mathrel{{=_{{\mathcal{S}}}\hskip 1.0pt}}{s_{2}}({v})$ holds for
all $v\in V$.

Now we use the relationship of arbitrary Mil-provable solutions of a guarded
LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ with the relative
extraction function $s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$ as stated by Lemma 13 in order to
demonstrate the solution uniqueness statement (SU). The proof can be viewed as
proceeding on the maximal length of body transition paths from vertices $v$,
where for descents from $v$ via a loop-entry transition into an inner loop the
statement of Lemma 27 is used. Again the use of the fixed-point rule
$\textrm{RSP}^{*}$ of Mil- is crucial, because any two Mil--provable solutions
of a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
cannot be expected to be Mil--provably equal in general.333As a simple
example, the use of $\textrm{RSP}^{*}$ is necessary for proving equal in Mil
the two Mil--provable solutions of the guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
${\underline{\mathcal{C}}}({(a\cdot a)^{*}\cdot 0})$ with the principal values
$a^{*}\cdot 0$ and $(a\cdot a)^{*}\cdot 0$, respectively.

######  Lemma 28 (provable equality of solutions of LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts).

Let $\underline{\mathcal{C}}$ be a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart,
and let ${\mathcal{S}}$ be an $\mathcal{EL}$-based proof system over
${\textit{StExp}}({\mathit{A}})$ such that $\text{\sf
ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$.

Then any two ${\mathcal{S}}$-provable solutions of $\underline{\mathcal{C}}$
are Mil-provably equal.

######  Proof 6.4.

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 LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
with guarded LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$, and let
${\mathcal{S}}$ an $\mathcal{EL}$-based proof system as assumed in the lemma.
In order to show that any two ${\mathcal{S}}$-provable solutions of
$\underline{\mathcal{C}}$ are Mil-provably equal, it suffices to show that
every ${\mathcal{S}}$-provable solution of $\underline{\mathcal{C}}$ is Mil-
provably equal to the extraction function $s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}$ of $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$.

For demonstrating this, let $s\mathrel{:}V\to{\textit{StExp}}({\mathit{A}})$
be an ${\mathcal{S}}$-provable solution of $\underline{\mathcal{C}}$. We have
to show that ${s}({w})\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ holds for all $w\in V$. We proceed
by complete induction on the well-founded relation
${\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}^{+}}$
(see Lemma 13, 2), which does not require us to treat base cases separately.
For our argument we assume to have given, underlying the definition of the
relative extraction function $t_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$
and the extraction function $s_{\underline{\mathcal{C}}}$, list
representations ${T_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ of the
transitions from $w$ in $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ as written
in Definition 11, for all $w\in V$.

Let $w\in V$ be arbitrary. On the basis of ${T_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ as in Definition 11 we argue as
follows, starting with a step in which we use that $s$ is an
${\mathcal{S}}$-provable solution of $\underline{\mathcal{C}}$ in view of the
assumed form of ${T_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})\,$:

$\displaystyle{s}({w})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{{\mathcal{S}}}\hskip
1.0pt}}$}\>{{\tau_{\underline{\mathcal{C}}}}({w})}+{\Bigl{(}{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{s}({w_{i}})}\Bigr{)}}+{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s}({u_{i}})}\Bigr{)}}\Bigr{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf ACI}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{s}({w_{i}})}\Bigr{)}}+{\Bigl{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})\Bigr{)}}\Bigr{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{({{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\mathrel{{\cdot}}{{s}({w})})}\Bigr{)}}+{\Bigl{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigr{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\>\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\>{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}}\mathrel{{\cdot}}{{s}({w})}}+{\Bigl{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigr{)}}$
(by axioms $({\text{assoc}}({{\cdot}}))$ and
$({\text{r-distr}}({+,{\cdot}}))$)
$\displaystyle\;\,\parbox[t]{0.0pt}{$\>\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\>{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}}\mathrel{{\cdot}}{{s}({w})}}+{\Bigl{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigr{)}}$
Since $\text{\sf
ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$,
and $\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}\mathrel{{\sqsubseteq}}\text{\sf Mil}$, we have
obtained the following provable equality: $\displaystyle{s}({w})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\>{{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}}\mathrel{{\cdot}}{{s}({w})}}+{\Bigl{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigr{)}}$

Now since ${\bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\bigr{)}}{\ndownarrow}$ holds, we can apply the rule
$\textrm{RSP}^{*}$ to this in order to obtain:

$\displaystyle{s}({w})$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\>\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\>{\Bigl{(}\sum_{i=1}^{n}{a_{i}}\mathrel{{\cdot}}{{t_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w_{i}},\hskip
0.5pt{w})}\Bigr{)}^{\\!*}\\!}\mathrel{{\cdot}}{\Bigl{(}{\Bigl{(}\sum_{i=1}^{m}{{\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{b}}_{i}}}\mathrel{{\cdot}}{{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({u_{i}})}\Bigr{)}}+{{\tau_{\underline{\mathcal{C}}}}({w})}\Bigr{)}}$
$\displaystyle\;\,\parbox[t]{0.0pt}{$\mathrel{{\equiv}}$}\>{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})\;\,\parbox[t]{0.0pt}{\mbox{}}\>\text{(by
the definition of $s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ in
Definition\leavevmode\nobreak\ \ref{def:extrsoluntil:extrsol})}$

Thus we have verified the proof obligation ${s}({w})\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}{s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ for
the induction step, for the vertex $w$ as picked.

By having performed the induction step, we have successfully carried out the
proof by complete induction on
${\leftarrow_{\text{{\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}bo}}}}$
that ${s}({w})\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({w})$ holds for all $w\in V$, and for an
arbitrary ${\mathcal{S}}$-provable solution $s$ of $\underline{\mathcal{C}}$.
This implies the statement of the lemma, that any two ${\mathcal{S}}$-provable
solutions of $\underline{\mathcal{C}}$ are Mil-provably equal.

######  Proposition 29.

For every $\mathcal{EL}$-based proof system ${\mathcal{S}}$ over
${\textit{StExp}}({\mathit{A}})$ with $\text{\sf
ACI}\mathrel{{\sqsubseteq}}{\mathcal{S}}\mathrel{{\precsim}}\text{\sf Mil}$,
provability by LLEE-witnessed coinductive proofs over ${\mathcal{S}}$ implies
derivability in Mil:

$\bigl{(}\;e_{1}\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}}}e_{2}\quad\;\Longrightarrow\quad\;e_{1}\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}e_{2}\;\bigr{)}\qquad\text{for all
$e_{1},e_{2}\in{\textit{StExp}}({\mathit{A}})$.}$ (20)

######  Proof 6.5.

For showing (20), let $e,f\in{\textit{StExp}}({\mathit{A}})$ be such that
$e\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\mathcal{S}}}}}f$. Then there is a LLEE-
witnessed coinductive proof
$\mathcal{LCP}=\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ 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}}$, which consists of a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ and ${\mathcal{S}}$-provable solutions
$L_{1},L_{2}\mathrel{:}{V}({\underline{\mathcal{C}}})\to{\textit{StExp}}({\mathit{A}})$
of $\underline{\mathcal{C}}$ with
$e_{1}\mathrel{{\equiv}}{L_{1}}({v_{\text{s}}})$ and
$e_{2}\mathrel{{\equiv}}{L_{2}}({v_{\text{s}}})$. By applying Lemma 28 to
$\mathcal{LCP}$ we find that $L_{1}$ and $L_{2}$ are Mil-provably equal. This
entails $e_{1}\mathrel{{\equiv}}{L_{1}}({v_{\text{s}}})\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}{L_{2}}({v_{\text{s}}})\mathrel{{\equiv}}e_{2}$, and thus
$e_{1}\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}e_{2}$.

$\begin{aligned} \scalebox{0.9}{ \leavevmode\hbox to142.44pt{\vbox
to166.86pt{\pgfpicture\makeatletter\hbox{\hskip
71.22102pt\lower-157.1581pt\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{ }
\par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-49.28146pt}{-125.2629pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
16.99234pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.65933pt}{-11.033pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${L_{i}}({v_{11}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
16.99234pt\hfil&\hfil\hskip 0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 16.99234pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.65933pt}{-11.033pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${L_{i}}({v_{21}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
16.99234pt\hfil\cr\vskip 35.56593pt\cr\hfil\hskip
15.59233pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.25932pt}{-11.033pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${L_{i}}({v_{1}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.59233pt\hfil&\hfil\hskip 0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 15.59233pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.25932pt}{-11.033pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${L_{i}}({v_{2}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.59233pt\hfil\cr\vskip 35.56593pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 15.29678pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.96378pt}{-11.033pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${L_{i}}({v_{\text{s}}})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
15.29678pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{{}{}}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.77779pt}{-0.85643pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\Large$\underline{\mathcal{C}}$, $\hskip
0.2pt\hat{\underline{\mathcal{C}}}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\par\par\par{ {}{}{}}{} {{}{{}{}}{}}{{}{{}{}}{}}{{}{}}{{}}
{{}{{}{}}{}}{{{}}{{}}}{{}}{{}{{}{}}{}}{{{}}{{}}}{ {}{}{}}{}{{}}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,1.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{-49.48146pt}{-28.932pt}\pgfsys@curveto{-70.82103pt}{-28.932pt}{-68.69391pt}{-71.60893pt}{-48.85417pt}{-76.92567pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.96593}{-0.25885}{0.25885}{0.96593}{-48.46782pt}{-77.0292pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.5,0,1}{}{}{}{}{{}}\pgfsys@moveto{-32.28912pt}{-72.83095pt}\pgfsys@lineto{-32.28912pt}{-38.265pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-32.28912pt}{-37.865pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-38.64546pt}{-65.92696pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}a}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-43.38817pt}{-53.86118pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}
{{}{{}{}}{}}{{}{{}{}}{}}{{}{}}{{}}
{{}{{}{}}{}}{{{}}{{}}}{{}}{{}{{}{}}{}}{{{}}{{}}}{ {}{}{}}{}{{}}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,1.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{-32.28912pt}{-89.89696pt}\pgfsys@curveto{-32.28912pt}{-104.12334pt}{-29.23842pt}{-125.9611pt}{-16.26949pt}{-129.43724pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.96591}{-0.2589}{0.2589}{0.96591}{-15.88313pt}{-129.5408pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{-21.7842pt}{-72.83095pt}\pgfsys@lineto{21.47662pt}{-37.71709pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.77643}{0.6302}{-0.6302}{0.77643}{21.6319pt}{-37.59105pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14433pt}{-51.61497pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$b$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{ {}{}{}}{}
{{}{{}{}}{}}{{}{{}{}}{}}{{}{}}{{}}
{{}{{}{}}{}}{{{}}{{}}}{{}}{{}{{}{}}{}}{{{}}{{}}}{ {}{}{}}{}{{}}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,1.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{49.48146pt}{-28.932pt}\pgfsys@curveto{70.82103pt}{-28.932pt}{68.69391pt}{-71.60893pt}{48.85417pt}{-76.92567pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.96593}{-0.25885}{0.25885}{-0.96593}{48.46782pt}{-77.0292pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.5,0,1}{}{}{}{}{{}}\pgfsys@moveto{32.28912pt}{-72.83095pt}\pgfsys@lineto{32.28912pt}{-38.265pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{32.28912pt}{-37.865pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{33.88817pt}{-67.11447pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}b}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{33.88817pt}{-53.86118pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{1}]}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}
{{}{{}{}}{}}{{}{{}{}}{}}{{}{}}{{}}
{{}{{}{}}{}}{{{}}{{}}}{{}}{{}{{}{}}{}}{{{}}{{}}}{ {}{}{}}{}{{}}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\pgfsys@setdash{0.8pt,1.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{32.28912pt}{-89.89696pt}\pgfsys@curveto{32.28912pt}{-104.12334pt}{29.23842pt}{-125.9611pt}{16.26949pt}{-129.43724pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.96591}{-0.2589}{0.2589}{-0.96591}{15.88313pt}{-129.5408pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par\par{ {}{}{}}{} {{}{}}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\pgfsys@color@rgb@stroke{0.82}{0.41}{0.12}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.82}{0.41}{0.12}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.82,0.41,0.12}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{-150.5889pt}\pgfsys@lineto{0.0pt}{-156.5581pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{0.0pt}{-150.5889pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{{}}{}{{{}} {}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.82,0.41,0.12}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.41,0.12}\pgfsys@color@rgb@stroke{0.82}{0.41}{0.12}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.82}{0.41}{0.12}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.82,0.41,0.12}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.20001pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-133.7959pt}\pgfsys@moveto{13.51506pt}{-133.7959pt}\pgfsys@curveto{13.51506pt}{-129.08163pt}{7.46425pt}{-125.26007pt}{0.0pt}{-125.26007pt}\pgfsys@curveto{-7.46425pt}{-125.26007pt}{-13.51506pt}{-129.08163pt}{-13.51506pt}{-133.7959pt}\pgfsys@curveto{-13.51506pt}{-138.51016pt}{-7.46425pt}{-142.33173pt}{0.0pt}{-142.33173pt}\pgfsys@curveto{7.46425pt}{-142.33173pt}{13.51506pt}{-138.51016pt}{13.51506pt}{-133.7959pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-133.7959pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{0.6pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@rgb@stroke{1}{1}{1}\pgfsys@invoke{
}\pgfsys@moveto{0.0pt}{-133.7959pt}\pgfsys@moveto{13.51506pt}{-133.7959pt}\pgfsys@curveto{13.51506pt}{-129.08163pt}{7.46425pt}{-125.26007pt}{0.0pt}{-125.26007pt}\pgfsys@curveto{-7.46425pt}{-125.26007pt}{-13.51506pt}{-129.08163pt}{-13.51506pt}{-133.7959pt}\pgfsys@curveto{-13.51506pt}{-138.51016pt}{-7.46425pt}{-142.33173pt}{0.0pt}{-142.33173pt}\pgfsys@curveto{7.46425pt}{-142.33173pt}{13.51506pt}{-138.51016pt}{13.51506pt}{-133.7959pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-133.7959pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{{{}{}}}{{}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.5,0,1}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-3.50943pt}{-122.39578pt}\pgfsys@lineto{-27.96483pt}{-42.98822pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.29433}{0.9557}{-0.9557}{-0.29433}{-28.08255pt}{-42.60596pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-18.71696pt}{-95.5931pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}a}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.84297pt}{-91.39429pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{{}}{}{}{{{}{}}}{{}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.5,0,1}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{3.50943pt}{-122.39578pt}\pgfsys@lineto{27.96483pt}{-42.98822pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.29433}{0.9557}{-0.9557}{0.29433}{28.08255pt}{-42.60596pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.67099pt}{-96.78061pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}b}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{7.75117pt}{-73.83363pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\pgfsys@color@rgb@stroke{0.5}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.5}{0}{1}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.5,0,1}\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}\small${\color[rgb]{0.5,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,1}[{2}]}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\par
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\end{aligned}\hskip
4.30554pt\begin{aligned}
{L_{i}}({v_{21}})&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}^{\text{\scriptsize(sol)}}\hskip
1.0pt}}$}\,{1}\mathrel{{\cdot}}{{L_{i}}({v_{2}})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}\,{L_{i}}({v_{2}})\\\\[-3.22916pt]
&\phantom{\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}^{\text{\scriptsize(sol)}}\hskip
1.0pt}}$}}\,\text{($\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}^{\text{\scriptsize(sol)}}\hskip 1.0pt}}$ means use
of `is {$\text{\text{\sf Mil}${}^{\boldsymbol{-}}$}$}-pro\\-vable
solution')}\\\
{L_{i}}({v_{2}})&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}^{\text{\scriptsize(sol)}}\hskip
1.0pt}}$}\,{{b}\mathrel{{\cdot}}{{L_{i}}({v_{21}})}}+{{1}\mathrel{{\cdot}}{{L_{i}}({v_{\text{s}}})}}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}\,{{b}\mathrel{{\cdot}}{{L_{i}}({v_{2}})}}+{{L_{i}}({v_{\text{s}}})}\\\\[-2.15277pt]
&\;\parbox[t]{0.0pt}{$\Downarrow${\text{\leavevmode\nobreak\
\leavevmode\nobreak\ applying $\text{$\textrm{RSP}^{*}$}$}}}\\\\[-2.15277pt]
{L_{i}}({v_{2}})&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\,{{b^{*}}}\mathrel{{\cdot}}{{L_{i}}({v_{\text{s}}})}\\\\[2.15277pt]
{L_{i}}({v_{11}})&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}^{\text{\scriptsize(sol)}}\hskip
1.0pt}}$}\,{1}\mathrel{{\cdot}}{{L_{i}}({v_{1}})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}\,{L_{i}}({v_{1}})\\\
{L_{i}}({v_{1}})&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\,{{a}\mathrel{{\cdot}}{{L_{i}}({v_{11}})}}+{{{b}\mathrel{{\cdot}}{{L_{i}}({v_{21}})}}+{{1}\mathrel{{\cdot}}{{L_{i}}({v_{\text{s}}})}}}\\\\[-1.07639pt]
&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\,{{a}\mathrel{{\cdot}}{{L_{i}}({v_{1}})}}+{{({{b}\mathrel{{\cdot}}{{b^{*}}}}+{1})}\mathrel{{\cdot}}{{L_{i}}({v_{\text{s}}})}}\\\\[-1.07639pt]
&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}$}\,{{a}\mathrel{{\cdot}}{{L_{i}}({v_{1}})}}+{{{b^{*}}}\mathrel{{\cdot}}{{L_{i}}({v_{\text{s}}})}}\\\\[-2.15277pt]
&\;\parbox[t]{0.0pt}{$\Downarrow${\text{\leavevmode\nobreak\
\leavevmode\nobreak\ applying $\text{$\textrm{RSP}^{*}$}$}}}\\\\[-2.15277pt]
{L_{i}}({v_{1}})&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\,{{a^{*}}}\mathrel{{\cdot}}{({{b^{*}}}\mathrel{{\cdot}}{{L_{i}}({v_{\text{s}}})})}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}\,{({{a^{*}}}\mathrel{{\cdot}}{{b^{*}}})}\mathrel{{\cdot}}{{L_{i}}({v_{\text{s}}})}\end{aligned}$

$\begin{aligned}
{L_{i}}({v_{\text{s}}})&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}^{\text{\scriptsize(sol)}}\hskip
1.0pt}}$}\,1+{{a}\mathrel{{\cdot}}{{L_{i}}({v_{11}})}}+{{b}\mathrel{{\cdot}}{{L_{i}}({v_{21}})}}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}\,1+{{a}\mathrel{{\cdot}}{{L_{i}}({v_{1}})}}+{{b}\mathrel{{\cdot}}{{L_{i}}({v_{2}})}}\\\\[-1.07639pt]
&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf Mil}}\hskip
1.0pt}}$}\,{({{a}\mathrel{{\cdot}}{({{a^{*}}}\mathrel{{\cdot}}{{b^{*}}})}}+{{b}\mathrel{{\cdot}}{{b^{*}}}})}\mathrel{{\cdot}}{{L_{i}}({v_{\text{s}}})}+1\\\\[-2.15277pt]
&\;\parbox[t]{0.0pt}{$\Downarrow${\text{\leavevmode\nobreak\
\leavevmode\nobreak\ applying $\text{$\textrm{RSP}^{*}$}$}}}\\\\[-2.15277pt]
{L_{i}}({v_{\text{s}}})&\;\parbox[t]{0.0pt}{$\mathrel{{=_{\text{\sf
Mil}}\hskip
1.0pt}}$}\,{{({{a}\mathrel{{\cdot}}{({{a^{*}}}\mathrel{{\cdot}}{{b^{*}}})}}+{{b}\mathrel{{\cdot}}{{b^{*}}}})^{*}}}\mathrel{{\cdot}}{1}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip
1.0pt}}\,{({{a}\mathrel{{\cdot}}{({{a^{*}}}\mathrel{{\cdot}}{{b^{*}}})}}+{{b}\mathrel{{\cdot}}{{b^{*}}}})^{*}}\,\mathrel{{=_{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}\hskip 1.0pt}}\,{s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{\text{s}}})\end{aligned}$

Figure 13. Showing for the coinductive proof
$\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ in Example 5 that the
principal value ${L_{i}}({v_{\text{s}}})$ of the Mil--provable solution
$L_{i}$ for $i\in\left\\{{1,2}\right\\}$ is Mil-provably equal to the
principal value ${s_{\hskip
0.2pt\hat{\underline{\mathcal{C}}}}}({v_{\text{s}}})$ of the solution
$s_{\hskip 0.2pt\hat{\underline{\mathcal{C}}}}$ extracted the underlying LLEE-
witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$.

We consider again the LLEE-witnessed coinductive proof
$\mathcal{CP}=\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ 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})^{*}}$
in Example 5. In Figure 13 we exhibit the extraction process of derivations in
Mil of
${L_{1}}({v_{\text{s}}})\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{s_{\underline{\mathcal{C}}}}({v})$
and
${L_{2}}({v_{\text{s}}})\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{s_{\underline{\mathcal{C}}}}({v})$
from the guarded LLEE-witness $\hskip 0.2pt\hat{\underline{\mathcal{C}}}$ of
$\underline{\mathcal{C}}$. These two derivations in Mil can be combined by
using $\mathcal{EL}$ rules in order to obtain a derivation in Mil of
${({{a^{*}}}\mathrel{{\cdot}}{{b^{*}}})^{*}}\mathrel{{\equiv}}{L_{1}}({v_{\text{s}}})\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}{L_{2}}({v_{\text{s}}})\mathrel{{\equiv}}{({a}+{b})^{*}}$.

######  Lemma 30.

The rules LCoProofn are correct for Mil, for all $n\in{\rm Nature}$. This
statement also holds effectively: Every derivation $\mathcal{D}$ in
${\text{\sf Mil}}{+}{\text{LCoProof${}_{n}$}}$ that consists of a bottommost
instance of LCoProofn, where $n\in{\rm Nature}$, whose immediate
subderivations are derivations in Mil can be transformed effectively into a
derivation $\mathcal{D}^{\prime}$ in Mil that has the same conclusion as
$\mathcal{D}$.

######  Proof 6.6.

We let $n\in{\rm Nature}$. In order to show correctness of the rule LCoProofn
for Mil, we consider a derivation $\mathcal{D}$ in ${\text{\sf
Mil}}{+}{\text{LCoProof${}_{n}$}}$ that has immediate subderivations
$\mathcal{D}_{1}$, …, $\mathcal{D}_{n}$ in Mil, and that terminates with an
instance $\iota$ of LCoProofn , where
$\Gamma\mathrel{{:=}}\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_{1}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{1}}\right\\}\,$:

$\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}_{n}$
$g_{n}\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}h_{n}$
$\iota$ LCoProofn
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$

and $e\mathrel{{\overset{\text{\scriptsize
LLEE}}{=\joinrel=\joinrel=}_{{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\Gamma}}}}f$ holds as side-condition on the
instance $\iota$ of LCoProofn. Then there is a LLEE-witnessed coinductive
proof $\mathcal{LCP}=\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ 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}$. We have to
show that there is a derivation $\mathcal{D}^{\prime}$ in Mil with the same
conclusion
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$.

Since $\mathcal{D}_{1}$, …, $\mathcal{D}_{n}$ are derivations in Mil, their
conclusions in $\Gamma$ are derivable in Mil. This implies ${\text{\sf
Mil}}{+}{\Gamma}\mathrel{{\precsim}}\text{\sf Mil}$. It follows that
$\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 Mil, that is, it holds:

$e\mathrel{{\overset{\text{\scriptsize LLEE}}{=\joinrel=\joinrel=}_{\text{\sf
Mil}}}}f\hskip 1.5pt{.}$

From this we obtain $e\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}f$ by applying
Proposition 29, which guarantees a derivation $\mathcal{D}^{\prime}$ in Mil
with conclusion
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
as desired. The proof of Proposition 29 furthermore guarantees that such a
derivation $\mathcal{D}^{\prime}$ in Mil can be constructed effectively from
the 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}$ (and hence over
Mil) and the derivations $\mathcal{D}_{1}$, …, $\mathcal{D}_{n}$ in Mil.

######  Theorem 31.

$\text{\sf cMil}\mathrel{{\precsim}}\text{\sf Mil}$. Moreover, every
derivation in cMil with conclusion
$e\mathrel{{\color[rgb]{0.25390625,0.41015625,0.8828125}\definecolor[named]{pgfstrokecolor}{rgb}{0.25390625,0.41015625,0.8828125}=}}f$
can be transformed effectively into a derivation in Mil that has the same
conclusion.

######  Proof 6.7.

Due to Lemma 30, every rule LCoProofn, for $n\in{\rm Nature}$, is correct for
Mil. Then by using Lemma 1, (i), we find that each of these rules are
admissible in Mil. This means that ${\text{\sf
Mil}}{+}{\text{LCoProof${}_{n}$}}\mathrel{\sim}\text{\sf Mil}$ holds for all
$n\in{\rm Nature}$, which implies, with an argument by induction on the
prooftree size of derivations in ${\text{\sf
Mil}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm Nature}}}$, that
${\text{\sf Mil}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm
Nature}}}\mathrel{\sim}\text{\sf Mil}$ holds as well. With this statement we
can now argue as follows:

cMil $\displaystyle{}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm
Nature}}}$ (by Definition 21)
$\displaystyle{}\mathrel{{\sqsubseteq}}{({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm
Nature}}})}{+}{\text{$\textrm{RSP}^{*}$}}\hskip 12.50002pt$ (by extension via
adding the rule $\textrm{RSP}^{*}$) $\displaystyle{}={({\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{$\textrm{RSP}^{*}$}})}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm
Nature}}}$ (by construing the same system differently)
$\displaystyle{}={{\text{\sf
Mil}}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm Nature}}}$ (by
Definition 2.1) $\displaystyle{}\mathrel{\sim}\text{\sf Mil}$
$\displaystyle\text{(as argued above)}\hskip 1.5pt{.}$

From this we obtain $\text{\sf cMil}\mathrel{{\precsim}}\text{\sf Mil}$ in
view of
$({{\sqsubseteq}}\cdot{{\sim}})\>\subseteq\>({{\precsim}}\cdot{{\sim}})\>\subseteq\>{\precsim}$.

For demonstrating the effective transformation statement of the theorem we use
the transformation from the proof of the implication “$\Leftarrow$” in Lemma
1, (i), which states that correct rules are also admissible. We have to show
that every derivation $\mathcal{D}$ in cMil can be transformed effectively
into a derivation $\mathcal{D}^{\prime}$ in Mil with the same conclusion. In
order to establish this statement by induction we prove it for all derivations
$\mathcal{D}$ in the extension ${\text{\sf
cMil}}{+}{\text{$\textrm{RSP}^{*}$}}={{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm
Nature}}}}{+}{\text{$\textrm{RSP}^{*}$}}={\text{\sf
Mil}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm Nature}}}$ of
cMil.

We proceed by induction on the number of instances of rules LCoProofn, for
$n\in{\rm Nature}$, in $\mathcal{D}$. Let $\mathcal{D}$ be a derivation
${{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm
Nature}}}}{+}{\text{$\textrm{RSP}^{*}$}}$. If $\mathcal{D}$ does not contain
an instance of LCoProofn with $n\in{\rm Nature}$, then $\mathcal{D}$ is
already a derivation in $\text{\sf Mil}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{$\textrm{RSP}^{*}$}}$, and no further
transformation is necessary. Otherwise $\mathcal{D}$ contains at least one
instance of LCoProofn with $n\in{\rm Nature}$. We pick an instance $\iota$ in
$\mathcal{D}$ of a rule LCoProof${}_{n_{0}}$ with $n_{0}\in{\rm Nature}$ that
is topmost among the instances of the coinductive rule in $\mathcal{D}$, that
is, none of the immediate subderivations of the instance $\iota$ in
$\mathcal{D}$ contains any instance of a rule LCoProofn for $n\in{\rm
Nature}$. Let $\mathcal{D}_{0}$ be the subderivation of $\mathcal{D}$ that
ends in $\iota$. Since $\iota$ is topmost, all of the immediate subderivations
of $\iota$ and $\mathcal{D}_{0}$ in $\mathcal{D}$ are derivations in
$\text{\sf Mil}={\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{$\textrm{RSP}^{*}$}}$, and
$\mathcal{D}_{0}$ is a derivation in ${{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\text{LCoProof${}_{n_{0}}$}}}{+}{\text{$\textrm{RSP}^{*}$}}={\text{\sf
Mil}}{+}{\text{LCoProof${}_{n_{0}}$}}$. Therefore we can apply the effective
part of Lemma 30 to the subderivation $\mathcal{D}_{0}$. We obtain a
derivation $\mathcal{D}^{\prime}_{0}$ in Mil with the same conclusion as
$\iota$ and $\mathcal{D}_{0}$. Then by replacing $\mathcal{D}_{0}$ in
$\mathcal{D}$ with $\mathcal{D}^{\prime}_{0}$ we obtain a derivation
$\tilde{\mathcal{D}}$ in ${{\text{\text{\sf
Mil}${}^{\boldsymbol{-}}$}}{+}{\left\\{{\text{LCoProof${}_{n}$}}\right\\}_{n\in{\rm
Nature}}}}{+}{\text{$\textrm{RSP}^{*}$}}$ that has the same conclusion as
$\mathcal{D}$, but that has one instance of a coinductive rule less than
$\mathcal{D}$. Now we can apply the induction hypothesis to
$\tilde{\mathcal{D}}$ in order to effectively transform it in a derivation
$\mathcal{D}^{\prime}$ in Mil that has the same conclusion as $\mathcal{D}$.
In this way we have performed the induction step.

We conclude this section with an illustrative application of the results
obtained here that provides in-roads for a completeness proof for Milner’s
system Mil. Specifically we apply Proposition 29, the transformation of LLEE-
witnessed coinductive proofs over Mil into derivations in Mil. We show (see
Corollary 33 below) that Milner’s system is complete for bisimilarity of chart
interpretations of star expressions when bisimilarity is witnessed by joint
expansion or joint minimization to a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
via functional
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
(see Definition 6). For showing this statement we must, however, use here
without proof a technical result from [Gra22a]: Mil-provable solutions of
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
can be transferred backwards over functional
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
(see Lemma 32). This statement is a generalization to
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
of Proposition 5.1 in [GF20a], which states that ${\mathcal{S}}$-provable
solutions of charts, for $\text{\sf ACI}\mathrel{{\sqsupseteq}}{\mathcal{S}}$,
can be transferred backwards over functional bisimulations.

Let $\underline{\mathcal{C}}$, $\underline{\mathcal{C}}_{1}$, and
$\underline{\mathcal{C}}_{2}$ be
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts.
We say that $\underline{\mathcal{C}}_{1}$ and $\underline{\mathcal{C}}_{2}$
are
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimilar
_via $\underline{\mathcal{C}}$ as (their) joint expansion_
($\underline{\mathcal{C}}_{1}$ and $\underline{\mathcal{C}}_{2}$ are
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimilar
_via $\underline{\mathcal{C}}$ as (their) joint minimization_) if
$\underline{\mathcal{C}}_{1}\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{$\leftarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}\underline{\mathcal{C}}\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}$\rightarrow$}}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}\underline{\mathcal{C}}_{2}$ holds (respectively, if
$\underline{\mathcal{C}}_{1}\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}$\rightarrow$}}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}\underline{\mathcal{C}}\mathrel{{\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}\hbox{\kern
0.21529pt\vbox{\hbox{\raise
0.43057pt\hbox{\kern-0.43057pt{$\leftarrow$}\kern-0.43057pt}}\hrule}\kern
0.43057pt}}}\underline{\mathcal{C}}_{2}$ holds).

######  Lemma 32 ($\sim\,$Lemma 3.8, (i), in [Gra22a]).

Mil-Provable solvability with principal value $e$ is preserved under converse
functional
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimilarity,
on weakly guarded
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts,
for all star expressions $e\in\textit{StExp}$.

$\underline{\mathcal{C}}$LLEE,
guarded${\mathcal{C}}({e_{1}})$${\mathcal{C}}({e_{2}})$$e_{1}\mathrel{{=_{\text{\sf
Mil}}\hskip 1.0pt}}e_{2}$Cor. 33, 33Cor. 33,
33${\mathcal{C}}({e_{1}})$${\mathcal{C}}({e_{2}})$$\underline{\mathcal{C}}$LLEE,
guarded Figure 14. Illustration of the statements (for arbitrary given
$e_{1},e_{2}\in\textit{StExp}$) of Corollary 33: Milner’s system Mil is
complete for
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimilarity
of chart interpretations via guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-charts
as joint expansion or as joint minimization.

######  Corollary 33.

The following two statements hold (see Figure 14 for their illustrations):
[label=()]

Mil is complete for
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimilarity
of chart interpretations of two star expressions via a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
as joint expansion.

Mil is complete for
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimilarity
of chart interpretations of two star expressions via a guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
as joint minimization.

######  Proof 6.8.

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

Due to Lemma 9, there are Mil--provable (and thus Mil-provable) solutions of
${\mathcal{C}}({e_{1}})$ and ${\mathcal{C}}({e_{2}})$ with principal values
$e_{1}$, and $e_{2}$, respectively. Then we obtain by applying Lemma 32, in
view of the converse functional
${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-bisimulations
from ${\mathcal{C}}({e_{1}})$ and ${\mathcal{C}}({e_{2}})$ to
$\underline{\mathcal{C}}$, that there are two Mil-provable solutions $L_{1}$
and $L_{2}$ of $\underline{\mathcal{C}}$ with the principal values $e_{1}$ and
$e_{2}$, respectively. These two Mil-provable solutions of the guarded LLEE
-${\color[rgb]{0.6875,0.09765625,0.09765625}\definecolor[named]{pgfstrokecolor}{rgb}{0.6875,0.09765625,0.09765625}1}$-chart
$\underline{\mathcal{C}}$ can be combined to obtain a LLEE-witnessed
coinductive proof $\langle\underline{\mathcal{C}},\hskip 0.5ptL\rangle$ 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 Mil. Thus we obtain:

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

From this we arrive at $e_{1}\mathrel{{=_{\text{\sf Mil}}\hskip 1.0pt}}e_{2}$