:: Standard Ordering of Instruction Locations :: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz :: :: Received April 14, 2000 :: Copyright (c) 2000-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, XBOOLE_0, SUBSET_1, SETFAM_1, AMI_1, FSM_1, FUNCT_4, FUNCOP_1, RELAT_1, TARSKI, STRUCT_0, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2, CAT_1, NAT_1, GLIB_000, XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, CARD_1, GOBOARD5, FUNCT_2, FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, AMISTD_1, EXTPRO_1, COMPOS_1, AMISTD_2, SCMFSA6B, QUANTAL1, GOBRD13, MEMSTR_0, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, ORDINAL1, CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1, PARTFUN1, XTUPLE_0, MCART_1, VALUED_1, DOMAIN_1, CARD_3, FINSEQ_1, FINSEQ_4, FUNCOP_1, FINSET_1, FUNCT_4, FUNCT_7, AFINSQ_1, PBOOLE, MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_2; constructors WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, COMPOS_1, EXTPRO_1, RELSET_1, PRE_POLY, GRAPH_2, AFINSQ_1, MCART_1, FUNCT_7, PBOOLE, XXREAL_1, FUNCT_4, MEASURE6, MEMSTR_0, XTUPLE_0; registrations SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, STRUCT_0, CARD_1, RELSET_1, FUNCT_4, AFINSQ_1, COMPOS_1, EXTPRO_1, PRE_POLY, MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0, INT_1; requirements NUMERALS, BOOLE, REAL, SUBSET, ARITHM; begin :: AMI-Struct reserve x for set, D for non empty set, k, n for Nat, z for Nat; reserve N for with_zero set, S for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i for Element of the InstructionsF of S, l, l1, l2, l3 for Nat, s for State of S; registration let N be with_zero set, S be with_non-empty_values AMI-Struct over N, i be Element of the InstructionsF of S, s be State of S; cluster ((the Execution of S).i).s -> Function-like Relation-like; end; registration let N; cluster non empty with_non-empty_values for AMI-Struct over N; end; definition let N be with_zero set; let S be non empty with_non-empty_values AMI-Struct over N; let T be InsType of the InstructionsF of S; attr T is jump-only means :: AMISTD_1:def 1 for s being State of S, o being Object of S, I being Instruction of S st InsCode I = T & o in Data-Locations S holds Exec(I, s).o = s.o; end; definition let N be with_zero set; let S be non empty with_non-empty_values AMI-Struct over N; let I be Instruction of S; attr I is jump-only means :: AMISTD_1:def 2 InsCode I is jump-only; end; reserve ss for Element of product the_Values_of S; definition let N,S; let l be Nat; let i be Element of the InstructionsF of S; func NIC(i,l) -> Subset of NAT equals :: AMISTD_1:def 3 { IC Exec(i,ss) : IC ss = l }; end; registration let N be with_zero set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i be Element of the InstructionsF of S, l be Nat; cluster NIC(i,l) -> non empty; end; definition let N,S,i; func JUMP i -> Subset of NAT equals :: AMISTD_1:def 4 meet the set of all NIC(i,l) ; end; definition let N,S; let l be Nat; func SUCC(l,S) -> Subset of NAT equals :: AMISTD_1:def 5 union the set of all NIC(i,l) \ JUMP i ; end; theorem :: AMISTD_1:1 for i being Element of the InstructionsF of S st for l being Nat holds NIC(i,l)={l} holds JUMP i is empty; theorem :: AMISTD_1:2 for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, il being Nat, i being Instruction of S st i is halting holds NIC(i,il) = {il}; begin :: Ordering of Instruction Locations definition let N, S; attr S is standard means :: AMISTD_1:def 6 for m, n being Nat holds m <= n iff ex f being non empty FinSequence of NAT st f/.1 = m & f/.len f = n & for n st 1 <= n & n < len f holds f/.(n+1) in SUCC(f/.n,S); end; theorem :: AMISTD_1:3 S is standard iff for k being Nat holds k+1 in SUCC(k,S) & for j being Nat st j in SUCC(k,S) holds k <= j; begin :: Standard trivial computer definition let N be with_zero set; func STC N -> strict AMI-Struct over N means :: AMISTD_1:def 7 the carrier of it = {0} & IC it = 0 & the InstructionsF of it = {[0,0,0],[1,0,0]} & the Object-Kind of it = (0 .--> 0) & the ValuesF of it = N --> NAT & ex f being Function of product the_Values_of it, product the_Values_of it st (for s being Element of product the_Values_of it holds f.s = s+*(0 .-->(In(s.0,NAT) + 1))) & the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> id product the_Values_of it); end; registration let N be with_zero set; cluster STC N -> finite non empty; end; registration let N be with_zero set; cluster STC N -> with_non-empty_values; end; registration let N be with_zero set; cluster STC N -> IC-Ins-separated; end; theorem :: AMISTD_1:4 for i being Instruction of STC N st InsCode i = 0 holds i is halting; theorem :: AMISTD_1:5 for i being Instruction of STC N st InsCode i = 1 holds i is non halting; theorem :: AMISTD_1:6 for i being Element of the InstructionsF of STC N holds InsCode i = 1 or InsCode i = 0; theorem :: AMISTD_1:7 for i being Instruction of STC N holds i is jump-only; registration let N; cluster -> ins-loc-free for Instruction of STC N; end; theorem :: AMISTD_1:8 for l being Nat st l = z holds SUCC(l,STC N) = {z, z+1}; registration let N be with_zero set; cluster STC N -> standard; end; registration let N be with_zero set; cluster STC N -> halting; end; registration let N be with_zero set; cluster standard halting for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; end; reserve T for standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; theorem :: AMISTD_1:9 for i being Instruction of STC N, s being State of STC N st InsCode i = 1 holds Exec(i,s).IC STC N = IC s + 1; theorem :: AMISTD_1:10 for l being Nat, i being Element of the InstructionsF of STC N st InsCode i = 1 holds NIC(i, l) = {l+1}; theorem :: AMISTD_1:11 for l being Nat holds SUCC(l,STC N) = {l, l + 1}; definition let N be with_zero set, S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i be Instruction of S; attr i is sequential means :: AMISTD_1:def 8 for s being State of S holds Exec(i, s).IC S = IC s + 1; end; theorem :: AMISTD_1:12 for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, il being Nat, i being Instruction of S st i is sequential holds NIC(i,il) = {il + 1}; registration let N; let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; cluster sequential -> non halting for Instruction of S; cluster halting -> non sequential for Instruction of S; end; theorem :: AMISTD_1:13 for T being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for i being Instruction of T st JUMP i is non empty holds i is non sequential; begin :: Closedness of finite partial states definition let N be with_zero set; let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let F be finite preProgram of S; attr F is really-closed means :: AMISTD_1:def 9 for l being Nat st l in dom F holds NIC (F/.l, l) c= dom F; end; ::$CD 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 F be NAT-defined (the InstructionsF of S)-valued Function; attr F is parahalting means :: AMISTD_1:def 11 for s being 0-started State of S for P being Instruction-Sequence of S st F c= P holds P halts_on s; end; theorem :: AMISTD_1:14 for N being with_zero set for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for F being finite preProgram of S holds F is really-closed iff for s being State of S st IC s in dom F for k being Nat holds IC Comput(F,s,k) in dom F; registration let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; cluster Stop S -> really-closed; end; ::$CT 2 registration let N be with_zero set; let S be standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; cluster really-closed trivial for MacroInstruction of S; end; theorem :: AMISTD_1:17 for i being Instruction of Trivial-AMI(N) holds i is halting; theorem :: AMISTD_1:18 for i being Element of the InstructionsF of Trivial-AMI N holds InsCode i = 0 ; begin :: Addenda :: from SCMPDS_9, 2008.03.10, A.T. theorem :: AMISTD_1:19 for N being with_zero set, S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, i being Instruction of S, l being Nat holds JUMP(i) c= NIC(i,l); theorem :: AMISTD_1:20 for i being Instruction of STC N, s being State of STC N st InsCode i = 1 holds Exec(i,s) = IncIC(s,1); registration let N; let p be PartState of STC N; cluster DataPart p -> empty; end; theorem :: AMISTD_1:21 for N being with_zero set for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for F being finite preProgram of S holds F is really-closed iff for s being State of S st IC s in dom F for P being Instruction-Sequence of S st F c= P for k being Nat holds IC Comput(P,s,k) in dom F; 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 for finite non halt-free non empty NAT-defined (the InstructionsF of S)-valued Function; end;