thus SCM is relocable1 :: thesis: SCM is relocable2

proof

thus for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),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

end;

let k be Element of NAT ; :: according to AMISTD_5:def 6 :: thesis: for b₁ being set
for b₂, b₃ being set holds
( not IC in proj1 b₁ or not NPP b₁ c= b₂ or not NPP (Relocated (b₁,k)) c= b₃ or for b₄, b₅ being set holds
( not ProgramPart b₁ c= b₄ or not Reloc ((ProgramPart b₁),k) c= b₅ or for b₆ being Element of NAT holds (Comput (b₄,b₂,b₆)) | (proj1 (DataPart b₁)) = (Comput (b₅,b₃,b₆)) | (proj1 (DataPart b₁)) ) )
let p be autonomic FinPartState of SCM; :: thesis: for b₁, b₂ being set holds
( not IC in proj1 p or not NPP p c= b₁ or not NPP (Relocated (p,k)) c= b₂ or for b₃, b₄ being set holds
( not ProgramPart p c= b₃ or not Reloc ((ProgramPart p),k) c= b₄ or for b₅ being Element of NAT holds (Comput (b₃,b₁,b₅)) | (proj1 (DataPart p)) = (Comput (b₄,b₂,b₅)) | (proj1 (DataPart p)) ) )
let s1, s2 be State of SCM; :: thesis: ( not IC in proj1 p or not NPP p c= s1 or not NPP (Relocated (p,k)) c= s2 or for b₁, b₂ being set holds
( not ProgramPart p c= b₁ or not Reloc ((ProgramPart p),k) c= b₂ or for b₃ being Element of NAT holds (Comput (b₁,s1,b₃)) | (proj1 (DataPart p)) = (Comput (b₂,s2,b₃)) | (proj1 (DataPart p)) ) )
assume A1: ( IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 ) ; :: thesis: for b₁, b₂ being set holds
( not ProgramPart p c= b₁ or not Reloc ((ProgramPart p),k) c= b₂ or for b₃ being Element of NAT holds (Comput (b₁,s1,b₃)) | (proj1 (DataPart p)) = (Comput (b₂,s2,b₃)) | (proj1 (DataPart p)) )
let P1, P2 be the Instructions of SCM -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart p c= P1 or not Reloc ((ProgramPart p),k) c= P2 or for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (DataPart p)) = (Comput (P2,s2,b₁)) | (proj1 (DataPart p)) )
assume A2: ( ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 ) ; :: thesis: for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (DataPart p)) = (Comput (P2,s2,b₁)) | (proj1 (DataPart p))
thus for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) by A1, Lm1, A2; :: thesis: verum