\begin{frame}[t]{Reachable in $\forestgreen{n}$ Steps}
  We search for formulas $\cformi{\forestgreen{n}}$ that express reachability in $\forestgreen{n}$ steps:
  \pause
  \begin{center}
  $    
  \begin{aligned}
    \cformi{0} \: & \funin \;\; 
      \formula{\equalto{\freevar{u}}{\freevar{v}}}
      \\[-0.25ex]\pause{}  
    \cformi{1} \: & \funin \;\; 
      \formula{\binpred{R}{\freevar{u}}{\freevar{v}}}
      \\[-0.25ex]\pause{}
    \cformi{2} \: & \funin \;\;
      \formula{\existsst{x_1}{(\logand{\binpred{R}{\freevar{u}}{x_1}}{\binpred{R}{x_1}{\freevar{v}}})}}
      \\[-0.25ex]\pause{}
    \cformi{3} \: & \funin \;\;
      \formula{\existsst{x_1}{\existsst{x_2}{
        (\logand{\binpred{R}{\freevar{u}}{x_1}}
                {\logand{\binpred{R}{x_1}{x_2}}
                        {\binpred{R}{x_2}{\freevar{v}}}})}}}
      \\[-0.5ex]\pause{}
    \vdots \; & \;\;\;\;\;\;\;\;\; \vdots
      \\[-0.5ex]  
    \cformi{\forestgreen{n}} \: & \funin
      \;\;
      \formula{\existsst{x_1}{\existsst{x_2}{\ldots\existsst{x_{\forestgreen{n}-1}}{
        (\logand{\binpred{R}{\freevar{u}}{x_1}}
                {\logand{\binpred{R}{x_1}{x_2}}
                        {\ldots\logandinf\binpred{R}{x_{\forestgreen{n}-1}}{\freevar{v}}}})}}}}
  \end{aligned}
  $
  \end{center}
  \pause
  
  \begin{goal}{}
    We work with constants $\const{c}$, $\const{d}$:
    we write $\formula{\bap{\cform}{\const{c}}{\const{d}}}$ for 
    $\substforin{\const{d}}{\freevar{v}}{\substforin{\const{c}}{\freevar{u}}{\cform}}$.  
  \end{goal}
  \begin{exampleblock}{}
    $\bap{\cformi{2}}{\const{c}}{\const{d}}$
    denotes the formula 
    $\formula{\existsst{x_1}{(\logand{\binpred{R}{\const{c}}{x_1}}{\binpred{R}{x_1}{\const{d}}})}}$.
  \end{exampleblock}
  \pause
  \begin{block}{Theorem}
    It holds for all models $\model{\amodel}\,$:
    \begin{talign}
      \model{\amodel} \satisfies \bap{\cformi{\forestgreen{n}}}{\const{c}}{\const{d}}
      \;\Longleftrightarrow\;
      \text{$\intin{\const{d}}{\model{\amodel}}$
         reachable from $\intin{\const{c}}{\model{\amodel}}$ 
         by $\forestgreen{n}$ $\intin{\sbinpred{R}}{\model{\amodel}}$-steps}
    \end{talign}
  \end{block}  
\end{frame}