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
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A1, FUNCT_4:26, SCMPDS_4:def 10;
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
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 10 :: thesis: ( not stop I c= s or ProgramPart s halts_on s )
AA: Initialize s = s by COMPOS_1:78;
assume stop I c= s ; :: thesis: ProgramPart s halts_on s
then A3: s = (Initialize s) +* (stop I) by AA, FUNCT_4:79;
I is_halting_on s by A2;
hence ProgramPart s halts_on s by A3, Def3; :: thesis: verum