let i be Instruction of SCM+FSA; :: thesis: ( not i destroys intloc 0 implies Macro i is good )
set I = Macro i;
A1: rng (Macro i) = {i,(halt SCM+FSA)} by COMPOS_1:67;
assume A2: not i destroys intloc 0 ; :: thesis: Macro i is good

now :: thesis: for x being Instruction of SCM+FSA st x in rng (Macro i) holds
not x destroys intloc 0

let x be Instruction of SCM+FSA; :: thesis: ( x in rng (Macro i) implies not b₁ destroys intloc 0 )
assume A3: x in rng (Macro i) ; :: thesis: not b₁ destroys intloc 0

per cases ( x = i or x = halt SCM+FSA ) by A1, A3, TARSKI:def 2;

suppose x = i ; :: thesis: not b₁ destroys intloc 0

hence not x destroys intloc 0 by A2; :: thesis: verum

end;

suppose x = halt SCM+FSA ; :: thesis: not b₁ destroys intloc 0

hence not x destroys intloc 0 by SCMFSA7B:5; :: thesis: verum

end;

end;

end;

then not Macro i destroys intloc 0 by SCMFSA7B:def 4;
hence Macro i is good by SCMFSA7B:def 5; :: thesis: verum