let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_halting_on s,p iff I is_halting_on Initialized s,p )
let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_halting_on s,p iff I is_halting_on Initialized s,p )
let I be really-closed Program of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 implies ( I is_halting_on s,p iff I is_halting_on Initialized s,p ) )
assume s . (intloc 0) = 1 ; :: thesis: ( I is_halting_on s,p iff I is_halting_on Initialized s,p )
then DataPart (Initialized s) = DataPart s by SCMFSA_M:19;
hence ( I is_halting_on s,p iff I is_halting_on Initialized s,p ) by Th1; :: thesis: verum