
\hyphenation{
 assump-tion
 in-volves
 non-classical
 conn-ection
 typi-cally
 tradi-tional
 frame-works
 con-clusion
 deriv-ation
}

%% Here begins the main text

\section{Introduction} \label{s-intro}

% this section should be an intro to the topics generally

In calculi for logical entailment, \emph{Craig interpolation} is the property
that for any entailment $A \vdash B$ between formulae, there exists an
\emph{interpolant} formula $I$ such that $A \vdash I$ and $I \vdash B$ are
both entailments of the calculus, while $I$ mentions only those variables or
nonlogical constants that are common to both $A$ and $B$.  It has long been
known that there are close connections between interpolation and other
central logical concerns (see e.g.~\cite{Feferman:08}); indeed, one of
Craig's original applications of interpolation was to give a new proof of
Beth's Definability Theorem~\cite{Craig:57-2}.  More recently, though, it has
transpired that interpolation has significant applications in program
verification as well.  For example, 
% it turns out to be very useful 
in inferring the invariants of program loops~\cite{McMillan:08}, and
% has also been centrally employed
in model checking ~\cite{Caniart:10}.

Recently, Brotherston and Gor\'e~\cite{brotherston-gore-interpolation}
gave a modular
proof of interpolation for a class of propositional substructural logics,
based on Belnap's \emph{display logic}~\cite{belnap-display}.  Roughly
speaking, display calculi are two-sided sequent calculi equipped with a
richer-than-usual notion of sequent structure and a principle by which
sequents can be rearranged so as to ``display'' any chosen substructure as
the \emph{entire} left or right hand side (much like rearranging a
mathematical equation for a chosen variable).  The main attraction of
display calculi is Belnap's general cut-elimination result,
which says that cut-elimination holds for any display calculus whose rules
satisfy 8 easily verifiable syntactic conditions.  Cut-elimination is
generally essential to the standard proof-theoretic approach to
interpolation, which is to proceed by induction on cut-free derivations.
Despite the availability of a general cut-elimination result, however, there
seem to have been no proofs on interpolation based on display calculi prior
to~\cite{brotherston-gore-interpolation},
probably due to the inherent complexity of
their sequent structure and display principles. Indeed, in line with this
general expectation, Brotherston and Gor\'e's proof is very technical,
involving many case distinctions, and many intricate properties of
substitutions. 
Moreover, due to space restrictions, most of the proofs are only sketched,
leaving the potential for errors.
Thus it makes sense to verify these intricate details using an interactive
theorem prover, to give us greater confidence in their very general
interpolation theorems.

In this paper, we report on the Isabelle formalisation of their results.
We discuss the difficulties in formalising their proofs and
describe the consequent differences between their proofs and ours.
We also highlight the usefulness of a programmable user interface.


Isabelle is an automated proof assistant.  % \cite{isabelle-ref}.
Its meta-logic is an intuitionistic typed higher-order logic, sufficient
to support the built-in inference steps of higher-order unification
and term rewriting.  Isabelle accepts inference rules of the form
$\alpha_1, \alpha_2, \ldots, \alpha_n, \Longrightarrow \beta$
where the $\alpha_i$ and $\beta$ are expressions of the Isabelle
meta-logic, or are expressions using a new syntax, defined by the
user, for some ``object logic''. Most users build on one of the
comprehensive ``object logics'' already supplied,
like Isabelle/HOL % \cite{IsLogHOL},
which is an Isabelle theory based on the higher-order
logic of Church % \cite{church-types}
HOL offers inductively defined sets, and recursive datatypes, which we use
extensively.  

% We assume the reader is familiar with basic
% proof-theory, ML and Isabelle/HOL.
% %
In the paper we show some Isabelle code, edited
to use mathematical symbols.
In it, a `\verb|?|' precedes a variable name.
The Appendix gives the actual Isabelle text
of many definitions and theorems.
Our Isabelle code can be found at
\url{http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/interp/}.  
HOW MANY LINES FOR THIS WORK?

%TO DO - include explanation of Isabelle notation

In Section~\ref{sec:preliminaries}, we briefly describe Display Logic,
and the system defined in \cite{brotherston-gore-interpolation}.
We % briefly introduce the Isabelle theorem prover, and
outline our approach to proving interpolation for the Display Logic system of 
\cite{brotherston-gore-interpolation}.

\input{jb_sec2}
%
\section{Interpolation for Display Calculi}
\label{sec:preliminaries}
% this section should be an intro to the system and work of Brotherston and
% Gor\'e

% Brotherston and Gor\'e \cite{brotherston-gore-interpolation}
% define a system containing structural connectives
% `;' (binary), `\#' (unary) and $\emptyset$ (nullary).
% They give display postulates sufficient to display any substructure;
% the form of their display postulates also builds in commutativity of `;` 
% on both left and right of consecutions.
% 
% They give structural rules for associativity, unit-weakening, 
% unit-contraction, contraction and weakening.
%  In our work the rules for associativity, unit-weakening and unit-contraction
% are often needed and we assume that they are always present.

In traditional sequent calculi, it is fairly straightforward to decorate each
rule with interpolants by building up the interpolant for the conclusion
sequent from the interpolants for the premise sequents.
this approach is harder in display calculi since the sequent $X \vdash Y$ 
goes through many transformations while displaying some substructure $Z$.
Brotherston \& Gor\'e therefore consider the following (LADI) property
\cite[Definition~3.4]{brotherston-gore-interpolation}:

(LADI): a rule with premises $\mathcal C_i$ and conclusion $\mathcal C$
satisfies the local $AD$ display interpolation property (LADI),
if given that, for all premises $\mathcal C_i$,
all sequents $\mathcal C_i'$ such that 
$\mathcal C_i' \equiv_{AD} \mathcal C_i$ satisfy the interpolation property,
all sequents $\mathcal C'$ such that 
$\mathcal C' \equiv_{AD} \mathcal C$ satisfy the interpolation property.

Although Brotherston and Gor\'e \cite{brotherston-gore-interpolation}
give the separate variants of the logical connectives 
$\top, \bot, \land$ and $\lor$ for the 
additive and multiplicative forms of the logical introduction rules,
we just use one connective for each of $\top, \bot, \land$ and $\lor$.
Although the additive and multiplicative forms are equivalent in the presence
of contraction and weakening, 
\cite{brotherston-gore-interpolation} contains results which 
are relevant to the situation where not all structural rules are included.
Thus they prove results for the both rules shown below,
even though the second rule is much easier to deal with.
$$
\frac{ X \vdash A \quad Y \vdash B}
{X, Y \vdash A \land B}
\qquad
\frac{ X \vdash A \quad X \vdash B}
{X \vdash A \land B}
$$
In the work described here, we first considered the second (additive) rule 
shown; we subsequently developed a proof dealing with the first 
(multiplicative) rule directly.

\section{The Isabelle mechanisation}

Our mechanisation builds on the work of Dawson \& Gor\'e 
\cite{dawson-gore-cut-admissibility} in formalising Display Logic. 
Some of our notation and choices of properties, lemmas, etc, are attributable
to this.  In particular, we use \texttt{Comma}, \texttt{Star} and \texttt{I}
for `;', `\#' and `$\emptyset$'.

The work in \cite{dawson-gore-cut-admissibility} is a deep embedding of rules
and of the variables in them, and we have followed that approach here
(see \cite{dawson-gore-gls} for our understanding of what this means,
and for more details).
That is, we define a language of formulae and structures, which
contains explicit structure and formula variables, for which we define explicit
substitution functions.
We also define the rules as specific data structures
(of which there is a small finite number,
such as those in Figure~\ref{f-rules}),
and infinitely many substitution instances of these rules.

\subsection{Formalising Display Logic in Isabelle}

An actual derivation in a Display Calculus involves structures
containing formulae which are composed of primitive propositions
(which we typically represent by $p,q,r$).  It uses rules which are
\emph{expressed} using structure and formula variables, typically
$X,Y,Z$ and $A,B,C$ respectively, to represent structures and formulae
made up from primitive propositions.  
We are using a ``deep embedding'' of variables, so 
our Isabelle formulation explicitly represents variables such as
$X,Y,Z$ and $A,B,C$, and defines substitution for them of 
given structures and formulae, which may themselves contain variables.
In our Isabelle formulation we use 
\texttt{SV} \textit{name} and \texttt{FV} \textit{name} to represent
formula and structure variables.
The constructor \texttt{PP} represents a primitive proposition variable $p$.

Formulae are therefore represented by the datatype
below:
% in Figure~\ref{fig:isabelle-formulae}. 
\begin{verbatim}
datatype formula = Btimes formula formula ("_ && _" [68,68] 67)
 | Bplus formula formula ("_ v _" [64,64] 63)
 | Bneg formula ("--_" [70] 70)  
 | Btrue ("T") | Bfalse("F") 
 | FV string | PP string 
\end{verbatim}

Structures are represented by the datatype below:
\begin{verbatim}
datatype structr = Comma structr structr 
 | Star structr | I | Structform formula | SV string   
\end{verbatim}
The operator \texttt{Structform} ``casts'' a formula into
a structure, since a formula is a special case of a structure.

The notation in parentheses in the definition of datatype
\texttt{formula}
%Figure~\ref{fig:isabelle-formulae}
describe an alternative infix syntax, closer to normal logical
syntax.  Some complex manipulation of the syntax, available
through Isabelle's ``parse translations'' and ``print translations'',
allows structure variables and constants to be prefixed by the symbol
\texttt{\$}, and the notations \texttt{FV}, \texttt{SV} and
\texttt{Structform} to be omitted. 

Sequents and rules are represented by the Isabelle/HOL
datatypes:
\begin{verbatim}
datatype sequent = Sequent structr structr 
datatype rule = Rule (sequent list) sequent 
\end{verbatim}

\texttt{Rule prems concl}
means a rule with list of premises \texttt{prems} and conclusion \texttt{concl}.  
A sequent \texttt{(Sequent X Y)} can also be represented as
\texttt{\$X |- \$Y}. Thus the term \texttt{Sequent (SV ''X'')
  (Structform (FV ''A''))} is printed, and may be entered, as
\texttt{(\$''X'' |- ''A'')}. 

Since a ``deep'' embedding requires handling substitution explicitly,
we defined functions to substitute for structure and
formula variables, in structures, sequents and rules. 
In particular, we have a operator
\begin{verbatim}
rulefs :: "rule set => rule set"
\end{verbatim}
where \texttt{rulefs} \textit{rules} is the set of substitution instances of
rules in the set \textit{rules}.
Also, when we refer to derivability using a set of rules,
this allows inferences using substitution instances of these rules,
and \texttt{derivableR} \textit{rules sequents} means the set of sequents which
can be derived from \textit{sequents} using \textit{rules}, instantiated.
\begin{verbatim}
derivableR  :: "rule set => sequent set => sequent set
\end{verbatim}

We also use some general functions to describe derivability,
for which we had many useful lemmas.  
A more detailed expository account of these is given in \cite{gore-india}.

\begin{verbatim}
types 'a psc = "'a list * 'a"       (* single step inference *)
consts
  derl      :: "'a psc set => 'a psc set"
  derrec    :: "'a psc set => 'a set => 'a set"
\end{verbatim}

\noindent
An inference rule of type \texttt{'a psc} is a list of premises \texttt{ps}
and a conclusion \texttt{c}. Then
\texttt{derl rls} is the set of
rules derivable from the rule set \texttt{rls} while
\texttt{derrec rls prems}
is the set of sequents derivable using rules \texttt{rls}
from the set \texttt{prems} of premises.  
We defined these using Isabelle's package for inductively defined sets.

Note that these functions do not envisage instantiation of rules.
In fact, we have the following relationship
between \texttt{derivableR} and \texttt{derrec},
using a function \texttt{PC}, defined as shown, to translate between types.
\begin{verbatim}
"PC (Rule ?prems ?concl) = (?prems, ?concl)"
"derivableR ?rules == derrec (PC ` rulefs ?rules)"
\end{verbatim}

The ``deep embedding'' approach to rules enables us
to express properties of rules, such as that no structure
variable appears in both antecedent and succedent positions; 
some of our lemmas apply to all display postulates satisfying conditions of
this sort.
We used this in \cite{dawson-gore-cut-admissibility} in showing that 
cut-admissibility applies whenever the structural rules were all of a
particular form (as in Belnap's cut elimination theorem).  
In regards to interpolation, possible future work may include showing that
interpolation results hold whenever rules are of a particular form, 
but our present work (except for some lemmas) do not do this.

The work in \cite{dawson-gore-cut-admissibility} is also a deep embedding of
proofs (where we took proof objects and explicitly manipulated them) but we
have \emph{not} done that here.

\subsection{Definitions relating to interpolation}


We define the following sets of rules:
\begin{description}
\item[\rm \texttt{dps}:] is the set of six display postulates
  in~\cite[Definition 2.5]{brotherston-gore-interpolation}
  (Display-equivalence)
\item[\rm \texttt{aidps}:] is \texttt{dps}, their inverses, and the
  associativity rule (ie, 13 rules)
\item[\rm \texttt{ilrules}:] is the unit-contraction and unit-weakening
  rules
\item[\rm \texttt{rlscf}:] is the set of all rules of the logic as
  shown in \cite[Figures 1 and 3]{brotherston-gore-interpolation},
  plus \texttt{aidps} (but, to shorten the verification task,
  we omitted the rules for implication $\to$)
\item[\rm \texttt{rlscf\_nw}:] is as \texttt{rlscf}, but excluding the
weakening rule
\end{description}


We define several predicates to do with interpolation:
\begin{verbatim}
interp :: "rule set => sequent => formula => bool"
edi :: "rule set => rule set => sequent => bool"
ldi :: "rule set => rule set => sequent list * sequent => bool"
cldi :: "rule set => rule set => sequent list * sequent => bool"
\end{verbatim}

\texttt{interp} \textit{rules} $(X \vdash Y)$ \textit{intp}
says that \texttt{intp} is an interpolant for $X \vdash Y$,
ie, that $X \vdash intp$ and $intp \vdash Y$ are derivable
(using \textit{rules})
and that the (formula) variables in $intp$ are among the formula variables of
the structures $X$ and $Y$.

\texttt{edi} \textit{lrules drules} $(X \vdash Y)$
(\emph{Extended Display Interpolation})
says that for all sequents $X' \vdash Y'$ from which $X \vdash Y$
is derivable using \textit{lrules},
$X' \vdash Y'$ has an interpolant (defined in terms of derivability using
\textit{drules})
(\textit{lrules} would typically be a set of display postulates)

\texttt{ldi} \textit{lrules drules} $(ps, c)$
(\emph{Local Display Interpolation})
says that the rule $(ps, c)$ preserves the property \texttt{edi}: that is,
if, for all $p \in ps$, \texttt{edi} \textit{lrules drules} $p$ holds,
then \texttt{edi} \textit{lrules drules} $c$ holds.
That is, if \texttt{lrules} is the set $AD$ of rules (our \texttt{aidps}),
and \texttt{drules} is the set of rules of the logic,
then the local $AD$-interpolation (LADI) property as defined in 
\cite[Definition 3.4]{brotherston-gore-interpolation}, for rule $(ps, c)$,
is that \texttt{ldi} \textit{lrules aidps} $(ps, c)$ holds.

Note that none of these definitions involves a condition that $X \vdash Y$ be
derivable.  
Of course, cut-admissibility would imply that if $X \vdash Y$ has an
interpolant then $X \vdash Y$ is derivable, but we avoid proving or using
cut-admissibility.
Even so, in most cases we do not need such a condition.
However we do need $X \vdash Y$ in the case of a
sequent $I \vdash Y, \#X$ produced by weakening and displaying $I$.
Thus we need a predicate with that condition:

\texttt{cldi} \textit{lrules drules} $(ps, c)$ 
(\emph{Conditional Local Display Interpolation})
says that if $c$ is is derivable using \textit{drules}, then 
\texttt{ldi} \textit{lrules drules} $(ps, c)$ holds.

However we also need variants of these predicates, called 
\texttt{interpn}, \texttt{edin}, \texttt{ldin} and \texttt{cldin},
where the derivation of interpolated sequents is from a given set of rules,
rather than from given rules and their substitution instances.
We use these in some subsequent lemmas which involve rule sets which are not
closed under substitution.

We mention here that many of our lemmas about these properties 
assume, although we do not specifically say so, that $AD$ (rule set
\texttt{aidps}) is used as $lrules$ in the above definitions,
and that the derivation rules, $drules$ in the above definitions,
contain the $AD$ rules.

Lemma 3.5 of \cite{brotherston-gore-interpolation} 
says that if all rules satisfy the local $AD$-interpolation property,
then the calculus has the interpolation property.
In fact the stronger result, Lemma~\ref{ldi-derl-cldi-ei}\ref{ldi-derl}
is true, that LADI is preserved under derivation.
But for the conditional local display interpolation property, 
a result analogous to the first-mentioned, only, of these results holds:
see Lemma~\ref{ldi-derl-cldi-ei}\ref{cldi-ex-interp}>
\begin{lemma}[\texttt{ldi\_derl, cldi\_ex\_interp}] \label{ldi-derl-cldi-ei}
\begin{enumerate}
\item \label{ldi-derl}
if a set of rules each
satisfies the local display interpolation property,
then so does a rule derived from them
\item \label{cldi-ex-interp}
if all the derivation rules satisfy the 
conditional local $AD$-interpolation property,
then the calculus has the interpolation property
\end{enumerate}
\end{lemma}

\subsection{Substitution of congruent occurrences} \label{s-cong}
In \cite[Lemmas 3.6, 3.7]{brotherston-gore-interpolation}
the concept of congruent occurrences of some structure $Z$ is used,
with substitution for such congruent occurrences.
Where two sequents $\mathcal C$ and $\mathcal C'$
are related by a display postulate, or sequence of them, 
a particular occurrence of $Z$ in $\mathcal C$ will correspond to 
a particular occurrence of $Z$ in $\mathcal C'$,
according to the sequence of display postulates used to obtain
$\mathcal C'$ from $\mathcal C$.

This concept looked rather difficult to define and express
precisely and formally
(we note that the in the notation in \cite{brotherston-gore-interpolation}, 
$\mathcal C[Z/A] \equiv_{AD} \mathcal C'[Z/A]$,
the meanings of $\mathcal C[Z/A]$ and $\mathcal C'[Z/A]$ depend on each other).

So we adopted the alternative approach, used successfully in 
\cite{dawson-gore-cut-admissibility}: 
rather than trying to define $\mathcal C'[Z/A]$ we would prove 
that there exists a sequent (call it $\mathcal C'_{Z/A}$)
satisfying $\mathcal C[Z/A] \equiv_{AD} \mathcal C'_{Z/A}$
and safisfying the property that some occurrences of $A$ in $\mathcal C'$
are replaced by $Z$ in $\mathcal C'_{Z/A}$.
This approach turned out to be sufficient for all the proofs discussed in this
paper.

In the proofs of cut-elimination in \cite{dawson-gore-cut-admissibility}
we defined and used a relation \texttt{seqrep},
defined as follows.
\begin{verbatim}
seqrep : "bool => structr => structr => (sequent * sequent) set"
\end{verbatim}
\begin{definition}[\texttt{seqrep}]
$(U, V) \in \texttt{seqrep}\ b\ X\ Y$ means that
some (or all or none) of the occurrences of $X$ in $U$ are replaced by $Y$
in $V$; otherwise $X$ and $Y$ are the same; the occurrences of $X$ which are
replaced by $Y$ must all be in succedent or antecedent position according to
whether $b$ is true or false
\end{definition}

For this we write $U\ ^X\!\!\leadsto^Y V$,
 where the appropriate value of $b$ is understood.

Analogous to Lemma 3.9 we proved the following result
about derivation using a set of inference rules satisfying:
\begin{itemize}
\item their conclusions do not contain formulae 
\item their structure variables are distinct
\item (Belnap's $C4$ condition)
when the conclusion and a premise of a rule both contain a structure variable,
then both occurrences are in antecedent or both are in succedent positions
\end{itemize}
(in Lemma 3.9 this sset of rules is the $AD$ rules).

\begin{lemma}[\texttt{SF\_some\_sub}] \label{SF-some-sub}
Where, for a formula $F$ and structure $Z$,
\begin{itemize}
\item ``derivable'' means using a set of rules satisfying the conditions above
\item if \texttt{concl} is derivable from \texttt{prems}
\item if \texttt{concl} $^F\!\!\leadsto^Z$  \texttt{sconcl}
\end{itemize}
then there exists a list \texttt{sprems} such that
\begin{itemize}
\item \texttt{sconcl} is derivable from \texttt{sprems}
\item if \texttt{prem$_n$} and \texttt{sprem$_n$}
are corresponding members of \texttt{prems} and \texttt{sprems},
then \texttt{prem$_n$} $^F\!\!\leadsto^Z$ \texttt{sprem$_n$}
\end{itemize}
\end{lemma}

Note that although we will use this where \texttt{?rules} is a set of display
postulates, this theorem does not require that the rules have only a single
premise.

The proof of this result used some results proved previously for
the cut-elimination work \cite{dawson-gore-cut-admissibility},
notably \texttt{extSubs}, which gives, essentially, a constructive expression
for \texttt{sprems}..

\subsection{Local Display Interpolation for Unary Rules} \label{s-unary}

Proposition 3.10 of \cite{brotherston-gore-interpolation} 
covers the display postulates, the associativity rule,
and the nullary or unary logical introduction rules.

The first case ($(\equiv_D)$, that is, any sequence of display postulates) of 
\cite[Proposition 3.10]{brotherston-gore-interpolation}
is covered by the following result (which holds independent of the choice of
set of derivation rules).

\begin{lemma}[\texttt{bi\_lrule\_ldi\_lem}] \label{l-dp-ldi}
Let rule $\rho$ be a substitution instance of a rule in $AD$.
Then $\rho$ has the LADI property.
\end{lemma}

The cases $(Id)$, $(\top R)$ and $(\bot L)$ of Proposition 3.10
would be trivial if it were true that nothing else is
display-equivalent to their conclusions;
this is not so, but we can use this lemma:

\begin{lemma}[\texttt{non\_bin\_lem\_gen}] \label{non-bin-lem-gen}
Assume the derivation rules include the rules for $\lnot$.
Consider a substitution instance $\rho$ of a rule in $AD$, 
whose premise does not contain any comma.
Then, if the premise of $\rho$ has an interpolant then so does the
conclusion of $\rho$.
\end{lemma}

Since the conclusions of the three nullary rules
$(Id)$, $(\top R)$ and $(\bot L)$ clearly themselves have interpolants,
Lemma~\ref{non-bin-lem-gen} shows they satisfy the extended display
interpolation property, and so the rules have the LADI property.
\begin{proposition}
The rules $(Id)$, $(\top R)$ and $(\bot L)$ satisfy the LADI property.
\end{proposition}

% Recall that \texttt{aidps} is the set of all $AD$ rules,
% and \texttt{rlscf} is the set of all rules of the calculus.

The remaining cases of Proposition 3.10 are the logical introduction rules with
a single premise.

For these we use the four lemmas (of which one is shown)
\begin{lemma}[\texttt{sdA1}] \label{l-sdA1}
if $\displaystyle \frac{Y' \vdash U}{Y \vdash U}$ 
is a logical introduction rule, and $W\ ^Y\!\!\leadsto^{Y'} W'$,
then $\displaystyle \frac{W' \vdash Z}{W \vdash Z}$ 
is derivable (ie, using $AD$ and the logical introduction rules)
\end{lemma}

Then from these lemmas we get 
\begin{lemma}[\texttt{seqrep\_interpA}] \label{seqrep-interpA}
if $\displaystyle \frac{Y' \vdash U}{Y \vdash U}$
is a logical introduction rule, 
formula variables in $Y'$ also appear in $Y$,
$W \vdash Z \ ^Y\!\!\!\leadsto^{Y'} W' \vdash Z'$ (in antecedent positions),
and $I$ is an interpolant for $W' \vdash Z'$,
then $I$ is also an interpolant for $W \vdash Z$
\end{lemma}

Finally we get the following result which gives Proposition 3.10 for single
premise logical introduction rules.
\begin{proposition}[\texttt{logA\_ldi}]
if $\displaystyle \frac{Y \vdash U}{F \vdash U}$ ($F$ a formula)
is a logical introduction rule
where the formula variables in $Y$ are also in $F$,
then that rule satisfies the LADI property
\end{proposition}

This last result requires the use of \texttt{SF\_some\_sub} (above).
We have analogous results for a logical introduction rule 
for a formula on the right.
% are \texttt{seqrep\_interpS} and \texttt{logS\_ldi}.

\subsection{Binary Additive Logical Introduction Rules} \label{s-lair2}

We now discuss extending the results for unary logical introduction rules
to the binary rules in the additive form; that is, where the rule contains a
single structure variable which appears uniformly in the premises and
conclusion.

This involved, first, defining an analogue of \texttt{seqrep},
which we called \texttt{lseqrep}. As with \texttt{seqrep},
we use the notation
\textit{U} $^Y\!\!\leadsto^{Ys}$ \textit{Us} 

\begin{verbatim}
lseqrep : "bool => structr => structr list => (sequent * sequent list) set" 
\end{verbatim}

\begin{definition}[\texttt{lseqrep}] \label{d-lseqrep}
$(U, Us) \in \texttt{lseqrep}\ b\ Y\ Ys$ means that
there is some occurrence of $Y$ in $U$ such that 
the $n$th member of $Us$ is obtained from $U$ by changing the occurrence of $Y$
to the $n$th member of $Ys$
\end{definition}

Note that, in contrast to \texttt{seqrep},
this definition involves exactly one occurrence of $Y$ in $U$.

% This simplification,
% that the replacement applies to exactly one occurrence of $Y$ in $U$,
% simplified the proofs considerably compared with the previous proof of the
% theorem \texttt{extSubs}, however the complication, that we have lists
% $Ys$ and $Us$, rather than single structures, complicated the proofs
% considerably.
Thus we have a result \texttt{mextSubs} which is analogous to \texttt{extSubs},
a complicated result which gives, constructively, the \texttt{spremss} of the
following theorem.

From there we proved \texttt{SF\_some1sub}, 
analogous to \texttt{SF\_some\_sub}.
In this case the rules must satisfy a slightly stricter set of requirements:
\begin{itemize}
\item their conclusions do not contain formulae 
\item each premise contains the same structure variables, in antecedent
positions and in succedent positions, as the conclusion
\item the structure variables of the conclusion and of each premise 
are distinct
\end{itemize}

\begin{lemma}[\texttt{SF\_some1sub}]
Where, for a formula $F$ and list $Z$ of structures,
\begin{itemize}
\item ``derivable'' means using a set of rules satisfying the conditions above
\item if \texttt{concl} is derivable from \texttt{prems}
\item if \texttt{concl} $^F\!\!\leadsto^{Zs}$ \texttt{sconcls} 
\end{itemize}
then there exists \texttt{spremss}
(this is a list of lists of sequents) where

\begin{itemize}
 \item for each \texttt{prem$_n$} in \texttt{prems},
 let \texttt{sprems$_n$} be the corresponding member of \texttt{spremss},
then 
 \texttt{prem$_n$} $^F\!\!\leadsto^{Zs}$ \texttt{sprems$_n$} 
\item
each member of \texttt{sconcls} is derivable from the corresponding member of
each list in \texttt{spremss}
\end{itemize}
\end{lemma}

Then, corresponding to Lemma~\ref{l-sdA1} (\texttt{sdA1}) in \S\ref{s-unary},
we have a lemma \texttt{msdA1} (and its three more counterparts).
This is like Lemma~\ref{l-sdA1} except that,
in its statement, $Y'$ and $W'$ can be lists.

Then, corresponding to Lemma~\ref{seqrep-interpA} (\texttt{seqrep\_interpA}),
we have the following lemma: again, the difference is that 
in the statement of Lemma~\ref{seqrep-interpA},
we replace $Y'$ by a list of structures and $W' \vdash Z'$ by a list of
sequents.

\begin{lemma}[\texttt{lseqrep\_interpA}] \label{lseqrep-interpA}
if a logical introduction rule has conclusion ${Y \vdash U}$
and premises ${Y_i \vdash U}$ for $Y_i \in Ys$,
formula variables in each $Y_i$ also appear in $Y$,
$W \vdash Z \ ^Y\!\!\!\leadsto^{Ys} Ss$ (in antecedent positions),
and for each $S_i = W_i \vdash Z_i \in Ss$
there exists an interpolant,
then there exists an interpolant for $W \vdash Z$
\end{lemma}

There are two major cases in the proof:
all the sequents $W_i$ are the same, or all the sequents $Z_i$ are the same.
This is because the relation {S} $^{Z}\!\!\leadsto^{Zs}$ {Ss} 
means that there is exactly one location in $S$ where the $Ss$ differ from $S$.
In those cases the proof uses the conjunction or disjunction, respectively,
of a list of interpolants.
Of course this idea is taken from the proof of 
\cite[Theorem 3.10]{brotherston-gore-interpolation}. % (Binary Rules).

From there we get the result \texttt{mlogA\_ldi}, analogous to
\texttt{logA\_ldi}, which basically says that additive logical rules satisfy the
local display interpolation property.
Analogous results for a logical introduction rule for a formula on the right
are \texttt{lseqrep\_interpS} and \texttt{mlogS\_ldi}.
 
\begin{proposition}[\texttt{mlogA\_ldi}]
if a logical introduction rule has conclusion ${F \vdash U}$ ($F$ a formula),
and premises ${Y_i \vdash U}$ for $Y_i \in Ys$,
and formula variables in each $Y_i$ also appear in $Y$,
then that rule satisfies the LADI property
\end{proposition}

\section{Structural Rules} \label{s-struct}

At this point we have a general modus operandi for proving local display
interpolation for a given rule $\rho$, with premises $ps_\rho$ and conclusion
$c_\rho$: identify a relation $rel$ such that
\begin{enumerate}
\item \label{r1} $(ps_\rho, c_\rho) \in rel$
\item \label{r2} whenever $c \equiv_{AD} c_\rho$, we can find a list 
$ps$ (often got from sequents in $ps_\rho$ using the 
same sequence of display postulates which get $c$ from $c_\rho$)
such that $p \equiv_{AD} p_\rho$ for each $p \in ps$ and corresponding 
$p_\rho \in ps_\rho$
\item \label{r3} whenever $(ps, c) \in rel$, $c$ is derivable from $ps$ 
(not used except to prove \ref{r4})
\item \label{r4} whenever $(ps, c) \in rel$,
  and each $p \in ps$ has an interpolant, then $c$ has an interpolant 
(proof of this will normally use \ref{r3}) 
\end{enumerate}

\subsection{Local Display Interpolation for Unit-Contraction, Contraction}
\label{s-ldi-uc-ctr}

This is relatively easy for the unit-contraction rule:
the relation $rel$ is given by:  
$(p, c) \in rel$ if $p$ is obtained from $c$ by deleting, 
somewhere in $c$, some $\#^n\emptyset$,
and we get \ref{r2} using roughly the same
sequence of display postulates.

% We proved the local display interpolation property for the unit contraction
% rules and for the contraction rule.

\begin{lemma}[\texttt{ex\_box\_uc}]
if sequent $Cd$ is obtained from $C$ by deleting one occurrence of some
$\#^n \emptyset$, and if $Cd' \rightarrow_{AD}^* Cd$, then there exists 
$C'$, such that $C' \rightarrow_{AD}^* C$, and 
$Cd'$ is obtained from $C'$ by deleting one occurrence of $\#^n \emptyset$.
\end{lemma}

% We accidentally made the error of first proving
% \texttt{ex\_box\_uc'} (which swaps $C(Cd)$ with $C'(Cd')$)
% but subsequently discovered this was easier to prove anyway.
% But to fix the error we also needed \texttt{inv\_der\_aidps}.

The proof of this required a good deal of programming repetitive use
of complex tactics similar to (but less complex than)
those described in \S\ref{s-del}. 

The following lemma gives \ref{r3} of the general proof method above.
\begin{lemma}[\texttt{delI\_der}]
If $(p, c) \in rel$ (defined above), and if the derivation rules include
$AD$ and the unit contraction rules, then $c$ is derivable from $p$
\end{lemma}

\begin{proposition}[\texttt{ldi\_ila, ldi\_ils}]
The unit contraction rules satisfy LADI. % the LADI property.
\end{proposition}

For the case of contraction, we defined a relation \texttt{mseqctr}:
$(C, C') \in \texttt{mseqctr}$ means that
$C'$ is obtained from $C$, by contraction of
substructures $(X,X)$ to $X$. 
Contractions may occur (of different substructures) in several places or
none.

\begin{lemma}[\texttt{ex\_box\_ctr}]
if sequent $Cd$ is obtained from $C$ by contraction(s) of substructure(s),
and if $Cd' \rightarrow_{AD}^* Cd$, then there exists 
$C'$, such that $C' \rightarrow_{AD}^* C$, and 
$Cd'$ is obtained from $C'$ by substructure contraction(s).
\end{lemma}

The proof of \texttt{ex\_box\_ctr} is a little more complex
that that for unit-contraction, because 
(for example) when 
$X; Y \vdash Z \equiv_{AD} X \vdash Z; \#Y$, and
$X; Y \vdash Z$ is obtained by contracting $(X; Y) ; (X; Y) \vdash Z$,
we need to show $(X; Y) ; (X; Y) \vdash Z \equiv_{AD} X;X \vdash Z; \#(Y;Y)$.

\begin{lemma}[\texttt{ctr\_der}]
If $(p, c) \in \texttt{mseqctr}$ (defined above),
and if the derivation rules include
$AD$ and the left contraction rule, then $c$ is derivable from $p$
\end{lemma}

\begin{proposition}[\texttt{ldi\_cA}]
The left contraction rule satisfies the LADI property.
\end{proposition}

% (Note that the system of \cite{brotherston-gore-interpolation}
% does not give a rule for contraction on the right, 
% it is derived from the rule for contraction on the left). 

\subsection{Lemma 4.2 (Deletion Lemma)} \label{s-del}

For weakening or unit-weakening, it is more difficult:
a sequence of display postulates applied to the conclusion
$X; \emptyset \vdash Y$ may give $\emptyset \vdash Y; \# X$,
so the same or similar sequence cannot be applied to the premise $X \vdash Y$.

For this situation we need Lemma 4.2 (Deletion Lemma):
this result says that for
$F$ a formula sub-structure occurrence in $C$, or $F = \emptyset$,
and $C \rightarrow_{AD}^* C'$,
then (in the usual case) $C \setminus F \rightarrow_{AD}^* C' \setminus F$,
where $C \setminus F$ and $C' \setminus F$ mean
deleting only particular occurrence(s) of $F$ in $C$,
and deleting the \emph{congruent} 
(corresponding) occurrence(s) of $F$ in $C'$,
where congruence is determined
by the course of the derivation of $C'$ from $C$.

We did not define congruent occurrences in this sense:
see the general discussion of this issue in \S\ref{s-cong}.
We thought it would be easier to define and use a relation \texttt{seqdel},
where $(C, C') \in \texttt{seqdel} ~\textit{Fs}$ means that
$C'$ is obtained from $C$ by deleting one
occurrence in $C$ of a structure in the set \textit{Fs}.

Then we proved the following result about deletion of a formula:

\begin{lemma}[\texttt{deletion}]
Let $F$ be a formula or $F = \emptyset$.
If sequent $Cd$ is obtained from $C$ by deleting an occurrence of some $\#^iF$,
and if $C \rightarrow_{AD}^* C'$, then either
\begin{enumerate}
\item
there exists $Cd'$, such that $Cd \rightarrow_{AD}^* Cd'$, and 
$Cd'$ is obtained from $C'$ by deleting an occurrence of some $\#^jF$, or
\item 
$C'$ is of the form $\#^nF \vdash \#^m (Z_1 ; Z_2)$ or 
 $\#^m (Z_1 ; Z_2) \vdash \#^nF$, where
 $Cd \rightarrow_{AD}^* (Z_1 \vdash \# Z_2)$, or 
 $Cd \rightarrow_{AD}^* (\# Z_1 \vdash Z_2)$
\end{enumerate}
\end{lemma}

Thus the premise is that $Cd$ is got from $C$ by deleting
instance(s) of the substructure formula $F$, possibly with some \# symbols.
%
The main clause of the result says that there exists $Cd'$
(this corresponds to $C' \setminus F$ in \cite{brotherston-gore-interpolation})
which is got from $Cd$ by deleting instance(s) of $\#^nF$ (for some $n$),
but there is also an exceptional case where $\#^nF$ is alone
on one side of the sequent.

The proof of this result required considerable ML programming of proof tactics.
The file \texttt{Del.ML} is devoted to these tactics and the intermediate
results proved for the proof of Lemma 4.2.

When we get cases as to the last rule used in the derivation 
$C \rightarrow_{AD}^* C'$, this gives 13 possibilities (``main cases'').

For each rule there are two main cases for the shape of the sequent 
after the preceding rule applications:
in the first, $\#^nF$ appears in $\#^nF, Z$ or $Z, \#^nF$
and so could be deleted ($F$ is ``delible''), and 
in the second,
the relevant occurrence of $\#^nF$ is the whole of one side of the sequent.

Then where, in the case of the associativity rule for example,
the sequent which is $(X; Y) ; Z \vdash W$ (instantiated) has $F$ delible,
$\#^nF$ may be equal to $X,Y$ or $Z$, or may be delible from $X,Y,Z$ or $W$.
(Certain further cases, such as that $\#^nF$ is $(X ; Y)$,
get eliminated automatically using results such as 
\texttt{stars\_Sf\_not\_Comma}, below).
The tactics \texttt{dvitacs} have been written to provide one set of tactics
which handle all these cases. 
The key component is the recursive tactic \texttt{sdvitac} which searches for a
way of showing that $F$ is delible from a given sequent 
(say $X; (Y ; Z) \vdash W$, in the above example).
Without the possibility of programming a tactic of this sort in Standard ML,
each of these seven cases,
and a similar (less numerous) set of cases for each of the
other 12 main cases, would require its own separate proof.

For the second case, where $\#^nF$ is equal to one side of the sequent
($W$ in the above example),
a variety of tactics is required:
for those display rules which move the comma from one side to the other
the tactics \texttt{mdiatacs} works for all,
but the other cases have to be done individually.

The proof threw up a number of (logically) 
trivial cases which nonetheless needed particular results to be included
as lemmas to be used automatically in simplification, such as
that we cannot have $X; Y = \#^n F$, for $F$ a formula.

We then proved this result for $F = \emptyset$ instead of a formula,
to give a theorem \texttt{deletion\_I};
the changes required in the proof were trivial.

\subsection{Local Display Interpolation for Unit-Weakening and Weakening} 
  \label{s-ldi-wk}

To handle weakening in a similar way, we considered two separate rules,
one to weaken with instances of $\#^n \emptyset$ and one 
to change any instance of $\emptyset$ to any formula.
Thus, where $Y_\emptyset$ means a structure like $Y$ but with every formula or
structure variable in it changed to $\emptyset$, a weakening is produced as
shown:
$$ X \vdash Z \Longrightarrow
 X, Y_\emptyset \vdash Z \Longrightarrow
 X, Y \vdash Z$$ 

% \vspace{-3ex}
% \begin{center}
% \bpf
% \A "$X \vdash Z$"
% \U "$X, Y_\emptyset \vdash Z$"
% \U "$X, Y \vdash Z$" 
% \epf
% \end{center}

We first consider the second of these,
replacing any instance of $\emptyset$ with a structural atom,
that is, a formula or a structure variable
which are atomic so far as the structure language is concerned.

We use the relation \texttt{seqrepI str\_atoms}:
$(c, p) \in \texttt{seqrepI str\_atoms}$ means that some occurrences of
$\emptyset$ in $p$ are changed to structural atoms in $c$.

% Note that \texttt{$(C, Cd) \in $ seqrepI $Fs$} 
% means that some occurrences in $C$
% of structures in $Fs$ are replaced by $I$ in $Cd$.

\begin{lemma}[\texttt{ex\_box\_repI\_atoms}]
If sequent $C$ is obtained from $Cd$ by replacing $\emptyset$ by structural
atoms,
and if $C' \rightarrow_{AD}^* C$, then there exists 
$Cd'$, such that $Cd' \rightarrow_{AD}^* Cd$, and 
$C'$ is obtained from $Cd'$ by replacing $\emptyset$ by structural 
atoms.
\end{lemma}

For this relation, property \ref{r2} was quite easy to prove,
since exactly the same sequence of $AD$-rules can be used.

We proved that there are derived rules permitting replacing instances of 
$\emptyset$ by anything, and this gave us that such rules, where the
replacement structure is a formula or structure variable, have the 
the local display interpolation property.

\begin{lemma}[\texttt{seqrepI\_der}]
If the derivation rules include weakening and unit-contraction,
and $(c, p) \in \texttt{seqrepI}\ Fs$, 
ie some occurrences of $\emptyset$ in $p$ are
replaced by anything in $c$, then $c$ is derivable from $p$.
\end{lemma}

The next lemma gives the LADI property, not for a rule of the system,
but for inferences $([p], c)$ where $(c, p) \in \texttt{seqrepI str\_atoms}$.

\begin{proposition}[\texttt{ldi\_repI\_atoms}] \label{ldi-repI-atoms}
Where $(c, p) \in \texttt{seqrepI str\_atoms}$, 
ie some occurrences of $\emptyset$ in $p$ are
replaced by structural atoms in $c$, 
$([p], c)$ has the LADI property.  
\end{proposition}

Next we consider the structural rules allowing insertion of $\#^n \emptyset$.

We use the variant of the theorem \texttt{deletion} (see \S\ref{s-del})
which applies to deletion of $\emptyset$ rather than of a formula.

Then we show that % the result of
inserting occurrences of anything preserves derivability.
% although we need it only for inserting occurrences $\#^n \emptyset$.

\begin{lemma}[\texttt{seqwk\_der}]
If the derivation rules include weakening,
and $(c, p) \in \texttt{seqdel} Fs$, 
$c$ is obtained from $p$ by a weakening of a substructure,
then $c$ is derivable from $p$.
\end{lemma}

Then we need the result that such rules satisfy the local display interpolation
property.  
In this case, though, where a sequent containing $\emptyset$
is rearranged by the display postulates such that the $\emptyset$ 
is alone on one side (such as where
$X \vdash Y; \emptyset$ is rearranged to $X; \#Y \vdash \emptyset$),
then the LADI property requires using the derivability
of $X \vdash Y$ rather than the fact that $X \vdash Y$ satisfies LADI.
Thus we can prove only the conditional local display interpolation property.

\begin{proposition}[\texttt{ldi\_wkI}] \label{ldi-wkI}
Provided the conclusion is derivable, 
and assuming that the derivation rules include weakening, unit contraction,
$(\emptyset \vdash \top)$ and $(\bot \vdash \emptyset)$,
a rule allowing $\#^n\emptyset$-weakening of a substructure
satisfies the conditional LADI property.
\end{proposition}

From here we define a set of rules called \texttt{ldi\_rules},
which does not contain 
the weakening rules or the multiplicative binary logical rules,
but does contain the relations of Propositions~\ref{ldi-wkI} and
\ref{ldi-repI-atoms}. 
We have that all of its rules satisfy the conditional LADI property,
so the system has interpolants.
We show this gives a deductive system equivalent to the given set of rules
\texttt{rlscf}, which system therefore also has interpolants.
Details are similar to the derivation of Theorem~\ref{rlscf-nw-interp}.

\begin{theorem}[\texttt{rlscf\_interp}]
The system of substitutable rules \texttt{rlscf}
satisfies display interpolation
\end{theorem}

\section{Binary Multiplicative Logical Introduction rules}
\label{s-mult}
As discussed above, these were handled, indirectly, using the 
corresponding binary additive logical introduction rules, and weakening.
However the possibility arises of a system which doesn't have the weakening
rules and uses the multiplicative rules.
So in this section we deal with these rules directly.

We dealt with these rules in two stages ---
firstly, weakening in occurrences of $\#^n\emptyset$,
then changing any occurrence of $\emptyset$ to any structural atom,
as shown below.

\vspace{-3ex}
\begin{center}
\bpf
\A "$X \vdash A$"
\U "$X, Y_\emptyset \vdash A$" "$wk_\emptyset^*$"
\A "$Y \vdash B$"
\U "$X_\emptyset, Y \vdash B$" "$wk_\emptyset^*$"
\B "$X, Y \vdash A \land B$" "(\texttt{ands\_rep})"
\epf
\end{center}

Here $X_\emptyset$ and $Y_\emptyset$ mean the structures $X$ and $Y$,
with each structural atom (formula or uninterpreted structure variable)
replaced by $\emptyset$.
The first stage, the inferences labelled $wk_\emptyset^*$ above,
are obtained by repeatedly 
weakening by occurrences of $\#^n\emptyset$ in some substructure.
The second stage (for which we define the relation \texttt{ands\_rep}),
consists of changing the $X_\emptyset$ of one premise, and the $Y_\emptyset$
of the other premise, to $X$ and $Y$ respectively.
For the second of these stages, then, 
when any sequence of display postulates is applied to 
$X, Y \vdash A \land B$, the same sequence can be applied to the two premises,
$X, Y_\emptyset \vdash A$ and $X_\emptyset, Y \vdash B$.
This simplifies the proof of local display interpolation for these rules.

For the first stage we proceed as described for \S\ref{s-ldi-wk},
except that we have the result for a system containing the unit-weakening rules
rather than a general weakening rule, thus getting the theorem

\begin{proposition}[\texttt{ldi\_wkI\_alt}]
Provided the conclusion is derivable, 
and assuming that the derivation rules include unit weakening, unit contraction,
and the left and right introduction rules for $\top$ and $\bot$,
% why all of these - compare ldi_wkI ??
a rule allowing $\#^nI$-weakening of a substructure
satisfies the conditional LADI property.
\end{proposition}

The second stage consists of the rule shown as \texttt{ands\_rep}
in the diagram.
Considering the four points at the start of \S\ref{s-struct},
since any display postulate applied to the conclusion can be appplied to the
premises, we need to define a suitable relation between conclusion and premises
which is preserved by applying any display postulate to them.
%
For this we define a relation \texttt{lseqrepm} between sequents,
analgous to \texttt{lseqrep} discussed in \S\ref{s-lair2}:
\begin{verbatim}
lseqrepm      :: "(structr * structr list) set =>
    bool => [structr, structr list] => (sequent * sequent list) set"
\end{verbatim}

\begin{definition}[\texttt{lseqrepm, repnI\_atoms}]
\begin{enumerate}
\item 
$(U, Us) \in \texttt{lseqrepm}\ orel\ b\ Y\ Ys$ means that
(as for \texttt{lseqrep}) there is one occurrence of $Y$ in $U$ which
is replaced by the $n$th member of $Ys$ in the $n$th member of $Us$;
this occurrence is at an antecedent or succedent position, according to whether
$b$ is \texttt{True} or \texttt{False}.
However elsewhere in $U$, each structural atom $A$ in $U$ is replaced by 
the $n$th member of $As$ in the $n$th member of $Us$, where
$(A, As) \in orel$;
\item 
$(A, As) \in \texttt{repnI\_atoms}$ iff one of the $As$ is $A$ and the rest of
the $As$ are $\emptyset$.
\end{enumerate}
\end{definition}

We use \texttt{lseqrepm} only with $orel = \texttt{repnI\_atoms}$.
%
For example, for the ($\land$R) rule, we use
$\texttt{lseqrepm\ repnI\_atoms\ True}\ (A \land B)\ [A, B]$ 
as the relation $rel$ of the four points at the start of \S\ref{s-struct}.
%
We get the following lemmas.

\begin{lemma}[\texttt{repm\_some1sub}]
Whenever $Y$ is a formula, and $(U, Us) \in \texttt{lseqrepm}\ orel\ b\ Y\ Ys$,
and $U$ is manipulated by a display
postulate (or sequence of them) to give $V$,
then the $Us$ can be manipulated by the same display postulate(s)
to give $Vs$ (respectively), where $(V, Vs) \in rel$
\end{lemma}

The following lemmas refer to derivation in the system
containing the \texttt{ands\_rep} rule (not the regular ($\land$R) rule),
and also unit-weakening and unit-contraction.

\begin{lemma}[\texttt{ands\_mix\_gen}]
Whenever $(V, Vs) \in rel$, then $V$ can be derived from the $Vs$.
\end{lemma}

As with Lemma~\ref{lseqrep-interpA}, this lemma relies on taking 
the conjunction or disjunction of interpolants of premises.
So the next two results require a deductive system containing 
the \texttt{ands\_rep} and \texttt{ora\_rep} rules, and also the
($\lor$R) and ($\land$L) rules.

\begin{lemma}[\texttt{lseqrepm\_interp\_andT}]
Whenever $(V, Vs) \in rel$, then we can construct an interpolant for $V$
from interpolants for the $Vs$
\end{lemma}

\begin{proposition}[\texttt{ldin\_ands\_rep}]
The rule \texttt{ands\_rep} satisfies LADI.
\end{proposition}

We then defined a set of rules called \texttt{ldi\_add} which contains
the rules of Definition 2.4 and
Figures 1 and 3 of \cite{brotherston-gore-interpolation},
except the weakening rule and the binary logical rules
$(\lor L)$ and $(\land R)$, with the rule \texttt{ands\_rep} (see diagram
above) and a corresponding rule \texttt{ora\_rep} included.
Note that these latter rules are not closed under substitution; therefore we
defined \texttt{ldi\_add} to consist of the rules, including their
substitution instances where relevant.
(Note that, as mentioned earlier, our formalisation had not included the
connective $\to$, or any rules for it).
Meanwhile we also defined the set \texttt{rlscf\_nw} of substitutable rules,
the rules of Definition 2.4 and Figures 1 and 3
of \cite{brotherston-gore-interpolation}, except weakening.


\begin{lemma}[\texttt{ldi\_add\_equiv}]
Let $C$ be the calculus consisting of the rules of Definition~2.4 and
Figures~1 and~3 of~\cite{brotherston-gore-interpolation} minus the
weakening rule. Then
the calculi
$C \setminus \{(\land\mathrm{R}), (\lor\mathrm{L})\}$ and
$C \cup \{\mathtt{ands\_rep}, \mathtt{ora\_rep}\}$
are deductively equivalent.
\end{lemma} 

\begin{theorem}[\texttt{ldi\_add\_interp, rlscf\_nw\_interp}]
\label{rlscf-nw-interp}
\begin{enumerate}
\item the system \texttt{ldi\_add} satisfies display interpolation
\item the system of substitutable rules
  \texttt{rlscf\_nw} satisfies display interpolation
\end{enumerate}
\end{theorem}

\begin{proof}
We have all rules in \texttt{ldi\_add} satisfying at least the conditional
local display interpolation property (\texttt{ldi\_add\_cldin}).
By \texttt{cldin\_ex\_interp}, this gives us that the system \texttt{ldi\_add}
satisfies display interpolation \texttt{ldi\_add\_interp},
and so therefore does the equivalent system of substitutable rules
\texttt{rlscf\_nw}.
\end{proof}



\section{Conclusions}
\label{s-concl-fw}
TO BE WRITTEN 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 
