let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS
for I, J being Program of holds
( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J )
let s be State of SCMPDS; :: thesis: for I, J being Program of holds
( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J )
let I, J be Program of ; :: thesis: ( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J )
DataPart s = DataPart (Initialize s) by MEMSTR_0:45;
hence ( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J ) by Th13; :: thesis: verum