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

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