for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory holds
IC s = IC S