mult(0, m) = 0
mult(1, m) = m
mult(n0, m) = add(mult(n,m),mult(n,m))
mult(n1, m) = add(add(mult(n,m),mult(n,m)), m)
Montrons par induction structurelle sur nat que \forall n \;m : nat, \left[\!| mult\left(n,m\right) |\!\right] = \left[\!| n |\!\right] \times \left[\!| m |\!\right]
Premier cas : \left[\!| mult\left(0,m\right) |\!\right] = 0 = 0 \times \left[\!| m |\!\right] = \left[\!| 0 |\!\right] \times \left[\!| m |\!\right]
Second cas : \left[\!| mult\left(1,m\right) |\!\right] = m = 1 \times \left[\!| m |\!\right] = \left[\!| 1 |\!\right] \times \left[\!| m |\!\right]
Hypothèse d'induction : \forall x:nat, n:nat \;\text{fixe}, \left[\!| mult\left(n,x\right) |\!\right] = \left[\!| n |\!\right] \times \left[\!| x |\!\right].
Alors, cas 3 et 4 :
\left[\!|mult(n0, x)|\!\right] = \left[\!|add(mult(n,x),mult(n,x))|\!\right]
= \left[\!|mult(n,x)|\!\right]+\left[\!|mult(n,x) |\!\right] par les propriétés de add
= \left[\!| n |\!\right] \times \left[\!| x |\!\right] + \left[\!| n |\!\right] \times \left[\!| x |\!\right] par l'hypothèse d'induction (2 fois)
= n\times x + n\times x = 2\times n \times x
= \left[\!| n0 |\!\right]_{nat} \times \left[\!| x |\!\right]_{nat}
\left[\!| mult(n1, x) |\!\right] = \left[\!|add(add(mult(n,x),mult(n,x)), x)|\!\right]
= \left[\!|add(mult(n,x),mult(n,x))|\!\right] + \left[\!|x)|\!\right] : prop. de add
= \left[\!|mult(n,x)|\!\right] +\left[\!|mult(n,x)|\!\right]+ \left[\!|x)|\!\right] : prop. de add
= \left[\!| n |\!\right] \times \left[\!| x |\!\right] + \left[\!| n |\!\right] \times \left[\!| x |\!\right] + \left[\!|x)|\!\right] : hyp. d'induction (2 fois)
= n \times x + n \times x + 1 \times x : sémantique de nat
= (2\times n + 1) \times x
= \left[\!| n1 |\!\right]_{nat} \times \left[\!| x |\!\right]_{nat}
