\begin{slide}{CP-Anwendung: Polynom-Interpretationen}

  \begin{itemize}\itemsep 1pt 
  \item Berechnungsmodell: Wortersetzung ($\approx$
    Turingmaschine)
  \item Programm: $ab \to ba$ ($\approx$ Bubble-Sort)

    Beispiel-Rechnung: $abab \to baab \to baba \to bbaa$
  \item Bewertung $W$ durch lineare Funktionen 
    $f_a(x) = Px+Q, f_b(x)=Rx+S$ mit $P,Q,R,S\in \NN$

    $W(abab) = f_a(f_b(f_a(f_b(0)))), \ldots$
  \item monoton: $x > y \Rightarrow f_a(x) > f_a(y)
    \wedge f_b(x)>f_b(y)$
  \item kompatibel mit Programm:
    $f_a(f_b(x) > f_b(f_a(x))$
  \item resultierendes Constraint-System für
    $P,Q,R,S$, 
  \item Lösung mittels Z3
  \end{itemize}

\end{slide}
