take Stop S ; :: thesis: Stop S is parahalting
let s be 0 -started State of S; :: according to AMISTD_1:def 10 :: thesis: for P being Instruction-Sequence of S st Stop S c= P holds
P halts_on s
let P be Instruction-Sequence of S; :: thesis: ( Stop S c= P implies P halts_on s )
assume A1: Stop S c= P ; :: thesis: P halts_on s
take 0 ; :: according to EXTPRO_1:def 8 :: thesis: ( 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; :: thesis: 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 ; :: thesis: verum