Beispiel Denotationale Semantik

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 ...
Behauptung:  monoton xs && monoton ys 
                 => monoton (merge xs ys)
Beweis d. Induktion 
       über length xs + length ys