Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### 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;

Back to top