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

proof

now

dom (Stop SCM+FSA) misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
then A1: Stop SCM+FSA c= (Stop SCM+FSA) +* (Start-At (0,SCM+FSA)) by FUNCT_4:33;
A2: dom (Stop SCM+FSA) c= dom ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))) by FUNCT_4:11;
A3: 0 in dom (Stop SCM+FSA) by AFINSQ_1:69;
A4: IC SCM+FSA in dom ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
let s be State of SCM+FSA; :: thesis: ( (Stop SCM+FSA) +* (Start-At (0,SCM+FSA)) c= s implies ProgramPart s halts_on s )
assume A5: (Stop SCM+FSA) +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: ProgramPart s halts_on s
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = CurInstr ((ProgramPart s),s) by EXTPRO_1:3
.= s . (IC s) by COMPOS_1:38
.= s . (IC ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)))) by A5, A4, GRFUNC_1:8
.= s . 0 by COMPOS_1:142
.= ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))) . 0 by A5, A2, A3, GRFUNC_1:8
.= (Stop SCM+FSA) . 0 by A1, A3, GRFUNC_1:8
.= halt SCM+FSA by AFINSQ_1:38 ;
hence ProgramPart s halts_on s by EXTPRO_1:30; :: thesis: verum

end;

then (Stop SCM+FSA) +* (Start-At (0,SCM+FSA)) is halting by EXTPRO_1:def 10;
hence Stop SCM+FSA is parahalting by SCMFSA6B:def 3; :: thesis: verum

end;

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

proof

now

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

end;

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

end;