for A being Data-Location
for a being Int-Location
for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds
S . A = s . a