\begin{slide}{Presburger-Arithmetik und große Zahlen}

(folgende Konstruktion ist ähnlich zu der,
die im tatsächlichen Beweis verwendet wird)

es gibt eine Folge von P-Formeln $F_0, F_1,\ldots$ mit
\begin{itemize}\itemsep 0pt
\item $|F_n| \in O(n)$
\item $F_n(x)\iff x=2^{2^n}$
\end{itemize}

Realisierung
\begin{itemize}\itemsep 0pt
\item 
verwende $G_n(x,y,z)$ mit Spezifikation
$x=2^{2^n} \wedge xy=z$

(die naive Implementierung ist aber zu groß)
\item
und Trick
(``the device preceding Theorem 8''):

$H(x_1)\wedge H(x_2)$ ist äquivalent zu

$\forall x\forall y: 
(x=x_1\vee \dots)\to \dots$
\end{itemize}

\end{slide}
