:: deftheorem defines SCM+FSA-Data*-Loc SCMFSA_I:def 1 :
SCM+FSA-Data*-Loc = INT \ NAT;