set Mi = Macro (halt SCM+FSA );

hereby :: according to SCMFSA6B:def 4 :: thesis: Macro (halt SCM+FSA ) is parahalting

A1: 0 in dom ((Macro (halt SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by SCMFSA6B:31;
let s be State of SCM+FSA ; :: thesis: ( (Macro (halt SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= s implies for k being Element of NAT holds (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) )
assume A2: (Macro (halt SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= s ; :: thesis: for k being Element of NAT holds (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 )
let k be Element of NAT ; :: thesis: (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 )
A3: s = Comput (ProgramPart s),s,0 by AMI_1:13;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Comput (ProgramPart s),s,0 = s by AMI_1:13;
then CurInstr (ProgramPart (Comput (ProgramPart s),s,0 )),(Comput (ProgramPart s),s,0 ) = CurInstr (ProgramPart s),s
.= s . 0 by A2, Y, SF_MASTR:67
.= ((Macro (halt SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) . 0 by A2, A1, GRFUNC_1:8
.= halt SCM+FSA by SCMFSA6B:33 ;
hence (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) by A3, AMI_1:52, NAT_1:2; :: thesis: verum

end;

thus Macro (halt SCM+FSA ) is parahalting by Lm1; :: thesis: verum