for S being COM-Struct
for P, Q being NAT -defined the InstructionsF of b₁ -valued finite Function
for k being Nat st P c= Q holds
Reloc (P,k) c= Reloc (Q,k)