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: ∀
xs, ys
:
monoton xs && monoton ys
⇒
monoton (merge xs ys)
Beweis: Indukt. über
length xs + length ys