\section{Notes - not for publication}
Therefore the procedure to test whether clause 3 of the bi-trace consistency
definition is satisfied, that is, whether $\{h'\vec\theta\}$ is a consistent 
theory for all $h$-respectful $\vec\theta$ is
\begin{itemize}
\item
note, $\vec\theta$ is $h$-respectful iff $\vec\theta$ is $h'$-respectful
\item
let $\Gamma = \{h'\}$
\item
to test if $\Gamma\vec\theta$ is consistent 
(if $\vec\theta$ is $h'$-respectful)
instead test if 
$\RNe {(\Gamma \vec\theta)}$ is consistent,
which is equivalent, by 
Lemma~\ref{l-tc-equiv}\ref{l-thy-cons-equivd} and \ref{l-nf-cons}) 
\item
by Theorem~\ref{t-nfs-comm}\ref{nfs-comm},
assuming keys are atomic,
$\RNe {(\Gamma \vec\theta)} =
(\GammaRNe) \vec\theta \setminus \Ne$ 
\item
so we consider whether $(\GammaRNe) \vec\theta \setminus \Ne$
is consistent
\item
this is equivalent to $(\GammaRNe) \vec\theta$
being consistent,
by Lemma~\ref{l-tc-equiv}\ref{l-thy-cons-equivd} 
\item 
note also that 
$(\Gamma \vec\theta)\!\!\Downarrow$ is reduced, obviously,
so 
$\RNe{(\Gamma \vec\theta)}$ is reduced 
by Lemma~\ref{l-Ne}\ref{l-rsmin-names},
so 
$(\GammaRNe) \vec\theta \setminus \Ne$ is reduced,
so 
$(\GammaRNe) \vec\theta$ is reduced
by Lemma~\ref{l-Ne}\ref{l-rsmin-names}
\item
so our task is to test whether 
$(\GammaRNe) \vec\theta$ is consistent,
using the information that it is reduced
(simpler definition of consistent for a reduced theory)
\item
let $\Gamma' = \GammaRNe$
\item
we can first let $\vec\theta$ be the null (identity) substitution
(which is clearly $h$-respectful), 
and so the consistency of $\Gamma'\vec\theta$ is finitely checkable.
So assume henceforth that $\Gamma$, and so 
$\Gamma' = \GammaRNe$, are consistent.
\end{itemize}

\noindent To test the consistency of $\Gamma' = \GammaRNe$,
\begin{itemize}
\item
Looking at the simpler definition of consistency for a reduced theory, 
and noting that keys are atomic, 
we see that if any key is a free name then the theory is inconsistent
(theorem \texttt{ka\_red}).
So assume keys are rigid names.
\item
The significant criterion for consistency, then, is:
if $(M,N), (M', N') \in \Gamma'\vec\theta$ then
$(M = M') \Leftrightarrow (N = N')$
(see \texttt{thy\_cons\_red\_def},
\texttt{is\_der\_virt\_red\_MR}, \texttt{is\_der\_virt\_red\_RM})
\item
So for each $M,M'$ in $\pi_1(\Gamma')$
work out the minimal substitution necessary to get $M\theta_1 = M'\theta_1$
(this is well-defined, like the most general unifier)

% \item
% Then, given this $\theta_1$, see if it respects $\pi_1(h')$.
% This requires testing whether $\{\pi_1(h'')\}\theta_1 \vdash \ldots$,
% for certain prefixes $h''$ of $h'$ --- this is easy because 
% $\{\pi_1(h'')\} \subseteq \{\pi_1(h')\}$ and so is reduced
% WRONG --- $\{\pi_1(h')\}$ need not be reduced
\end{itemize}

\noindent We may need to further specialise $\theta_1$ to make it respectful.
\begin{itemize}
\item we're seeking $\theta_1$ to make $M'\theta_1 = M''\theta_1$
where $\theta_1$ is $h$-respectful
\item this gives mgu containing, eg, $x \leadsto M$, as described above
\item to make this respectful we need
$\{h'\}\theta_1 \vdash M$ (where $h'$ is the part of $h$ prior to $x$)
\item now look at $\{h'\}\!\!\Downarrow$ and the reduced components of $M$,
as in Boreale
\item want each reduced component of $M$ to be contained in
$\{h'\}\!\!\Downarrow$, as per Boreale, after further substitution
\item so for each reduced component of $M$, select a member of
$\{h'\}\!\!\Downarrow$, and unify them --- this gives a further substitution
\item this is the first point again, so we get a recursive finite procedure
\end{itemize}

\noindent Once we have a respectful substitution $\theta_1$:
\begin{itemize}
\item
If $\theta_1$ respects $\pi_1(h')$,
there is a unique $\theta_2$ such that 
$\vec\theta = (\theta_1, \theta_2)$ respects $h$.
Calculating this should be finite --- 
see Isabelle definitions of \texttt{match\_rc1} and \texttt{second\_sub}
\item
Then it should be simpler to test whether $N\theta_2 = N'\theta_2$
\item
We would then need to do the same procedure, reflected, ie,
So for each $N,N'$ in $\pi_2(\Gamma')$, get $\theta_2$, 
such that $N\theta_2 = N'\theta_2$,
calculate the unique $\theta_1$ such that $\vec\theta$ respects $h$,
and test whether $M\theta_1 = M'\theta_1$ 
\end{itemize}

\begin{verbatim}
ka_red : "[| ka_oth ?oth; ?oth : rsmin oth_red UNIV; thy_cons ?oth;
         (Enc ?Mp ?Mk, Enc ?Np ?Nk) : ?oth |] ==>
	?Mk : Rigids & ?Nk : Rigids & (?Mk, ?Nk) ~: ?oth"
\end{verbatim}

\newpage
\subsection{Further developments}
(the above was written in preparing the TPHOLs paper). Since then:

\newcommand\entvs{\texttt{entvs}}
\newcommand\entvss{\texttt{entvss}}

\subsubsection{where keys are atomic}
A procedure was developed to recursively get towards a respectful substitution,
theory \texttt{Spi\_Mgrs}

\subsubsection{where keys are not necessarily atomic}
We make use of a different formulation of observer theory entailment 
called \texttt{indist\_norm}, where the $(el)$ rule uses $\vdash_r$ derivation
for the keys, and omits the keys from the antecedent of the second premise
(this makes no difference, because of a cut-elimination result).

$$
\infer[(el)]
{\Gamma, {(\encM,\encN)} \vdash M \eqm N}
{\Gamma, {(\encM,\encN)} \vdash_r M_k \eqm N_k &
\Gamma, {(\encM,\encN)}, (M_p, N_p) \vdash M \eqm N}
$$

In fact, where the premises hold, 
then also $\Gamma \vdash_r M_k \eqm N_k$
(because $\vdash_r$ cannot use messages on the left larger than the 
messages on the right),
and then cut-elimination (twice) and the $(er)$ rule
gives $\Gamma, (M_p, N_p) \vdash M \eqm N$

We define a ``reduction'' of a theory which may or may not be valid
according to whether a pair of keys is derivable or not, and keep the
derivation of keys as a constraint.
The reduction \entvs\ is given by 
\begin{align*}
\Gamma, (\pairM,\pairN) & \longrightarrow
  ((\Gamma, (\pairM,\pairN), (M_a, N_a)), (M_b, N_b), \{\}) \\
\Gamma, (\encM,\encN) & \longrightarrow
  ((\Gamma, (\encM,\encN), (M_p, N_p)), \{\Gamma \vdash_r (M_k, N_k)\})
\end{align*}
provided that the resulting theory is not a subset of the original one.
The second component of the result is a constraint which needs to be satisfied
for the reduction to be appropriate.

We define the reduction so that the resulting theory contains the original one,
this is to preserve respectfulness of a substitution.
Where the reduction is used repeatedly, it acts on the first component, and the
set of constraints is accumulated.
Thus we define a second relation \entvss:

\begin{verbatim}
entvs :: "((obs_thy * obs_seq set) * obs_thy) set"
entvss :: "(obs_thy * obs_seq set) relation"

entvss.I : "((?S', ?Vs), ?S) : entvs ==>
  ((?S', ?Vs Un ?Us), ?S, ?Us) : entvss"
\end{verbatim}

Significant results are:

\begin{verbatim}
idv_red_nkr_not_idv :
  "[| (?G, ?MN) : indist; ~ is_der_virt (?G, ?MN); finite ?G |]
     ==> EX H. (H, ?G) : oth_red_nkr & (EX h:H. ~ is_der_virt (?G, h))" 
\end{verbatim}

\noindent
if $(T, Ts) \in \entvs$ and all constraints in $Ts\theta$ 
are satisfied (ie $\vdash_r$ holds for them)
then $T\theta \vdash (M \eqm N)\theta $ iff $S\theta \vdash (M \eqm N)\theta $ 
\begin{verbatim}
subst_entvs_iff  : "[| ((?T, ?Ts), ?S) : entvs;
            Ball (subst_seq ?fg ` ?Ts) is_der_virt |] ==>
    ((subst_pr ?fg ` ?T, ?MN) : indist) = ((subst_pr ?fg ` ?S, ?MN) : indist)" 
\end{verbatim}

We then defined an \entvs-minimal theory with respect to a particular
(respectful) substitution $\theta$ as one for which any \entvs-reduction
includes one which gives a constraint which, after substitution by $\theta$,
is not satisfied:

\begin{verbatim}
 "min_entvs ?fg ?G == ALL G' Ds.  ((G', Ds), ?G) : entvs -->
   (EX T:Ds. ~ is_der_virt (subst_seq ?fg T))" 
\end{verbatim}

Then we get theorems \texttt{entvs\_min\_resp} and \texttt{satvss\_cond}:

\begin{verbatim}
ide_conds_def : "ide_conds ?ns ?fg ?G ==
         finite ?G & thy_cons ?G & min_entvs ?fg ?G &
	 thy_strl_resp ?fg ?ns ?G & fn_oth ?G <= Union (set ?ns)" 

entvs_min_resp_Ne : "[| ide_conds ?ns ?fg ?G;
    (subst_pr ?fg ` ?G, ?MN) : indist |] ==> 
  is_der_virt (subst_pr ?fg ` (?G - Ne), ?MN)" : Thm.thm

satvss_cond "[| finite ?G; ?G <= range pair;
    thy_strl_resp ?fg ?ns ?G; fn_oth ?G <= Union (set ?ns) |] ==> 
  satvss (subst_vs ?fg (?G, ?Ss)) ?MN =
  (EX H Ts. ((H, Ts), ?G, ?Ss) : entvss^* &
  Ball (insert (subst_pr ?fg ` H, ?MN) (subst_seq ?fg ` Ts)) is_der_virt)" 
\end{verbatim}

That is, we can calculate \entvss\ (finite) from $\Gamma$
\emph{before} substitution, giving a number of sets of constraints, 
and the condition that $\Gamma\theta \vdash M\theta_1 \eqm N\theta_2$ 
is tested by testing whether $\Delta\theta \vdash_r X\theta_1 \eqm Y\theta_2$ 
for each constraint $\Delta \vdash_r X \eqm Y$ in one of the sets obtained.

Thus we are given a constraint $\Delta \vdash_r X \eqm Y$, or rather,
$\Delta\theta \vdash_r X\theta_1 \eqm Y\theta_2$, 
where the respectful $\theta$ is to be determined.
Where $\Delta$ does not contain pairs $(x,x) \in \Ne$, 
getting a set of most general solutions is straightforward (DETAILS ??) 
but this is not so in general. 

So, questions: 
\begin{itemize}
\item Can we get constraints in \texttt{satvss\_cond} where 
the theories do not contain pairs, or equivalently,
where each condition 
$\Delta\theta \vdash_r X\theta_1 \eqm Y\theta_2$ 
is replaced by 
$(\Delta \setminus \Ne)\theta \vdash_r X\theta_1 \eqm Y\theta_2$ ?
(Note, probably can for the first constraint, see the proof of 
\texttt{entvs\_min\_resp\_Ne} from \texttt{entvs\_min\_resp})

\item if we redefine \texttt{min\_entvs} thus:
\begin{verbatim}
min_entvs_Ne_def : "min_entvs_Ne ?fg ?G ==
  ALL G' Ds.  ((G', Ds), ?G) : entvs -->
    (EX (H, K):Ds. ~ is_der_virt (subst_pr ?fg ` (H - Ne), subst_pr ?fg K))" 
\end{verbatim}
is it equivalent?

\item
Can we get a new notion of a ``normal derivation'' wrt a particular
respectful substitution $\theta$ where the derivations of key pairs 
are not just $\vdash_r$, but of the form
$(\Gamma - \Ne) \theta \vdash_r M_k\theta_1 \eqm N_k\theta_2$ ?
(Note - getting the result about normal derivations involves
showing that keys can be derived by $\vdash_r$, not just $\vdash$,
and respectful substitutions give that if 
$\Gamma \theta \vdash \ldots$ then $(\Gamma - \Ne) \theta \vdash \ldots$,
can we combine these two effects?)
\end{itemize}

Answer to the last question is yes.  
We define, inductively, a proof of this form by \texttt{indist\_nvs},
and, further, one where the main premise gets smaller as you go up
(ie, in the left rules, the main premise 
does not contain the principal formula), by \texttt{indist\_nvs\_excl}.
(This last permits proofs by induction on the size of the formula).
These define proofs which essentially never use any $(x,x)\vec\theta$ on the
left-hand side.
Then we proved, in \texttt{indist\_ne\_nsv}, that if 
$S \theta \vdash M\theta$ then the derivation can be done using 
rules of \texttt{indist\_nvs\_excl}.
(It only works for single sided proofs because of the way substitution can make
a consistent theory inconsistent).

Finally we got the theorem 
\begin{verbatim}
resp_ex_orkvss : 
  "[| finite ?G; subst_seq ?fg (?G, ?MN) : indist; ?G <= range pair;
    thy_strl_resp ?fg ?ns ?G; fn_oth ?G <= Union (set ?ns) |] ==>
  EX H Vs. ((H, Vs), ?G, {}) : orkvss^* & 
    (ALL (K, X):insert (H, ?MN) Vs. is_der_virt (subst_seq ?fg (K - Ne, X)))" 
\end{verbatim}
Here \texttt{orkvss} is similar to \texttt{entvss},
except that when it reduces a compound formula (pair or encrypt) it removes it.