:: On the compositions of macro instructions, Part III :: by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec :: :: Received July 22, 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 AMI_1, SCMFSA_2, FSM_1, CARD_1, SCMFSA6B, FUNCT_1, RELAT_1, ARYTM_3, FUNCT_4, SCMFSA6A, TARSKI, XBOOLE_0, CIRCUIT2, NUMBERS, GRAPHSP, AMI_3, XXREAL_0, SF_MASTR, FUNCOP_1, STRUCT_0, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, AOFA_I00, EXTPRO_1, SCMFSA6C, COMPOS_1, NAT_1, AMISTD_1, FRECHET, TURING_1; notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, INT_1, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, FUNCOP_1, FUNCT_4, PBOOLE, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, EXTPRO_1, AMISTD_1, FUNCT_7, SCMFSA_M, SCMFSA_2, SCMFSA10, SCMFSA6A, SF_MASTR, SCMFSA6B, XXREAL_0; constructors DOMAIN_1, SETWISEO, XXREAL_0, INT_2, SCMFSA6A, SF_MASTR, SCMFSA6B, RELSET_1, PRE_POLY, AMISTD_1, AMISTD_2, PBOOLE, FUNCT_4, MEMSTR_0, SCMFSA_1, SCMFSA_M, FUNCT_7, SCMFSA10, COMPOS_2; registrations FUNCT_1, FUNCOP_1, XREAL_0, INT_1, SCMFSA_2, SF_MASTR, SCMFSA6B, ORDINAL1, RELSET_1, COMPOS_1, STRUCT_0, EXTPRO_1, FUNCT_4, MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A, SCMFSA10, AMISTD_2; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin :: Consequences of the main theorem from SCMFSA6B reserve x for set, i for Instruction of SCM+FSA, a,b for Int-Location, f for FinSeq-Location, l, l1 for Nat, s,s1,s2 for State of SCM+FSA, P,P1,P2 for Instruction-Sequence of SCM+FSA; theorem :: SCMFSA6C:1 for I being keeping_0 parahalting really-closed Program of SCM+FSA, J being parahalting really-closed Program of SCM+FSA holds IExec(I ";" J,P,s).a = IExec(J,P,IExec(I,P,s)).a; theorem :: SCMFSA6C:2 for I being keeping_0 parahalting really-closed Program of SCM+FSA, J being parahalting really-closed Program of SCM+FSA holds IExec(I ";" J,P,s).f = IExec(J,P,IExec(I,P,s)).f; begin :: Properties of simple macro instructions ::$CD definition let i be Instruction of SCM+FSA; :: attr i is parahalting means :: :Def1: :: Macro i is parahalting; attr i is keeping_0 means :: SCMFSA6C:def 2 Macro i is keeping_0; end; registration cluster halt SCM+FSA -> keeping_0; end; registration let i be sequential Instruction of SCM+FSA; cluster Macro i -> parahalting; end; registration let a, b be Int-Location; let f be FinSeq-Location; cluster (f,a) := b -> keeping_0; end; registration let a be Int-Location, f be FinSeq-Location; cluster f :=<0,...,0> a -> keeping_0; end; registration let a be read-write Int-Location, b be Int-Location; cluster a := b -> keeping_0; cluster AddTo(a, b) -> keeping_0; cluster SubFrom(a, b) -> keeping_0; cluster MultBy(a, b) -> keeping_0; end; registration cluster keeping_0 sequential for Instruction of SCM+FSA; end; registration let i be keeping_0 Instruction of SCM+FSA; cluster Macro i -> keeping_0; end; registration let a, b be read-write Int-Location; cluster Divide(a, b) -> keeping_0; end; registration let a be Int-Location, f be FinSeq-Location, b be read-write Int-Location; cluster b := (f,a) -> keeping_0; end; registration let f be FinSeq-Location, b be read-write Int-Location; cluster b :=len f -> keeping_0; end; registration let i be sequential Instruction of SCM+FSA; cluster Macro i -> really-closed; end; :: registration :: let i be keeping_0 Instruction of SCM+FSA; :: cluster Macro i -> really-closed; :: coherence; :: end; registration let i be sequential Instruction of SCM+FSA, J be parahalting really-closed Program of SCM+FSA; cluster i ";" J -> parahalting really-closed; end; registration let I be parahalting really-closed Program of SCM+FSA, j be sequential Instruction of SCM+FSA; cluster I ";" j -> parahalting really-closed; end; registration let i,j be sequential Instruction of SCM+FSA; cluster i ";" j -> parahalting really-closed; end; registration let i be keeping_0 sequential Instruction of SCM+FSA, J be keeping_0 really-closed Program of SCM+FSA; cluster i ";" J -> keeping_0; end; registration let I be keeping_0 really-closed Program of SCM+FSA, j be keeping_0 sequential Instruction of SCM+FSA; cluster I ";" j -> keeping_0; end; registration let i, j be keeping_0 sequential Instruction of SCM+FSA; cluster i ";" j -> keeping_0; end; begin :: Consequenses of the main theorem ::$CT theorem :: SCMFSA6C:4 DataPart s1 = DataPart s2 implies DataPart Exec (i, s1) = DataPart Exec (i, s2); theorem :: SCMFSA6C:5 for i being sequential Instruction of SCM+FSA holds Exec(i,Initialized s) = IExec(Macro i,P,s); theorem :: SCMFSA6C:6 for I being keeping_0 parahalting really-closed Program of SCM+FSA, j being sequential Instruction of SCM+FSA holds IExec(I ";" j,P,s).a = Exec(j,IExec(I,P,s)).a; theorem :: SCMFSA6C:7 for I being keeping_0 parahalting really-closed Program of SCM+FSA, j being sequential Instruction of SCM+FSA holds IExec(I ";" j,P,s).f = Exec(j,IExec(I,P,s)).f; theorem :: SCMFSA6C:8 for i being keeping_0 sequential Instruction of SCM+FSA, j being sequential Instruction of SCM+FSA holds IExec(i ";" j,P,s).a = Exec(j, Exec(i,Initialized s)).a; theorem :: SCMFSA6C:9 for i being keeping_0 sequential Instruction of SCM+FSA, j being sequential Instruction of SCM+FSA holds IExec(i ";" j,P,s).f = Exec(j, Exec(i, Initialized s)).f; begin :: An example definition let a, b be Int-Location; func swap (a, b) -> Program of SCM+FSA equals :: SCMFSA6C:def 3 FirstNotUsed Macro (a := b) := a ";" (a := b) ";" (b := FirstNotUsed Macro (a := b)); end; registration let a, b be Int-Location; cluster swap(a,b) -> parahalting really-closed; end; registration let a, b be read-write Int-Location; cluster swap(a,b) -> keeping_0; end; theorem :: SCMFSA6C:10 for a, b being read-write Int-Location holds IExec(swap(a,b),P,s).a = s.b & IExec(swap(a,b),P,s).b = s.a; theorem :: SCMFSA6C:11 UsedI*Loc swap(a, b) = {}; registration let i,j be sequential Instruction of SCM+FSA; cluster i ';' j -> really-closed; end; registration let I be really-closed MacroInstruction of SCM+FSA, j be sequential Instruction of SCM+FSA; cluster I ';' j -> really-closed; end; registration let i be sequential Instruction of SCM+FSA, J be really-closed MacroInstruction of SCM+FSA; cluster i ';' J -> really-closed; end;