

\section{Substitutions which may give a consistent theory} \label{s-cons}

We now discuss the criteria for a theory to be consistent, 
and show how to express these in a way that is relevant to the results
of \S\ref{s-fsrs}.
Firstly we note \cite[Theorem~17(b)]{dawson-tiu-fotesb}
(\texttt{subst\_reduce\_Ne\_tc}).
Use of this result may in practice lead to shorter computations.

\comment{
\begin{verbatim}
reduce_subs_Ne_indist_thy : "[| finite ?oth;
    thy_strl_resp ?f ?ns ?oth; fn_oth ?oth <= Union (set ?ns) |] ==>
  ((subst_oth ?f ?oth, ?MN) : indist) =
    ((subst_oth ?f (reduce ?oth - Ne), ?MN) : indist)"

subst_reduce_Ne_tc : "[| validbt ?bt; ?bt : bt_resp ?f |] ==>
  thy_cons (subst_oth ?f (oth_of ?bt)) =
    thy_cons (subst_oth ?f (reduce (oth_of ?bt) - Ne))" 
\end{verbatim}
}

In \cite{dawson-tiu-fotesb} we gave several criteria for a theory $\Gamma$ 
to be consistent, but the ones which led to decidability of this question 
involved applying certain criteria to $\Gamma\!\!\Downarrow$.
Here we are interested in the consistency of $\Gamma\theta$,
so this approach would involve looking at 
$\Gamma\theta\!\!\Downarrow$, for all respectful $\theta$.

We are considering all respectful substitutions
$\vec\theta = (\theta_1, \theta_2)$ for a bi-trace $h$,
where $h$ projects to single messages traces $s_1$ and $s_2$
We can use \cite[Theorem~20]{dawson-tiu-fotesb},
which says that given $s_1$-respectful $\theta_1$, 
there is a unique $\theta_2$ such that 
$\vec\theta = (\theta_1, \theta_2)$ is $h$-respectful.

Where $\Gamma = \{h\}$, the theory got from $h$ by forgetting the 
$i/o$ markings and the orderings,
let $\Sigma = \{s_1\}$, similarly, so $\Sigma = \pi_1(\Gamma)$.
Then we can use Lemma~\ref{l-indist-resp-ex-orkvss-red}, 
by which we can get all $\Sigma\theta_1\!\!\Downarrow$ 
($\theta_1$ $s_1$-respectful) by looking at a finite number of 
message sets $\Sigma'$ 
(such that $\Sigma \longrightarrow^* (\Sigma', \mathcal C'_R)$).

We need to find the respectful substitutions $\theta_1$ for 
a given $(H, Vs)$ in Lemma~\ref{l-indist-resp-ex-orkvss-red}.

