for i being Instruction of SCM+FSA
for p being preProgram of SCM+FSA st i in rng p holds
UsedIntLoc i c= UsedILoc p by Lm1;