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

begin

begin

theorem :: SCMFSA_5:1

canceled;

theorem :: SCMFSA_5:2

canceled;

theorem :: SCMFSA_5:3

canceled;

theorem :: SCMFSA_5:4

canceled;

theorem :: SCMFSA_5:5

canceled;

theorem :: SCMFSA_5:6

canceled;

theorem :: SCMFSA_5:7

canceled;

theorem :: SCMFSA_5:8

canceled;

theorem :: SCMFSA_5:9

canceled;

theorem :: SCMFSA_5:10

canceled;

theorem :: SCMFSA_5:11

canceled;

theorem Th12: :: SCMFSA_5:12

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

proof end;

registration

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

proof end;

end;