let a be Int-Location ; :: thesis: not Stop SCM+FSA destroysdestroy a

now

let i be Instruction of SCM+FSA ; :: thesis: ( i in rng (Stop SCM+FSA ) implies not i destroysdestroy a )
A1: rng (Stop SCM+FSA ) = {(halt SCM+FSA )} by AFINSQ_1:36;
assume i in rng (Stop SCM+FSA ) ; :: thesis: not i destroysdestroy a
then i = halt SCM+FSA by A1, TARSKI:def 1;
hence not i destroysdestroy a by SCMFSA7B:11; :: thesis: verum

end;

hence not Stop SCM+FSA destroysdestroy a by SCMFSA7B:def 4; :: thesis: verum