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

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
I1: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by SCMPDS_4:5;
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A1, I1, 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: ( Initialize (stop I) c= s implies ProgramPart s halts_on s )
I1: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by SCMPDS_4:5;
assume Initialize (stop I) c= s ; :: thesis: ProgramPart s halts_on s
then A3: s = (Initialize s) +* (stop I) by I1, FUNCT_4:79;
I is_halting_on s by A2;
hence ProgramPart s halts_on s by A3, Def3; :: thesis: verum

end;

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