\section{Reflection: why is it possible?} \label{intl}

%Before discussing Display Logic and the availability in it
%of a method for imitating a subterm rewrite capability,
We now try to elucidate the aspects of these logics
which make the subterm rewrite capabilities possible.

The technique for rewriting in LPF can be explained and justified in terms of
Window Inference.
In Window Inference, as described by Robinson \& Staples \cite{wi},
one could transform an expression such as
$(A \to B) \land C$ to an equivalent expression by focussing on $A$, and
transforming it to an expression $A'$, where, under the assumptions 
$\lnot B$ and $C$, $A $ is equivalent to $ A'$.
Grundy \cite{jgwi} shows how this could be extended from equivalence to any
pre-order, and discusses the extension to non-classical logics;
he has also implemented it (for classical logic) in HOL \cite{jgwimp}.

We can fit the results on LPF into the Window Inference framework.
The following results are in the format of window rules \cite[\S3.4]{jgwi}.
$$ \frac 
{x \sqsubseteq y}
{g(x, \ldots) \sqsubseteq g(y, \dots)}
\qquad \qquad 
%\qquad (g \mbox{ as in Lemma \ref{lpflem})}
%$$
%$$
\frac
{p \sqsubseteq q}
{p \Longrightarrow q}
%\qquad (p \mbox{ and $q$ boolean)}
$$
where $g$ is as in Lemma \ref{lpflem}
and $p$ and $q$ are boolean.
These two results combine to give Lemma \ref{lpflem}.
Window Inference using these rules is equivalent to the procedure we have
described.
It should be noted that these window rules do not introduce any contextual
assumptions.

It seems much more difficult to formulate, in terms of Window Inference,
the mothod we will describe for rewriting in Display Logic.
This is because, in Display Logic, although we ``focus'' on a sub-expression,
the logical steps used always involve the \emph{whole} expression 
(usually a variant of it obtained using the display postulates,
but an expression of roughly the same size).

The following discussion may help to indicate the underlying
differences between the methods.

Consider a group (of which an example would be
real \emph{invertible} $n \times n$ matrices),
with the multiplication operation `$*$'.
Given an equation $A = B * C$, we can ``display'' $B$ by rewriting
the equation as $A * C^{-1} = B$, making use of the invertibility of $C$.
Suppose we also have an equality (which may be a general rule instantiated),
$B = D$.
Then we can use the transitivity of equality to replace $B$ by $D$,
and reverse the transformation by which we displayed $B$, thus:
\begin{center}
\vpf
\bpf
\A "$A = B * C$"
\U "$A * C^{-1} = B$" 
\A "$B = D$"
\B "$A * C^{-1} = D$" 
\U "$A = D * C$"
\epf
\end{center}

Now consider a semigroup (of which an example would be \emph{all}
real $n \times n$ matrices, with the multiplication operation).
Here we cannot take the inverse of a given element.
However, given the equality $B = D$,
we can multiply both sides by $C$ to get $B * C = D * C$,
and prove the same result thus:
\begin{center}
\vpf
\bpf
\A "$A = B * C$"
\A "$B = D$"
\U "$B * C = D * C$" 
\B "$A = D * C$"
\epf
\end{center}

This second proof uses the congruence of equality, in the form
$$ \frac {B = D \qquad C = C'} {B * C = D * C'} $$
In that way the method used strongly resembles the method used for LPF,
where there is repeated use of rules of the form 
$$ \frac {\texttt{rep}(B,D) \qquad \texttt{rep}(C,C')}
{\texttt{rep}(B \textit{ op } C,D \textit{ op } C')} $$

The method of the first proof above
has some similarity to the method used for Display Logic,
in that a selected subterm is ``displayed'' and transformed, and then
the steps used to ``display'' the subterm are reversed.
However, Display Logic does not have equalities or inverses;
the ability to display a chosen subterm relies on the other features of
the underlying logics that enable residuation, as discussed in 
\S\ref{DL-resid}.