let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds
( I is_halting_onInit s iff I is_halting_on Initialize s )
let I be Program of SCM+FSA ; :: thesis: ( I is_halting_onInit s iff I is_halting_on Initialize s )
set s1 = s +* (Initialized I);
set s2 = (Initialize s) +* (I +* (Start-At (insloc 0 )));
A1: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
( I is_halting_onInit s iff s +* (Initialized I) is halting ) by Def5;
hence ( I is_halting_onInit s iff I is_halting_on Initialize s ) by A1, SCMFSA7B:def 8; :: thesis: verum