for k being Element of NAT
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₂ -autonomic FinPartState of SCM
for s1, s2, s3 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 & s3 = s1 +* (DataPart s2) holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of NAT holds DataPart (Comput (P1,s3,i)) = DataPart (Comput (P2,s2,i)) by Lm1;