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_{1} being set holds

( not stop (Load i) c= b_{1} or b_{1} 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

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

( not stop (Load i) c= b

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