22/77
\begin{frame}
\frametitle{Examples}

\begin{exampleblock}{$R(a,a) \;\vdash\; \myex{x}{\myex{y}{R(x,y)}}$}
\begin{tikzpicture}
\naturaldeduction{
\mpause[1]{
\proofstep{$R(a,a)$}{premise};
}
\mpause{
\proofstep{$\myex{y}{R(a,y)}$}{$\exists_i$ 1};
}
\mpause{
\proofstep{$\myex{x}{\myex{y}{R(x,y)}}$}{$\exists_i$ 2};
}
}
\end{tikzpicture}
\\
\mpause[2]{\hint{For line 2:\quad $R(a,a) = R(a,y) [a/y]$}}
\\
\mpause{\hint{For line 3:\quad $\myex{y}{R(a,y)} = \myex{y}{R(x,y)} [a/x]$}}
\end{exampleblock}
\pause\pause\pause\pause

\begin{exampleblock}{$\myall{x}{\myall{y}{R(x,y)}} \;\vdash\; \myex{x}{\myall{y}{R(x,y)}}$}
\begin{tikzpicture}
\naturaldeduction{
\mpause[1]{
\proofstep{$\myall{x}{\myall{y}{R(x,y)}}$}{premise};
}
\mpause{
\proofstep{$\myall{y}{R(z,y)}$}{$\forall_e$ 1};
}
\mpause{
\proofstep{$\myex{x}{\myall{y}{R(x,y)}}$}{$\exists_i$ 2};
}
}
\end{tikzpicture}
\\
\mpause[2]{\hint{For line 2\mpause{, 3}:\quad $\myall{y}{R(z,y)} = \myall{y}{R(x,y)} [z/x]$}}
\end{exampleblock}
\end{frame}