Considerare il seguente algoritmo, noto con il nome di insertion sort, per ordinare una lista di numeri:

isort [] = [] isort (x : l) = insert x (isort l)

dove insert è stata definita nella sessione di allenamento (e su insert sono state dimostrate certe proprietà).

insert x [] = x : []

insert x (y : l) = if x <= y then x : y : l else y : (insert x l)

Teorema: sorted (isort l) = true

Procediamo per Ind. strutt. su l per dimostrare

sorted (isort l) = true

Caso []:

sorted(isort []) = true

ovvero sorted [] = true

ovvero true = true

Ovvio

Caso x : l:

Per ipotesi induttiva, sorted (isort l) = true ( II )

Dobbiamo dimostrare forall x, sorted(isort x : l) = true

Ovvero forall x, sorted(insert x (isort l)) = true