:: deftheorem defines Initialized SCMFSA_M:def 1 :
for I being PartState of SCM+FSA holds Initialized I = I +* (Initialize ((intloc 0) .--> 1));