:: deftheorem defines SCM-Exec SCMRING1:def 15 :
for R being Ring
for b₂ being Action of (SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)) holds
( b₂ = SCM-Exec R iff for x being Element of SCM-Instr R
for y being SCM-State of R holds (b₂ . x) . y = SCM-Exec-Res (x,y) );