let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds DataPart s = DataPart (s +* (Initialized I))
let I be Program of SCMPDS ; :: thesis: DataPart s = DataPart (s +* (Initialized I))
Initialized I = I +* (Start-At (inspos 0 )) by SCMPDS_4:def 2;
hence DataPart s = DataPart (s +* (Initialized I)) by Th8; :: thesis: verum