Il existe quantité de méthodes pour prouver la terminaison d'un système de réécriture. La démarche couramment usitée consiste à affecter à chaque terme une valeur de complexité. Si cette valeur (positive) décroît au moins de 1 à chaque pas de réécriture, alors la terminaison est assurée. En 1979, Lankford se fait le porte drapeau de l'interprétation des termes par des fonctions polynomiales. Ce travail consiste en l'implantation d'un tel ordre dans le système CiME. Après avoir décrit plus en détail les ordres polynomiaux, nous exposerons les grandes lignes de l'implantation. Nous donnons enfin une application de cette méthode en vérifiant la terminaison de quelques lambda-calculs avec substitutions explicites.