:: On the compositions of macro instructions :: by Andrzej Trybulec , Yatsuka Nakamura and Noriko Asamoto :: :: Received June 20, 1996 :: Copyright (c) 1996-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, SUBSET_1, AMI_1, SCMFSA_2, EXTPRO_1, FUNCT_4, AMI_3, FUNCOP_1, RELAT_1, FUNCT_1, TARSKI, XBOOLE_0, CARD_1, CAT_1, NAT_1, ARYTM_3, XXREAL_0, AMISTD_2, VALUED_1, FSM_1, GRAPHSP, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, SCMFSA6A, RELOC, MEMSTR_0, SCMPDS_4, TURING_1, AMISTD_1, FRECHET, COMPOS_1, SCMPDS_5; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, NAT_D, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1, AMISTD_2, FUNCOP_1, XXREAL_0, SCMFSA_M; constructors WELLORD2, DOMAIN_1, XXREAL_0, INT_2, AMISTD_2, SCMFSA_2, RELSET_1, VALUED_1, AMI_3, PRE_POLY, AMISTD_1, FUNCT_7, MEMSTR_0, SCMFSA_1, SCMFSA_M, NAT_D, COMPOS_2, AFINSQ_1; registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0, INT_1, SCMFSA_2, FUNCT_4, RELAT_1, VALUED_1, SCMFSA10, AMISTD_2, COMPOS_1, EXTPRO_1, AMI_3, COMPOS_0, NAT_1, AMISTD_1, COMPOS_2, AFINSQ_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve l, m, n for Nat, i,j,k for Instruction of SCM+FSA, I,J,K for Program of SCM+FSA; ::$CD definition let P be preProgram of SCM+FSA; func Directed P -> preProgram of SCM+FSA equals :: SCMFSA6A:def 2 P +~ (halt SCM+FSA,goto card P); projectivity; end; registration let I be Program of SCM+FSA; cluster Directed I -> initial non empty; end; theorem :: SCMFSA6A:1 not halt SCM+FSA in rng Directed I; theorem :: SCMFSA6A:2 Reloc(Directed I, m) = ((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto (m + card I)))* Reloc(I, m); reserve a,b for Int-Location, f for FinSeq-Location, s,s1,s2 for State of SCM+FSA; theorem :: SCMFSA6A:3 InsCode i in {0,6,7,8} or Exec(i,s).IC SCM+FSA = IC s + 1; ::$CT 4 theorem :: SCMFSA6A:8 for s1,s2 being State of SCM+FSA, n being Nat, i being Instruction of SCM+FSA holds IC s1 + n = IC s2 & DataPart s1 = DataPart s2 implies IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) & DataPart Exec(i,s1) = DataPart Exec(IncAddr(i,n),s2); ::$CT 6 begin :: The composition of macroinstructions definition ::$CD let I,J be Program of SCM+FSA; func I ";" J -> Program of SCM+FSA equals :: SCMFSA6A:def 4 stop Directed I ';' J; end; registration let I be Program of SCM+FSA, J be halt-ending Program of SCM+FSA; cluster I ";" J -> halt-ending; end; registration let P be preProgram of SCM+FSA; cluster Directed P -> halt-free; end; registration cluster halt-free for Program of SCM+FSA; end; registration let I be Program of SCM+FSA, J be unique-halt Program of SCM+FSA; cluster I ";" J -> unique-halt; end; theorem :: SCMFSA6A:15 for I,J being Program of SCM+FSA, l being Nat st l in dom I & I.l <> halt SCM+FSA holds (I ";" J).l = I.l; theorem :: SCMFSA6A:16 for I,J being Program of SCM+FSA holds Directed I c= I ";" J; theorem :: SCMFSA6A:17 for I,J being Program of SCM+FSA holds dom I c= dom (I ";" J); theorem :: SCMFSA6A:18 for I,J being Program of SCM+FSA holds I +* (I ";" J) = (I ";" J); begin :: The compostion of instruction and macroinstructions definition let i, J; func i ";" J -> Program of SCM+FSA equals :: SCMFSA6A:def 5 Macro i ";" J; end; definition let I, j; func I ";" j -> Program of SCM+FSA equals :: SCMFSA6A:def 6 I ";" Macro j; end; definition let i,j; func i ";" j -> Program of SCM+FSA equals :: SCMFSA6A:def 7 Macro i ";" Macro j; end; registration cluster sequential for Instruction of SCM+FSA; end; registration cluster sequential -> No-StopCode for Instruction of SCM+FSA; end; registration let i,j be sequential Instruction of SCM+FSA; cluster i ";" j -> halt-ending unique-halt; end; registration let I be MacroInstruction of SCM+FSA, j be sequential Instruction of SCM+FSA; cluster I ";" j -> halt-ending unique-halt; end; registration let i be sequential Instruction of SCM+FSA, J be MacroInstruction of SCM+FSA; cluster i ";" J -> halt-ending unique-halt; end; theorem :: SCMFSA6A:19 i ";" j = Macro i ";" j; theorem :: SCMFSA6A:20 i ";" j = i ";" Macro j; theorem :: SCMFSA6A:21 card(I ";" J) = card I + card J; theorem :: SCMFSA6A:22 for I being preProgram of SCM+FSA holds I is halt-free implies Directed I = I; theorem :: SCMFSA6A:23 for I being preProgram of SCM+FSA, k being Element of NAT holds Reloc(Directed I,k) = Reloc(I,k) +~ (halt SCM+FSA,goto(card I + k)); theorem :: SCMFSA6A:24 for I,J being Program of SCM+FSA holds Directed (I ";" J) = I ";" Directed J; theorem :: SCMFSA6A:25 I ";" J ";" K = I ";" (J ";" K); theorem :: SCMFSA6A:26 I ";" J ";" k = I ";" (J ";" k); theorem :: SCMFSA6A:27 I ";" j ";" K = I ";" (j ";" K); theorem :: SCMFSA6A:28 I ";" j ";" k = I ";" (j ";" k); theorem :: SCMFSA6A:29 i ";" J ";" K = i ";" (J ";" K); theorem :: SCMFSA6A:30 i ";" J ";" k = i ";" (J ";" k); theorem :: SCMFSA6A:31 i ";" j ";" K = i ";" (j ";" K); theorem :: SCMFSA6A:32 i ";" j ";" k = i ";" (j ";" k); theorem :: SCMFSA6A:33 card(i ";" J) = card J + 2; theorem :: SCMFSA6A:34 card(I ";" j) = card I + 2; theorem :: SCMFSA6A:35 card(i ";" j) = 4; theorem :: SCMFSA6A:36 for I being preProgram of SCM+FSA holds card Directed I = card I; theorem :: SCMFSA6A:37 for I being Program of SCM+FSA holds card stop Directed I = card stop I; theorem :: SCMFSA6A:38 Reloc(J,card I) c= I ";" J; theorem :: SCMFSA6A:39 dom(I ";" J) = dom I \/ dom Reloc(J, card I); theorem :: SCMFSA6A:40 n in dom Reloc(J,card I) implies (I ";" J).n = Reloc(J,card I).n; begin :: closedness registration let I be really-closed Program of SCM+FSA; cluster stop Directed I -> really-closed; end; registration let I,J be really-closed Program of SCM+FSA; cluster I ";" J -> really-closed; end; theorem :: SCMFSA6A:41 for I,J being MacroInstruction of SCM+FSA, n being Nat st n < LastLoc I holds (I ";" J).n = I.n;