let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 10 :: thesis: ( stop (Load (halt SCMPDS)) c= s implies ProgramPart s halts_on s )
set m = Load (halt SCMPDS);
set m0 = stop (Load (halt SCMPDS));
assume A1: stop (Load (halt SCMPDS)) c= s ; :: thesis: ProgramPart s halts_on s
A4: IC s = 0 by COMPOS_1:def 16;
take 0 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart s),s,0)) in proj1 (ProgramPart s) & CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = halt SCMPDS )
IC (Comput ((ProgramPart s),s,0)) in NAT ;
hence IC (Comput ((ProgramPart s),s,0)) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = halt SCMPDS
A5: (Load (halt SCMPDS)) . 0 = halt SCMPDS by FUNCOP_1:87;
dom (Load (halt SCMPDS)) = {0} by FUNCOP_1:19;
then A7: 0 in dom (Load (halt SCMPDS)) by TARSKI:def 1;
then A8: 0 in dom (stop (Load (halt SCMPDS))) by FUNCT_4:13;
u: Comput ((ProgramPart s),s,0) = s by EXTPRO_1:3;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = (stop (Load (halt SCMPDS))) . 0 by A1, A8, A4, Y, u, GRFUNC_1:8
.= halt SCMPDS by A5, A7, AFINSQ_1:def 4 ;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = halt SCMPDS ; :: thesis: verum