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 )

for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p ; :: thesis: I is InitHalting

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 A3:
for s being State of SCM+FSAfor 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;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

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

hence
I is InitHalting
; :: thesis: verumfor 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;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