:: deftheorem defines StepTimes SFMASTR2:def 3 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds StepTimes (a,I,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s))));