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.