\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}} \end{picture}}(\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}c)$, see [6] for a detailed
explanation.

As a final point, we note that there are left-sequential, binary connectives
for which the distinction between short-circuit evaluation and full evaluation
does not exist, such as the _left-sequential biconditional_ and the _left-
sequential exclusive or_ , defined by Cornets de Groot in [11] by
$x~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-0.98,0.58){\circle*{0.6}}
\end{picture}}y=y\scalebox{0.78}{\raisebox{0.1pt}[0.0pt][0.0pt]{$\;\lhd\;$}}x\scalebox{0.78}{\raisebox{0.1pt}[0.0pt][0.0pt]{$\;\rhd\;$}}({\sf
F}\scalebox{0.78}{\raisebox{0.1pt}[0.0pt][0.0pt]{$\;\lhd\;$}}y\scalebox{0.78}{\raisebox{0.1pt}[0.0pt][0.0pt]{$\;\rhd\;$}}{\sf
T})$ and
$x~{}\mathbin{\begin{picture}(1.5,1.8)(-0.5,0.0)\put(-0.8,0.0){$\oplus$}
\put(-1.02,0.56){\circle*{0.6}} \end{picture}}y=({\sf
F}\scalebox{0.78}{\raisebox{0.1pt}[0.0pt][0.0pt]{$\;\lhd\;$}}y\scalebox{0.78}{\raisebox{0.1pt}[0.0pt][0.0pt]{$\;\rhd\;$}}{\sf
T})\scalebox{0.78}{\raisebox{0.1pt}[0.0pt][0.0pt]{$\;\lhd\;$}}x\scalebox{0.78}{\raisebox{0.1pt}[0.0pt][0.0pt]{$\;\rhd\;$}}y$,
respectively. It immediately follows that
$x~{}\mathbin{\begin{picture}(1.5,1.8)(-0.5,0.0)\put(-0.8,0.0){$\oplus$}
\put(-1.02,0.56){\circle*{0.6}}
\end{picture}}y=x~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-0.98,0.58){\circle*{0.6}}
\end{picture}}\neg y$ and
$\neg(x~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-0.98,0.58){\circle*{0.6}}
\end{picture}}y)=x~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-0.98,0.58){\circle*{0.6}}
\end{picture}}\neg y$. In [17], the notations
${~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-0.98,0.58){\circle{0.6}}
\end{picture}}}$ and
$~{}\mathbin{\begin{picture}(1.5,1.8)(-0.5,0.0)\put(-0.8,0.0){$\oplus$}
\put(-1.02,0.56){\circle{0.6}} \end{picture}}$ are used, and below we use the
symbols ${~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-1.38,0.02){{\small$\leftarrow$}}
\end{picture}}}$ and
$~{}\mathbin{\begin{picture}(1.5,1.8)(-0.5,0.0)\put(-0.8,0.0){$\oplus$}
\put(-1.62,0.02){{\small$\leftarrow$}} \end{picture}}$, expressing only left-
sequentiality. Regarding expressiveness, we note that in FFEL extended with
$~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-1.38,0.02){{\small$\leftarrow$}}
\end{picture}}$, the evaluation tree of
$a~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-1.38,0.02){{\small$\leftarrow$}}
\end{picture}}b$ is $({\sf T}\unlhd b\unrhd{\sf F})\unlhd a\unrhd({\sf
F}\unlhd b\unrhd{\sf T})$. However, it easily follows that not all uniform
evaluation trees can be expressed in FFEL with
${~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-1.38,0.02){{\small$\leftarrow$}}
\end{picture}}}$.666Suppose $A=\\{a\\}$. Then there are $5\cdot 4^{4}\cdot
3^{3}$ terms composed of four elements of $\\{a,\neg
a,a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf
T},a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}\\}$ and the three
connectives in
$\\{~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}},~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}},~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-1.38,0.02){{\small$\leftarrow$}}
\end{picture}}\\}$ that have evaluation trees of depth 4. It is not hard to
prove that these terms represent all closed terms with evaluation trees of
depth 4. However, there are $2^{16}$ such trees.  Of course, in MFEL and all
stronger FELs, the left-sequential biconditional
$x~{}\mathbin{\begin{picture}(1.9,1.8)(-0.5,0.0)
\put(-0.8,0.0){$\leftrightarrow$} \put(-1.38,0.02){{\small$\leftarrow$}}
\end{picture}}y$ is definable by $h(x,y,\neg y)$.

Related work. In the recent paper [3] we view _Conditional logic_ , which was
defined in 1990 by Guzmán and Squier [12], as a short-circuit logic, and
locate C$\ell$SCL, i.e., the two-valued variant of this SCL, in between MSCL
and SSCL.777The name C$\ell$SCL was chosen because CSCL is already used for
“Contractive SCL” [4], the short-circuit logic that (only) contracts adjacent
atoms:
$a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}a=a$, but
$(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}}
\end{picture}}b)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}}
\end{picture}}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}b)$ and
$a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}b$ have different evaluation
trees.  In [3] it was also established that three-valued conditional logic
defines a fully evaluated sublogic that is equivalent to Bochvar’s strict
three-valued logic [8]; this is the logic we now call
$\textup{$\textrm{C$\ell$FEL}$}^{\sf U}$. It is remarkable that also for the
two-valued case, the typical axiom
$x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}y=y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}x$ is a consequence of the
distinguishing C$\ell$SCL-axiom

$(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}}
\end{picture}}y)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}}
\end{picture}}x)=(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}}
\end{picture}}x)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}}
\end{picture}}(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}y).$

This particular consequence led us to C$\ell$FEL, a FEL in between MFEL and
SFEL that can be motivated as a sublogic of C$\ell$SCL. Thus, we locate
C$\ell$FEL in a hierarchy of two-valued FELs, and we derive its existence and
motivation both from the three-valued logic
$\textup{$\textrm{C$\ell$SCL}$}^{\sf U}$, and thus from Bochvar’s logic, and
from the consideration to adopt a full evaluation strategy.

With regard to the family of FELs, it remains a challenge to find related
work. This is also the case for the (somewhat larger) family of SCLs, apart
from [12] and our own papers on SCLs.

## References

  * [1] Bergstra, J.A., Bethke, I., and Rodenburg, P.H. (1995). A propositional logic with 4 values: true, false, divergent and meaningless, _Journal of Applied Non-Classical Logics_ , 5(2):199-217.
https://doi.org/10.1080/11663081.1995.10510855

  * [2] Bergstra, J.A. and Ponse, A. (2015). Evaluation trees for proposition algebra.
https://doi.org/10.48550/arXiv.1504.08321 [cs.LO].

  * [3] Bergstra, J.A. and Ponse, A. (2023). Conditional logic as a short-circuit logic.
https://doi.org/10.48550/arXiv.2304.14821 [cs.LO].

  * [4] Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2010 / 2013). Short-circuit logic. (First version appeared in 2010.)  https://doi.org/10.48550/arXiv.1010.3674 [cs.LO,math.LO].
  * [5] Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2018). Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant.
https://doi.org/10.48550/arXiv.1810.02142 [cs.LO,math.LO].

  * [6] Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2021).  Non-commutative propositional logic with short-circuit evaluation.  _Journal of Applied Non-Classical Logics_ , 31(3-4):234-278 (online available).
https://doi.org/10.1080/11663081.2021.2010954

  * [7] Blok, A. (2011). _Side-Effecting Logic_ , unpublished.
  * [8] Bochvar, D.A. (1938). On a 3-valued logical calculus and its application to the analysis of contradictions (in Russian). Matematicheskii Sbornik, 4(2):287-308.
  * [9] Burris, S.N. and Sankappanavar, H.P. (2012).  _A Course in Universal Algebra - The Millennium Edition_.  Available at http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html.
  * [10] Church, A. (1956). _Introduction to Mathematical Logic_. Princeton University Press.
  * [11] Cornets de Groot, S.H. (2012).  Logical systems with left-sequential versions of NAND and XOR.  MSc. thesis Logic, University of Amsterdam (June 2020).
https://eprints.illc.uva.nl/id/eprint/1743/1/MoL-2020-02.text.pdf.

  * [12] Guzmán, F. and Squier, C.C. (1990). The algebra of conditional logic. _Algebra Universalis_ , 27:88-110. https://doi.org/10.1007/BF01190256
  * [13] Hoare, C.A.R. (1985). A couple of novelties in the propositional calculus.  _Zeitschrift für Mathematische Logik und Grundlagen der Mathematik_ , 31(2):173-178. https://doi.org/10.1002/malq.19850310905
  * [14] Kleene, S.C. (1938).  On a notation for ordinal numbers. _Journal of Symbolic Logic_ , 3:150-155.
  * [15] McCarthy, J. (1963).  A basis for a mathematical theory of computation. In P. Braffort and D. Hirschberg (eds.), _Computer Programming and Formal Systems_ , pages 33–70, North-Holland, Amsterdam.
  * [16] McCune W. (2008). The GUI: Prover9 and Mace4 with a graphical user interface. Prover9-Mace4 Version 0.5B. (Prover9-Mace4-v05B.zip, March 14, 2008).
https://www.cs.unm.edu/~mccune/prover9/gui/v05.html.

  * [17] Papuc, D. and Ponse, A. (2022). Non-commutative propositional logic with short-circuited biconditional and NAND. https://doi.org/10.48550/arXiv.2203.09321 [cs.LO].
  * [18] Ponse, A. and Staudt, D.J.C. (2018).  An independent axiomatisation for free short-circuit logic.  _Journal of Applied Non-Classical Logics_ , 28(1), 35-71 (online available).
https://doi.org/10.1080/11663081.2018.1448637

  * [19] Staudt, D.J.C. (2012).  Completeness for two left-sequential logics.  MSc. thesis Logic, University of Amsterdam (May 2012). https://doi.org/10.48550/arXiv.1206.1936 [cs.LO].

##  Appendix A Proofs - Section 2

Correctness of $\bm{f}$. To prove that
$f:{\mathcal{SP}_{\\!A}}\to\textup{FNF}$ is indeed a normalization function we
need to prove that for all FEL-terms $P$, $f(P)$ terminates,
$f(P)\in\textup{FNF}$ and $\textup{$\textrm{EqFFEL}$}\vdash f(P)=P$. To arrive
at this result, we prove several intermediate results about the functions
$f^{n}$ and $f^{c}$, roughly in the order in which their definitions were
presented in Section 2. For the sake of brevity we will not explicitly prove
that these functions terminate. To see that each function terminates consider
that a termination proof would closely mimic the proof structure of the lemmas
dealing with the grammatical categories of the images of these functions.

######  Lemma A.1.

For any $P^{\sf F}$ and $P^{\sf T}$, $\textup{$\textrm{EqFFEL}$}\vdash P^{\sf
F}=P^{\sf
F}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}$ and
$\textup{$\textrm{EqFFEL}$}\vdash P^{\sf T}=P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T}$.

###### Proof.

We prove both claims simultaneously by induction. In the base case we have
${\sf F}={\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}$ by (FFEL5), which is
equal to ${\sf
F}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}$ by (FFEL8) and (FFEL1).
The base case for the second claim follows from that for the first claim by
duality.

For the induction we have
$a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf
F}=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(P^{\sf
F}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by the induction
hypothesis and the result follows from (FFEL4). For the second claim we again
appeal to duality. ∎

######  Lemma A.2.

The following equations can be derived by equational logic and EqFFEL.

  1. 1.

$x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(z~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))=(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}y)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(z~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$

  2. 2.

$\neg x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf
T})=\neg(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T}))$

###### Proof.

$\displaystyle
x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(z~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}))$
$\displaystyle=x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}((\neg
y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}z)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by (FFEL4) and Lemma
2.6.1 $\displaystyle=(\neg
x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\neg
y)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(z~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by (FFEL4) and Lemma
2.6.1 $\displaystyle=\neg(\neg
x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\neg
y)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(z~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by Lemma 2.6.1
$\displaystyle=(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}y)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(z~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}),$ by (FFEL2)
$\displaystyle\neg
x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T})$ $\displaystyle=\neg
x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by (FFEL10)
$\displaystyle=\neg(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}\neg(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}))$ by (FFEL2) and (FFEL3)
$\displaystyle=\neg(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\neg(\neg
y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\neg{\sf T}))$ by (FFEL8) and
(FFEL1)
$\displaystyle=\neg(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T})).$ by (FFEL2)

∎

######  Lemma A.3.

For all $P\in\textup{FNF}$, if $P$ is a ${\sf T}$-term then $f^{n}(P)$ is an
${\sf F}$-term, if it is an ${\sf F}$-term then $f^{n}(P)$ is a ${\sf
T}$-term, if it is a ${\sf T}$-$*$-term then so is $f^{n}(P)$, and

$\textup{$\textrm{EqFFEL}$}\vdash f^{n}(P)=\neg P.$

###### Proof.

We start with proving the claims for ${\sf T}$-terms, by induction on $P^{\sf
T}$. In the base case $f^{n}({\sf T})={\sf F}$. It is immediate that
$f^{n}({\sf T})$ is an ${\sf F}$-term. The claim that
$\textup{$\textrm{EqFFEL}$}\vdash f^{n}({\sf T})=\neg{\sf T}$ is immediate by
(FFEL1). For the inductive case we have that
$f^{n}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf
T})=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}f^{n}(P^{\sf T})$, where we may
assume that $f^{n}(P^{\sf T})$ is an ${\sf F}$-term and that
$\textup{$\textrm{EqFFEL}$}\vdash f^{n}(P^{\sf T})=\neg P^{\sf T}$. The
grammatical claim now follows immediately from the induction hypothesis.
Furthermore, noting that by the induction hypothesis we may assume that
$f^{n}(P^{\sf T})$ is an ${\sf F}$-term, we have:

$\displaystyle
f^{n}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf T})$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}f^{n}(P^{\sf T})$ by definition
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(f^{n}(P^{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by Lemma A.1
$\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(f^{n}(P^{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by Lemma 2.6.1
$\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}f^{n}(P^{\sf T})$ by Lemma A.1
$\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\neg P^{\sf T}$ by induction
hypothesis
$\displaystyle=\neg(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf T}).$ by (FFEL3) and
(FFEL2)

For ${\sf F}$-terms we prove our claims by induction on $P^{\sf F}$. In the
base case $f^{n}({\sf F})={\sf T}$. It is immediate that $f^{n}({\sf F})$ is a
${\sf T}$-term. The claim that $\textup{$\textrm{EqFFEL}$}\vdash f^{n}({\sf
F})=\neg{\sf F}$ is immediate by the dual of (FFEL1). For the inductive case
we have that
$f^{n}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf
F})=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}f^{n}(P^{\sf F})$, where we may
assume that $f^{n}(P^{\sf F})$ is a ${\sf T}$-term and
$\textup{$\textrm{EqFFEL}$}\vdash f^{n}(P^{\sf F})=\neg P^{\sf F}$. It follows
immediately from the induction hypothesis that
$f^{n}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf F})$ is a ${\sf T}$-term.
Furthermore, noting that by the induction hypothesis we may assume that
$f^{n}(P^{\sf F})$ is a ${\sf T}$-term, we prove the remaining claim as
follows:

$\displaystyle
f^{n}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf F})$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}f^{n}(P^{\sf F})$ by definition
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}(f^{n}(P^{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T})$ by Lemma A.1
$\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}(f^{n}(P^{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T})$ by the dual of Lemma
2.6.1 $\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}f^{n}(P^{\sf F})$ by Lemma A.1
$\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}\neg P^{\sf F}$ by induction
hypothesis
$\displaystyle=\neg(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf F}).$ by (FFEL3) and
(FFEL2)

To prove the lemma for ${\sf T}$-$*$-terms we first verify that the auxiliary
function $f^{n}_{1}$ returns a $*$-term and that for any $*$-term $P$,
$\textup{$\textrm{EqFFEL}$}\vdash f^{n}_{1}(P)=\neg P$. We show this by
induction on the number of $\ell$-terms in $P$. For the base cases, i.e., for
$\ell$-terms, it is immediate that $f^{n}_{1}(P)$ is a $*$-term. If $P$ is an
$\ell$-term with a positive determinative atom we have:

$\displaystyle
f^{n}_{1}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf T})$ $\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf T}$ by definition
$\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T})$ by Lemma A.1
$\displaystyle=\neg(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T}))$ by Lemma A.2.2
$\displaystyle=\neg(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf T}).$ by Lemma A.1

If $P$ is an $\ell$-term with a negative determinative atom the proof proceeds
the same, substituting $\neg a$ for $a$ and applying (FFEL3) where needed. For
the inductive step we assume that the result holds for $*$-terms with fewer
$\ell$-terms than
$P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{d}$ and
$P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q^{c}$. We note that each
application of $f^{n}_{1}$ changes the main connective (not occurring inside
an $\ell$-term) and hence the result is a $*$-term. Derivable equality is,
given the induction hypothesis, an instance of (the dual of) (FFEL2).

With this result we can now see that $f^{n}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{*})$ is indeed a ${\sf
T}$-$*$-term. Furthermore we find that:

$\displaystyle f^{n}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{*})$ $\displaystyle=P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}f^{n}_{1}(Q^{*})$ by definition
$\displaystyle=P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\neg Q^{*}$ as shown above
$\displaystyle=(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\neg Q^{*}$ by Lemma A.1
$\displaystyle=\neg(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}\neg Q^{*}$ by Lemma 2.6.2
$\displaystyle=\neg P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}\neg Q^{*}$ by Lemma A.1
$\displaystyle=\neg(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{*}).$ by (FFEL2) and (FFEL3)

Hence for all $P\in\textup{FNF}$, $\textup{$\textrm{EqFFEL}$}\vdash
f^{n}(P)=\neg P$. ∎

######  Lemma A.4.

For any ${\sf T}$-term $P$ and $Q\in\textup{FNF}$, $f^{c}(P,Q)$ has the same
grammatical category as $Q$ and

$\textup{$\textrm{EqFFEL}$}\vdash
f^{c}(P,Q)=P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q.$

###### Proof.

By induction on the complexity of the first argument. In the base case we see
that $f^{c}({\sf T},P)=P$ and hence has the same grammatical category as $P$.
Derivable equality follows from (FFEL5).

For the induction step we make a case distinction on the grammatical category
of the second argument. If the second argument is a ${\sf T}$-term we have
that
$f^{c}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf T},Q^{\sf
T})=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}f^{c}(P^{\sf T},Q^{\sf T})$,
where we assume that $f^{c}(P^{\sf T},Q^{\sf T})$ is a ${\sf T}$-term and
$\textup{$\textrm{EqFFEL}$}\vdash f^{c}(P^{\sf T},Q^{\sf T})=P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T}$. The grammatical claim
follows immediately from the induction hypothesis. The claim about derivable
equality is proved as follows:

$\displaystyle
f^{c}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf T},Q^{\sf T})$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}f^{c}(P^{\sf T},Q^{\sf T})$ by
definition
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T})$ by induction
hypothesis
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(Q^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T}))$ by Lemma A.1
$\displaystyle=(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(Q^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T})$ by Lemma 2.6.3
$\displaystyle=(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T}.$ by Lemma A.1

If the second argument is an ${\sf F}$-term we assume that $f^{c}(P^{\sf
T},Q^{\sf F})$ is an ${\sf F}$-term and that $\textup{$\textrm{EqFFEL}$}\vdash
f^{c}(P^{\sf T},Q^{\sf F})=P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf F}$. The grammatical claim
follows immediately from the induction hypothesis. Derivable equality is
proved as follows:

$\displaystyle
f^{c}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf T},Q^{\sf F})$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}f^{c}(P^{\sf T},Q^{\sf F})$ by
definition
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf F})$ by induction
hypothesis
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(Q^{\sf
F}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}))$ by Lemma A.1
$\displaystyle=(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(Q^{\sf
F}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by Lemma A.2.1
$\displaystyle=(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf F}.$ by Lemma A.1

Finally, if the second argument is a ${\sf T}$-$*$-term then
$f^{c}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf T},Q^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}R^{*})=f^{c}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf T},Q^{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{*}$. The fact that this is a
${\sf T}$-$*$-term follows from the fact that
$f^{c}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P^{\sf T},Q^{\sf T})$ is a ${\sf
T}$-term as was shown above. Derivable equality follows from the case where
the second argument is a ${\sf T}$-term and (FFEL4). ∎

######  Lemma A.5.

For any ${\sf T}$-$*$-term $P$ and ${\sf F}$-term $Q$, $f^{c}(P,Q)$ is an
${\sf F}$-term and

$\textup{$\textrm{EqFFEL}$}\vdash
f^{c}(P,Q)=P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q.$

###### Proof.

By (FFEL4) and Lemma A.4 it suffices to show that $f^{c}_{2}(P^{*},Q^{\sf F})$
is an ${\sf F}$-term and that $\textup{$\textrm{EqFFEL}$}\vdash
f^{c}_{2}(P^{*},Q^{\sf
F})=P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf F}$. We prove this by
induction on the number of $\ell$-terms in $P^{*}$. In the base cases, i.e.,
$\ell$-terms, the grammatical claims follow from Lemma A.4. The claim about
derivable equality in the case of $\ell$-terms with positive determinative
atoms follows from Lemma A.4 and (FFEL4). For $\ell$-terms with negative
determinative atoms it follows from Lemma A.4, Lemma A.1, (FFEL7), (FFEL4) and
(FFEL8).

For the induction step we assume the claims hold for any $*$-terms with fewer
$\ell$-terms than
$P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{d}$ and
$P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q^{c}$. In the case of
conjunctions we have
$f^{c}_{2}(P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{d},R^{\sf
F})=f^{c}_{2}(P^{*},f^{c}_{2}(Q^{d},R^{\sf F}))$ and the grammatical claim
follows from the induction hypothesis (applied twice). Derivable equality
follows from the induction hypothesis and (FFEL4).

For disjunctions we have
$f^{c}_{2}(P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q^{c},R^{\sf
F})=f^{c}_{2}(P^{*},f^{c}_{2}(Q^{c},R^{\sf F}))$ and the grammatical claim
follows from the induction hypothesis (applied twice). The claim about
derivable equality is proved as follows:

$\displaystyle
f^{c}_{2}(P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q^{c},R^{\sf F})$
$\displaystyle=f^{c}_{2}(P^{*},f^{c}_{2}(Q^{c},R^{\sf F}))$ by definition
$\displaystyle=P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(Q^{c}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{\sf F})$ by induction
hypothesis
$\displaystyle=P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(Q^{c}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(R^{\sf
F}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}))$ by Lemma A.1
$\displaystyle=(P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}Q^{c})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(R^{\sf
F}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})$ by Lemma A.2.1
$\displaystyle=(P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}Q^{c})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{\sf F}.$ by Lemma A.1

∎

######  Lemma A.6.

For any ${\sf F}$-term $P$ and $Q\in\textup{FNF}$, $f^{c}(P,Q)$ is an ${\sf
F}$-term and

$\textup{$\textrm{EqFFEL}$}\vdash
f^{c}(P,Q)=P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q.$

###### Proof.

We make a case distinction on the grammatical category of the second argument.
If the second argument is a ${\sf T}$-term we proceed by induction on the
first argument. In the base case we have $f^{c}({\sf F},P^{\sf
T})=f^{n}(P^{\sf T})$ and the result is by Lemma A.3, Lemma A.1, (FFEL7) and
(FFEL8). In the inductive case we have
$f^{c}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P^{\sf F},Q^{\sf
T})=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}f^{c}(P^{\sf F},Q^{\sf T})$,
where we assume that $f^{c}(P^{\sf F},Q^{\sf T})$ is an ${\sf F}$-term and
$\textup{$\textrm{EqFFEL}$}\vdash f^{c}(P^{\sf F},Q^{\sf T})=P^{\sf
F}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T}$. The result now
follows from the induction hypothesis and (FFEL4).

If the second argument is an ${\sf F}$-term the proof is almost the same,
except that we need not invoke Lemma A.3 or (FFEL8) in the base case.

Finally, if the second argument is a ${\sf T}$-$*$-term we again proceed by
induction on the first argument. In the base case we have $f^{c}({\sf
F},P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{*})=f^{c}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{*},{\sf F})$. The grammatical
claim now follows from Lemma A.5 and derivable equality follows from Lemma A.5
and (FFEL7). For for the inductive case the results follow from the induction
hypothesis and (FFEL4). ∎

######  Lemma A.7.

For any ${\sf T}$-$*$-term $P$ and ${\sf T}$-term $Q$, $f^{c}(P,Q)$ has the
same grammatical category as $P$ and

$\textup{$\textrm{EqFFEL}$}\vdash
f^{c}(P,Q)=P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q.$

###### Proof.

By (FFEL4) it suffices to prove the claims for $f^{c}_{1}$, i.e., that
$f^{c}_{1}(P^{*},Q^{\sf T})$ has the same grammatical category as $P^{*}$ and
that $\textup{$\textrm{EqFFEL}$}\vdash f^{c}_{1}(P^{*},Q^{\sf
T})=P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T}$. We prove this by
induction on the number of $\ell$-terms in $P^{*}$. In the base case we deal
with $\ell$-terms and the results follow from Lemma A.4 and (FFEL4).

For the inductive cases we assume that the results hold for any $*$-term with
fewer $\ell$-terms than
$P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{d}$ and
$P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q^{c}$. In the case of
conjunctions the results follow from the induction hypothesis and (FFEL4). In
the case of disjunctions the grammatical claim follows from the induction
hypothesis. For derivable equality we have:

$\displaystyle
f^{c}_{1}(P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q^{c},R^{\sf T})$
$\displaystyle=P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}f^{c}_{1}(Q^{c},R^{\sf T})$ by
definition
$\displaystyle=P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(Q^{c}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{\sf T})$ by induction
hypothesis
$\displaystyle=P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(Q^{c}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(R^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T}))$ by Lemma A.1
$\displaystyle=(P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}Q^{c})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(R^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}{\sf T})$ by Lemma 2.6.3
$\displaystyle=(P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}Q^{c})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{\sf T}.$ by Lemma A.1

∎

######  Lemma A.8.

For any $P,Q\in\textup{FNF}$, $f^{c}(P,Q)$ is in FNF and

$\textup{$\textrm{EqFFEL}$}\vdash
f^{c}(P,Q)=P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q.$

###### Proof.

By the four preceding lemmas it suffices to show that $f^{c}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{*},R^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}S^{*})$ is in FNF and that
$\textup{$\textrm{EqFFEL}$}\vdash f^{c}(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{*},R^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}S^{*})=(P^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}Q^{*})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(R^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}S^{*})$. By (FFEL4), in turn, it
suffices to prove that $f^{c}_{3}(P^{*},Q^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{*})$ is a $*$-term and that
$\textup{$\textrm{EqFFEL}$}\vdash f^{c}_{3}(P^{*},Q^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}R^{*})=P^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(Q^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{*})$. We prove this by
induction on the number of $\ell$-terms in $R^{*}$. In the base case we have
that $f^{c}_{3}(P^{*},Q^{\sf
T}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{\ell})=f^{c}_{1}(P^{*},Q^{\sf
T})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R^{\ell}$. The results follow
from Lemma A.7 and (FFEL4).

For the inductive cases we assume that the results hold for all $*$-terms with
fewer $\ell$-terms than
$R^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}S^{d}$ and
$R^{*}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}S^{c}$. For conjunctions the
result follows from the induction hypothesis and (FFEL4) and for disjunctions
it follows from Lemma A.7 and (FFEL4). ∎

Theorem 2.9. For any $P\in{\mathcal{SP}_{\\!A}}$, $f(P)$ terminates,
$f(P)\in\textup{FNF}$ and $\textup{$\textrm{EqFFEL}$}\vdash f(P)=P$.

###### Proof.

By induction on the complexity of $P$. If $P$ is an atom, the result is by
(FFEL5) and (FFEL6). If $P$ is ${\sf T}$ or ${\sf F}$ the result is by
identity. For the induction we assume that the result holds for all FEL-terms
of lesser complexity than
$P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q$ and
$P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q$. The result now follows from
the induction hypothesis, Lemma A.3, Lemma A.8 and (FFEL2). ∎

Correctness of $\bm{g}$.

Theorem 2.18. For all $P\in\textup{FNF}$, $g(\mathit{fe}(P))=P$, i.e.
$g(\mathit{fe}(P))$ is syntactically equal to $P$ for $P\in\textup{FNF}$.

###### Proof.

We first prove that for all ${\sf T}$-terms $P$, $g^{\sf
T}(\mathit{fe}(P))=P$, by induction on $P$. In the base case $P={\sf T}$ and
we have $g^{\sf T}(\mathit{fe}(P))=g^{\sf T}({\sf T})={\sf T}=P$. For the
inductive case we have
$P=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q^{\sf T}$ and

$\displaystyle g^{\sf T}(\mathit{fe}(P))$ $\displaystyle=g^{\sf
T}(\mathit{fe}(Q^{\sf T})\unlhd a\unrhd\mathit{fe}(Q^{\sf T}))$ by definition
of $\mathit{fe}$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}g^{\sf T}(\mathit{fe}(Q^{\sf
T}))$ by definition of $g^{\sf T}$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q^{\sf T}$ by induction
hypothesis $\displaystyle=P.$

Similarly, we see that for all ${\sf F}$-terms $P$, $g^{\sf
F}(\mathit{fe}(P))=P$, by induction on $P$. In the base case $P={\sf F}$ and
we have $g^{\sf F}(\mathit{fe}(P))=g^{\sf F}({\sf F})={\sf F}=P$. For the
inductive case we have
$P=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf F}$ and

$\displaystyle g^{\sf F}(\mathit{fe}(P))$ $\displaystyle=g^{\sf
F}(\mathit{fe}(Q^{\sf F})\unlhd a\unrhd\mathit{fe}(Q^{\sf F}))$ by definition
of $\mathit{fe}$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}g^{\sf F}(\mathit{fe}(Q^{\sf
F}))$ by definition of $g^{\sf F}$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf F}$ by induction
hypothesis $\displaystyle=P.$

Now we check that for all $\ell$-terms $P$, $g^{\ell}(\mathit{fe}(P))=P$. We
observe that either
$P=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T}$ or $P=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T}$. In the first case we
have

$\displaystyle g^{\ell}(\mathit{fe}(P))$
$\displaystyle=g^{\ell}(\mathit{fe}(Q^{\sf T})\unlhd a\unrhd\mathit{fe}(Q^{\sf
T})[{\sf T}\mapsto{\sf F}])$ by definition of $\mathit{fe}$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}g^{\sf T}(\mathit{fe}(Q^{\sf
T}))$ by definition of $g^{\ell}$
$\displaystyle=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T}$ as shown above
$\displaystyle=P.$

In the second case we have that

$\displaystyle g^{\ell}(\mathit{fe}(P))$
$\displaystyle=g^{\ell}(\mathit{fe}(Q^{\sf T})[{\sf T}\mapsto{\sf F}]\unlhd
a\unrhd\mathit{fe}(Q^{\sf T}))$ by definition of $\mathit{fe}$
$\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}g^{\sf T}(\mathit{fe}(Q^{\sf
T}))$ by definition of $g_{\ell}$ $\displaystyle=\neg
a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q^{\sf T}$ as shown above
$\displaystyle=P.$

We now prove that for all $*$-terms $P$, $g^{*}(\mathit{fe}(P))=P$, by
induction on $P$ modulo the complexity of $\ell$-terms. In the base case we
are dealing with $\ell$-terms. Because an $\ell$-term has neither a cd nor a
dd we have $g^{*}(\mathit{fe}(P))=g^{\ell}(\mathit{fe}(P))=P$, where the first
equality is by definition of $g^{*}$ and the second was shown above. For the
induction we have either
$P=Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R$ or
$P=Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}R$. In the first case note that
by Theorem 2.15, $\mathit{fe}(P)$ has a cd and no dd. So we have

$\displaystyle g^{*}(\mathit{fe}(P))$
$\displaystyle=g^{*}(\textup{cd}_{1}(\mathit{fe}(P))[\triangle_{1}\mapsto{\sf
T},\triangle_{2}\mapsto{\sf
F}])~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}g^{*}(\textup{cd}_{2}(\mathit{fe}(P)))$ by definition of $g^{*}$
$\displaystyle=g^{*}(\mathit{fe}(Q))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}g^{*}(\mathit{fe}(R))$ by Theorem
2.15
$\displaystyle=Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R$ by induction hypothesis
$\displaystyle=P.$

In the second case, again by Theorem 2.15, $\mathit{fe}(P)$ has a dd and no
cd. So we have that

$\displaystyle g^{*}(\mathit{fe}(P))$
$\displaystyle=g^{*}(\textup{dd}_{1}(\mathit{fe}(P))[\triangle_{1}\mapsto{\sf
T},\triangle_{2}\mapsto{\sf
F}])~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}g^{*}(\textup{dd}_{2}(\mathit{fe}(P)))$ by definition of $g^{*}$
$\displaystyle=g^{*}(\mathit{fe}(Q))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}g^{*}(\mathit{fe}(R))$ by Theorem
2.15
$\displaystyle=Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}R$ by induction hypothesis
$\displaystyle=P.$

Finally, we prove the theorem’s statement by making a case distinction on the
grammatical category of $P$. If $P$ is a ${\sf T}$-term, then $\mathit{fe}(P)$
has only ${\sf T}$-leaves and hence $g(\mathit{fe}(P))=g^{\sf
T}(\mathit{fe}(P))=P$, where the first equality is by definition of $g$ and
the second was shown above. If $P$ is an ${\sf F}$-term, then $\mathit{fe}(P)$
has only ${\sf F}$-leaves and hence $g(\mathit{fe}(P))=g^{\sf
F}(\mathit{fe}(P))=P$, where the first equality is by definition of $g$ and
the second was shown above. If $P$ is a ${\sf T}$-$*$-term, then it has both
${\sf T}$ and ${\sf F}$-leaves and hence, letting
$P=Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R$,

$\displaystyle g(\mathit{fe}(P))$ $\displaystyle=g^{\sf
T}(\textup{tsd}_{1}(\mathit{fe}(P))[\triangle\mapsto{\sf
T}])~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}g^{*}(\textup{tsd}_{2}(\mathit{fe}(P)))$ by definition of $g$
$\displaystyle=g^{\sf
T}(\mathit{fe}(Q))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}g^{*}(\mathit{fe}(R))$ by Theorem
2.17
$\displaystyle=Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R$ as shown above
$\displaystyle=P,$

which completes the proof. ∎

##  Appendix B Proofs - Section 4

In order to show that the relation $=_{\mathit{mfe}}$ is indeed a congruence,
we first repeat a part of [6, La.3.3], except that we generalise its clause 5
to clause 2 below.888The proof of clause 5 of [6, La.3.3] (p.266) contains two
errors in Case $c=a$, correct is: “and by induction $L_{a}(X_{1}[{\sf
T}\mapsto Y])=L_{a}(X_{1})[{\sf T}\mapsto L_{a}(Y)]=L_{a}(X)[{\sf T}\mapsto
L_{a}(Y)]$” (cf. Case $b=a$ in the proof below and take $Z={\sf F}$).

######  Lemma B.1.

For all $a\in A$, $f\in\\{L,R\\}$ and $X,Y,Z\in\mathcal{T}_{A}$,

$1.$

$\mathit{m}(f_{a}(X[{\sf T}\mapsto{\sf F},{\sf F}\mapsto{\sf
T}]))=\mathit{m}(f_{a}(X))[{\sf T}\mapsto{\sf F},{\sf F}\mapsto{\sf T}]$,

$2.$

$f_{a}(X[{\sf T}\mapsto Y,{\sf F}\mapsto Z])=f_{a}(X)[{\sf T}\mapsto
f_{a}(Y),{\sf F}\mapsto f_{a}(Z)]$,

###### Proof.

Clause 1 is Lemma 3.3.4 in [6]. We prove clause 2 by induction on the
structure of $X$. The base cases are trivial.

If $X=X_{1}\unlhd b\unrhd X_{2}$, distinguish the cases $b=a$ and $b\neq a$:
Case $b=a$, subcase $f=L$: $L_{a}(X[{\sf T}\mapsto Y,{\sf F}\mapsto
Z])=L_{a}(X_{1}[{\sf T}\mapsto Y,{\sf F}\mapsto Z])$ and by induction,
$L_{a}(X_{1}[{\sf T}\mapsto Y,{\sf F}\mapsto Z])=L_{a}(X_{1})[{\sf T}\mapsto
L_{a}(Y),{\sf F}\mapsto L_{a}(Z)]$. By $L_{a}(X)=L_{a}(X_{1})$, we are done.
The other subcase $f=R$ follows in a similar way.
Case $b\neq a$, subcase $f=L$:

$\displaystyle L_{a}(X[{\sf T}\mapsto Y,{\sf F}\mapsto Z])$
$\displaystyle=L_{a}(X_{1}[{\sf T}\mapsto Y,{\sf F}\mapsto Z])\unlhd b\unrhd
L_{a}(X_{2}[{\sf T}\mapsto Y,{\sf F}\mapsto Z])$
$\displaystyle\stackrel{{\scriptstyle\text{IH}}}{{=}}L_{a}(X_{1})[{\sf
T}\mapsto L_{a}(Y),{\sf F}\mapsto L_{a}(Z)]\unlhd b\unrhd L_{a}(X_{2})[{\sf
T}\mapsto L_{a}(Y),{\sf F}\mapsto L_{a}(Z)]$ $\displaystyle=L_{a}(X)[{\sf
T}\mapsto L_{a}(Y),{\sf F}\mapsto L_{a}(Z)].$

The other subcase $f=R$ follows in a similar way. ∎

Lemma 4.4. The relation $=_{\mathit{mfe}}$ is a congruence.

###### Proof.

Define $\text{$\widetilde{\neg}$}X:\mathcal{T}_{A}\to\mathcal{T}_{A}$ and
$X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}}
\end{picture}}Y,~{}X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){{$\widetilde{\vee}$}}
\put(-0.46,1.3){\circle*{0.7}}
\end{picture}}Y:\mathcal{T}_{A}\times\mathcal{T}_{A}\to\mathcal{T}_{A}$ by

$\displaystyle\text{$\widetilde{\neg}$}X$ $\displaystyle=X[{\sf T}\mapsto{\sf
F},{\sf F}\mapsto{\sf T}],$
$\displaystyle~{}X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y$ $\displaystyle=X[{\sf
T}\mapsto Y,{\sf F}\mapsto Y[{\sf T}\mapsto{\sf F}]],$ $\displaystyle
X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){{$\widetilde{\vee}$}}
\put(-0.46,1.3){\circle*{0.7}} \end{picture}}Y$ $\displaystyle=X[{\sf
T}\mapsto Y[{\sf F}\mapsto{\sf T}],{\sf F}\mapsto Y].$

Hence, $\text{$\widetilde{\neg}$}(\mathit{fe}(P))=\mathit{fe}(\neg P)$,
$\mathit{fe}(P)~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}}
\end{picture}}(Q)=\mathit{fe}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q)$, and
$\mathit{fe}(P)~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){{$\widetilde{\vee}$}}
\put(-0.46,1.3){\circle*{0.7}}
\end{picture}}\mathit{fe}(Q)=\mathit{fe}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}Q)$. It suffices to show that for
$X,Y\in\mathcal{T}_{A}$, if $\mathit{m}(X)=\mathit{m}(X^{\prime})$ and
$\mathit{m}(Y)=\mathit{m}(Y^{\prime})$, then
$\mathit{m}(\text{$\widetilde{\neg}$}X)=\mathit{m}(\text{$\widetilde{\neg}$}X^{\prime})$,
$\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}}
\end{picture}}Y)=\mathit{m}(X^{\prime}~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y^{\prime})$, and
$\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){{$\widetilde{\vee}$}}
\put(-0.46,1.3){\circle*{0.7}}
\end{picture}}Y)=\mathit{m}(X^{\prime}~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){{$\widetilde{\vee}$}}
\put(-0.46,1.3){\circle*{0.7}} \end{picture}}Y^{\prime})$.

The case for $\text{$\widetilde{\neg}$}X$ follows by case distinction on the
form of $X$. The base cases $X\in\\{{\sf T},{\sf F}\\}$ are trivial, and if
$X=X_{1}\unlhd a\unrhd X_{2}$, then $\mathit{m}(X)=\mathit{m}(X^{\prime})$
implies that $X^{\prime}=X_{1}^{\prime}\unlhd a\unrhd X_{2}^{\prime}$ for some
$X_{1}^{\prime},X_{2}^{\prime}\in\mathcal{T}_{A}$, and

$\mathit{m}(L_{a}(X_{1}))=\mathit{m}(L_{a}(X_{1}^{\prime}))\quad\text{and}\quad\mathit{m}(R_{a}(X_{2}))=\mathit{m}(R_{a}(X_{2}^{\prime})).$
(Aux3)

Write $\bm{[\textit{{\small neg}}]}$ for the leaf replacement $[{\sf
T}\mapsto{\sf F},{\sf F}\mapsto{\sf T}]$ and derive

$\displaystyle\mathit{m}(\text{$\widetilde{\neg}$}X)$
$\displaystyle=\mathit{m}((X_{1}\unlhd a\unrhd X_{2})\bm{[\textit{{\small
neg}}]})$ $\displaystyle=\mathit{m}(L_{a}(X_{1}\bm{[\textit{{\small
neg}}]}))\unlhd a\unrhd\mathit{m}(R_{a}(X_{2}\bm{[\textit{{\small neg}}]}))$
$\displaystyle=\mathit{m}(L_{a}(X_{1}^{\prime}\bm{[\textit{{\small
neg}}]}))\unlhd a\unrhd\mathit{m}(R_{a}(X_{2}^{\prime}\bm{[\textit{{\small
neg}}]}))$ by La.B.1.1 and (Aux3)
$\displaystyle=\mathit{m}(\text{$\widetilde{\neg}$}X^{\prime}).$

The case for
$\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}}
\end{picture}}Y)=\mathit{m}(X^{\prime}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Y^{\prime})$: for readability we
split the proof obligation into two parts.

(A)
$\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}}
\end{picture}}Y)=\mathit{m}(X^{\prime}~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y)$. This follows by induction
on the depth of $X$. The base cases $X\in\\{{\sf T},{\sf F}\\}$ are simple:
note that if $X={\sf T}$ and $\mathit{m}(X)=\mathit{m}(X^{\prime})$, then
$X^{\prime}={\sf T}$ and we are done, and similarly if $X={\sf F}$.

If $X=X_{1}\unlhd a\unrhd X_{2}$ and $\mathit{m}(X)=\mathit{m}(X^{\prime})$,
then by (Aux3), $X^{\prime}=X_{1}^{\prime}\unlhd a\unrhd X_{2}^{\prime}$ for
some $X_{1}^{\prime},X_{2}^{\prime}\in\mathcal{T}_{A}$ with
$\mathit{m}(L_{a}(X_{1}))=\mathit{m}(L_{a}(X_{1}^{\prime}))$ and
$\mathit{m}(R_{a}(X_{2}))=\mathit{m}(R_{a}(X_{2}^{\prime}))$. Write

$\displaystyle\bm{[\textit{{\small fulland} $Y$}]}$ $\displaystyle\text{ for
$[{\sf T}\mapsto Y,{\sf F}\mapsto Y[{\sf T}\mapsto{\sf F}]]$},$
$\displaystyle\bm{[\textit{{\small fulland} $L_{a}(Y)$}]}$
$\displaystyle\text{ for $[{\sf T}\mapsto L_{a}(Y),{\sf F}\mapsto
L_{a}(Y)[{\sf T}\mapsto{\sf F}]]$},$ $\displaystyle\bm{[\textit{{\small
fulland} $R_{a}(Y)$}]}$ $\displaystyle\text{ for $[{\sf T}\mapsto
R_{a}(Y),{\sf F}\mapsto R_{a}(Y)[{\sf T}\mapsto{\sf F}]]$}.$

Derive

$\displaystyle\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y)$
$\displaystyle=\mathit{m}((X_{1}\unlhd a\unrhd
X_{2})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y)$
$\displaystyle=\mathit{m}(X_{1}\bm{[\textit{{\small fulland} $Y$}]}\unlhd
a\unrhd X_{2}\bm{[\textit{{\small fulland} $Y$}]})$
$\displaystyle=\mathit{m}(L_{a}(X_{1}\bm{[\textit{{\small fulland}
$Y$}]}))\unlhd a\unrhd\mathit{m}(R_{a}(X_{2}\bm{[\textit{{\small fulland}
$Y$}]}))$ $\displaystyle=\mathit{m}(L_{a}(X_{1})\bm{[\textit{{\small fulland}
$L_{a}(Y)$}]})\unlhd a\unrhd\mathit{m}(R_{a}(X_{2})\bm{[\textit{{\small
fulland} $R_{a}(Y)$}]})$ by La.B.1.2
$\displaystyle=\mathit{m}(L_{a}(X_{1})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}L_{a}(Y))\unlhd
a\unrhd\mathit{m}(R_{a}(X_{2})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}R_{a}(Y))$
$\displaystyle=\mathit{m}(L_{a}(X_{1}^{\prime})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}L_{a}(Y))\unlhd
a\unrhd\mathit{m}(R_{a}(X_{2}^{\prime})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}R_{a}(Y))$ by IH and (Aux3)
$\displaystyle=...=\mathit{m}(X^{\prime}~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y).$

(B)
$\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}}
\end{picture}}Y)=\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y^{\prime})$. This follows by
induction on the depth of $X$. The base cases $X\in\\{{\sf T},{\sf F}\\}$ are
trivial. If $X=X_{1}\unlhd a\unrhd X_{2}$ derive

$\displaystyle\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y)$
$\displaystyle=\mathit{m}((X_{1}\unlhd a\unrhd
X_{2})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y)$
$\displaystyle=\mathit{m}(X_{1}\bm{[\textit{{\small fulland} $Y$}]}\unlhd
a\unrhd X_{2}\bm{[\textit{{\small fulland} $Y$}]})$
$\displaystyle=\mathit{m}(L_{a}(X_{1}\bm{[\textit{{\small fulland}
$Y$}]}))\unlhd a\unrhd\mathit{m}(R_{a}(X_{2}\bm{[\textit{{\small fulland}
$Y$}]}))$ $\displaystyle=\mathit{m}(L_{a}(X_{1})\bm{[\textit{{\small fulland}
$L_{a}(Y)$}]})\unlhd a\unrhd\mathit{m}(R_{a}(X_{2})\bm{[\textit{{\small
fulland} $R_{a}(Y)$}]})$ by La.B.1.2
$\displaystyle=\mathit{m}(L_{a}(X_{1})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}L_{a}(Y))\unlhd
a\unrhd\mathit{m}(R_{a}(X_{2})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}R_{a}(Y))$
$\displaystyle=\mathit{m}(L_{a}(X_{1})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}L_{a}(Y^{\prime}))\unlhd
a\unrhd\mathit{m}(R_{a}(X_{2})~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}R_{a}(Y^{\prime}))$ by IH
$\displaystyle=...=\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){$\widetilde{\wedge}$}
\put(-0.66,-0.1){\circle*{0.7}} \end{picture}}Y^{\prime}).$

The proof for the case
$\mathit{m}(X~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){{$\widetilde{\vee}$}}
\put(-0.46,1.3){\circle*{0.7}}
\end{picture}}Y)=\mathit{m}(X^{\prime}~{}\mathbin{\begin{picture}(1.6,1.8)(-0.4,0.0)\put(-0.8,0.0){{$\widetilde{\vee}$}}
\put(-0.46,1.3){\circle*{0.7}} \end{picture}}Y^{\prime})$ is similar. ∎

For the continuation of the proof of Lemma 4.6, we use results about short-
circuit connectives and the memorising short-circuit evaluation function
$\mathit{mse}(P)=\mathit{m}(\mathit{se}(P))$ defined in [6] (which is
available online); for the function $\mathit{m}$ see Definition 4.2 and below
we recall the definition of the short-circuit evaluation function
$\mathit{se}$. In particular, we use the definability of the connectives
${~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}}$ and
${~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}}$ in short-circuit logic (cf.
Section 7).

Given a set of atoms $A$, the set ${\mathcal{S}_{A}}$ of closed terms with
short-circuit connectives is defined by the following grammar ($a\in A$):

$P::={\sf T}\mid{\sf F}\mid a\mid\neg P\mid
P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}P\mid
P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}} \end{picture}}P.$

For $a\in A$, the evaluation function
$\mathit{se}:{\mathcal{S}_{A}}\to\mathcal{T}_{A}$ and the translation function
$\mathit{t}:{\mathcal{SP}_{\\!A}}\to{\mathcal{S}_{A}}$ are defined by

$\displaystyle\mathit{se}({\sf T})={\sf T},~{}\mathit{se}({\sf F})={\sf
F},~{}~{}$ $\displaystyle\mathit{t}({\sf T})={\sf T},~{}~{}\mathit{t}({\sf
F})={\sf F},$ $\displaystyle\mathit{se}(a)={\sf T}\unlhd a\unrhd{\sf F},$
$\displaystyle\mathit{t}(a)=a,~{}$ $\displaystyle\mathit{se}(\neg
P)=\mathit{se}(P)[{\sf T}\mapsto{\sf F},{\sf F}\mapsto{\sf T}],~{}$
$\displaystyle\mathit{t}(\neg P)=\neg(\mathit{t}(P)),~{}$
$\displaystyle\mathit{se}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}Q)=\mathit{se}(P)[{\sf
T}\mapsto\mathit{se}(Q)],$
$\displaystyle\mathit{t}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}Q)=(\mathit{t}(P)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}}
\end{picture}}(\mathit{t}(Q)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}{\sf
F}))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}\mathit{t}(Q),$
$\displaystyle\mathit{se}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}} \end{picture}}Q)=\mathit{se}(P)[{\sf
F}\mapsto\mathit{se}(Q)],$
$\displaystyle\mathit{t}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}Q)=(\mathit{t}(P)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}}
\end{picture}}(\mathit{t}(Q)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}} \end{picture}}{\sf
T}))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}} \end{picture}}\mathit{t}(Q).$

######  Lemma B.2.

For all $P\in{\mathcal{SP}_{\\!A}}$,
$\mathit{fe}(P)=\mathit{se}(\mathit{t}(P))$.

###### Proof.

By structural induction on $P$. The base cases are immediate, and so is
$\mathit{fe}(\neg P)=\mathit{se}(\mathit{t}(\neg P))$.

For the case
$P=Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R$, derive

$\displaystyle\mathit{se}(\mathit{t}(P))$
$\displaystyle=\mathit{se}((\mathit{t}(Q)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}}
\end{picture}}(\mathit{t}(R)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}{\sf
F}))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}\mathit{t}(R))$
$\displaystyle=\mathit{se}(\mathit{t}(Q)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}}
\end{picture}}(\mathit{t}(R)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}{\sf F}))[{\sf
T}\mapsto\mathit{se}(\mathit{t}(R))]$
$\displaystyle=(\mathit{se}(\mathit{t}(Q))[{\sf
F}\mapsto\mathit{se}(\mathit{t}(R)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}} \end{picture}}{\sf F})])[{\sf
T}\mapsto\mathit{se}(\mathit{t}(R))].$
$\displaystyle=(\mathit{se}(\mathit{t}(Q))[{\sf
F}\mapsto\mathit{se}(\mathit{t}(R))[{\sf T}\mapsto{\sf F}])[{\sf
T}\mapsto\mathit{se}(\mathit{t}(R))]$
$\displaystyle=\mathit{se}(\mathit{t}(Q))[{\sf
T}\mapsto\mathit{se}(\mathit{t}(R)),~{}{\sf
F}\mapsto\mathit{se}(\mathit{t}(R))[{\sf T}\mapsto{\sf F}][{\sf
T}\mapsto\mathit{se}(\mathit{t}(R))]]$
$\displaystyle=\mathit{se}(\mathit{t}(Q))[{\sf
T}\mapsto\mathit{se}(\mathit{t}(R)),~{}{\sf
F}\mapsto\mathit{se}(\mathit{t}(R))[{\sf T}\mapsto{\sf F}]]$ by redundancy,
$\mathit{se}(\mathit{t}(R))[{\sf T}\mapsto{\sf F}]$ has no ${\sf T}$-leaves
$\displaystyle=\mathit{fe}(Q)[{\sf T}\mapsto\mathit{fe}(R),{\sf
F}\mapsto\mathit{fe}(R)[{\sf T}\mapsto{\sf F}]]$ by IH
$\displaystyle=\mathit{fe}(P).$

The case
$P=Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}R$ follows in a similar way. ∎

###### Continuation of the proof of Lemma 4.6.

For a variable $v\in\\{x,y,z\\}$, define $\mathit{t}(v)=v$. It follows with
_Prover9_ that

$\textup{$\textrm{EqMSCL}$}\vdash\mathit{t}((x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}y)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}z)=\mathit{t}((\neg
x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}z))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}z)),$ (46)

where EqMSCL consists of the axioms (Mem1)–(Mem5) in Table 4, see Comment B.3
below. From [6, Thm.4.1] it follows that for all $P,Q\in{\mathcal{S}_{A}}$,
$\textup{$\textrm{EqMFEL}$}\vdash
P=Q\Longrightarrow\mathit{m}(\mathit{se}(P))=\mathit{m}(\mathit{se}(Q))$.
Hence, for all $P,Q,R\in{\mathcal{SP}_{\\!A}}$,

$\mathit{m}(\mathit{se}(\mathit{t}((P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}Q)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}R)))=\mathit{m}(\mathit{se}(\mathit{t}((\neg
P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}R))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R)))),$

so, what has to be proved, i.e.,

$\mathit{m}(\mathit{fe}((P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}Q)~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R))=\mathit{m}(\mathit{fe}((\neg
P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}R))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}R))),$

follows from Lemma B.2. ∎

######  Comment B.3.

A proof with _Prover9_ ’s options lpo and unfold, and with as assumptions the
five axioms of EqMSCL was obtained in 0.02s. The syntax of the proven goal for
_Prover9_ , that is, the $\mathit{t}$()-translation of (46) where `^,v,`',1,0
stand for
${~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\wedge$}
\put(-0.54,-0.2){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,-0.2){\circle{0.6}}
\end{picture}}},~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.54,1.54){{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color<EMAIL_ADDRESS>\put(-0.54,1.54){\circle{0.6}} \end{picture}},\neg,{\sf T},{\sf F}$, is:

    (((x ^ (y v 1)) v y) v (z ^ 0)) ^ z =
      (((x’ v (((y v (z ^ 0)) ^ z) ^ 0)) ^ ((y v (z ^ 0)) ^ z)) ^ (((x v (z ^ 0)) ^ z) v 1))
    v ((x v (z ^ 0)) ^ z).

##  Appendix C Proofs - Section 6

We start with two auxiliary lemmas.

######  Lemma C.1.

$\textup{$\textrm{EqMFEL}$}\vdash(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}y)=(x~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(y~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}x)$.

###### Proof.

With _Prover9_ with options lpo and unfold: 0.2s. ∎

######  Lemma C.2.

For all $\beta\in A^{s}_{o}$ and $P\in{\mathcal{SP}_{\\!A}}$ such that
$\alpha(P)\subset\\{\beta\\}$,
$\textup{$\textrm{EqMFEL}$}\vdash\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})=\widetilde{}{\sf
F}_{\beta}$.

###### Proof.

By induction on the length of $\beta$. The base case $\beta=\epsilon$ is
trivial.

For $\beta=a\gamma~{}(a\in A)$, thus $\widetilde{}{\sf
F}_{\beta}=a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\widetilde{}{\sf F}_{\gamma}$, we
apply structural induction on $P$, and we note that from Lemma 2.6.3 and
$\widetilde{}{\sf F}_{\gamma}=\widetilde{}{\sf
F}_{\gamma}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}$ it follows that

$\widetilde{}{\sf
F}_{\beta}=(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}\widetilde{}{\sf F}_{\gamma}.$
(C.$\dagger$)

The base cases: 1) the case $P\in\\{{\sf T},{\sf F}\\}$ is trivial; 2) if
$P=a$, then by (C.$\dagger$) and the dual of $\eqref{C1}$, $\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})=((a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}\widetilde{}{\sf
F}_{\gamma})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})=\widetilde{}{\sf
F}_{\beta}$; 3) if $P\in\\{\gamma\\}$, then by (C.$\dagger$),
$\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})=((a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}\widetilde{}{\sf
F}_{\gamma})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})=(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}(\widetilde{}{\sf
F}_{\gamma}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))\stackrel{{\scriptstyle\text{IH}}}{{=}}(a~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}\widetilde{}{\sf
F}_{\gamma}=\widetilde{}{\sf F}_{\beta}$.

If $P=\neg P_{1}$, then $\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}(\neg
P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})\stackrel{{\scriptstyle\eqref{FFEL8}}}{{=}}\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})\stackrel{{\scriptstyle\text{IH}}}{{=}}\widetilde{}{\sf F}_{\beta}$.

If
$P=P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P_{2}$, then $\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}((P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}P_{2})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F})=\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}((P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(P_{2}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))\stackrel{{\scriptstyle\eqref{C4}^{\prime}}}{{=}}\\\ (\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}(\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P_{2}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))\stackrel{{\scriptstyle\text{IH}}}{{=}}\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}\widetilde{}{\sf
F}_{\beta}=\widetilde{}{\sf F}_{\beta}$, where $\eqref{C4}^{\prime}$ is the
dual of (C4).

If
$P=P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}P_{2}$, then $\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}((P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}P_{2})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})\stackrel{{\scriptstyle\eqref{M1}}}{{=}}\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}((\neg
P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(P_{2}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))\stackrel{{\scriptstyle\text{La.\ref{la:feqs}.1}}}{{=}}\\\
\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}((P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}(P_{2}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf F}))=(\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}((P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}P_{2})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}(\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))\stackrel{{\scriptstyle(pc),\text{IH}}}{{=}}\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}} \end{picture}}\widetilde{}{\sf
F}_{\beta}=\widetilde{}{\sf F}_{\beta}$,
where (pc) refers to the previous case
$P=P_{1}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P_{2}$. ∎

###### Continuation of the proof of Lemma 6.7.

1\. Let $P,Q\in{\mathcal{SP}_{\\!A}}$. We have to prove that

$\mathit{mfe}(\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q))=\mathit{mfe}(\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P)),$

where $\beta\in A^{s}_{o}$ satisfies
$\\{\beta\\}=\alpha(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q)$. By soundness of EqMFEL
(Lemma 4.6), it suffices to prove that for any $\beta\in A^{s}_{o}$ that
satisfies $\alpha(P)\subset\\{\beta\\}$,

$\textup{$\textrm{EqMFEL}$}\vdash\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q)=\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P).$

Derive

$\displaystyle\textup{$\textrm{EqMFEL}$}\vdash\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q)$
$\displaystyle=(\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F}))~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q)$ by Lemma C.2
$\displaystyle=\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}((P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}Q))$
$\displaystyle=\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}((P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}{\sf
F})~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P))$ by Lemma C.1
$\displaystyle=\widetilde{}{\sf
F}_{\beta}~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.0){$\vee$}
\put(-0.42,1.4){\circle*{0.6}}
\end{picture}}(Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P).$ (as above)

2\. The soundness of $\textup{$\textrm{C$\ell$FEL}$}^{\sf U}$ follows as in 1,
the additional case is that for any $P\in{\mathcal{SP}_{\\!A}}^{\\!{\sf
U}}\setminus{\mathcal{SP}_{\\!A}}$ and $Q\in{\mathcal{SP}_{\\!A}}^{\\!{\sf
U}}$,
$\mathit{clfe}(P~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}}
\end{picture}}Q)=\mathit{clfe}(Q~{}\mathbin{\begin{picture}(1.4,1.8)(-0.3,0.0)\put(-0.6,0.2){$\wedge$}
\put(-0.46,0.0){\circle*{0.6}} \end{picture}}P)={\sf U}.$ ∎