let i be Instruction of SCMPDS; :: thesis: ( ( for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = (IC s) + 1 ) implies Load i is parahalting )
assume A1: for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = (IC s) + 1 ; :: thesis: Load i is parahalting
set m0 = stop (Load i);
let t be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 7 :: thesis: for b₁ being set holds
( not stop (Load i) c= b₁ or b₁ 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 A2, COMPOS_1:57;
then (stop (Load i)) . 1 = Q . 1 by A3, GRFUNC_1:2;
then A6: Q . 1 = halt SCMPDS by A2, COMPOS_1:59;
0 in dom (stop (Load i)) by A2, COMPOS_1:57;
then A7: (stop (Load i)) . 0 = Q . 0 by A3, GRFUNC_1:2;
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 A4, A7, A8, A2, COMPOS_1:58 ;
hence CurInstr (Q,(Comput (Q,t,1))) = halt SCMPDS by A5, A6, PBOOLE:143; :: thesis: verum