:: deftheorem defines SCM-Chg AMI_2:def 7 :
for s being SCM-State
for u being natural Number holds SCM-Chg (s,u) = s +* (NAT .--> u);