\begin{frame}[t]{Quantification by Varying the Environment}
  \begin{minipage}{0.49\textwidth}
    Model and environment:
    \medskip
      
    \scalebox{.75}{
    \begin{tikzpicture}[dom/.style={circle,draw=orange!50!black,very thick,fill=orange!50!white,inner sep=2pt}]
      \node (1) [dom] {1};
      \node (2) [below of=1,dom] {2};
      \node (3) [below of=2,dom] {3};
      \node (4) [below of=3,dom] {4};
      \begin{scope}[node distance=30mm]
        \node (x) [left of=2] {$x$};
        \node (y) [left of=3] {$y$};
        \node (z) [left of=4] {$z$};
      \end{scope}
      \begin{scope}[shorten <= 2mm, shorten >= 2mm, very thick, >=stealth]
        \draw [->] (x) to (2);
        \draw [->] (y) to[bend left=20] (4);
        \draw [->] (z) to[bend right=20] (4) ;     %node [pos=.5] {A};
      \end{scope}
    \end{tikzpicture}
    }
  \end{minipage}
  \begin{minipage}{0.49\textwidth} 
    \begin{itemize}
      \item domain: $\model{\adomain} = \{1,2,3,4\}$
      \item $\intin{\sunpred{L}}{\model{\amodel}} = {<}$
      \medskip
      \item environment $\saluf$: 
            \begin{itemize}   
              \item $\aluf{\freevar{x}} = 2$
              \item $\aluf{\freevar{y}} = \saluf(\freevar{z}) = 4$
            \end{itemize}
     \end{itemize}
  \end{minipage}
  
  \hspace*{-4ex}  
  \begin{minipage}{.51\textwidth}
    \bigskip
    \bigskip 
    \begin{itemize}
     \item<2>
       Now $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\binpred{L}{y}{x}}$
       % $\M \;\not\mw_\saluf Lyx$
     \item<3>
       But: $\model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{y}{\,\binpred{L}{y}{\freevar{x}}}}$ 
          % $\M \;\mw_\saluf \eris y Lyx$, 
       \\
       because 
       $\model{\amodel} \satisfieslookup{\saluf[\freevar{y}\mapsto 1]} \formula{\binpred{L}{\freevar{y}}{\freevar{x}}}$   
       % $\M \;\mw_{\saluf[y\mapsto 1]}  Lyx$
    \item<4->   
      Also
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\existsst{y}{\, \binpred{L}{y}{x}}}}$ $\;\;$?   
      %$\M \;\mw_\saluf \alle x\eris y Lyx$? 
    \item<5->
      No: 
        $\model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto 1]} \formula{\existsst{y}{\,\binpred{L}{y}{\freevar{x}}}}$ 
        %$\M \;\not\mw_{\saluf[x\mapsto 1]} \eris y Lyx$
    \end{itemize} 
  \end{minipage}
  %
  \hspace*{2ex}
  \begin{minipage}{.25\textwidth}
    \onslide<3>{\scalebox{.6}{
    \begin{tikzpicture}[
        dom/.style={circle,draw=orange!50!black,very thick,fill=orange!50!white,
                    inner sep=2pt}]
      \node (1) [dom] {1};
      \node (2) [below of=1,dom] {2};
      \node (3) [below of=2,dom] {3};
      \node (4) [below of=3,dom] {4};
      \begin{scope}[node distance=30mm]
        \node (x) [left of=2] {$x$};
        \node (y) [left of=3] {$y$};
        \node (z) [left of=4] {$z$};
      \end{scope}
      \begin{scope}[shorten <= 2mm, shorten >= 2mm, very thick, >=stealth]
        \draw [->] (x) to (2);
        \draw [green!60!black,->] (y) to[bend left=10] (1);
        \draw [->] (z) to[bend right=20] (4) ;     %node [pos=.5] {A};
      \end{scope}
    \end{tikzpicture}
    }}
  \end{minipage}
  %\hspace*{1ex}
  \begin{minipage}{.23\textwidth}
    \bigskip
    \bigskip
    \bigskip
    
    \onslide<5->{\scalebox{.6}{
    \begin{tikzpicture}[
        dom/.style={circle,draw=orange!50!black,very thick,fill=orange!50!white,
                    inner sep=2pt}]
      \node (1) [dom] {1};
      \node (2) [below of=1,dom] {2};
      \node (3) [below of=2,dom] {3};
      \node (4) [below of=3,dom] {4};
      \node (a) at (y) [xshift=20mm, yshift=-3mm] {\Large ?}; 
      \begin{scope}[node distance=30mm]
        \node (x) [left of=2] {$x$};
        \node (y) [left of=3] {$y$};
        \node (z) [left of=4] {$z$};
      \end{scope}
      \begin{scope}[shorten <= 2mm, shorten >= 2mm, very thick, >=stealth]
        \draw [red,->] (x) to[bend left=10] (1);
        \draw [green!60!black,->] (y) to[bend right=10] (a);
        \draw [->] (z) to[bend right=20] (4);
      \end{scope}
    \end{tikzpicture}
    }}
  \end{minipage} 
\end{frame}