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

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

assume A1: I is InitHalting ; :: thesis: for s being State of SCM+FSA holds I is_halting_onInit s
let s be State of SCM+FSA; :: thesis: I is_halting_onInit s
Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by A1, EXTPRO_1:def 10;
hence I is_halting_onInit s by Def5; :: thesis: verum

end;

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

now

let s be State of SCM+FSA; :: thesis: ( Initialized I c= s implies ProgramPart s halts_on s )
assume Initialized I c= s ; :: thesis: ProgramPart s halts_on s
then A3: s = s +* (Initialized I) by FUNCT_4:79;
I is_halting_onInit s by A2;
hence ProgramPart s halts_on s by A3, Def5; :: thesis: verum

end;

then Initialized I is halting by EXTPRO_1:def 10;
hence I is InitHalting by Def2; :: thesis: verum