for s being SCM+FSA-State
for I being Element of SCM-Instr holds s | SCM-Memory is SCM-State