\newpage
\appendix
\section{Isabelle definitions and theorems}
\subsection{Definitions of message equivalence deducibility} \label{ded-eqv}

\begin{lemma} % [\texttt{indist\_wk, indist\_alt}]
\begin{enumerate}
\item \cite[Lemma~7]{tiu-trace-based-bisim-full}
  \texttt{\upshape(indist\_wk, indist\_alt\_wk)}
  Weakening (that is, augmenting $\Gamma$) is admissible (in both systems)
\item \texttt{\upshape(indist\_alt)} the same % message equivalence
sequents ${\Gamma \vdash M \leftrightarrow N}$ 
  are deducible in both systems
\end{enumerate}
\end{lemma}

In Isabelle we defined, inductively, sets of sequents
\texttt{indist} and \texttt{indist\_alt}, which are the sets of sequents
derivable in the two systems.
Subsequently we found it helpful to define the corresponding
sets of rules explicitly, calling them 
\texttt{indpsc} and \texttt{indpsc\_alt}.
The distinction between these approaches is illustrated by the two expressions
of the rule $(pr)$ in the text below.
Note that the set \texttt{indpsc} is the infinite set of all % possible 
instantiations of the six rules shown in Figure~\ref{f-msg-ind}.
\begin{verbatim}
"[| (?oth, ?Ma, ?Na) : indist; (?oth, ?Mb, ?Nb) : indist |] ==>
  (?oth, (Mpair ?Ma ?Mb, Mpair ?Na ?Nb)) : indist"
"([(?oth, ?Ma, ?Na), (?oth, ?Mb, ?Nb)],
  (?oth, (Mpair ?Ma ?Mb, Mpair ?Na ?Nb))) : indpsc" 
\end{verbatim}
This provides an example of shallow or deep embedding of inference rules,
discussed in \cite{dawson-gore-gls-ca},
and illustrates a point made in the discussion there,
% The theorem \texttt{indpsc\_le\_alt}
% illustrates a point made in the discussion in \cite{dawson-gore-gls-ca},
that formalising the rules as explicit objects enables us to express
notions such as \texttt{indpsc} $\subseteq$ \texttt{indpsc\_alt}.
As discussed in \cite{dawson-gore-gls-ca},
\texttt{derrec} $rls\ \{\}$ means the set of things
(here, sequents $\Gamma \vdash M \leftrightarrow N$)
derivable using the set of inference rules $rls$.
%
\begin{verbatim}
indist_wk : "[| (?oth, ?MN) : indist; ?oth <= ?othl |] ==>
  (?othl, ?MN) : indist"
indist_alt : "indist_alt == indist" 
indpsc_le_alt : "indpsc <= indpsc_alt"
indist_derrec : "indist == derrec indpsc {}"
\end{verbatim}
% indist_alt_derrec : "indist_alt == derrec indpsc_alt {}"

\subsection{Invertibility and cut-admissibility} \label{inv-ca}
Lemma 6 of \cite{tiu-trace-based-bisim-full}
gives invertibility of the right rules $(pr)$ and $(er)$,
and Lemma 5 gives invertibility-like results for the left rules
$(pl)$ and $(el)$.
We proved these as \texttt{pr\_inv}, \texttt{er\_inv}, 
\texttt{pl\_inv}, \texttt{el\_inv}. 
In \cite[Lemma~10]{tiu-trace-based-bisim-full} a ``cut-admissibility'' result
\begin{center}
If $\Gamma \vdash M \eqm N$ and $\Delta, (M,N) \vdash R \eqm T$
then $\Gamma \cup \Delta \vdash R \eqm T$
\end{center}
is proved from Lemma 5,
by induction on the derivation of $\Gamma \vdash M \eqm N$.
In Isabelle we showed that it can also be proved from Lemma 6,
by induction on the derivation of
$\Delta, (M,N) \vdash R \eqm T$.
In fact we found it easier to prove cut-admissibility
directly for the modified system of Figure~\ref{f-msg-ind}.
We actually proved a stronger result involving several cut-formulae:
% (which doesn't directly follow from the simpler result,
% if the index set $I$ is infinite):

\begin{theorem}[\texttt{indist\_alt\_ca}] \label{t-indist-alt-ca}
If $\Gamma \vdash M_i \eqm N_i$ for all $i \in I$, and
$\Delta' \vdash R \eqm T$,
where $\Delta' \subseteq \Delta \cup \{(M_i, N_i)\,|\,i \in I\} $,
then $\Gamma \cup \Delta \vdash R \eqm T$
\end{theorem}

\begin{verbatim}
indist_alt_ca : "[| (?Del', ?RT) : indist_alt;
  ?Del' <= ?Del Un ?MNs; ALL MNi:?MNs. (?Gam, MNi) : indist_alt |]
                  ==> (?Del Un ?Gam, ?RT) : indist_alt" 
\end{verbatim}

Note how we also used a stronger inductive hypothesis, whose assumption
is an inequality ($\Delta' \subseteq \ldots$); 
this was {much} easier to prove in Isabelle
than if the ``$\subseteq$'' were ``='' instead.

We noted that the cut-admissibility result easily implies Lemmas 5 and 6
(so proving both before proving cut-admissibility was redundant).
We also observed that these cut-admissibility proofs, unusually, did not
require the inductive assumption that cut is admissible for smaller objects,
which is because INSERT REASON.

In fact if we remove $(M_k, N_k)$ from the second premise of $(el)$
in Figure~\ref{f-msg-ind}, we get another set of rules which is apparently
weaker, for which we called the derivable sequents \texttt{indist\_nk\_alt}.
There is a corresponding cut-admissibility result for 
\texttt{indist\_nk\_alt} (called \texttt{indist\_nk\_alt\_ca}),
which can be used to show that the systems 
\texttt{indist\_k\_alt} and \texttt{indist\_alt} are equivalent.


\subsection{Isabelle theorems for \texttt{smpsc} and Lemma~\ref{l-smpsc}}
  \label{v-smpsc}
In mathematical notation we can just write
write $\pi_1$ or $\pi_2$ to denote the projection to the first or second
component, for pairs, theories, sequents and rules,
eg, \texttt{smpsc} = $\pi_1$(\texttt{indpsc}).
But the definition in Isabelle, \texttt{smpsc\_def}, uses
\texttt{seqmap fst}, which applies \texttt{fst} (ie, $\pi_1$)
to each member of the antecedent and to the consequent of a sequent,
and \texttt{pscmap} $f$, which applies $f$ to each premise and to the
conclusion of a rule.
\begin{verbatim}
pair_def : "pair == %x. (x, x)"
smpsc_def : "smpsc == pscmap (seqmap fst) ` indpsc" 
smpsc_alt : "smseq : smpsc == pscmap (seqmap pair) smseq : indpsc" 

slice_derrec_smpsc_empty :
  "?c : derrec indpsc {} ==> seqmap fst ?c : derrec smpsc {}"
derrec_smpsc_eq :
  "(?c : derrec smpsc {}) = (seqmap pair ?c : derrec indpsc {})"
smpsc_ex_indpsc_der : "[| (fst ` ?oth, ?M) : derrec smpsc {};
    thy_cons ?oth |] ==> EX N. (?oth, ?M, N) : derrec indpsc {}" 
\end{verbatim}

\subsection{Decidability of $\vdash$} \label{app-vdash-decidable}
The simplest approach to proving decidability of $\vdash$
uses the fact that there only finitely many sequents 
which will appear in a proof, or in an attempted backwards proof,
of a given sequent.
(The proof given in \S\ref{s-dec-red} is more complex but leads to a
more computationally efficient approach for determining theory consistency).

We define the set of pairs which might appear in a sequent in a 
backwards proof of a given sequent $\Gamma \vdash M \eqm N$:
for a pair $(M, N)$ of messages, \texttt{pairs\_of\_msgs} $(M, N)$ 
is the set of pairs of messages obtained by ``decomposing'' $(M, N)$,
including $(M, N)$ and partially decomposed pairs,
and \texttt{pairs\_of\_seq} $(\Gamma, (M, N))$ returns all pairs in 
$\Gamma$ or $(M, N)$.
Then \texttt{rules\_in\_pairs} $S$ is the set of rules such that 
all the pairs of any of the sequents in the rule are in $S$.

\begin{verbatim}
inductive "pairs_of_msgs MN"
  intros
    id : "MN : pairs_of_msgs MN"
    pa : "(Mpair Ma Mb, Mpair Na Nb) : pairs_of_msgs MN ==> 
      (Ma, Na) : pairs_of_msgs MN"
    pb : "(Mpair Ma Mb, Mpair Na Nb) : pairs_of_msgs MN ==> 
      (Mb, Nb) : pairs_of_msgs MN"
    ep : "(Enc Mp Mk, Enc Np Nk) : pairs_of_msgs MN ==> 
      (Mp, Np) : pairs_of_msgs MN"
    ek : "(Enc Mp Mk, Enc Np Nk) : pairs_of_msgs MN ==> 
      (Mk, Nk) : pairs_of_msgs MN"

primrec
  "pairs_of_seq (G, MN) = (UN p: insert MN G. pairs_of_msgs p)"

inductive "rules_in_pairs Ps" 
  intros
    I : "ALL s : insert c (set ps). pairs_of_seq s <= Ps ==> 
      (ps, c) : rules_in_pairs Ps"
\end{verbatim}

We find that a sequent $\Gamma \vdash M \eqm N$ has finitely many pairs. 

\begin{verbatim}
finite_pairs_of_seq : "finite ?G ==> finite (pairs_of_seq (?G, ?MN))"
\end{verbatim}

Given a finite set $S$ of pairs, there are only finitely many sequents 
whose pair sets are contained in $S$,
and the same holds for rules provided that we bound the number of premise
sequents.
Consequently there are only finitely many instantiations of the rules in
Figure~\ref{f-msg-ind} whose pairs are in a given set $S$. 
(Recall that \texttt{inspsc} is the infinite set of all instantiations of
the six rules shown in Figure~\ref{f-msg-ind}).

\begin{verbatim}
finite_seqs_pairs_in : "finite ?S ==> finite {seq. pairs_of_seq seq <= ?S}"
finite_rules : "finite ?S ==> finite {(ps, c). length ps <= 2 & 
   insert c (set ps) <= {seq. pairs_of_seq seq <= ?S}}"
finite_indpsc : "finite ?S ==> finite (indpsc Int rules_in_pairs ?S)" 
\end{verbatim}

Now we find that the pairs of premises of rules in \texttt{inspsc}
are contained in the pairs of the conclusion, and
consequently, whenever any sequent $\Gamma \vdash M \eqm N$
is derivable using rules in \texttt{inspsc}, 
then it is derivable using only those rules whose pairs are 
in the set of pairs of $\Gamma \vdash M \eqm N$.

\begin{verbatim}
indpsc_pairs : "[| (?ps, ?c) : indpsc; ?p : set ?ps |] ==>
   pairs_of_seq ?p <= pairs_of_seq ?c"
derrec_indpsc_pairs : "?seq : derrec indpsc {} ==>
   ?seq : derrec (indpsc Int rules_in_pairs (pairs_of_seq ?seq)) {}"
\end{verbatim}

Combining all these we find that given a sequent $\Gamma \vdash M \eqm N$
that we wish to derive, we know that the only rules used in the derivation will 
be those whose pairs are in \texttt{pairs\_of\_seq} $(\Gamma, (M, N))$,
and there are only finitely many of these.
Further, since no derivation need contain the same sequent twice,
no rule (that is, instantiated rule) need be used twice,
so the process of searching for a derivation of a given end-sequent
$\Gamma \vdash M \eqm N$ will necessarily be finite.

\subsection{Isabelle theorems for Lemma~\ref{l-red-nc}} \label{v-red-nc}
\begin{verbatim}
red_nc : "(?oia, ?oib) : oth_red ==> 
  ((?oia, ?x) : indist) = ((?oib, ?x) : indist)" 
nf_nc : "finite ?oia ==>
  ((nf oth_red ?oia, ?MN) : indist) = ((?oia, ?MN) : indist)" 
\end{verbatim}


\subsection{Proof of confluence of $\longrightarrow$} \label{or-confl}
Confluence of $\longrightarrow$ is reasonably easy to see
since the side condition for the second rule is of the form
$ {\Gamma' \vdash M_k \leftrightarrow N_k} $
where $\Gamma'$ is exactly the theory being reduced, and,
from Lemma~\ref{l-red-nc}, this condition (for a particular $M_k,N_k$) 
will continue to hold, or not, when other reductions have changed $\Gamma'$.

But it was not easy to prove confluence the natural way in Isabelle,
since there are so many cases.
Two reductions, each of which may use either rule, gives four cases.
Then either of these reductions may introduce the same pair
which is removed by the other reduction, so it then needs to be removed again.
This gives four sub-cases for each of the main cases,
and each case required at some point an instantiation specific to that case.

We therefore devised an alternative proof.
This proof used the fact that reduction is well-founded 
although that is not necessary to prove confluence.

Firstly we simplified the main result by changing the side condition 
for the second rule, by defining $\longrightarrow_K$ for a set $K$,
which remains fixed throughout the reduction process.
This $K$ will eventually be equated to the set
$\{(M_k, N_k)\,|\, \Gamma \vdash M_k \eqm N_k$ 
(which, as noted above, remains unchanged as $\Gamma$ gets reduced).
Thus, in defining $\longrightarrow_K$,
the side condition for the second rule is simply $(M_k, N_k) \in K$.

The key lemmas here follow.
Lemma~\ref{l-key-confl}\ref{l-oth-red-k-lem} 
encapsulates the multitude of cases referred to above.
Lemma~\ref{l-key-confl}\ref{l-oth-red-k-min} is proved by well-founded
induction, based on the fact that reduction is well-founded.
%
\begin{lemma} \label{l-key-confl} For a set $K$,
\begin{enumerate}
\item \texttt{\upshape(oth\_red\_k\_lem)} \label{l-oth-red-k-lem}
if $\Gamma \longrightarrow_K \Gamma'$, $p \in \Gamma \setminus \Gamma'$ and
$p \in \Delta$, 
then there exists $\Delta'$ such that 
$\Delta \longrightarrow_K \Delta'$ and
$\Delta \setminus \{p\} \subseteq \Delta' \subseteq \Delta \cup \Gamma'$
\item \texttt{\upshape(oth\_red\_k\_min )} \label{l-oth-red-k-min}
% $\Theta$ is in the well-founded part of \longrightarrow_K,
Suppose $\Gamma \longrightarrow_K \Gamma'$ and
$\Delta \longrightarrow_K \Delta'$.
Let $\Theta' = \Gamma' \cup \Delta' \setminus (\Gamma \setminus \Gamma')
 \setminus (\Delta \setminus \Delta')$.
If $\Theta' \subseteq \Theta \subseteq
  \Gamma \cup \Delta \cup \Gamma' \cup \Delta'$ then 
  $\Theta \longrightarrow_K^* \Theta'$.  
\end{enumerate}
\end{lemma}

\begin{verbatim}
oth_red_k_lem : 
 "[| (?G', ?G) : oth_red_k ?K; ?b : ?D; ?b : ?G - ?G' |] ==>
   EX D'.  (D', ?D) : oth_red_k ?K & ?D - {?b} <= D' & D' <= ?D Un ?G'"

oth_red_k_min : "[| ?T : wfp (oth_red_k ?K);
  (?G', ?G) : oth_red_k ?K; (?D', ?D) : oth_red_k ?K;
     ?T' = ?G' Un ?D' - (?G - ?G') - (?D - ?D');
     ?T' <= ?T; ?T <= ?G Un ?D Un ?G' Un ?D' |]
  ==> (?T', ?T) : (oth_red_k ?K)^*" 
\end{verbatim}

From here we successively proved the following results
\begin{lemma} \label{l-oth-red-confl}
\begin{enumerate}
\item \texttt{\upshape(oth\_red\_k\_confl)}
If, for a set $K$,
$\Gamma \longrightarrow_K \Delta'$ and 
$\Gamma \longrightarrow_K \Delta''$ 
then there exists $\Theta$ such that
$\Delta' \longrightarrow_K^* \Theta$ and 
$\Delta'' \longrightarrow_K^* \Theta$ 
\item \texttt{\upshape(oth\_red\_confl)}
If $\Gamma \longrightarrow \Delta'$ and 
$\Gamma \longrightarrow \Delta''$ 
then there exists $\Theta$ such that
$\Delta' \longrightarrow^* \Theta$ and 
$\Delta'' \longrightarrow^* \Theta$ 
\item \texttt{\upshape(oth\_red\_confl\_rtc)}
If $\Gamma \longrightarrow^* \Delta'$ and 
$\Gamma \longrightarrow^* \Delta''$ 
then there exists $\Theta$ such that
$\Delta' \longrightarrow^* \Theta$ and 
$\Delta'' \longrightarrow^* \Theta$ 
\end{enumerate}
\end{lemma}

\begin{verbatim}
oth_red_k_confl :
   "[| finite ?G; (?D, ?G) : oth_red_k ?K; (?D', ?G) : oth_red_k ?K |]
      ==> EX T. (T, ?D) : (oth_red_k ?K)^* & (T, ?D') : (oth_red_k ?K)^*"
oth_red_confl : 
   "[| finite ?G; (?D, ?G) : oth_red; (?D', ?G) : oth_red |]
      ==> EX T. (T, ?D) : oth_red^* & (T, ?D') : oth_red^*" 
oth_red_confl_rtc :
   "[| finite ?G; (?D, ?G) : oth_red^*; (?D', ?G) : oth_red^* |]
      ==> EX T. (T, ?D) : oth_red^* & (T, ?D') : oth_red^*" 
\end{verbatim}

We define \texttt{nf\_props} $r\ x\ y$ to mean that $y$ has the properties of a
$r$-normal form of $x$, and show
easily (in \texttt{nf\_unique}) from this definition
that such a $y$ is unique.
% Then we define $\texttt{nf}\ r\ x$ to be this $y$, when it exists.
We define $\texttt{nf}\ r\ x = \epsilon y.\ \texttt{nf\_props}\ r\ x\ y$,
which means some $y$ satisfying \texttt{nf\_props} $r\ x$, if such $y$ exists;
otherwise some $y$ of the right type.
Then, if such a $y$ exists,
then the definition \texttt{nf} $r\ x$ refers to it.
% Having confluence and termination, it is a standard result,
% and easy to show in Isabelle,
% that we have a normal form $y$
% such that \texttt{nf\_props} $r\ x\ y$.
% satisfying these properties.  

The definition \texttt{nf\_def} is 
$\texttt{nf}\ r\ x = \epsilon y.\ \texttt{nf\_props}\ r\ x\ y$, which means 
some $y$ satisfying \texttt{nf\_props} $r\ x$, if such $y$ exists;
otherwise some $y$ of the right type.
\begin{verbatim}
tri_prop_def : "tri_prop ?r ?x ?y == ALL z. (z, ?x) : ?r^* --> (?y, z) : ?r^*"
rsmin_def : "rsmin ?r ?S == {x : ?S. ALL y. (y, x) : ?r --> y ~: ?S}" 
nf_props_def : "nf_props ?r ?x ?y == 
  (?y, ?x) : ?r^* & ?y : rsmin ?r UNIV & tri_prop ?r ?x ?y" 
nf_unique : "nf_props ?r ?x ?nx ==> ?nx = nf ?r ?x" 
nf_def : "nf ?r ?x == SOME y. nf_props ?r ?x y" 
\end{verbatim}

It is a standard result, and easy in Isabelle,
that confluence and termination give normal forms
satisfying these properties.  

\begin{theorem}[\texttt{nf\_oth\_red}] \label{a-t-nf-oth-red}
Any theory $\Gamma$ has a $\longrightarrow$-normal form $\GammaR$ 
\end{theorem}

\begin{verbatim}
nf_oth_red : "finite ?x ==> nf_props oth_red ?x (nf oth_red ?x)" 
\end{verbatim}

\subsection{Isabelle theorems for Theorem~\ref{t-red-alt}} \label{v-red-alt}
\begin{verbatim}
red_alt_lem : "(?othe, ?M, ?N) : indist ==>
  (?othe - {(Enc ?Qp ?M, Enc ?Rp ?Rk)}, ?M, ?N) : indist |
               (EX oth'. (oth', ?othe) : oth_red_alt)" 

oth_red_alt_lem : "(?D, ?G) : oth_red ==> EX D'. (D', ?G) : oth_red_alt"
rsmin_or_alt : "rsmin oth_red_alt UNIV = rsmin oth_red UNIV" 
nf_acc_alt : "finite ?G ==> (nf oth_red ?G, ?G) : oth_red_alt^*"
nf_alt : "[| finite ?G; nf_props oth_red ?G ?D |] ==>
  nf_props oth_red_alt ?G ?D" 
nf_same : "finite ?G ==> nf oth_red_alt ?G = nf oth_red ?G" 
\end{verbatim}

As noted in the text we may further change $\longrightarrow'$ 
by deleting the $(M_k,N_k)$ from the second rule:
call the resulting relation $\longrightarrow''$, 
or, in Isabelle, \texttt{oth\_red\_nk}.

Use of cut-admissibility shows that Lemma~\ref{l-red-nc}\ref{red-nc}
applies to this relation as it does to $\longrightarrow$, ie
\begin{verbatim}
red_nk_nc : "(?G', ?G) : oth_red_nk ==>
    ((?G', ?x) : indist) = ((?G, ?x) : indist)" 
\end{verbatim}
Clearly the same theories are irreducible for $\longrightarrow'$
as for $\longrightarrow''$. 
We did not establish confluence for this relation but noted that if 
$\Gamma \longrightarrow''^* \Delta$ and $\Delta$ is
$\longrightarrow''$-irreducible, then, by Lemma~\ref{l-Ne}\ref{nf-equiv-der},
$\Delta \setminus\ \Ne = \RNe\Gamma $.
\begin{verbatim}
red_nk_same_ex_Ne : "[| (?D, ?G) : oth_red_nk^*;
      ?D : rsmin oth_red_nk UNIV; finite ?G |] ==> 
    ?D - Ne = reduce ?G - Ne" 
\end{verbatim}

\subsection{Isabelle theorems for Lemma~\ref{l-nf-no-left}}
\label{v-nf-no-left}
\begin{verbatim}
nf_no_left : "[| ?seq : derrec indpsc {}; fst ?seq : rsmin oth_red UNIV |]
          ==> ?seq : derrec indpsc_virt {}" 

virt_dec : "(?seq : derrec indpsc_virt {}) = is_der_virt ?seq" 
\end{verbatim}

\subsection{Definitions used in \texttt{reduce}} \label{v-red-pair-enc}
\begin{verbatim}
consts
  red_pair :: "msg * msg => obs_thy => obs_thy"
  red_enc :: "msg * msg => obs_thy => obs_thy"
  reduce :: "obs_thy => obs_thy"

recdef "red_pair" "{}"
  "red_pair (Mpair Ma Mb, Mpair Na Nb) =
    (%oth. insert (Ma, Na) (insert (Mb, Nb) oth))"
  "red_pair p = (%oth. oth)"

recdef "red_enc" "{}"
  "red_enc (Enc Mp Mk, Enc Np Nk) =
    (%oth. insert (Mp, Np) (insert (Mk, Nk) oth))"
  "red_enc p = (%oth. oth)"
\end{verbatim}

\subsection{Isabelle theorems for Theorem~\ref{t-reduce}}
 \label{v-reduce} 
\begin{verbatim}
reduce_nf : "finite ?x ==> nf oth_red ?x = reduce ?x"
reduce_nf_alt : "finite ?x ==> nf oth_red_alt ?x = reduce ?x" 

virt_reduce : "finite ?oth ==> 
  is_der_virt (reduce ?oth, ?MN) = ((?oth, ?MN) : indist)"

idvr_reduce : "finite ?S ==>
  ((?S, ?M, ?N) : indist) = is_der_virt_red (reduce ?S, ?M, ?N) 

reduce_nc : "((reduce ?oib, ?MN) : indist) = ((?oib, ?MN) : indist)" 
\end{verbatim}

\subsection{Definitions and theorems for single message sets} \label{a-sms}
\begin{verbatim}
reduce_ss_def : "reduce_ss S == fst ` reduce (pair ` S)" 
idv_ss_def : "idv_ss seq == is_der_virt (seqmap pair seq)" 
reduce_paired : "G <= range pair ==> reduce G <= range pair" 
idv_reduce_ss : "finite S ==> 
  ((S, M) : derrec smpsc {}) = idv_ss (reduce_ss S, M)" 
\end{verbatim}

\comment{ red_comps stuff omitted 
\subsection{Isabelle theorem for Lemma~\ref{l-rc-reduce}} \label{v-rc-reduce}
\begin{verbatim}
rc_reduce = "finite ?S ==> ((?S, ?M) : derrec smpsc {}) =
       (red_comps (reduce_ss ?S) ?M <= reduce_ss ?S)" 
\end{verbatim}
}

\subsection{Isabelle theorem for Theorem~\ref{l-Ne}} \label{v-l-Ne}
\begin{verbatim}
nf_equiv_der : "[| finite ?otha; finite ?othb |] ==>
  (ALL MN. ((?otha, MN) : indist) = ((?othb, MN) : indist)) =
     (nf oth_red ?otha - Ne = nf oth_red ?othb - Ne)" :
\end{verbatim}

\subsection{Definition of \texttt{is\_der\_virt\_red}} \label{v-is-der-virt-red}
\begin{verbatim}
recdef "is_der_virt_red" "measure (%(oth, M, N). size M)"
  "is_der_virt_red (oth, Name i, Name j) = ((Name i, Name j) : oth | i = j)"
  "is_der_virt_red (oth, Mpair Ma Mb, Mpair Na Nb) =
    (is_der_virt_red (oth, Ma, Na) & is_der_virt_red (oth, Mb, Nb))"
  "is_der_virt_red (oth, Enc Mp Mk, Enc Np Nk) =
    (if is_der_virt_red (oth, Mk, Nk) then is_der_virt_red (oth, Mp, Np)
      else (Enc Mp Mk, Enc Np Nk) : oth)" 
  "is_der_virt_red (oth, M, N) = ((M, N) : oth)"
\end{verbatim}
The following is the theorem which says that 
if $\Gamma$ is reduced, then 
\texttt{is\_der\_virt\_red} $(\Gamma, (M,N))$ iff
\texttt{is\_der\_virt} $(\Gamma, (M,N))$.
\begin{verbatim}
is_der_virt_red : "?oth : rsmin oth_red UNIV ==>
  is_der_virt (?oth, ?M, ?N) = is_der_virt_red (?oth, ?M, ?N)"
\end{verbatim}

\subsection{Isabelle theorems for Lemma~\ref{l-tc-equiv}}
  \label{v-tc-equiv}
\begin{verbatim}
thy_cons_equiv :
   "thy_cons ?oth =
      (ALL M N.
          (?oth, M, N) : indist -->
          ((M : Mpairs) = (N : Mpairs) &
           (M : Encs) = (N : Encs) & (M : Rigids) = (N : Rigids)) &
          (ALL Mp Mk Np Nk.
              M = Enc Mp Mk & N = Enc Np Nk -->
              (fst ` ?oth, Mk) : derrec smpsc {} |
              (snd ` ?oth, Nk) : derrec smpsc {} -->
              (?oth, Mk, Nk) : indist) &
          (ALL R.
              ((?oth, M, R) : indist --> R = N) &
              ((?oth, R, N) : indist --> R = M)))" 

thy_cons_equivd : "thy_cons ?oth = thy_cons (?oth - Ne)" 

nf_cons : "finite ?oth ==> thy_cons (nf oth_red ?oth) = thy_cons ?oth" 

cons_der_same : "[| finite ?oth; finite ?oth';
    ALL MN. ((?oth, MN) : indist) = ((?oth', MN) : indist) |]
        ==> thy_cons ?oth = thy_cons ?oth'" 
\end{verbatim}

\subsection{Isabelle theorems for Theorem~\ref{t-thy-cons-red}}
  \label{v-thy-cons-red}
\begin{verbatim}
tc_red_iff : "finite ?S ==> thy_cons ?S = thy_cons_red (reduce ?S)"
\end{verbatim}


\subsection{Definitions of a consistent bi-trace}
  \label{vd-bt-cons}
Definition~\ref{d-bt-cons} can be modelled in Isabelle
using its \texttt{recdef} feature, where the definition is recursive,
depending on the consistency of smaller bi-traces.
In Isabelle we define \texttt{bt\_cons\_rec} in this way.
Here, the \texttt{size} of a bi-trace is simply its length as a list.

\begin{verbatim}
recdef "bt_cons_rec" "measure size"
  "bt_cons_rec [] = True"
  "bt_cons_rec (In MN # bt) = (bt_cons_rec bt & (oth_of bt, MN) : indist)"
  "bt_cons_rec (Out MN # bt) = (bt_cons_rec bt & 
     (ALL subs. bt : bt_resp subs --> bt_cons_rec (subst_bt subs bt) -->
         thy_cons (oth_of (subst_bt subs (Out MN # bt)))))"
\end{verbatim}

We also defined \texttt{bt\_cons}, an inductively defined set,
where $h \in$ \texttt{bt\_cons} iff $h$ satisfies the variant of
Definition~\ref{d-bt-cons} with the underlined words omitted.

An inductively defined set in Isabelle is the unique largest set
which satisfies the given clauses such as (a) to (c) of
Definition~\ref{d-bt-cons}.
This is the least fixpoint of a certain function.
Here, it would include all bi-traces which can be shown to be consistent by
repeated use of the given clauses.

\begin{verbatim}
inductive "bt_cons"
  intros
    NilI : "[] : bt_cons"
    InI : "bt : bt_cons ==> (oth_of bt, MN) : indist ==> (In MN # bt) : bt_cons"
    OutI : "bt : bt_cons ==> ALL subs. bt : bt_resp subs -->
        thy_cons (oth_of (subst_bt subs (Out MN # bt))) ==>
      (Out MN # bt) : bt_cons"
\end{verbatim}

But with the underlined words included, 
the we could not define bi-trace consistency as an inductively defined set.
This is because to show that one bi-trace is consistent
may lead to another bi-trace not being consistent; 
the resulting inductively defined set, if allowed, would be the least
fixpoint (however defined) of some non-monotonic function, 
and so would not have the required properties.

\comment{
You imagine building up the set in question by adding objects which are,
according to the clauses, in the set.
However, with the underlined words included, 
if you add a member to the set of consistent bi-traces, 
then this may invalidate a previous addition, by clause (c), 
of a bi-trace to the set.

Having first defined bi-trace consistency in this way 
(ie, the set \texttt{bt\_cons}, corresponding to Definition~\ref{d-bt-cons}
with the underlined words omitted),
we proved Lemma~\ref{l-pres-bt-cons}.
This would have been enough to show that this definition satisfies the 
equality implicit in Definition~\ref{d-bt-cons},
but did not show that Definition~\ref{d-bt-cons} is a valid definition.
To do this we formulated the recursive definition of the function
\texttt{bt\_cons\_rec},
depending recursively on the consistency of smaller bi-traces.
We then showed, in \texttt{bt\_cons\_equiv}
that \texttt{bt\_cons\_rec} and \texttt{bt\_cons} describe the same thing.
}

\begin{proposition}[\texttt{bt\_cons\_equiv}] \label{p-bt-cons-equiv}
Omitting the underlined words from Definition~\ref{d-bt-cons}
defines the same notion of bi-trace consistency
\end{proposition}

\begin{verbatim}
bt_cons_equiv : "validbt ?bt ==> bt_cons_rec ?bt = (?bt : bt_cons)" 
\end{verbatim}

\subsection{Isabelle theorems for Lemma~\ref{l-pres-bt-cons}}
 \label{v-bt-cons-equiv} \label{v-pres-bt-cons}
Our Isabelle proofs of 
Lemma~\ref{l-pres-bt-cons}\ref{l-bt-resp-comp} and \ref{l-cons-subs-bt},
that is, of \texttt{bt\_resp\_comp} and \texttt{cons\_subs\_bt},
actually used Definition~\ref{d-bt-cons} with the underlined words omitted.
\begin{verbatim}
subst_indist : "[| (?oth, ?MN) : indist;
  ALL n:fn_msgs ?MN Un fn_oth ?oth.
    (subst_oth ?subs ?oth, subst_nat ?subs n) : indist |] ==>
  (subst_oth ?subs ?oth, subst_pr ?subs ?MN) : indist" 

bt_resp_comp : "[| ?bt : bt_resp ?subs; validbt ?bt;
  subst_bt ?subs ?bt : bt_resp ?subsa; ?bt : bt_cons |] ==>
  ?bt : bt_resp (comp_psub ?subsa ?subs)"

cons_subs_bt : "[| ?bt : bt_cons; validbt ?bt; ?bt : bt_resp ?subs |] 
  ==> subst_bt ?subs ?bt : bt_cons" 
\end{verbatim}

Arguably, as a consequence of Lemma~\ref{l-pres-bt-cons}\ref{l-cons-subs-bt}
the words underlined in Definition~\ref{d-bt-cons} should be redundant.
To be precise, $h \in$ \texttt{bt\_cons} iff $h$ satisfies 
the clauses of Definition~\ref{d-bt-cons}.
Then, to show that 
$h \in\ \texttt{bt\_cons} \Leftrightarrow \texttt{bt\_cons\_rec}\ h$
requires also that the clauses of Definition~\ref{d-bt-cons}
\emph{uniquely} define a function.
This consideration justifies the effort of making a separate definition,
\texttt{bt\_cons\_rec}, in Isabelle,
and then proving the equivalence, Proposition~\ref{p-bt-cons-equiv},
that is, \texttt{bt\_cons\_equiv}.

\subsection{Definition of \texttt{fn\_bt}, the free names of a bi-trace}
\label{v-fn-bt}
\begin{verbatim}
primrec
  "rem_io (In mp) = mp"
  "rem_io (Out mp) = mp" 

primrec
  "fn_msgs (M, N) = fn_msg M Un fn_msg N"

primrec
  Nil : "fn_bt [] = []"
  Cons : "fn_bt (mmp # mmps) = fn_msgs (rem_io mmp) # fn_bt mmps" 
\end{verbatim}

\subsection{Definition and theorems for \texttt{thy\_strl\_resp}
  and Theorem~\ref{t-thy-resp}}
  \label{v-thy-resp}
\begin{definition}
For a theory $\Gamma$ and a list $\textit{ns}$ of sets of free names,
and a substitution pair $\theta$,
\texttt{thy\_strl\_resp} $\theta\ \textit{ns}\ \Gamma$ holds if,
for each $n \in \textit{ns}$ and $x \in n$,
$\Gamma' \vdash x\theta_1 \eqm x\theta_2$,
where $\Gamma'$ is obtained by deleting from $\Gamma$ all message pairs 
containing free names which are not in some $n'$ that appears
after $n$ in $\textit{ns}$ 
\end{definition}

\begin{verbatim}
"thy_strl_resp ?f [] ?oth = True"
"thy_strl_resp ?f (?n # ?ns) ?oth = (thy_strl_resp ?f ?ns ?oth &
  (ALL x:?n. (subst_oth ?f (?oth - oth_ctg_fns (- Union (set ?ns))),
    subst_nat ?f x) : indist))"
\end{verbatim}

\begin{theorem} \label{t-thy-resp}
\begin{enumerate}
\item
\texttt{\upshape(thy\_strl\_resp\_reduce)} \label{thy-strl-resp-reduce}
If \texttt{thy\_strl\_resp} $\vec\theta\ ns\ \Gamma$ then
\texttt{thy\_strl\_resp} $\vec\theta\ ns\ \GammaR$ 
\item
\texttt{\upshape(bt\_thy\_strl\_resp)} \label{bt-thy-strl-resp}
if $\vec\theta$ is $h$-respectful then 
\texttt{thy\_strl\_resp} $\vec\theta\ (\texttt{fn\_bt}\ h)\ \{h\}$ 
\end{enumerate}
\end{theorem}

\begin{verbatim}
thy_strl_resp_reduce :
  "thy_strl_resp ?f ?ns ?oth ==> thy_strl_resp ?f ?ns (reduce ?oth)"

bt_thy_strl_resp : "[| validbt ?bt; ?bt : bt_resp ?f |] ==>
  thy_strl_resp ?f (fn_bt ?bt) (oth_of ?bt)" 
\end{verbatim}

\subsection{Isabelle theorem \texttt{bt\_sm\_resp}} \label{v-bt-sm-resp}
\begin{verbatim}
bt_sm_resp : "[| ?f = (?fl, ?fr); ?bt : bt_resp ?f |] ==>
  map (map_io fst) ?bt : sm_resp ?fl" 
\end{verbatim}

\subsection{Isabelle theorems for Theorem~\ref{t-bit-con}}
 \label{v-bit-con}
\begin{verbatim}
nf_subst_nf_Ne : "[| validbt ?bt; ?bt : bt_resp ?f |] ==>
  reduce (subst_oth ?f (oth_of ?bt)) - Ne =
  reduce (subst_oth ?f (reduce (oth_of ?bt) - Ne)) - Ne" 
\end{verbatim}


\subsection{Isabelle theorems for Theorem~\ref{t-subs-not-red-ka}} 
 \label{v-subs-not-red-ka}
\begin{verbatim}
subs_not_red_ka : "[| ka_oth ?oth; finite ?oth; thy_cons ?oth;
    ?oth : rsmin oth_red UNIV |] ==>
  subst_oth ?f (?oth - Ne) : rsmin oth_red UNIV" 
\end{verbatim}

\subsection{Isabelle theorems for Theorem~\ref{t-subst-exists-unique}}
  \label{v-subst-exists-unique}
\begin{verbatim}
subst_unique : "[| ?bt : bt_resp ?f; ?bt : bt_resp ?g;
    ?bt : bt_cons; validbt ?bt |] ==>
    (map (map_io (fst o subst_pr ?f)) ?bt =
      map (map_io (fst o subst_pr ?g)) ?bt) =
    (map (map_io (snd o subst_pr ?f)) ?bt =
       map (map_io (snd o subst_pr ?g)) ?bt)" 

subst_exists :
   "[| map (map_io fst) ?bt : sm_resp ?fl; ?bt : bt_cons; validbt ?bt |]
         ==> EX fr. ?bt : bt_resp (?fl, fr)" 
\end{verbatim}

\subsection{Definition of \texttt{match\_rc1}} \label{vd-match-rc1}
\begin{verbatim}
primrec
  Names : "match_rc1 oth (Name i) = Some (Name i)"
  Rigid : "match_rc1 oth (Rigid i) = 
    (if (EX msg. (Rigid i, msg) : oth) then 
      Some (SOME msg. (Rigid i, msg) : oth) else None)"
  Mpair : "match_rc1 oth (Mpair Ma Mb) = 
    (if match_rc1 oth Ma = None | match_rc1 oth Mb = None then None
    else Some (Mpair (the (match_rc1 oth Ma)) (the (match_rc1 oth Mb))))"
  Enc : "match_rc1 oth (Enc Mp Mk) = 
    (if match_rc1 oth Mk = None then 
      if (EX msg. (Enc Mp Mk, msg) : oth) then 
        Some (SOME msg. (Enc Mp Mk, msg) : oth) else None
    else if match_rc1 oth Mp = None then None
    else Some (Enc (the (match_rc1 oth Mp)) (the (match_rc1 oth Mk))))"
\end{verbatim}

\subsection{Isabelle theorems for Theorem~\ref{t-match-rc1}}
  \label{vt-match-rc1}
\begin{verbatim}
match_rc1_iff_idvr : "thy_cons_red ?oth ==>
  is_der_virt_red (?oth, ?M, ?N) = (match_rc1 ?oth ?M = Some ?N)" 

match_rc1_indist : "[| finite ?S; thy_cons ?S |] ==>
  ((?S, ?M, ?N) : indist) = (match_rc1 (reduce ?S) ?M = Some ?N)"
\end{verbatim}

\subsection{Definition of \texttt{second\_sub}} \label{v-second-sub}
\begin{verbatim}
primrec 
  Nil : "second_sub [] f n = Name n"
  Cons : "second_sub (mmp # bt) f n = 
    (if n : fn_oth (oth_of bt) then second_sub bt f n
    else if n ~: fn_msgs (rem_io mmp) then Name n 
    else the (match_rc1 (reduce (subst_oth (f, second_sub bt f) (oth_of bt))) 
      (f n)))"
\end{verbatim}
The following theorem shows that \texttt{second\_sub}
does in fact compute the $\theta_2$ of Theorem~\ref{t-subst-exists-unique}.
\begin{verbatim}
second_sub : "[| map (map_io fst) ?bt : sm_resp ?fl;
      ?bt : bt_cons; validbt ?bt |] ==> 
    ?bt : bt_resp (?fl, second_sub ?bt ?fl)"), 
\end{verbatim}