:: deftheorem defines UsedI*Loc SF_MASTR:def 5 :
for X being set holds UsedI*Loc X = union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } ;