\begin{align*}
  \hat{\varphi}_{EUF} \quad := \quad f_{ab} = x \land f_{xy} \neq g_a \lor f_{mn} = b \lor f_{g_{a}y} \neq a
\end{align*}

\begin{align*}
     \varphi_{FC} \quad := \quad & (a=m  \land b=n \rightarrow f_{ab} = f_{mn}) \land \\
                                 & (a=x  \land b=y \rightarrow f_{ab} = f_{xy}) \land \\
                                 & (a=g_a\land b=y \rightarrow f_{ab} = f_{g_{a}y}) \land \\
                                 & (m=g_a\land y=n \rightarrow f_{mn} = f_{g_{a}y}) \land \\
                                 & (m=x  \land y=n \rightarrow f_{xy} = f_{mn}) \land \\
                                 & (x=g_a\land y=y \rightarrow f_{xy} = f_{g_{a}y})
\end{align*}
\begin{align*}
     \varphi_{E} \quad := \hat{\varphi}_{EUF} \wedge \varphi_{FC}
\end{align*}