75/179
\begin{frame}
  \frametitle{Example}

  \begin{exampleblock}{}
  Prove \quad$\neg\neg p \to (\neg q \to r),\; p,\; \neg r \vdash q$\quad
  \emph{without} \;$\neg\neg_i$\; and \;MT.
  \medskip

  \begin{tikzpicture}
  \naturaldeduction{
    \mpause[1]{
      \proofstep{$\neg\neg p \to (\neg q \to r)$}{premise};
    }
    \mpause{
      \proofstep{$p$}{premise};
    }
    \mpause{
      \proofstep{$\neg r$}{premise};
    }
    \mpause{
      \proofbox{
        \mpause{
          \proofstep{$\neg p$}{assumption};
        }
        \mpause{
          \proofstep{$\bot$}{$\neg_e$ 2,4};
        }
      }
      \mpause{
        \proofstep{$\neg\neg p$}{$\neg_i$ 4--5};
      }
    }
    \mpause{
      \proofstep{$\neg q \to r$}{$\to_e$ 6,1};
    }
    \mpause{
      \proofbox{
        \mpause{
          \proofstep{$\neg q$}{assumption};
        }
        \mpause{
          \proofstep{$r$}{$\to_e$ 8,7};
        }
        \mpause{
          \proofstep{$\bot$}{$\neg_e$ 9,3};
        }
      }
      \mpause{
        \proofstep{$\neg\neg q$}{$\neg_i$ 8--10};
      }
    }
    \mpause{
      \proofstep{$q$}{$\neg\neg_e$ 11};
    }
  }
  \end{tikzpicture}
  \end{exampleblock}
\end{frame}