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 SF_MASTR:64;
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 SF_MASTR:65;
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
Z: (ProgramPart s) /. (IC s) = s . (IC s) by AMI_1:150;
u: Comput (ProgramPart s),s,0 = s by AMI_1:13;
CurInstr (ProgramPart s),(Comput (ProgramPart s),s,0 ) = CurInstr (ProgramPart s),s by u
.= s . (IC s) by Z, AMI_1:def 16
.= s . (s . (IC SCM+FSA )) by AMI_1:def 15
.= s . (((Stop SCM+FSA ) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA )) by A5, A4, GRFUNC_1:8
.= s . 0 by SF_MASTR:66
.= ((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 AMI_1:146; :: thesis: verum

end;

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

end;

thus Stop SCM+FSA does_not_destroy 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 i does_not_destroy intloc 0 )
A1: rng (Stop SCM+FSA ) = {(halt SCM+FSA )} by AFINSQ_1:36;
assume i in rng (Stop SCM+FSA ) ; :: thesis: i does_not_destroy intloc 0
then i = halt SCM+FSA by A1, TARSKI:def 1;
hence i does_not_destroy intloc 0 by Th11; :: thesis: verum

end;

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

end;