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