\documentclass{article}
\usepackage[a4paper, total={7in, 10in}]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{minted}
\usepackage{amssymb, amsmath}

\begin{document}
\section{Récursivité enveloppée}
\begin{align*}
	f\ \text{est récursive enveloppée} \overset{\text{def}}{\iff} \exists \ldots,\ \forall x \in D_f,\ f(x) = \begin{cases}
		\text{valeur de base} & \text{si $x$ est un cas de base} \\
		g(x, f(h_1(x)), \ldots, f(h_k(x))) & \text{sinon}
\end{cases}
\end{align*}	
\section{Récursivité terminale}
\begin{align*}
	f\ \text{est récursive terminale} \overset{\text{def}}{\iff} \exists \ldots,\ \forall x \in D_f,\ f(x) = \begin{cases}
		\text{valeur de base} & \text{si $x$ est un cas de base} \\
		f(g(x)) & \text{sinon}
\end{cases}
\end{align*}
\section{Ordre lexicographique}
\begin{align*}
	\forall (a, b), (c, d) \in E^2,\ (a, b) \le_{\text{lex}} (c, d) \overset{\text{def}}{\iff} a <_E c \ \text{ou}\ (a = c\ \text{et}\ b \le_E d)
\end{align*}
\section{Terminaison}
\begin{align*}
	\forall E \in \text{bien ordonnés},\ \forall f : E\to F,\ f\ \text{termine} \overset{\text{def}}{\iff} \begin{cases}
		f\ \text{récursive} \\
		\min E \in \text{cas de base} \\
		\text{les appels récursifs se font sur des} \\
		\text{éléments de $E$ strictement plus petits}
\end{cases}
\end{align*}
\section{Correction}
\subsection{Pour les récursives}
\begin{align*}
	E\ \text{bien ordonné} \implies \left( \left( \forall x \in E,\ \left( \forall y < x,\ P(y) \right) \implies P(x) \right) \implies \forall x \in E,\ P(x) \right)
\end{align*}

\begin{align*}
	f\ \text{correcte} \impliedby \begin{cases}
		f\ \text{récursive} \\
		f : E \to F \\
		f\ \text{termine} \\
		f\ \text{correcte sur les cas de base} \\
		\text{sur les autres cas, $f$ est correcte en supposant qu'elle l'est sur ses appels récursifs}
\end{cases}
\end{align*}
\subsection{Sur les itératives}

On trouve un invariant de boucle (une expression qui dépend de l'index d'itération et qui est vraie peut importe la valeur de l'index)
\end{document}