95/369
\begin{frame}
\begin{lemma}
Let $\AA$ well-founded monotone $\Sigma$-algebra.
Then $>_\AA$ is closed under contexts.
\end{lemma}
\pause

\begin{proof}
Let $s,t \in \TTlong$ such that $t >_\AA s$. \pause
We show $C[s] >_\AA C[t]$ for every $C[\;]$.\pause\smallskip

That is: $[C[t],\alpha] > [C[s],\alpha]$ for every $\alpha : \VV \to A$.\pause\smallskip

Let $\alpha : \VV \to A$. \pause We show $[C[t],\alpha] > [C[s],\alpha]$ by induction over structure of $C[\;]$:
\vspace{-.6em}
\begin{align*}
\onslide<7-> C[\;] \equiv [\;] \Rightarrow\ &\onslide<8->\interpret{C[t]} = \interpret{t} > \interpret{s} = \interpret{C[s]}\\
\onslide<9->C[\;] \equiv f(t_1,\ldots,t_n) \Rightarrow\
&\onslide<10->\text{Let $i$ such that $t_i$ contains the hole $\Box$.}\\
&\onslide<11->\text{Then $C[u] = f(t_1,\ldots,t_i[u],\ldots,t_n)$. Hence}\\
&\onslide<12->\text{\quad$[C[s],\alpha] = [f]([t_1,\alpha],\ldots,[t_i[s],\alpha],\ldots,[t_n,\alpha])$.}\\
&\onslide<13->\text{\quad$[C[t],\alpha] = [f]([t_1,\alpha],\ldots,[t_i[t],\alpha],\ldots,[t_n,\alpha])$.}\\
&\onslide<14->\text{By IH $\interpret{t_i[t],\alpha} > \interpret{t_i[s],\alpha}$}.\\
&\onslide<15->\text{By monotonicity $\interpret{C[t],\alpha} > \interpret{C[s],\alpha}$.}
\end{align*}
\end{proof}
\end{frame}