set ii = (DataLoc 0 ,0 ) := 0 ;
set m0 = stop (Load ((DataLoc 0 ,0 ) := 0 ));
set m1 = Initialized (stop (Load ((DataLoc 0 ,0 ) := 0 )));
set SA0 = Start-At (inspos 0 );
let s be State of SCMPDS ; :: according to AMI_1:def 26,SCMPDS_4:def 10 :: thesis: ( not Initialized (stop (Load ((DataLoc 0 ,0 ) := 0 ))) c= s or s is halting )
assume A1: Initialized (stop (Load ((DataLoc 0 ,0 ) := 0 ))) c= s ; :: thesis: s is halting
take 1 ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation s,1) = halt SCMPDS
Start-At (inspos 0 ) c= Initialized (stop (Load ((DataLoc 0 ,0 ) := 0 ))) by FUNCT_4:26;
then A2: Start-At (inspos 0 ) c= s by A1, XBOOLE_1:1;
dom (Start-At (inspos 0 )) = {(IC SCMPDS )} by FUNCOP_1:19;
then IC SCMPDS in dom (Start-At (inspos 0 )) by TARSKI:def 1;
then A3: IC s = (Start-At (inspos 0 )) . (IC SCMPDS ) by A2, GRFUNC_1:8
.= inspos 0 by FUNCOP_1:87 ;
A4: ( inspos 0 in dom (stop (Load ((DataLoc 0 ,0 ) := 0 ))) & inspos 1 in dom (stop (Load ((DataLoc 0 ,0 ) := 0 ))) ) by Th9;
stop (Load ((DataLoc 0 ,0 ) := 0 )) c= s by A1, SCMPDS_4:57;
then A5: ( (stop (Load ((DataLoc 0 ,0 ) := 0 ))) . (inspos 0 ) = s . (inspos 0 ) & (stop (Load ((DataLoc 0 ,0 ) := 0 ))) . (inspos 1) = s . (inspos 1) ) by A4, GRFUNC_1:8;
then A6: ( s . (inspos 0 ) = (DataLoc 0 ,0 ) := 0 & s . (inspos 1) = halt SCMPDS ) by Th10;
A7: IC (Exec ((DataLoc 0 ,0 ) := 0 ),s) = Next (inspos 0 ) by A3, SCMPDS_2:57
.= inspos (0 + 1) ;
Computation s,(0 + 1) = Following (Computation s,0 ) by AMI_1:14
.= Following s by AMI_1:13
.= Exec ((DataLoc 0 ,0 ) := 0 ),s by A3, A5, Th10 ;
hence CurInstr (Computation s,1) = halt SCMPDS by A6, A7, AMI_1:def 13; :: thesis: verum