thus for k being Element of NAT
for q being NAT -defined the Instructions of (STC N) -valued finite non halt-free Function
for p being non empty b₂ -autonomic FinPartState of (STC N)
for s1, s2 being State of (STC N) st IC in dom p & p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of NAT holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) by Lm1; :: according to AMISTD_5:def 5 :: thesis: verum