\begin{frame} \frametitle{Examples} \vspace{-1ex} \begin{exampleblock}{$\myall{x}{(P(x) \vee Q(x))} \;\vdash\; \myall{x}{P(x)} \vee \myex{x}{Q(x)}$} \pause {\small \renewcommand{\lineheight}{.5cm}% regelafstand \begin{tikzpicture} \naturaldeduction{ \proofstep{$\myall{x}{(P(x) \vee Q(x))}$}{premise}; \proofbox{ \proofstep{$\neg (\myall{x}{P(x)} \vee \myex{x}{Q(x)})$}{assumption}; \namedproofbox{$y$}{ \proofstep{$P(y) \vee Q(y)$}{$\forall_e\;$ 1}; \proofbox{ \proofstep{$P(y)$}{assumption}; } \proofbox{ \proofstep{$Q(y)$}{assumption}; \proofstep{$\myex{x}{Q(x)}$}{$\exists_i\;$ 5}; \proofstep{$\myall{x}{P(x)} \vee \myex{x}{Q(x)}$}{$\vee_{i2}\;$ 7}; \proofstep{$\bot$}{$\neg e\;$ 2,7}; \proofstep{$P(y)$}{$\bot_e\;$ 8}; } \proofstep{$P(y)$}{$\vee_e\;$ 3, 4--4, 5--9}; } \proofstep{$\myall{x}{P(x)}$}{$\forall_i\;$ 3--10}; \proofstep{$\myall{x}{P(x)} \vee \myex{x}{Q(x)}$}{$\vee_{i1}\;$ 11}; \proofstep{$\bot$}{$\neg_e\;$ 2,12}; } \proofstep{$\myall{x}{P(x)} \vee \myex{x}{Q(x)}$}{PBC\; 2--13}; } \end{tikzpicture}} \end{exampleblock} \end{frame}