:: deftheorem defines UsedILoc SF_MASTR:def 2 :
for X being set holds UsedILoc X = union { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } ;