let i be Instruction of SCMPDS; :: thesis: ( ( for s being State of SCMPDS holds (Exec (i,s)) . () = (IC s) + 1 ) implies Load i is parahalting )
assume A1: for s being State of SCMPDS holds (Exec (i,s)) . () = (IC s) + 1 ; :: thesis:
set m0 = stop (Load i);
let t be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 7 :: thesis: for b1 being set holds
( not stop (Load i) c= b1 or b1 halts_on t )

A2: stop (Load i) = Macro i ;
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( not stop (Load i) c= Q or Q halts_on t )
assume A3: stop (Load i) c= Q ; :: thesis: Q halts_on t
take 1 ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (Q,t,1)) in proj1 Q & CurInstr (Q,(Comput (Q,t,1))) = halt SCMPDS )
IC (Comput (Q,t,1)) in NAT ;
hence IC (Comput (Q,t,1)) in dom Q by PARTFUN1:def 2; :: thesis: CurInstr (Q,(Comput (Q,t,1))) = halt SCMPDS
A4: IC t = 0 by MEMSTR_0:def 11;
then A5: IC (Exec (i,t)) = 0 + 1 by A1;
1 in dom (stop (Load i)) by ;
then (stop (Load i)) . 1 = Q . 1 by ;
then A6: Q . 1 = halt SCMPDS by ;
0 in dom (stop (Load i)) by ;
then A7: (stop (Load i)) . 0 = Q . 0 by ;
A8: Q /. (IC t) = Q . (IC t) by PBOOLE:143;
Comput (Q,t,(0 + 1)) = Following (Q,(Comput (Q,t,0))) by EXTPRO_1:3
.= Following (Q,t)
.= Exec (i,t) by ;
hence CurInstr (Q,(Comput (Q,t,1))) = halt SCMPDS by ; :: thesis: verum