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 State of SCMPDS ; :: according to AMI_1:def 26,SCMPDS_4:def 10 :: thesis:
assume A1: Initialize (stop (Load ((DataLoc 0 ,0 ) := 0 ))) c= s ; :: thesis:
A2: stop (Load ((DataLoc 0 ,0 ) := 0 )) c= s by A1, SCMPDS_4:57;
take 1 ; :: according to AMI_1:def 20 :: thesis:
IC (Comput (ProgramPart s),s,1) in NAT ;
hence IC (Comput (ProgramPart s),s,1) in dom (ProgramPart s) by COMPOS_1:34; :: thesis:
dom (Start-At 0 ,SCMPDS ) = {(IC SCMPDS )} by FUNCOP_1:19;
then A3: IC SCMPDS in dom (Start-At 0 ,SCMPDS ) by TARSKI:def 1;
Start-At 0 ,SCMPDS c= Initialize (stop (Load ((DataLoc 0 ,0 ) := 0 ))) by FUNCT_4:26;
then Start-At 0 ,SCMPDS c= s by A1, XBOOLE_1:1;
then A4: IC s = (Start-At 0 ,SCMPDS ) . (IC SCMPDS ) by A3, GRFUNC_1:8
.= 0 by FUNCOP_1:87 ;
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;
Z: (ProgramPart (Comput (ProgramPart s),s,1)) /. (IC (Comput (ProgramPart s),s,1)) = (Comput (ProgramPart s),s,1) . (IC (Comput (ProgramPart s),s,1)) by COMPOS_1:38;
NX: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,1) by AMI_1:123;
Comput (ProgramPart s),s,(0 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,0 ) by AMI_1:14
.= Following (ProgramPart s),s by AMI_1:13
.= Exec ((DataLoc 0 ,0 ) := 0 ),s by A4, A7, Th10, Y ;
then CurInstr (ProgramPart s),(Comput (ProgramPart s),s,1) = halt SCMPDS by A6, A5, Z, NX, AMI_1:def 13;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,1) = halt SCMPDS ; :: thesis: