:: deftheorem defines SCM+FSA-OK SCMFSA_1:def 4 :
SCM+FSA-OK = (SCM+FSA-Memory --> 2) +* SCM-OK;