On considère comme une macro-instruction l'image j+(k) par réécriture d'une instruction k de A. On exécute en parallèle les codes A et j+(A). On donne au départ des valeurs indéfinies à t et à tous les qii Î I. On montre facilement, par récurrence, qu'à chaque pas s Î IN (un pas correspond à l'exécution d'une instruction ou d'une macro-instruction)
(Formellement, comme c'est évidemment vrai au début du programme, il suffit de vérifier que si la propriété est vérifiée pour s, elle l'est aussi pour s+1. Soit k Î A la position du programme dans A à l'instant s. Si l'instruction k effectue un saut dans A à l'instruction l, alors compte tenu de la correspondance entre les valeurs des registres, l'instruction j+(k) effectue un saut à l'instruction l de j+(A), donc le programme est à l'instruction l Î A et j+(l) Î j+(A) à l'instant s+1.
Ainsi, à une trace d'exécution de A correspond une trace d'exécution de j+(A) ayant un comportement identique vis à vis de l'extérieur. Comme l'exécution est déterministe, la trace observée pour j+(A) est la seule possible.