let i be Instruction of SCM+FSA ; :: thesis: ( i does_not_destroy intloc 0 implies Macro i is good )
set I = Macro i;
A1: rng (Macro i) c= {i,(halt SCM+FSA )} by FUNCT_4:65;
assume A2: i does_not_destroy intloc 0 ; :: thesis: Macro i is good

now

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

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

suppose x = i ; :: thesis: b₁ does_not_destroy intloc 0

hence x does_not_destroy intloc 0 by A2; :: thesis: verum

end;

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

hence x does_not_destroy intloc 0 by SCMFSA7B:11; :: thesis: verum

end;

end;

end;

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