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

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

assume A1: I is parahalting ; :: thesis: for s being State of SCM+FSA holds I is_halting_on s
let s be State of SCM+FSA; :: thesis: I is_halting_on s
( I +* (Start-At (0,SCM+FSA)) c= s +* (I +* (Start-At (0,SCM+FSA))) & I +* (Start-At (0,SCM+FSA)) is halting ) by A1, FUNCT_4:26, SCMFSA6B:def 3;
then ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) halts_on s +* (I +* (Start-At (0,SCM+FSA))) by EXTPRO_1:def 10;
hence I is_halting_on s by Def8; :: thesis: verum

end;

assume A2: for s being State of SCM+FSA holds I is_halting_on s ; :: thesis: I is parahalting

now

let s be State of SCM+FSA; :: thesis: ( I +* (Start-At (0,SCM+FSA)) c= s implies ProgramPart s halts_on s )
assume I +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: ProgramPart s halts_on s
then A3: s = s +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
I is_halting_on s by A2;
hence ProgramPart s halts_on s by A3, Def8; :: thesis: verum

end;

then I +* (Start-At (0,SCM+FSA)) is halting by EXTPRO_1:def 10;
hence I is parahalting by SCMFSA6B:def 3; :: thesis: verum