let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being really-closed Program of SCM+FSA
for l being Nat holds
( I is_halting_on s,P iff I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I )
let s be State of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA
for l being Nat holds
( I is_halting_on s,P iff I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I )
let I be really-closed Program of SCM+FSA; :: thesis: for l being Nat holds
( I is_halting_on s,P iff I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I )
let l be Nat; :: thesis: ( I is_halting_on s,P iff I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I )
DataPart s = DataPart (s +* (Start-At (l,SCM+FSA))) by MEMSTR_0:79;
hence ( I is_halting_on s,P iff I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I ) by Th1; :: thesis: verum