let i be Instruction of SCMPDS; :: thesis: ( ( for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = succ (IC s) ) implies Load i is parahalting )
assume A1: for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = succ (IC s) ; :: 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 )
XX: 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 A2: 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
A3: IC t = 0 by MEMSTR_0:def 8;
then A4: IC (Exec (i,t)) = succ 0 by A1
.= 0 + 1 ;
1 in dom (stop (Load i)) by COMPOS_1:57, XX;
then (stop (Load i)) . 1 = Q . 1 by A2, GRFUNC_1:2;
then A5: Q . 1 = halt SCMPDS by COMPOS_1:59, XX;
0 in dom (stop (Load i)) by COMPOS_1:57, XX;
then A6: (stop (Load i)) . 0 = Q . 0 by A2, GRFUNC_1:2;
A7: 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) by EXTPRO_1:2
.= Exec (i,t) by A3, A6, COMPOS_1:58, A7, XX ;
hence CurInstr (Q,(Comput (Q,t,1))) = halt SCMPDS by A4, A5, PBOOLE:143; :: thesis: verum