for s being State of SCM+FSA
for i being Instruction of SCM holds s | SCM-Memory is State of SCM