let I be Program of SCM+FSA; :: 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 Initialize ((intloc 0) .--> 1) is I -halted )
assume A1: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ; :: thesis: Initialize ((intloc 0) .--> 1) is I -halted
let s be State of SCM+FSA; :: according to EXTPRO_1:def 11 :: thesis: ( not Initialize ((intloc 0) .--> 1) c= s or for b₁ being set holds
( not I c= b₁ or b₁ halts_on s ) )
assume Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for b₁ being set holds
( not I c= b₁ or b₁ halts_on s )
then Initialize ((intloc 0) .--> 1) c= s ;
then A2: s +* (Initialize ((intloc 0) .--> 1)) = s by FUNCT_4:98;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I c= P or P halts_on s )
assume A3: I c= P ; :: thesis: P halts_on s
A4: P +* I = P by A3, FUNCT_4:98;
I is_halting_on Initialized s,P by A1;
then P +* I halts_on Initialize (Initialized s) ;
hence P halts_on s by A2, A4, MEMSTR_0:44; :: thesis: verum