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
A2: I +* (Start-At (insloc 0 )) c= s +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
I +* (Start-At (insloc 0 )) is halting by A1, SCMFSA6B:def 3;
then s +* (I +* (Start-At (insloc 0 ))) is halting by A2, AMI_1:def 26;
hence I is_halting_on s by Def8; :: thesis: verum

end;

assume A3: 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 (insloc 0 )) c= s implies s is halting )
assume I +* (Start-At (insloc 0 )) c= s ; :: thesis: s is halting
then ( I is_halting_on s & s = s +* (I +* (Start-At (insloc 0 ))) ) by A3, FUNCT_4:79;
hence s is halting by Def8; :: thesis: verum

end;

then I +* (Start-At (insloc 0 )) is halting by AMI_1:def 26;
hence I is parahalting by SCMFSA6B:def 3; :: thesis: verum