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

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