:: deftheorem defines times* SFMASTR2:def 1 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds times* (a,I) = while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))));