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 +* (Initialized I);
set s2 = (Initialized s) +* (Initialize I);
set p1 = p +* I;
A1: ProgramPart I = I by RELAT_1:209;
A2: s +* (Initialized I) = (Initialized s) +* (Initialize I) by SCMFSA8A:13;
( I is_halting_onInit s,p iff p +* I halts_on s +* (Initialized I) ) by Def5;
hence ( I is_halting_onInit s,p iff I is_halting_on Initialized s,p ) by A2, SCMFSA7B:def 8, A1; :: thesis: verum