let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( I is_halting_onInit s,p iff I is_halting_on Initialized s,p )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds
( I is_halting_onInit s,p iff I is_halting_on Initialized s,p )
let I be Program of SCM+FSA; :: thesis: ( I is_halting_onInit s,p iff I is_halting_on Initialized s,p )
set s1 = Initialized s;
set p1 = p +* I;
A2: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
( I is_halting_onInit s,p iff p +* I halts_on Initialized s ) by Def5;
hence ( I is_halting_onInit s,p iff I is_halting_on Initialized s,p ) by A2, SCMFSA7B:def 7; :: thesis: verum