let I be Program of SCM+FSA; :: thesis: ( I is InitHalting iff for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p )
hereby :: thesis: ( ( for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p ) implies I is InitHalting )
assume A1: I is InitHalting ; :: thesis: for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p
let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p
let p be Instruction-Sequence of SCM+FSA; :: thesis: I is_halting_onInit s,p
A2: I c= p +* I by FUNCT_4:25;
Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
then p +* I halts_on Initialized s by A2, A1;
hence I is_halting_onInit s,p ; :: thesis: verum
end;
assume A3: for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p ; :: thesis: I is InitHalting
now :: thesis: for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
for p being Instruction-Sequence of SCM+FSA st I c= p holds
p halts_on s
let s be State of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies for p being Instruction-Sequence of SCM+FSA st I c= p holds
p halts_on s )
assume Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for p being Instruction-Sequence of SCM+FSA st I c= p holds
p halts_on s
then A4: s = Initialized s by FUNCT_4:98;
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( I c= p implies p halts_on s )
assume I c= p ; :: thesis: p halts_on s
then A5: p +* I = p by FUNCT_4:98;
I is_halting_onInit s,p by A3;
hence p halts_on s by A4, A5; :: thesis: verum
end;
hence I is InitHalting ; :: thesis: verum