let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I, J being Program of SCM+FSA holds
( I is_closed_on Initialized s,P iff I is_closed_on s +* (Initialize ((intloc 0) .--> 1)),P +* J )
let s be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA holds
( I is_closed_on Initialized s,P iff I is_closed_on s +* (Initialize ((intloc 0) .--> 1)),P +* J )
let I, J be Program of SCM+FSA; :: thesis: ( I is_closed_on Initialized s,P iff I is_closed_on s +* (Initialize ((intloc 0) .--> 1)),P +* J )
DataPart (Initialized s) = DataPart (s +* (Initialize ((intloc 0) .--> 1))) ;
hence ( I is_closed_on Initialized s,P iff I is_closed_on s +* (Initialize ((intloc 0) .--> 1)),P +* J ) by Th6; :: thesis: verum