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 Initialized I is_halting_on 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 Initialized I is_halting_on s,P ; :: thesis: Initialized I is halting

now

let s be State of SCM+FSA; :: thesis: ( Initialized I 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 A3: Initialized I 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
A5: P +* I = P by A4, FUNCT_4:79;
Initialized I = Initialize (I +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then Start-At (0,SCM+FSA) c= Initialized I by FUNCT_4:26;
then A6: s +* (Initialize (Initialized I)) = s +* (Initialized I) by FUNCT_4:79;
Initialized I is_halting_on s,P by A2;
then A7: P +* I halts_on s +* (Initialize (Initialized I)) by SCMFSA7B:def 8, A1;
s +* (Initialize (Initialized I)) = s by A3, A6, FUNCT_4:79;
hence P halts_on s by A7, A5; :: thesis: verum

end;

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