:: deftheorem defines SCMPDS SCMPDS_2:def 1 :
SCMPDS = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #);