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