:: Relocability for { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 22, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

theorem Th1: :: SCMFSA_5:1

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

proof end;

registration

cluster SCM+FSA -> relocable1 relocable2 ;

coherence
( SCM+FSA is relocable1 & SCM+FSA is relocable2 ) by Th1;

end;