\begin{slide}{Append ist assoziativ}
\begin{verbatim}
data List a = Nil | Cons a ( List a ) 
    deriving (Show, Eq)
append :: List a -> List a -> List a 
append xs ys = case xs of
    Nil        -> ys
    Cons x xs' -> Cons x ( append xs' ys )
\end{verbatim}
Behauptung:  
\begin{verbatim}
forall a :: Type, forall xs, ys, zs :: List a
  append xs (append ys zs) 
    == append (append xs ys) zs
\end{verbatim}
Beweis:

Fall 1: \verb|xs = Nil| (Induktionsanfang)
Fall 2: \verb|xs = Cons x xs'| (Induktionsschritt)

\newpage

Fall 1: \verb|xs = Nil| (Induktionsanfang)
\begin{verbatim}
append Nil (append ys zs) 
   =?= append (append Nil ys) zs
(append ys zs) =?= append (append Nil ys) zs
(append ys zs) =?= append      ys zs
\end{verbatim}
Terme sind identisch

Fall 2: \verb|xs = Cons x xs'| (Induktionsschritt)
\begin{verbatim}
append (Cons x xs') (append ys zs) 
   =?= append (append (Cons x xs') ys) zs
Cons x (append xs' (append ys zs))
   =?= append (Cons x (append xs' ys)) zs
Cons x (append xs' (append ys zs))
   =?= Cons x (append (append xs' ys) zs)
\end{verbatim}
Teilterme sind äquivalent nach Induktionsannahme

\end{slide}
