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 COMPOS_1:146, 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 EXTPRO_1:3;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Comput ((ProgramPart s),s,0) = s by EXTPRO_1:3;
then CurInstr ((ProgramPart (Comput ((ProgramPart s),s,0))),(Comput ((ProgramPart s),s,0))) = CurInstr ((ProgramPart s),s)
.= s . 0 by A2, Y, COMPOS_1:143
.= ((Macro (halt SCM+FSA)) +* (Start-At (0,SCM+FSA))) . 0 by A2, A1, GRFUNC_1:8
.= halt SCM+FSA by COMPOS_1:148, SCMFSA6B:33 ;
hence (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) by A3, EXTPRO_1:6, NAT_1:2; :: thesis: verum

end;

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