\documentclass{rtaloop}
\rtalabel{syntactic}


\begin{document}
\begin{problem}{Claude Kirchner, J. Zhang}{}{June 1993}

\begin{abstract}
What is the syntactic type of (mid-, three-way) distributivity?
\end{abstract}

What is the syntactic type (maximum number of top-level steps needed in an
equational proof \cite{BC92:alp}) of the  distributivity axiom?
What is the syntactic type of ``three-way'' commutativity:
\[
\begin{array}{l}
  f(x, y, z) = f(x, z, y) = f(y, x, z) = f(y, z, x) = f(z, x, y) = f(z, y, x)\\
  f(f(x, y, z), u, x) = f(x, y, f(z, u, x))
\end{array}
\]
What are the unification type, decidability, and syntactic type
of ``mid-commutativity'': $(x+y)+(u+v) = (x+u)+(y+v)$?

\end{problem}
\end{document}