:: deftheorem defines SCM+FSA SCMFSA_2:def 1 :
SCM+FSA = AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);