Théorème

Si 

• R est l'environnement de la machine

• E est l'environnement du langage source

• c (loc (v , map)  , R) = c (v , E)

Alors

outcome (compile (e , t) , R)  =_t a (ac , value (e , E) , R)

        -> compiler le programme revient à mettre dans l'accumulateur le résultat du programme

              et seul l'accumlateur et les registres d'adresses > ou égale à t sont modifiés