:: deftheorem defines Following EXTPRO_1:def 6 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for p being the InstructionsF of b₂ -valued Function holds Following (p,s) = Exec ((CurInstr (p,s)),s);