thus Stop SCM+FSA is parahalting ; :: thesis: Stop SCM+FSA is good
let i be Instruction of SCM+FSA; :: according to SCMFSA7B:def 4,SCMFSA7B:def 5 :: thesis: ( not i in rng (Stop SCM+FSA) or not i destroys intloc 0 )
A6: rng (Stop SCM+FSA) = {(halt SCM+FSA)} by AFINSQ_1:33;
assume i in rng (Stop SCM+FSA) ; :: thesis: not i destroys intloc 0
then i = halt SCM+FSA by A6, TARSKI:def 1;
hence not i destroys intloc 0 ; :: thesis: verum