\documentclass{rtaloop}
\rtalabel{conditional-surjective}


\begin{document}
\begin{problem}{Roel C. de Vrijer}{}{April 1991}

\begin{abstract}
Is a certain conditional rewrite system, which is a linearization of
Combinatory Logic extended with surjective pairing, confluent?
\end{abstract}

Is the following semi-equational conditional term rewriting system
(a linearization of Combinatory Logic extended with surjective pairing)
confluent:
\begin{eqnarray*}
Ix & \rightarrow & x\\
Kxy & \rightarrow & x\\
Sxyz & \rightarrow & (xz)(yz)\\
D_{1}(Dxy) & \rightarrow & x\\
        D_{2}(Dxy) & \rightarrow & y\\
x \leftrightarrow^* y \Rightarrow      D(D_{1}x)(D_{2}y)& \rightarrow & x\\
x \leftrightarrow^* y \Rightarrow    D(D_{1}x)(D_{2}y)& \rightarrow &y 
\end{eqnarray*}
If yes, does an effective normal form strategy exist for it?
See \cite{KV89:ic}\cite{V89:lics}.

\end{problem}
\end{document}