:: deftheorem defines SCM+FSA-Memory SCMFSA_1:def 2 :
SCM+FSA-Memory = SCM-Memory \/ SCM+FSA-Data*-Loc;