:: deftheorem defines Exec EXTPRO_1:def 2 :
for N being with_zero set
for S being with_non-empty_values AMI-Struct over N
for I being Instruction of S
for s being State of S holds Exec (I,s) = ( the Execution of S . I) . s;