Procediamo per induzione strutturale su l

Caso []:

Dobbiamo dimostrare forall x, count x [] = count x (isort [])

Ovvero forall x, count x [] = count x []

Sia x un numero naturale

Dobbiamo dimostrare count x [] = count x []

Ovvero 0 = 0

Ovvio

Caso y : l:

Per ipotesi induttiva count x l = count x (isort l) ( II )

Dobbiamo dimostrare forall x, forall y, count x (y : l) = count x (isort (y : l)),

Ovvero forall x, forall y, count x (y : l) = count x (insert y (isort l)),

Ovvero forall x, forall y,

(if x == y then 1 else 0) + count x l = count x (insert y (isort l)),

Per II ci riduciamo a dimostrare

(if x == y then 1 else 0) + count x (isort l) = count x (insert y (isort l))

Siano x, y numeri naturali

Caso x == y:

Dobbiamo dimostrare 1 + count x (isort l) = count x (insert y (isort l)),

Ovvero per Lemma 1a, 1 + count x (isort l) = 1 + count x (isort l),

Ovvio per II

Caso non x == y:

Dobbiamo dimostrare 0 + count x (isort l) = count x (insert y (isort l)),

Ovvero per Lemma 1b, 0 + count x (isort l) = 0 + count x (isort l),

Ovvio II

Lemma 1a: forall x, y tc x == y, count x (insert y l) = count x l + 1

Lemma 1b: forall x, y tc non x == y, count x (insert y l) = count x l + 0