\renewcommand\cfile{trcond.tex}

\thrm{notK4} is restricted to \M-sequents with at most four point variables.
We now prove a theorem which
characterizes the \M-sequents which can be translated using
steps \ref{Mst1} to \ref{Mstlst},
regardless of the number of point variables they contain.
The characterization is
in terms of the corresponding graph;
for brevity, we will refer to ``translating the graph''.
We will assume throughout that the graphs have no vertices of degree~0
(ie, vertices with no incident edges), noting that 
steps \ref{Mst1} to \ref{Mstlb1} 
neither produce nor remove such vertices.

\begin{defn} \label{trcdefn}
We define a \bfi{path} in an undirected graph 
to be a sequence of \emph{distinct} vertices $v_0, v_1, \ldots, v_n$,
where each two successive vertices $v_{i-1}$ and $v_i$ are joined
by an edge of the graph.
We may use the notation $x \ldots y \ldots z$ to mean a path
$v_0, v_1, \ldots, v_n$, for some $n \geq 0$,
where $x = v_0$, $y = v_i$ for some $i$,
$0 \leq i \leq n$, and $z = v_n$.
That is, this notation allows $x$ and $y$, or $y$ and $z$,
to be the same vertex.

%where each edge $e_i$ joins vertices $v_{i-1}$ and $v_i$, and there
%are no repeated vertices.
An undirected graph with vertices $x,y$, with $x \neq y$, is
\textbf{\boldmath $(x,y)$-orderable}\index{orderable|textbf}
if it satisfies conditions \ref{trcondp} and \ref{trcondv} below.
It is \textbf{\boldmath $(x,y)$-directible}\index{directible|textbf}
if it satisfies conditions \ref{trcondp} and \ref{trconde} below.
%except possibly $x=y$):
\begin{enumerate}
\renewcommand\labelenumi{(\alph{enumi})}
\renewcommand\theenumi\labelenumi
\item \label{trcondp}
there do not exist paths of the form
$$x \ldots z \ldots w \ldots y 
\qquad \mbox{and} \qquad x \ldots w \ldots z \ldots y $$
with $w \not = z$ 
\item \label{trcondv}
every vertex lies on a path from $x$ to $y$.
\item \label{trconde}
every edge, other than a loop, lies on a path from $x$ to $y$.
\end{enumerate}
An \M-sequent, or a sequent obtained in the course of translation from
\M\ to \dRA\, is 
\textbf{\boldmath $(x,y)$-orderable} 
(\textbf{\boldmath $(x,y)$-directible}) if its
corresponding graph is
$(x,y)$-orderable ($(x,y)$-directible).
\end{defn}

We first prove some lemmata used in the proof of \thrm{trcond}.

\begin{lemma} \label{lem:trnc}
Let $\mathcal S$ be a sequent, 
and let $G$ be its corresponding graph.
Let $\mathcal S'$ be the result of applying one or more translation steps
\ref{Mst1} to \ref{Mstlb1}, other than using \ref{Mst;}
to remove $x$ or $y$, to $\mathcal S$,
and let $G'$ be its corresponding graph.
Then
\begin{enumerate}
\renewcommand\labelenumi{(\roman{enumi})}
\renewcommand\theenumi{\labelenumi}
\item \label{trnc-o}
  if $G$ is $(x,y)$-orderable then $G'$ is $(x,y)$-orderable
\item \label{trnc-d}
  $G$ is $(x,y)$-directible if and only if $G'$ is $(x,y)$-directible.
\end{enumerate}
\end{lemma} 

\proof\
Firstly, we note that steps \ref{Mstmv} and \ref{Mstbl} 
do not change the shape of the graph.
Step \ref{Mst,} collapses multiple edges into one;
clearly this also does not change whether the graph satisfies 
conditions \ref{trcondp}, \ref{trcondv} or \ref{trconde}.

Next, we note that steps \ref{Mst;'} and \ref{Mst;`} remove a loop 
(corresponding to a formula $x[R]x$).
Now a loop cannot appear as an edge in any path,
%except where the path consists only of the loop,
as paths do not have repeated vertices.
%other than (possibly) their endpoints.
Therefore removing a loop does not change whether the graph satisfies 
conditions \ref{trcondp}, \ref{trcondv} or \ref{trconde}.

Step \ref{Mst;} is slightly more difficult.
Suppose it changes graph $G$ to $G'$,
changing edges $(u,t)$ and $(t,v)$ in $G$
to edge $(u,v)$ in $G'$.
Then it changes any path
$\ldots ,u,t,v, \ldots$ in $G$ to a path 
$\ldots ,u,v, \ldots$ in $G'$.
Since \ref{Mst;} requires that $v$ be of degree~2
(the point variable $t$ appears only in the formulae affected by \ref{Mst;}), 
the only paths in $G$
affected by \ref{Mst;} are those containing the edges $(u,t)$ and $(t,v)$.
Also, if $P = \ldots ,u,t,v, \ldots$ is a sequence of successive vertices
joined by edges, but does not satisfy the definition of a path
only because the vertex $t$ is repeated,
then either $u$ or $v$ must be repeated also.
That is, step \ref{Mst;} cannot change 
%something that would be a path but for repeated vertices into a path.
$P$ in $G$ to a path in $G'$.
Therefore step \ref{Mst;} does not change 
whether the graph satisfies condition~\ref{trconde}.

In the same way, if $G$ 
satisfies condition \ref{trcondv},
then so does $G'$.
(The converse need not hold: if $G'$ 
satisfies condition \ref{trcondv},
we can say only that
every vertex of $G$, except possibly $t$, lies on a path from $x$ to $y$.)

It is easy to see that step \ref{Mst;} does not change 
whether the graph satisfies condition~\ref{trcondp}, 
unless $w$ or $z$ is the vertex deleted.

Say $G$ fails to satisfy condition~\ref{trcondp}, and that vertex
$z$ (in the statement of condition~\ref{trcondp}) 
is deleted by step \ref{Mst;}, changing edges 
$(u,z)$ and $(z,v)$ to an edge $(u,v)$.
Then the paths in condition~\ref{trcondp} become (without loss of generality)
$$x \ldots u,v \ldots w \ldots y 
\qquad \mbox{and} \qquad x \ldots w \ldots u,v \ldots y $$
or
$$x \ldots u,v \ldots w \ldots y 
\qquad \mbox{and} \qquad x \ldots w \ldots v,u \ldots y $$
In both these cases the facts 
that $u \not = v$ and 
that the paths contain no repeated vertices 
show that $u \not = w$, and we have paths
$$x \ldots u \ldots w \ldots y 
\qquad \mbox{and} \qquad x \ldots w \ldots u \ldots y $$
so the new graph $G'$ also fails condition~\ref{trcondp}.

Conversely, suppose that the graph $G'$ resulting from step \ref{Mst;}
fails condition~\ref{trcondp}.
Then, as mentioned above, inserting a vertex $t$ into an edge $(u,v)$
does not create a repeated vertex if there were none before, so
the graph before the \ref{Mst;} step also fails condition~\ref{trcondp}.
$\Box$

\begin{lemma} \label{lem:trconv}
Let $G$ be an $(x,y)$-orderable graph.
%and $x,y$ be vertices of $G$,
%satisfying conditions \ref{trcondp} and \ref{trcondv}
%of \thrm{trcond}.
Assume that $G$ has no vertices of degree~2
other than possibly $x$ or $y$, and no multiple edges.
Then $G$ has only two vertices, $x$ and $y$.
\end{lemma}

\proof\
Let $G$ be a counterexample to this lemma with minimum number of vertices.
Thus $G$ satisfies all the conditions of \lem{trconv} but has more than
two vertices.
Condition \ref{trcondv} implies that $G$ is connnected.
%(as we are disregarding vertices of degree~0 throughout).

Firstly, we show that there is no cut-vertex, that is, 
a vertex whose removal makes the graph disconnected.
Suppose that $w$ is a vertex whose removal (together with its incident
edges) leaves at least two connected components $G_1, G_2, \dots, G_n$ 
($n \geq 2$).
Then $w$ is of degree at least 2; but by the hypothesis only $x$ and $y$ 
may have degree~2, so $w$ is of degree at least 3.
Let $u$ be a vertex in $G_1$.
Since, by condition \ref{trcondv}, there is a path from $x$ to $y$ via $u$,
either $x$ or $y$ must be in $G_1$, as otherwise $w$ would be a repeated vertex
on the path.
That is, the path would have to begin at $x$ in some $G_i$ ($i \neq 1$),
cross over to $G_1$ and $u$ via $w$,
and then cross over to $y$ in some $G_j$ ($j \neq 1$) via $w$.
Likewise either $x$ or $y$ must be in $G_k$ for each $k = 1,2,\ldots,n$.
Thus $n = 2$.
Say $x \in G_1$ and $y \in G_2$, which implies $x \not = w$ and $y \not = w$.
As $w$ is 
of degree at least 3, suppose without loss of generality that $w$
is joined to at least two vertices in $G_1$.
For $i = 1,2$,
let $G'_i$ consist of $G_i$ and $w$ (including the edges of $G$ joining
$w$ to $G_i$).

Since, by condition \ref{trcondv}, there is a path $P$ from $x$ to $y$ via $w$,
there is a path $P_2$ from $w$ to $y$.
$P_2$ must lie entirely within $G'_2$, otherwise the vertex $w$ 
would be repeated in $P_2$.
Now let $P_1$ be any path from $x$ to $w$;
then $P_1$ must lie entirely within $G'_1$.
So the only vertex in both $P_1$ and $P_2$ is $w$, so
$P_1$ can be extended, using $P_2$, to a path from $x$ to $y$.
It follows from this that $G'_1$ is $(x,w)$-orderable
%(satisfies conditions \ref{trcondp} and \ref{trcondv} for $(x,w)$)
as well as satisfying the other conditions of this lemma,
which makes it a smaller counterexample.
Therefore $G$ has no cut-vertex.

It follows from this that $G$ has no vertices of degree~1.

Choose any path $P$ from $x$ to $y$.
Suppose that this path, and all incident edges, are deleted from $G$,
leaving a graph with connected components $C_1, C_2, \ldots$
(some of which may be isolated vertices).
Consider one such connected component $C$, 
and let the edges between it and $P$ be 
$(u_1, v_1), (u_2, v_2), \ldots$, with
$u_i \in P$ and $v_i \in C$.
We look at cases according to how many distinct $u_i$ there are. 
If there is only one, then it is a cut-vertex, which cannot be the case,
as shown above.

If there are exactly two, say $u_1$ and $u_2$, with $u_1$ closer than $u_2$ to
$x$ along $P$, then define $C'$ to consist of $C, u_1,u_2$ together with 
$(u_1, v_1), (u_2, v_2)$, and any other edges 
%$(u_i, v_i)$ where $u_i = u_1$ or $u_i = u_2$.
joining $C$ to $u_1$ or $u_2$.
We show $C'$  
satisfies conditions \ref{trcondp} and \ref{trcondv} for $(u_1,u_2)$.
For condition \ref{trcondp}, use the fact that
paths from $u_1$ to $u_2$ in $C'$ can be extended to
paths from $x$ to $y$ in $G$, using appropriate parts of $P$.
For condition \ref{trcondv},
let vertex $w$ be given in $C'$.
There is a path from $x$ to $y$ in $G$ containing $w$;
as it has no repeated vertices, this path goes through
$u_1$ once and $u_2$ once, and so gives the required path 
from $u_1$ to $u_2$ in $C'$ containing $w$.
It can be seen that $C'$ and $u_1,u_2$  
satisfies the other conditions of this lemma, which makes it a smaller
counterexample.

If there are (at least) three distinct $u_i$, say $u_1,u_2,u_3,\ldots$
(in that order along $P$),
then we have paths
$$x \ldots u_1,v_1 \ldots v_2,u_2 \ldots u_3 \ldots y
\qquad \mbox{and} \qquad
x \ldots u_1 \ldots u_2,v_2 \ldots v_3,u_3 \ldots y$$
giving a counterexample to condition \ref{trcondp}.
Therefore there are no connnected components $C_i$;
that is, there are no vertices not on the path $P$.

That is, every path from $x$ to $y$ contains every vertex of $G$.
Suppose $G$ has a vertex $u$, other than $x$ and $y$.
So $u$ has degree at least 3.
Let $P$ be a path from $x$ to $y$; as shown above, it contains every vertex of
$G$.
As $u$ has degree at least 3, and as $G$ has no multiple edges,
there must be an edge $\{u,v\}$ with $v$ not adjacent to $u$ in $P$.
Let $v$ lie between $u$ and (say) $x$ in $P$;
then 
$x \ldots v,u \dots y$ is a path which does not contain every vertex of $G$,
a contradiction.
Therefore $G$ has only the vertices $x$ and $y$.
$\Box$

\begin{thm} \label{thrm:trcond}
An \M-sequent can be translated into a \dRA-sequent,
using point variables $(x,y)$,
for $x \not=y$, if and only if
its corresponding undirected graph $G$
is $(x,y)$-orderable, 
equivalently, if it is $(x,y)$-directible.
\end{thm}

\proof\
\textmd{\textsl{The theorem holds if $G$ is not connected :}} \\
Recall that we are assuming that graphs do not have isolated vertices.
Thus any connected component contains edges.
Therefore a graph with more than one connected component 
fails to satisfy conditions \ref{trconde} and \ref{trcondv}, and so is not
$(x,y)$-directible or $(x,y)$-orderable. 
Also a graph with more than one connected component 
cannot be translated, as none of the translation steps
\ref{Mst1} to \ref{Mstlb1} reduces the number of connected components,
and the final step \ref{Mstfin} requires exactly one connected component.
Therefore the theorem holds for a graph with more than one connected component.
We henceforth assume that $G$ is connected.

\textmd{\textsl{
  $G$ is $(x,y)$-directible $\Longrightarrow$ $G$ is $(x,y)$-orderable :}} \\
As there are no isolated vertices,
it is easy to see that
condition \ref{trconde} implies condition \ref{trcondv},
and so if $G$ is $(x,y)$-directible then it is $(x,y)$-orderable. 

%From \lem{trnc}\ref{trnc-d}
%we have that steps \ref{Mst1} to \ref{Mstlb1} 
%do not affect whether the graph is $(x,y)$-directible, and
%and if a graph is $(x,y)$-orderable then
%steps \ref{Mst1} to \ref{Mstlb1} 
%change it into a graph which still
%is $(x,y)$-orderable.

\textmd{\textsl{
  $G$ is not $(x,y)$-directible $\Longrightarrow$
  $G$ cannot be translated :}} \\
By \lem{trnc}\ref{trnc-d},
if we start with a graph $G$ that is not $(x,y)$-directible, 
and apply any translation steps \ref{Mst1} to \ref{Mstlb1}
(other than using \ref{Mst;} to delete $x$ or $y$),
we end up with a graph $G'$ that is not $(x,y)$-directible. 
Since the translation finishes with the only use of step \ref{Mstfin}, 
and step \ref{Mstfin} requires a
graph $G'$ that is a single edge (not a loop, since $x \neq y$), 
which is $(x,y)$-directible, 
a graph $G$ that is not $(x,y)$-directible 
cannot be translated using $(x,y)$.

\textmd{\textsl{
  $G$ cannot be translated $\Longrightarrow$
  $G$ is not $(x,y)$-orderable :}} \\
Conversely, suppose a graph $G$ cannot be translated using $(x,y)$.
Firstly, apply translation steps
(other than using \ref{Mst;} to delete $x$ or $y$)
until no further step
(other than \ref{Mstbl}, which doesn't change the graph)
can be applied; call the resulting graph $G'$.
As step \ref{Mstfin} cannot be applied, 
there must be a vertex $u$ other than $x$ or $y$;
as steps \ref{Mst,} and \ref{Mst;} cannot be applied,
there are no multiple edges, and no vertices of degree~2
other than (possibly) $x$ and $y$.
Then, by \lem{trconv}, $G'$ is not $(x,y)$-orderable; 
by \lem{trnc}\ref{trnc-o}, $G$ is not $(x,y)$-orderable. 
%since steps \ref{Mst1} to \ref{Mstlb1} 
%do not affect whether the graph is $(x,y)$-directible, 
%$G$ also is not $(x,y)$-directible. 
$\Box$

\renewcommand\cfile{}