\begin{frame} \small \begin{block}{Well-Founded Induction} \smallskip given \begin{itemize} \item strongly normalizing ARS $\AA = \ARS$ \item<2-> % property \BLUE{P} of ARSs that satisfies \quad % $\text{\BLUE{P}}(\AA) \quad\iff\quad % \forall a \colon \text{\BLUE{P}}(a)$ property \BLUE{P} over the elements of $\AA$ \end{itemize} \medskip \onslide<3-> to conclude \begin{itemize} \item % $\text{\BLUE{P}}(\AA)$ $\forall a \in A \colon \text{\BLUE{P}}(a)$ \end{itemize} \medskip \onslide<4-> it is sufficient to prove \begin{itemize} \item if $\underbrace{\BLACK{\text{$\text{\BLUE{P}}(b)$ for every $b$ with $a \to b$}}}_{\text{\small \alert<4>{induction hypothesis}}}$ then $\text{\BLUE{P}}(a)$ \end{itemize} for arbitrary element $a$ \onslide<5-> \[ \biggl(\forall a \colon \Bigl(\forall b \colon a \to b ~\Longrightarrow~ \text{\BLUE{P}}(b)\Bigr) ~\Longrightarrow~ \text{\BLUE{P}}(a)\biggr) \quad\Longrightarrow\quad \forall a \colon \text{\BLUE{P}}(a) \qquad\qquad \] \end{block} \end{frame}