Dimostriamo i due lemmi precedenti. Per evitare di fare il lavoro due volte, compattiamo il loro enunciato in un unico enunciato che andiamo a dimostrare.

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

Procediamo per induzione strutturale su l per dimostrare

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

Caso []:

Dobbiamo dimostrare forall x, forall y,

count x (insert y []) = count x [] + if x == y then 1 else 0

Ovvero forall x, forall y, count x (y : []) = 0 + if x == y then 1 else 0

Ovvero forall x, forall y, (if x == y then 1 else 0) + count x [] = 0 + if x == y then 1 else 0

Ovvero forall x, forall y, (if x == y then 1 else 0) + 0 = 0 + if x == y then 1 else 0

Siano x, y fissati

Procediamo per casi

Caso x == y:

Dobbiamo dimostrare (if x == y then 1 else 0) + 0 = 0 + if x == y then 1 else 0

Ovvero 1 + 0 = 0 + 1

Ovvio per proprietà della somma

Caso non x == y:

Dobbiamo dimostrare (if x == y then 1 else 0) + 0 = 0 + if x == y then 1 else 0

Ovvero 0 + 0 = 0 + 0

Ovvio per proprietà della somma

Caso t : l:

Per ipotesi induttiva, forall x, forall y, count x (insert y l) = count x l + if x == y then 1 else 0 ( II )

Dobbiamo dimostrare forall x, forall y, forall t,

count x (insert y (t : l)) = count x (t : l) + if x == y the 1 else 0

Ovvero forall x, forall y, forall t,

count x (if y ≤ t then y : t : l else t : (insert y l)) = (if x == t then 1 else 0) + count x l

• if x == y then 1 else 0

Siano x, y, t fissati

Per ipotesi induttiva ci riduciamo a dimostrare

count x (if y ≤ t then y : t : l else t : (insert y l)) = count x (insert y l) + if x == t then 1 else 0

Procediamo per casi:

Caso y ≤ t:

Dobbiamo dimostrare count x (y : t : l) = count x (insert y l) + if x == t then 1 else 0

Ovvero

(if x == y then 1 else o) + count x (t : l) = count x (insert y l) + if x == t then 1 else 0

Ovvero

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

Ovvero per II:

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

Procediamo per casi:

Caso x == t:

count x (insert y l) + 1 = count x (insert y l) + 1

Ovvio

Caso non x == t:

count x (insert y l) + 0 = count x (insert y l) + 0

Ovvio

Caso non y ≤ t:

Dobbiamo dimostrare count x (t : insert y l) = count x (insert y l) + if x == t then 1 else 0

Ovvero

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

Procediamo per casi

Caso x == t:

1 + count x (insert y l) = count x (insert y l) + 1

Ovvio per associatività della somma

Caso non x == t:

0 + count x (insert y l) = count x (insert y l) + 0

Ovvio per associatività della somma

QED