for S being non empty 1-sorted
for d1 being Element of SCM-Data-Loc
for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S