| · | Supposons que l'évaluation de a s'arête. Si son évaluation s'arête sur une erreur on a ¬ C(a) donc A(a). Sinon, comme le programme ne boucle pas, il s'évalue en une valeur donc C(a) est correct; d'autre part, let x = a in b est incorrect, i.e. ¬ ( C (let x = a in b)), donc on a A(A). |
| · | Supposons maintenant que l'évaluation de a boucle. En particulier, son évaluation ne s'arête pas sur une valeur, donc elle est correcte, i.e. ¬ ( C(a)) est faux. De plus, l'évaluation de let x = a in b boucle également donc, C(let x = a in b). Donc finalement A(a) est faux. |