let s be State of SCMPDS ; :: according to AMI_1:def 26,SCMPDS_4:def 10 :: thesis: ( not Initialize (stop (Load (halt SCMPDS ))) c= s or ProgramPart s halts_on s )
set m = Load (halt SCMPDS );
set m0 = stop (Load (halt SCMPDS ));
set m1 = Initialize (stop (Load (halt SCMPDS )));
assume A1: Initialize (stop (Load (halt SCMPDS ))) c= s ; :: thesis: ProgramPart s halts_on s
dom (Start-At 0 ,SCMPDS ) = {(IC SCMPDS )} by FUNCOP_1:19;
then A2: IC SCMPDS in dom (Start-At 0 ,SCMPDS ) by TARSKI:def 1;
then A3: IC SCMPDS in dom (Initialize (stop (Load (halt SCMPDS )))) by FUNCT_4:13;
A4: IC (Initialize (stop (Load (halt SCMPDS )))) = (Initialize (stop (Load (halt SCMPDS )))) . (IC SCMPDS )
.= (Start-At 0 ,SCMPDS ) . (IC SCMPDS ) by A2, FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
take 0 ; :: according to AMI_1:def 20 :: 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 (stop (Load (halt SCMPDS ))) misses dom (Start-At 0 ,SCMPDS ) by Th54;
then A6: stop (Load (halt SCMPDS )) c= Initialize (stop (Load (halt SCMPDS ))) by FUNCT_4:33;
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;
then A9: 0 in dom (Initialize (stop (Load (halt SCMPDS )))) by FUNCT_4:13;
u: Comput (ProgramPart s),s,0 = s by AMI_1:13;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
CurInstr (ProgramPart s),(Comput (ProgramPart s),s,0 ) = CurInstr (ProgramPart s),s by u
.= s . (IC (Initialize (stop (Load (halt SCMPDS ))))) by A1, A3, Y, GRFUNC_1:8
.= (Initialize (stop (Load (halt SCMPDS )))) . 0 by A1, A9, A4, GRFUNC_1:8
.= (stop (Load (halt SCMPDS ))) . 0 by A6, A8, GRFUNC_1:8
.= halt SCMPDS by A5, A7, Th37 ;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,0 ) = halt SCMPDS ; :: thesis: verum