130/155
\begin{frame}{Everybody Votes for At Most One Person}
  We translate in a few steps.
  \pause\medskip
  
  \begin{block}{\sentence{Jan votes for at most one person}}
    \pause 
    $\formula{\forallst{x}{\forallst{y}{(
        \binpred{V}{\const{j}}{x} \logandinf \binpred{V}{\const{j}}{y} \logimpinf \equalto{x}{y} 
     )}}}$
  \end{block}
  \pause\medskip
  
  Now a property:
  \begin{block}{\sentence{$\freevar{z}$ votes for at most one person:}}
    \pause
    $\formula{\forallst{x}{\forallst{y}{(
       \binpred{V}{\freevar{z}}{x} \logandinf \binpred{V}{\freevar{z}}{y} \logimpinf \equalto{x}{y}    
     )}}}$
  \end{block}
  \pause\medskip
  
  The sentence `\sentence{Everybody votes for at most one person.}'
  states that this property is shared by everyone ($\formula{\forall \freevar{z}}$):\pause{}  

  \begin{block}{\sentence{Everybody votes for at most one person:}}
    \pause
    $\formula{\forallst{\chocolate{z}}{\forallst{x}{\forallst{y}{(
       \binpred{V}{\chocolate{z}}{x} \logandinf \binpred{V}{\chocolate{z}}{y} \logimpinf \equalto{x}{y}    
     )}}}}$
  \end{block}
\end{frame}