thus SCM is relocable1 :: thesis: SCM is relocable2
proof
thus for k being Element of NAT
for q being NAT -defined the Instructions of SCM -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= 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 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 b1 being set
for b2 being set
for b3, b4 being set holds
( not IC in proj1 b2 or not b2 c= b3 or not IncIC (b2,k) c= b4 or for b5, b6 being set holds
( not b1 c= b5 or not Reloc (b1,k) c= b6 or for b7 being Element of NAT holds (Comput (b5,b3,b7)) | (proj1 (DataPart b2)) = (Comput (b6,b4,b7)) | (proj1 (DataPart b2)) ) )
let q be NAT -defined the Instructions of SCM -valued finite non halt-free Function; :: thesis: for b1 being set
for b2, b3 being set holds
( not IC in proj1 b1 or not b1 c= b2 or not IncIC (b1,k) c= b3 or for b4, b5 being set holds
( not q c= b4 or not Reloc (q,k) c= b5 or for b6 being Element of NAT holds (Comput (b4,b2,b6)) | (proj1 (DataPart b1)) = (Comput (b5,b3,b6)) | (proj1 (DataPart b1)) ) )
let p be non empty q -autonomic FinPartState of SCM; :: thesis: for b1, b2 being set holds
( not IC in proj1 p or not p c= b1 or not IncIC (p,k) c= b2 or for b3, b4 being set holds
( not q c= b3 or not Reloc (q,k) c= b4 or for b5 being Element of NAT holds (Comput (b3,b1,b5)) | (proj1 (DataPart p)) = (Comput (b4,b2,b5)) | (proj1 (DataPart p)) ) )
let s1, s2 be State of SCM; :: thesis: ( not IC in proj1 p or not p c= s1 or not IncIC (p,k) c= s2 or for b1, b2 being set holds
( not q c= b1 or not Reloc (q,k) c= b2 or for b3 being Element of NAT holds (Comput (b1,s1,b3)) | (proj1 (DataPart p)) = (Comput (b2,s2,b3)) | (proj1 (DataPart p)) ) )
assume A1: ( IC in dom p & p c= s1 & IncIC (p,k) c= s2 ) ; :: thesis: for b1, b2 being set holds
( not q c= b1 or not Reloc (q,k) c= b2 or for b3 being Element of NAT holds (Comput (b1,s1,b3)) | (proj1 (DataPart p)) = (Comput (b2,s2,b3)) | (proj1 (DataPart p)) )
let P1, P2 be Instruction-Sequence of SCM; :: thesis: ( not q c= P1 or not Reloc (q,k) c= P2 or for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (DataPart p)) = (Comput (P2,s2,b1)) | (proj1 (DataPart p)) )
assume A2: ( q c= P1 & Reloc (q,k) c= P2 ) ; :: thesis: for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (DataPart p)) = (Comput (P2,s2,b1)) | (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