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;
then A2: dom (Stop SCM+FSA ) c= dom ((Stop SCM+FSA ) +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;
dom (Stop SCM+FSA ) = {0 } by AFINSQ_1:36, CARD_1:87;
then A3: 0 in dom (Stop SCM+FSA ) by TARSKI:def 1;
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 (Comput (ProgramPart s),s,0 )),(Comput (ProgramPart s),s,0 ) = CurInstr (ProgramPart s),s by u
.= s . (IC s) by AMI_1:def 16, Z
.= 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