let i be Instruction of SCM+FSA; :: thesis: ( not i destroys intloc 0 implies Macro i is good )
assume not i destroys intloc 0 ; :: thesis: Macro i is good
then not Macro i destroys intloc 0 by Th77;
hence Macro i is good by SCMFSA7B:def 5; :: thesis: verum