\begin{slide}{Beispiel Denotationale Semantik}
\begin{verbatim}
monoton :: Ord a => [a] -> Bool
monoton (x : y : zs) = 
    x <= y && monoton (y:zs)
monoton  _ = True

merge :: Ord a => [a] -> [a] -> [a]
merge [] ys = ys ; merge xs [] = xs
merge (x:xs) (y:ys) = 
    if x <= y then x : merge ... ...
              else ...
\end{verbatim}
Behauptung: $\forall$ \verb|xs, ys|:
\verb|monoton xs && monoton ys|
$\Rightarrow$
\verb|monoton (merge xs ys)|

Beweis: Indukt. über 
\verb|length xs + length ys|

\end{slide}
