let i be Instruction of SCMPDS; ( ( 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)
; Load i is parahalting
set m0 = stop (Load i);
set m1 = Initialize (stop (Load i));
let t be 0 -started State of SCMPDS; SCMPDS_4:def 10 ( not stop (Load i) c= t or ProgramPart t halts_on t )
assume A2:
stop (Load i) c= t
; ProgramPart t halts_on t
take
1
; EXTPRO_1:def 7 ( IC (Comput ((ProgramPart t),t,1)) in proj1 (ProgramPart t) & CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,1))) = halt SCMPDS )
IC (Comput ((ProgramPart t),t,1)) in NAT
;
hence
IC (Comput ((ProgramPart t),t,1)) in dom (ProgramPart t)
by COMPOS_1:34; CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,1))) = halt SCMPDS
A3:
IC t = 0
by COMPOS_1:def 16;
then A4: IC (Exec (i,t)) =
succ 0
by A1
.=
0 + 1
;
1 in dom (stop (Load i))
by Th9;
then
(stop (Load i)) . 1 = t . 1
by A2, GRFUNC_1:8;
then A5:
t . 1 = halt SCMPDS
by Th10;
0 in dom (stop (Load i))
by Th9;
then A6:
(stop (Load i)) . 0 = t . 0
by A2, GRFUNC_1:8;
A7:
(ProgramPart t) /. (IC t) = t . (IC t)
by COMPOS_1:38;
Comput ((ProgramPart t),t,(0 + 1)) =
Following ((ProgramPart t),(Comput ((ProgramPart t),t,0)))
by EXTPRO_1:4
.=
Following ((ProgramPart t),t)
by EXTPRO_1:3
.=
Exec (i,t)
by A3, A6, Th10, A7
;
hence
CurInstr ((ProgramPart t),(Comput ((ProgramPart t),t,1))) = halt SCMPDS
by A4, A5, COMPOS_1:38; verum