let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS holds
( I is_closed_on s,P iff I is_closed_on Initialize s,P )
let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS holds
( I is_closed_on s,P iff I is_closed_on Initialize s,P )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s,P iff I is_closed_on Initialize s,P )
thus ( I is_closed_on s,P implies I is_closed_on Initialize s,P ) :: thesis: ( I is_closed_on Initialize s,P implies I is_closed_on s,P )

proof

assume for k being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) ; :: according to SCMPDS_6:def 2 :: thesis: I is_closed_on Initialize s,P
hence for k being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize (Initialize s)),k)) in dom (stop I) ; :: according to SCMPDS_6:def 2 :: thesis: verum

end;

assume for k being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize (Initialize s)),k)) in dom (stop I) ; :: according to SCMPDS_6:def 2 :: thesis: I is_closed_on s,P
hence for k being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) ; :: according to SCMPDS_6:def 2 :: thesis: verum