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)
- si le programme A est à l'instruction k, alors le programme j+(A) est à l'instruction j+(k);
- les valeurs des qii Î I sont toutes identiques dans le programme j+(A) et égales à la valeur de t dans le programme A;
- pour tous les autres temporaires de A leur valeur dans j+(A) est
égale à leur valeur dans A.
(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.
- Si l'instruction l lit une valeur v dans t (la valeur de t à
l'instant s), la macro-instruction j+(l) lit à la place
la valeur de qi, donc v, pour un certain i de I.
- Si l'instruction l écrit v dans t , alors l'instruction j+(l)
écrit v dans pj puis écrit la valeur de pj donc v dans tous les
qi i Î I. )
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.