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

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

assume A1: I is InitHalting ; :: thesis: for s being State of SCM+FSA holds I is_halting_on Initialized s
let s be State of SCM+FSA; :: thesis: I is_halting_on Initialized s
I is_halting_onInit s by A1, Th36;
hence I is_halting_on Initialized s by Th41; :: thesis: verum

end;

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

now

let s be State of SCM+FSA; :: thesis: I is_halting_onInit s
I is_halting_on Initialized s by A2;
hence I is_halting_onInit s by Th41; :: thesis: verum

end;

hence I is InitHalting by Th36; :: thesis: verum