\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}