:: deftheorem defines SCMPDS-Exec SCMPDS_1:def 21 :
for b₁ being Action of SCMPDS-Instr,(product (SCM-VAL * SCM-OK)) holds
( b₁ = SCMPDS-Exec iff for x being Element of SCMPDS-Instr
for y being SCM-State holds (b₁ . x) . y = SCM-Exec-Res (x,y) );