for s being State of SCM+FSA
for iloc being Nat
for a being Int-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a