take
Stop S
; Stop S is parahalting
let s be 0 -started State of S; AMISTD_1:def 10 for P being Instruction-Sequence of S st Stop S c= P holds
P halts_on s
let P be Instruction-Sequence of S; ( Stop S c= P implies P halts_on s )
assume A1:
Stop S c= P
; P halts_on s
take
0
; EXTPRO_1:def 8 ( IC (Comput (P,s,0)) in dom P & CurInstr (P,(Comput (P,s,0))) = halt S )
A2:
0 in dom (Stop S)
by COMPOS_1:3;
dom (Stop S) c= dom P
by A1, RELAT_1:11;
then A3:
0 in dom P
by A2;
A4:
IC s = 0
by MEMSTR_0:def 11;
hence
IC (Comput (P,s,0)) in dom P
by A3; CurInstr (P,(Comput (P,s,0))) = halt S
thus CurInstr (P,(Comput (P,s,0))) =
P /. 0
by A4
.=
P . 0
by A3, PARTFUN1:def 6
.=
(Stop S) . 0
by A1, A2, GRFUNC_1:2
.=
halt S
; verum