let i be Instruction of SCMPDS; ( ( 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
; Load i is parahalting
set m0 = stop (Load i);
let t be 0 -started State of SCMPDS; SCMPDS_4:def 7 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; ( not stop (Load i) c= Q or Q halts_on t )
assume A3:
stop (Load i) c= Q
; Q halts_on t
take
1
; EXTPRO_1:def 8 ( 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; 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; verum