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 0 -started State of SCMPDS; :: according to SCMPDS_4:def 10 :: thesis: ( not stop (Load i) c= t or ProgramPart t halts_on t )
assume A3: stop (Load i) c= t ; :: thesis: ProgramPart t halts_on t
take 1 ; :: according to EXTPRO_1:def 7 :: 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
A5: IC t = 0 by COMPOS_1:def 16;
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;
V: (ProgramPart t) /. (IC t) = t . (IC t) by COMPOS_1:38;
Comput ((ProgramPart t),t,(0 + 1)) = Following ((ProgramPart t),(Comput ((ProgramPart t),t,0))) by EXTPRO_1:4
.= Following ((ProgramPart t),t) by EXTPRO_1:3
.= Exec (i,t) by A5, A8, Th10, V ;
hence CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,1))) = halt SCMPDS by A6, A7, COMPOS_1:38; :: thesis: verum