set SA0 = Start-At (0,SCMPDS);
set ii = (DataLoc (0,0)) := 0;
set m0 = stop (Load ((DataLoc (0,0)) := 0));
set m1 = Initialize (stop (Load ((DataLoc (0,0)) := 0)));
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 10 :: thesis: ( not stop (Load ((DataLoc (0,0)) := 0)) c= s or ProgramPart s halts_on s )
assume A2: stop (Load ((DataLoc (0,0)) := 0)) c= s ; :: thesis: ProgramPart s halts_on s
take 1 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart s),s,1)) in proj1 (ProgramPart s) & CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,1))) = halt SCMPDS )
IC (Comput ((ProgramPart s),s,1)) in NAT ;
hence IC (Comput ((ProgramPart s),s,1)) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,1))) = halt SCMPDS
A4: IC s = 0 by COMPOS_1:def 16;
then A5: IC (Exec (((DataLoc (0,0)) := 0),s)) = succ 0 by SCMPDS_2:57
.= 0 + 1 ;
1 in dom (stop (Load ((DataLoc (0,0)) := 0))) by Th9;
then (stop (Load ((DataLoc (0,0)) := 0))) . 1 = s . 1 by A2, GRFUNC_1:8;
then A6: s . 1 = halt SCMPDS by Th10;
0 in dom (stop (Load ((DataLoc (0,0)) := 0))) by Th9;
then A7: (stop (Load ((DataLoc (0,0)) := 0))) . 0 = s . 0 by A2, GRFUNC_1:8;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Comput ((ProgramPart s),s,(0 + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,0))) by EXTPRO_1:4
.= Following ((ProgramPart s),s) by EXTPRO_1:3
.= Exec (((DataLoc (0,0)) := 0),s) by A4, A7, Th10, Y ;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,1))) = halt SCMPDS by A6, A5, COMPOS_1:38; :: thesis: verum