let i be Instruction of SCMPDS ; :: thesis:
set SA0 = Start-At 0 ,SCMPDS ;
assume A1: for s being State of SCMPDS holds (Exec i,s) . (IC SCMPDS ) = succ (IC s) ; :: thesis:
set m0 = stop (Load i);
set m1 = Initialized (stop (Load i));
let t be State of SCMPDS ; :: according to AMI_1:def 26,SCMPDS_4:def 10 :: thesis:
assume A2: Initialized (stop (Load i)) c= t ; :: thesis:
A3: stop (Load i) c= t by A2, SCMPDS_4:57;
take 1 ; :: according to AMI_1:def 20 :: thesis:
IC (Comput (ProgramPart t),t,1) in NAT ;
hence IC (Comput (ProgramPart t),t,1) in dom (ProgramPart t) by AMI_1:143; :: thesis:
dom (Start-At 0 ,SCMPDS ) = {(IC SCMPDS )} by FUNCOP_1:19;
then A4: IC SCMPDS in dom (Start-At 0 ,SCMPDS ) by TARSKI:def 1;
Start-At 0 ,SCMPDS c= Initialized (stop (Load i)) by FUNCT_4:26;
then Start-At 0 ,SCMPDS c= t by A2, XBOOLE_1:1;
then A5: IC t = (Start-At 0 ,SCMPDS ) . (IC SCMPDS ) by A4, GRFUNC_1:8
.= 0 by FUNCOP_1:87 ;
then A6: IC (Exec i,t) = succ 0 by A1
.= 0 + 1 ;
1 in dom (stop (Load i)) by Th9;
then (stop (Load i)) . 1 = t . 1 by A3, GRFUNC_1:8;
then A7: t . 1 = halt SCMPDS by Th10;
0 in dom (stop (Load i)) by Th9;
then A8: (stop (Load i)) . 0 = t . 0 by A3, GRFUNC_1:8;
Z: (ProgramPart (Comput (ProgramPart t),t,1)) /. (IC (Comput (ProgramPart t),t,1)) = (Comput (ProgramPart t),t,1) . (IC (Comput (ProgramPart t),t,1)) by AMI_1:150;
V: (ProgramPart t) /. (IC t) = t . (IC t) by AMI_1:150;
Comput (ProgramPart t),t,(0 + 1) = Following (ProgramPart t),(Comput (ProgramPart t),t,0 ) by AMI_1:14
.= Following (ProgramPart t),t by AMI_1:13
.= Exec i,t by A5, A8, Th10, V ;
then CurInstr (ProgramPart (Comput (ProgramPart t),t,1)),(Comput (ProgramPart t),t,1) = halt SCMPDS by A6, A7, AMI_1:def 13, Z;
hence (ProgramPart t) /. (IC (Comput (ProgramPart t),t,1)) = halt SCMPDS by AMI_1:145; :: thesis: