thus Stop SCM+FSA is parahalting :: thesis: Stop SCM+FSA is good

proof

A1: 0 in dom (Stop SCM+FSA) by AFINSQ_1:65;
A2: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 10 :: thesis: for b₁ being set holds
( not Stop SCM+FSA c= b₁ or b₁ halts_on s )
A3: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not Stop SCM+FSA c= P or P halts_on s )
assume A4: Stop SCM+FSA c= P ; :: thesis: P halts_on s
A5: dom P = NAT by PARTFUN1:def 2;
CurInstr (P,(Comput (P,s,0))) = CurInstr (P,s)
.= P . (IC s) by A5, PARTFUN1:def 6
.= P . (IC (Start-At (0,SCM+FSA))) by A3, A2, GRFUNC_1:2
.= P . 0 by FUNCOP_1:72
.= (Stop SCM+FSA) . 0 by A1, A4, GRFUNC_1:2
.= halt SCM+FSA ;
hence P halts_on s by EXTPRO_1:29; :: thesis: verum

end;

thus not Stop SCM+FSA destroys intloc 0 :: according to SCMFSA7B:def 5 :: thesis: verum

proof

now :: thesis: for i being Instruction of SCM+FSA st i in rng (Stop SCM+FSA) holds
not i destroys intloc 0

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (Stop SCM+FSA) implies 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

end;

hence not Stop SCM+FSA destroys intloc 0 ; :: thesis: verum

end;