In order to the have possibility of verifying assembler programs written for the VAMP (Verified Architecture Microprocessor 1) using the abstract software machine we need to relate the VAMP formal specification with the abstract software machine specification. The software machine does not support interrupt handling and therefore programs to be executed on this machine should not produce any interrupts. In the previous work [11] the conditions for absence of interrupts were identified and their validity was proved using the PVS verification system. Besides that, a theorem was established which states that under certain conditions (including the conditions for absence of interrupts) the execution of a program on the software machine is equivalent to the execution of this program on the VAMP.