let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being State of SCMPDS
for I, J being Program of SCMPDS 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 SCMPDS holds
( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J )
let I, J be Program of SCMPDS; :: thesis: ( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J )
DataPart s = DataPart (Initialize s) by COMPOS_1:80;
hence ( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J ) by Th36; :: thesis: verum