Informatique-Cycles et unification

Contexte.
Soit G un graphe orienté dont les arcs sont étiquetés par des entiers naturels. On suppose que :
A0. Les arcs sortants d’un sommet donné sont étiquetés par des entiers consécutifs en partant de 0.
A1. G est acyclique.
Le graphe G est représenté en Python par une variable globale G.
C’est un dictionnaire dont les clés sont les sommets et les valeurs sont des listes représentant les arcs sortants.
L’étiquette d’un arc correspond à son indice dans la liste.
En particulier, les étiquettes des arcs sont implicites et l’hypothèse A0 est automatiquement satisfaite.
Dans ce problème, certaines des fonctions étudiées modifient G en ajoutant de nouveaux arcs.
L’hypothèse A1 est un invariant qui sera maintenu en toute circonstance.

Organisation du sujet.
La première partie étudie finement un parcours en profondeur pour pouvoir vérifier efficacement qu’un nouvel arc ne crée pas de cycles dans G.
La deuxième partie étudie les notions de forme normale et d’unification dans G.
Cette partie