let aa be Int-Location ; :: thesis: Stop SCM+FSA does_not_refer aa
A1: rng (Stop SCM+FSA ) = {(halt SCM+FSA )} by AFINSQ_1:36;
let i be Instruction of SCM+FSA ; :: according to SCMFSA7B:def 2 :: thesis: ( not i in proj2 (Stop SCM+FSA ) or i does_not_refer aa )
assume i in rng (Stop SCM+FSA ) ; :: thesis: i does_not_refer aa
then i = halt SCM+FSA by A1, TARSKI:def 1;
hence i does_not_refer aa by SCMFSA8C:78; :: thesis: verum