for s being State of SCMPDS
for iloc being Nat
for a being Int_position holds s . a = (s +* (Start-At (iloc,SCMPDS))) . a