Beispiel Verifikation

app x y = case x of
    [] -> y
    h : t -> h : app t y

Beweise

app x (app y z) == app (app x y) z

Beweismethode: Induktion nach x.

• Induktionsanfang: x == [] ...
• Induktionsschritt: x == h : t ...