:: deftheorem defines FinSeq-Locations SCMFSA_2:def 3 :
FinSeq-Locations = SCM+FSA-Data*-Loc ;