\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],\alpha} = \interpret{t,\alpha} > \interpret{s,\alpha} = \interpret{C[s],\alpha}\\ \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}