let I be Program of ; :: thesis: ( I is parahalting iff for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_halting_on s,P )
thus ( I is parahalting implies for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_halting_on s,P ) by FUNCT_4:25; :: thesis: ( ( for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_halting_on s,P ) implies I is parahalting )
assume A1: for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_halting_on s,P ; :: thesis: I is parahalting
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 7 :: thesis: for b₁ being set holds
( not stop I c= b₁ or b₁ halts_on s )
let P be Instruction-Sequence of SCMPDS; :: thesis: ( not stop I c= P or P halts_on s )
A2: Initialize s = s by MEMSTR_0:44;
assume stop I c= P ; :: thesis: P halts_on s
then A3: P = P +* (stop I) by FUNCT_4:98;
I is_halting_on s,P by A1;
hence P halts_on s by A3, A2; :: thesis: verum