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