now

let s be State of SCM+FSA ; :: thesis: ( (Stop SCM+FSA ) +* (Start-At (insloc 0 )) c= s implies s is halting )
assume A1: (Stop SCM+FSA ) +* (Start-At (insloc 0 )) c= s ; :: thesis: s is halting
dom (Stop SCM+FSA ) misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then A2: Stop SCM+FSA c= (Stop SCM+FSA ) +* (Start-At (insloc 0 )) by FUNCT_4:33;
then A3: dom (Stop SCM+FSA ) c= dom ((Stop SCM+FSA ) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
dom (Stop SCM+FSA ) = {(insloc 0 )} by AFINSQ_1:36, CARD_1:87;
then A4: insloc 0 in dom (Stop SCM+FSA ) by TARSKI:def 1;
A5: IC SCM+FSA in dom ((Stop SCM+FSA ) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
CurInstr (Computation s,0 ) = CurInstr s by AMI_1:13
.= s . (IC s) by AMI_1:def 17
.= s . (s . (IC SCM+FSA )) by AMI_1:def 15
.= s . (((Stop SCM+FSA ) +* (Start-At (insloc 0 ))) . (IC SCM+FSA )) by A1, A5, GRFUNC_1:8
.= s . (insloc 0 ) by SF_MASTR:66
.= ((Stop SCM+FSA ) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A1, A3, A4, GRFUNC_1:8
.= (Stop SCM+FSA ) . (insloc 0 ) by A2, A4, GRFUNC_1:8
.= halt SCM+FSA by AFINSQ_1:38 ;
hence s is halting by AMI_1:def 20; :: thesis: verum

end;

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