let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st s . (intloc 0 ) = 1 holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on Initialized s & I is_halting_on Initialized s ) )
let I be Program of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 implies ( I is_closed_on s & I is_halting_on s iff ( I is_closed_on Initialized s & I is_halting_on Initialized s ) ) )
assume s . (intloc 0 ) = 1 ; :: thesis: ( I is_closed_on s & I is_halting_on s iff ( I is_closed_on Initialized s & I is_halting_on Initialized s ) )
then DataPart (Initialized s) = DataPart s by SCMFSA8C:27;
hence ( I is_closed_on s & I is_halting_on s iff ( I is_closed_on Initialized s & I is_halting_on Initialized s ) ) by SCMFSA8B:8; :: thesis: verum