for s, t being State of SCMPDS holds s +* (t | SCM-Data-Loc) is State of SCMPDS ;