Abstract : In this paper, we present an attempt to build a calculus of explicit substitution expected to be confluent on open terms, to preserve strong normalisation and to simulate one step `b-reduction. We show why our attempt failed and we explain how we found a counter-example to the strong normalisation or termination of the substitution calculus. As a consequence, we provide also a counter-example to the strong normalisation of another calculus, namely~`t (the substitution calculus of `l`t) of Riòs, for which the problem was open.
Résumé : Dans cet article, nous rendons compte d'une tentative pour construire un calcul de substitutions explicite sensé être confluent sur les termes ouverts, préserver la forte normalisation et simuler la `b-r\'eduction en une seule étape. Nous montrons pourquoi notre tentative a échoué et nous expliquons comment nous avons trouvé un contrexemple à la terminaison du calcul de substitutions. Comme conséquence nous exhibons un contrexemple à la forte normalisation d'un autre calcul à savoir le calcul `t (le calcul de substitution de `l`t) de Riòs, pour lequel le problème était ouvert.