The abstract of the Mizar article:

Relocability for \SCMFSA

by

Andrzej Trybulec, and

Yatsuka Nakamura

Received February 22, 1996

MML identifier: SCMFSA_5

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_1, SCMFSA_2, RELOC, AMI_3, FUNCT_4, AMI_5, BOOLE, RELAT_1,
      FUNCT_1, CAT_1, AMI_2, ARYTM_1, NAT_1, ABSVALUE, FINSEQ_1, FINSEQ_2,
      CARD_3, FINSET_1, PARTFUN1, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XCMPLX_0, XREAL_0, ABSVALUE,
      NAT_1, INT_1, CARD_3, PARTFUN1, CQC_LANG, RELAT_1, FUNCT_1, FINSEQ_1,
      FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_2, FUNCT_4, FUNCT_7, STRUCT_0, AMI_1,
      AMI_3, AMI_5, SCMFSA_2, SCMFSA_4;
 constructors NAT_1, AMI_5, RELOC, FUNCT_7, SCMFSA_4, DOMAIN_1, FINSEQ_4,
      MEMBERED;
 clusters AMI_1, SCMFSA_2, RELSET_1, FUNCT_1, INT_1, SCMFSA_4, FRAENKEL, AMI_5,
      MEMBERED;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin  :: Relocatability

reserve j, k, m for Nat;

definition
 let p be FinPartState of SCM+FSA, k be Nat;
 func Relocated( p, k ) -> FinPartState of SCM+FSA equals
:: SCMFSA_5:def 1

  Start-At ((IC p)+k)+* IncAddr(Shift(ProgramPart(p),k),k)+*DataPart p;
end;

theorem :: SCMFSA_5:1
 for p being FinPartState of SCM+FSA,k being Nat
  holds DataPart(Relocated(p,k)) = DataPart(p);

theorem :: SCMFSA_5:2
 for p being FinPartState of SCM+FSA,k being Nat
  holds ProgramPart(Relocated(p,k)) = IncAddr(Shift(ProgramPart(p),k),k);

theorem :: SCMFSA_5:3
 for p being FinPartState of SCM+FSA
 holds dom ProgramPart(Relocated(p,k))
           = { insloc(j+k):insloc j in dom ProgramPart(p) };

theorem :: SCMFSA_5:4
 for p being FinPartState of SCM+FSA, k being Nat,
     l being Instruction-Location of SCM+FSA
  holds l in dom p iff l+k in dom Relocated(p,k);

theorem :: SCMFSA_5:5
 for p being FinPartState of SCM+FSA , k being Nat
  holds IC SCM+FSA in dom Relocated(p,k);

theorem :: SCMFSA_5:6
 for p being FinPartState of SCM+FSA, k being Nat
  holds IC Relocated(p,k) = (IC p) + k;

theorem :: SCMFSA_5:7
 for p being FinPartState of SCM+FSA,
     k being Nat,
     loc being Instruction-Location of SCM+FSA,
     I being Instruction of SCM+FSA
  st loc in dom ProgramPart p & I = p.loc
  holds IncAddr(I, k) = (Relocated(p, k)).(loc + k);

theorem :: SCMFSA_5:8
 for p being FinPartState of SCM+FSA,k being Nat
  holds Start-At (IC p + k) c= Relocated(p,k);

theorem :: SCMFSA_5:9
 for s being data-only FinPartState of SCM+FSA,
     p being FinPartState of SCM+FSA,
     k being Nat st IC SCM+FSA in dom p
  holds
   Relocated((p +* s), k) = Relocated(p,k) +* s;

theorem :: SCMFSA_5:10
 for k being Nat,
     p being autonomic FinPartState of SCM+FSA ,
     s1, s2 being State of SCM+FSA
    st p c= s1 & Relocated(p,k) c= s2
  holds p c= s1 +* s2|(Int-Locations \/ FinSeq-Locations);

begin :: Main theorems of relocatability

theorem :: SCMFSA_5:11
   for k being Nat
 for p being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom p
 for s being State of SCM+FSA st
     p c= s
 for i being Nat
  holds (Computation (s +* Relocated(p,k))).i
       = (Computation s).i +* Start-At (IC (Computation s ).i + k)
        +* ProgramPart (Relocated(p,k));

theorem :: SCMFSA_5:12
 for k being Nat,
     p being autonomic FinPartState of SCM+FSA ,
     s1, s2, s3 being State of SCM+FSA
    st IC SCM+FSA in dom p & p c= s1 & Relocated(p,k) c= s2 &
       s3 = s1 +* s2|(Int-Locations \/ FinSeq-Locations)
    holds for i being Nat holds
     IC (Computation s1).i + k = IC (Computation s2).i &
     IncAddr(CurInstr((Computation s1).i), k) = CurInstr((Computation s2).i) &
     (Computation s1).i|dom (DataPart p)
          = (Computation s2).i|dom (DataPart (Relocated(p,k))) &
     (Computation s3).i|(Int-Locations \/ FinSeq-Locations) =
     (Computation s2).i|(Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA_5:13
 for p being autonomic FinPartState of SCM+FSA ,
     k being Nat
  st IC SCM+FSA in dom p
  holds
  p is halting iff Relocated(p,k) is halting;

theorem :: SCMFSA_5:14
 for k being Nat
 for p being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom p
 for s being State of SCM+FSA st Relocated(p,k) c= s
  holds
  for i being Nat holds
    (Computation s).i
     = (Computation(s +* p)).i +* Start-At (IC(Computation(s +* p)).i + k)
       +* s|dom ProgramPart p +* ProgramPart (Relocated(p,k));

theorem :: SCMFSA_5:15
  for k being Nat
  for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p
  for s being State of SCM+FSA st p c= s & Relocated(p,k) is autonomic
 holds
  for i being Nat holds
   (Computation s).i
    = (Computation(s +* Relocated(p,k))).i
      +* Start-At (IC(Computation(s +* Relocated(p,k))).i -' k)
      +* s|dom ProgramPart Relocated(p,k) +* ProgramPart (p);

theorem :: SCMFSA_5:16
 for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p
 for k being Nat
   holds
  p is autonomic iff Relocated(p,k) is autonomic;

theorem :: SCMFSA_5:17
 for p being halting autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom p
 for k being Nat holds
  DataPart(Result(p)) = DataPart(Result(Relocated(p,k)));

:: Relocatability

theorem :: SCMFSA_5:18
   for F being PartFunc of FinPartSt SCM+FSA, FinPartSt SCM+FSA,
     p being FinPartState of SCM+FSA st IC SCM+FSA in dom p & F is data-only
 for k being Nat
   holds
 p computes F iff Relocated( p,k) computes F;