let I be Program of SCMPDS ; :: thesis: ( I is parahalting iff for s being State of SCMPDS holds I is_halting_on s )
set IsI = Initialized (stop I);

hereby :: thesis: ( ( for s being State of SCMPDS holds I is_halting_on s ) implies I is parahalting )

assume A1: I is parahalting ; :: thesis: for s being State of SCMPDS holds I is_halting_on s
let s be State of SCMPDS ; :: thesis: I is_halting_on s
s +* (Initialized (stop I)) is halting by A1, FUNCT_4:26, SCMPDS_4:63;
hence I is_halting_on s by Def3; :: thesis: verum

end;

assume A2: for s being State of SCMPDS holds I is_halting_on s ; :: thesis: I is parahalting

now

let s be State of SCMPDS ; :: thesis: ( Initialized (stop I) c= s implies s is halting )
assume Initialized (stop I) c= s ; :: thesis: s is halting
then ( I is_halting_on s & s = s +* (Initialized (stop I)) ) by A2, FUNCT_4:79;
hence s is halting by Def3; :: thesis: verum

end;

then Initialized (stop I) is halting by AMI_1:def 26;
hence I is parahalting by SCMPDS_4:def 10; :: thesis: verum