let I be Program of SCM+FSA; :: thesis: ( I is InitHalting iff for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_onInit s,p )

hereby :: thesis: ( ( for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_onInit s,p ) implies I is InitHalting )

assume A2: I is InitHalting ; :: thesis: for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_onInit s,p
let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_onInit s,p
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: I is_halting_onInit s,p
A3: I c= p +* I by FUNCT_4:26;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by A3, Def2, A2;
hence I is_halting_onInit s,p by Def5; :: thesis: verum

end;

assume A4: for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_onInit s,p ; :: thesis: I is InitHalting

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 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
then A5: s = s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:103, FUNCT_4:104;
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( I c= p implies p halts_on s )
assume I c= p ; :: thesis: p halts_on s
then A6: p +* I = p by FUNCT_4:103, FUNCT_4:104;
I is_halting_onInit s,p by A4;
hence p halts_on s by A5, Def5, A6; :: thesis: verum

end;

hence I is InitHalting by Def2; :: thesis: verum