**Description** Sistemare la seconda parte dell'ex8 dando una dimostrazione formale della non-terminazione