theorem :: SCMFSA_M:8

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