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


begin

begin

theorem Th1: :: SCMFSA_5:1
for k being Element of NAT
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b2 -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 Element of 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)) )
proofend;

registration
cluster SCM+FSA  ->  relocable1 relocable2 ;
coherence
 ( SCM+FSA is relocable1 & SCM+FSA is relocable2 )
proofend;
end;