Réponse:   La fonction réécrit est récursive. Cependant l'argument de chaque appel récursif est un sous-arbre strict de l'argument de l'appel principal, sauf dans le premier cas du filtrage: l'argument de l'appel principal est alors un noeud de la forme G1_EE(u,v) et l'argument de l'appel récursif est un noeud de même forme G1_EE(u',v') tel que u' soit un sous-arbre strict de u. On ne peut donc passer par le premier cas de filtrage qu'un nombre fini de fois; ensuite l'argument de l'appel récursif ne peut que décroître strictement.