let I be Program of SCM+FSA; :: thesis: ( I is InitHalting iff for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,p )
thus ( I is InitHalting implies for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,p ) by Th23, Th27; :: thesis: ( ( for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,p ) implies I is InitHalting )
assume for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,p ; :: thesis: I is InitHalting
then for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p by Th27;
hence I is InitHalting by Th23; :: thesis: verum