let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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 = s +* (Initialize ((intloc 0) .--> 1));
set p1 = p +* I;
A2: s +* (Initialize ((intloc 0) .--> 1)) = s +* (Initialize (Initialize ((intloc 0) .--> 1))) by FUNCT_4:99
.= Initialize (s +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= Initialize (Initialized s) ;
( I is_halting_onInit s,p iff p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) ) by Def5;
hence ( I is_halting_onInit s,p iff I is_halting_on Initialized s,p ) by A2, SCMFSA7B:def 8; :: thesis: verum