for s being State of SCM+FSA st s . (intloc 0) = 1 holds
Initialize s = Initialized s