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