\begin{frame}[t]{At Most One}
  \examplemodel
  \pause\bigskip
  
  \sentence{At most one $R$-loop:}
  \pause
  \begin{talign}
    \model{\amodel} \satisfies  
    \formula{\forallst{x}{\forall{y}{(\binpred{{\black{R}}}{x}{x} \logandinf \binpred{{\black{R}}}{y}{y} \logimpinf \equalto{x}{y})}}}
  \end{talign}
  \pause
  \sentence{Not at least two $R$-loops:}
  \pause
  \begin{talign}
    \model{\amodel} \satisfies  
    \formula{\lognot{\existsst{x}{\existsst{y}{(\binpred{{\black{R}}}{x}{x} \logandinf \binpred{{\black{R}}}{y}{y} \logandinf \notequalto{x}{y})}}}}
  \end{talign}
  \pause
  Both sentences are equivalent because:
  \begin{scenter}
    \sentence{at most one} ($\le 1$)  $\iff$ \sentence{not at least two} (not $\ge 2$)
  \end{scenter}
\end{frame}