\subsection{Use of properties of the Display Calculus}
\cc{Bel-props}
\cc{start of props.tex}
\label{Bel-props}

Belnap's cut-elimination theorem states that any Display Calculus
satisfying his properties (C2) to (C8) satisfies the cut-elimination theorem.
Here we trace the use of these properties in the proof for the 
specific case of \dRA.
We refer to the conditions in the form given by Kracht \cite{kracht-power}.

We proved properties which are satisfied by each rule of \dRA.
They use the following definitions:

\texttt{rls} is the set of rules of \dRA.

\texttt{ruleInOrInv} \texttt{rule rules} : 
either \texttt{rule} or its inverse is a member of \texttt{rules}

\texttt{seqNoSSF} \texttt{seq} :
if a formula appears on one side of the $\vdash$ in
\texttt{seq} then the whole of that side is a formula.

\texttt{seqSVs} \texttt{seq} : a list of the structure variables in 
\texttt{seq}.

\texttt{noDups} \texttt{list} : 
\texttt{list} contains no member more than once. 

\texttt{seqSVs'} \texttt{bool seq} : a list of the structure variables in 
antecedent or succedent (depending on \texttt{bool}) positions in
\texttt{seq}.

The following three results are used in the proofs of 
\texttt{makeCutLP} and \texttt{makeCutRP}.

In the conclusion of a rule, no structure has a sub-structure which is a
formula 

\begin{verbatim}
seqNoSSF_rls =
  "ruleInOrInv ?rule rls ==> seqNoSSF (conclRule ?rule)" : thm
\end{verbatim}

No structure variable appears more than once in the conclusion of a rule.

\begin{verbatim}
noDupSVs_rls =
  "ruleInOrInv ?rule rls ==> noDups (seqSVs (conclRule ?rule))" : thm
\end{verbatim}

If a structure variable appears in the conclusion of a rule 
in antecedent [succedent] position, 
then it does not appear in a premise of that rule 
in succedent [antecedent] position. 

\begin{verbatim}
noSVsAS_rls =
  "[| ruleInOrInv ?rule rls; ?prem : set (premsRule ?rule);
      ?s : set (seqSVs' ?b (conclRule ?rule)) |]
   ==> ?s ~: set (seqSVs' (~ ?b) ?prem)" 
\end{verbatim}

Note that an earlier version of our work used the following rule,
which is actually stronger than required, but makes the proof simpler.

If a structure variable appears in a premise of a rule,
in antecedent [succedent] position, 
then it also appears in the conclusion of that rule 
in antecedent [succedent] position. 

\begin{verbatim}
noNewSVs_rls =
  "[| ruleInOrInv ?rule rls; ?prem : set (premsRule ?rule);
      ?s : set (seqSVs' ?b ?prem) |]
   ==> ?s : set (seqSVs' ?b (conclRule ?rule))" 
\end{verbatim}

The result \texttt{orC8}, and the corresponding results for each logical
connective, form Belnap's condition (C8).

Belnap's condition (C3) is equivalent to \texttt{noDupSVs\_rls}.

His condition (C4) says that if a
structure variable appears anywhere in a rule in an 
antecedent (succedent) position, then it does not appear in a 
succedent (antecedent) position.
In fact all we actually need for the proof is \texttt{noSVsAS\_rls},
which is weaker than (C4), since 
\texttt{noSVsAS\_rls} permits a structure variable to appear 
in both antecedent and succedent positions in the premises,
provided that it does not appear in the conclusion.

(C4) is implied by \texttt{noDupSVs\_rls} and \texttt{noNewSVs\_rls}
(which we had used originally).
However \texttt{noNewSVs\_rls} is stronger than it needs to be for this
result, since (C4) permits structure variables to appear in the 
premise(s) but not in the conclusion.
Note that Display Calculi generally do satisfy \texttt{noNewSVs\_rls}.

Our theorem \texttt{seqNoSSF\_rls} is equivalent to Belnap's (C5),
since, in Kracht's formulation, formula variables can never be parameters. 

Under Kracht's formulation, Belnap's (C2), (C6) and (C7) are trivially 
satisfied.