let i be Instruction of SCMPDS ; :: thesis: ( ( for s being State of SCMPDS holds (Exec i,s) . (IC SCMPDS ) = succ (IC s) ) implies Load i is parahalting )
set SA0 = Start-At 0 ,SCMPDS ;
assume A1: for s being State of SCMPDS holds (Exec i,s) . (IC SCMPDS ) = succ (IC s) ; :: thesis: Load i is parahalting
set m0 = stop (Load i);
set m1 = Initialize (stop (Load i));
let t be State of SCMPDS ; :: according to AMI_1:def 26,SCMPDS_4:def 10 :: thesis: ( not Initialize (stop (Load i)) c= t or ProgramPart t halts_on t )
assume A2: Initialize (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 (Comput (ProgramPart t),t,1) in proj1 (ProgramPart t) & CurInstr (ProgramPart t),(Comput (ProgramPart t),t,1) = halt SCMPDS )
IC (Comput (ProgramPart t),t,1) in NAT ;
hence IC (Comput (ProgramPart t),t,1) in dom (ProgramPart t) by COMPOS_1:34; :: thesis: CurInstr (ProgramPart t),(Comput (ProgramPart t),t,1) = halt SCMPDS
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= Initialize (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 COMPOS_1:38;
V: (ProgramPart t) /. (IC t) = t . (IC t) by COMPOS_1:38;
NX: ProgramPart t = ProgramPart (Comput (ProgramPart t),t,1) by AMI_1:123;
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 t),(Comput (ProgramPart t),t,1) = halt SCMPDS by A6, A7, Z, NX, AMI_1:def 13;
hence CurInstr (ProgramPart t),(Comput (ProgramPart t),t,1) = halt SCMPDS ; :: thesis: verum