\documentclass{rtaloop}
\rtalabel{conditional}


\begin{document}
\begin{problem}{Yoshihito Toyama}{}{April 1991}

\begin{abstract}
Is the extension of Combinatory Logic by Boolean constants confluent?
\end{abstract}

Consider the following extension of Combinatory Logic with constants
$T$ (true), $F$ (false), $C$ (conditional):
\begin{eqnarray*}
Ix & \rightarrow & x\\
Kxy & \rightarrow & x\\
Sxyz & \rightarrow & (xz)(yz)\\
CTxy & \rightarrow & x\\
CFxy & \rightarrow & y\\
x \leftrightarrow^* y \Rightarrow    Czxy & \rightarrow & x
\end{eqnarray*}
Is this (non-terminating) ``semi-equational''  (or ``natural'', as such are
called in \cite{DO90:tcs}) conditional rewrite system confluent? 
Note that if we take the above system plus the rule
$x \leftrightarrow^* y \Rightarrow   Czxy \rightarrow y$,
the resulting conditional rewrite system {\em is\/} confluent (cf. \cite{K92:ox}\cite{V90:free}).

\end{problem}
\end{document}