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

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