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