let I be Program of SCM+FSA; :: thesis: ( ( for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on Initialized s,P ) implies Initialized I is halting )
A1: ProgramPart (Initialized I) = I by SCMFSA6A:33;
assume A2: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on Initialized s,P ; :: thesis: Initialized I is halting
XX: NPP (Initialized I) = Initialize ((intloc 0) .--> 1) by SCMFSA6A:79;

now

let s be State of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P halts_on s )
assume B3: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P halts_on s
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( I c= P implies P halts_on s )
assume A4: I c= P ; :: thesis: P halts_on s
B6: s +* (Initialize ((intloc 0) .--> 1)) = Initialized s
.= Initialize (Initialized s) by FUNCT_4:104, SCMFSA6B:4 ;
I is_halting_on Initialized s,P by A2;
then A7: P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by B6, SCMFSA7B:def 8;
s +* (Initialize ((intloc 0) .--> 1)) = s by B3, FUNCT_4:103, FUNCT_4:104;
hence P halts_on s by A7, A4, FUNCT_4:103, FUNCT_4:104; :: thesis: verum

end;

hence Initialized I is halting by A1, XX, EXTPRO_1:def 10; :: thesis: verum