:: Relocable Instructions :: by Andrzej Trybulec :: :: Received November 20, 2010 :: Copyright (c) 2010-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, ARYTM_1, ARYTM_3, CARD_1, AMI_1, XBOOLE_0, RELAT_1, TARSKI, FUNCOP_1, GLIB_000, GOBOARD5, AMISTD_1, FUNCT_1, STRUCT_0, VALUED_1, FSM_1, FUNCT_4, TURING_1, CIRCUIT2, AMISTD_2, PARTFUN1, EXTPRO_1, NAT_1, RELOC, AMISTD_5, COMPOS_1, MSUALG_1, FINSET_1, QUANTAL1, MEMSTR_0, SCMFSA6B; notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, PBOOLE, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, CARD_3, FINSEQ_1, FUNCOP_1, NAT_D, FUNCT_7, VALUED_0, VALUED_1, AFINSQ_1, MEASURE6, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2; constructors WELLORD2, REALSET1, NAT_D, AMISTD_1, XXREAL_2, PRE_POLY, AFINSQ_1, ORDINAL4, VALUED_1, AMISTD_2, PBOOLE, RELSET_1, FUNCT_7, FUNCT_4, MEMSTR_0, MEASURE6, XTUPLE_0; registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, AMISTD_1, FUNCT_4, RELSET_1, GRFUNC_1, ORDINAL1, VALUED_1, COMPOS_1, EXTPRO_1, AMISTD_2, MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Relocable instructions theorem :: AMISTD_5:1 for N be with_zero set for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for I be Instruction of S st I is jump-only for k be Nat holds IncAddr(I,k) is jump-only; registration let N be with_zero set, S be with_explicit_jumps IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N, I be IC-relocable Instruction of S, k be Nat; cluster IncAddr(I,k) -> IC-relocable; end; definition let N be with_zero set, S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of S; attr I is relocable means :: AMISTD_5:def 1 for j,k being Nat, s being State of S holds Exec(IncAddr(I,j+k),IncIC(s,k)) = IncIC(Exec(IncAddr(I,j),s),k); end; registration let N be with_zero set, S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; cluster relocable -> IC-relocable for Instruction of S; end; definition let N be with_zero set, S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; attr S is relocable means :: AMISTD_5:def 2 for I being Instruction of S holds I is relocable; end; theorem :: AMISTD_5:2 for N being with_zero set, I being Instruction of STC N, s be State of STC N, k being Nat holds Exec(I,IncIC(s,k)) = IncIC(Exec(I,s),k); definition let N be with_zero set; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; attr S is IC-recognized means :: AMISTD_5:def 3 for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic FinPartState of S st p is non empty holds IC S in dom p; end; theorem :: AMISTD_5:3 for N being with_zero set for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds S is IC-recognized iff for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic FinPartState of S st DataPart p <> {} holds IC S in dom p; registration let N be with_zero set; cluster Data-Locations STC N -> empty; end; registration let N be with_zero set; let p be PartState of STC N; cluster DataPart p -> empty; end; registration let N be with_zero set; cluster STC N -> IC-recognized relocable; end; registration let N be with_zero set; cluster relocable IC-recognized for standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; end; registration let N be with_zero set; let S be relocable halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; cluster -> relocable for Instruction of S; end; reserve k for Nat; theorem :: AMISTD_5:4 for N be with_zero set for S be relocable halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for INS being Instruction of S, s being State of S holds Exec(IncAddr(INS,k),IncIC(s,k)) = IncIC(Exec(INS,s),k); theorem :: AMISTD_5:5 for N be with_zero set for S be relocable halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for INS being Instruction of S, s being State of S, j, k being Nat st IC s = j+k holds Exec(INS, DecIC(s,k)) = DecIC(Exec(IncAddr(INS, k), s),k); registration let N be with_zero set; cluster relocable IC-recognized for halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; end; reserve N for with_zero set, S for IC-recognized halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; theorem :: AMISTD_5:6 for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of S holds IC S in dom p; definition let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; attr S is CurIns-recognized means :: AMISTD_5:def 4 for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of S for s being State of S st p c= s for P being Instruction-Sequence of S st q c= P for i being Nat holds IC Comput(P,s,i) in dom q; end; registration let N; cluster STC N -> CurIns-recognized; end; registration let N be with_zero set; cluster relocable IC-recognized CurIns-recognized for halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; end; reserve S for IC-recognized CurIns-recognized halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; theorem :: AMISTD_5:7 for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of S, s1,s2 being State of S st p c= s1 & p c= s2 for P1,P2 being Instruction-Sequence of S st q c= P1 & q c= P2 for i being Nat holds IC Comput(P1,s1,i) = IC Comput(P2,s2,i) & CurInstr(P1,Comput(P1,s1,i)) = CurInstr(P2,Comput(P2,s2,i)); reserve S for relocable IC-recognized CurIns-recognized halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; theorem :: AMISTD_5:8 for k being Nat for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic FinPartState of S st IC S in dom p for s being State of S st p c= s for P being Instruction-Sequence of S st q c= P for i being Nat holds Comput(P +* Reloc(q,k),s +* IncIC( p,k),i) = IncIC(Comput(P,s,i),k); theorem :: AMISTD_5:9 for k being Nat for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic FinPartState of S st IC S in dom p for s being State of S st IncIC(p,k) c= s holds for P being Instruction-Sequence of S st Reloc(q,k) c= P for i being Nat holds Comput(P,s,i) = IncIC(Comput(P+*q,s+* p,i),k); reserve m,j for Nat; theorem :: AMISTD_5:10 for k being Nat for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being non empty FinPartState of S st IC S in dom p for s being State of S st p c= s & IncIC(p,k) is Reloc(q,k)-autonomic for P being Instruction-Sequence of S st q c= P for i being Nat holds Comput(P,s,i) = DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k); theorem :: AMISTD_5:11 for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being non empty FinPartState of S st IC S in dom p for k being Nat holds p is q-autonomic iff IncIC(p,k) is Reloc(q,k)-autonomic; definition let N,S; attr S is relocable1 means :: AMISTD_5:def 5 for k being Nat for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of S, s1, s2 being State of S st p c= s1 & IncIC( p,k) c= s2 for P1,P2 being Instruction-Sequence of S st q c= P1 & Reloc(q,k) c= P2 for i being Nat holds IncAddr(CurInstr(P1,Comput(P1,s1,i)),k) = CurInstr(P2,Comput(P2,s2,i)); attr S is relocable2 means :: AMISTD_5:def 6 for k being Nat for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of S, s1, s2 being State of S st p c= s1 & IncIC( p,k) c= s2 for P1,P2 being Instruction-Sequence of S st q c= P1 & Reloc(q,k) c= P2 for i being Nat holds Comput(P1,s1,i)|dom DataPart p = Comput(P2,s2,i)|dom DataPart p; end; registration let N; cluster STC N -> relocable1 relocable2; end; registration let N be with_zero set; cluster relocable1 relocable2 for relocable IC-recognized CurIns-recognized halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; end; reserve S for relocable1 relocable2 relocable IC-recognized CurIns-recognized halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; theorem :: AMISTD_5:12 for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic non empty FinPartState of S, k being Nat st IC S in dom p holds p is q-halted iff IncIC(p,k) is Reloc(q,k)-halted; theorem :: AMISTD_5:13 for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-halted q-autonomic non empty FinPartState of S st IC S in dom p for k being Nat holds DataPart(Result(q, p)) = DataPart Result(Reloc(q,k),IncIC( p,k)); registration let N,S; let q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function; let p be q-autonomic q-halted non empty FinPartState of S, k be Nat; cluster IncIC(p,k) -> Reloc(q,k)-halted; end; theorem :: AMISTD_5:14 for F being data-only PartFunc of FinPartSt S, FinPartSt S, l being Nat for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function, p being q-autonomic q-halted non empty FinPartState of S st IC S in dom p for k being Nat holds q, p computes F iff Reloc(q,k), IncIC( p,k) computes F; reserve S for IC-recognized CurIns-recognized halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; theorem :: AMISTD_5:15 for q be non halt-free finite (the InstructionsF of S)-valued NAT-defined Function for p being q-autonomic FinPartState of S st IC S in dom p holds IC p in dom q; definition let N be with_zero set; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let k be Nat; let F be NAT-defined (the InstructionsF of S)-valued Function; attr F is k-halting means :: AMISTD_5:def 7 for s being k-started State of S for P being Instruction-Sequence of S st F c= P holds P halts_on s; end; registration let N be with_zero set; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; cluster parahalting -> 0-halting for NAT-defined (the InstructionsF of S)-valued Function; cluster 0-halting -> parahalting for NAT-defined (the InstructionsF of S)-valued Function; end;