<reponame>wenkokke/nodcap
\begin{definition}[Structural congruence]\label{def:nc-equiv}
  We extend \cref{def:cp-equiv} with the following equivalences:
  \[
    \begin{array}{llll}
      \ncEquivPoolComm
      & \tm{\ncPool{P}{Q}}
      & \equiv \;
      & \tm{\ncPool{Q}{P}}
      \\
      \ncEquivPoolAss1
      & \tm{\ncPool{P}{\ncPool{Q}{R}}}
      & \equiv \;
      & \tm{\ncPool{\ncPool{P}{Q}}{R}}
      \\
      \ncRedKappaPool1
      & \tm{\cpCut{x}{\ncPool{P}{Q}}{R}}
      & \equiv \;
      & \tm{\ncPool{P}{\cpCut{x}{Q}{R}}} \quad \text{if} \; \notFreeIn{x}{P} 
      \\
      \ncRedKappaPool2
      & \tm{\ncPool{P}{\cpCut{x}{Q}{R}}}
      & \equiv \;
      & \tm{\cpCut{x}{\ncPool{P}{Q}}{R}}
    \end{array}
  \]
\end{definition} 
%%% Local Variables:
%%% TeX-master: "main"
%%% End:
