:: Constant assignment macro instructions of SCM+FSA, Part II :: by Noriko Asamoto :: :: Received August 27, 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, FINSEQ_1, AMI_1, SCMFSA_2, RELAT_1, SCMFSA_7, ARYTM_3, ARYTM_1, TARSKI, FUNCT_1, XXREAL_0, PARTFUN1, CAT_1, NAT_1, CARD_1, FUNCOP_1, SCMFSA6A, ORDINAL4, AMI_3, FUNCT_4, INT_1, GRAPHSP, FSM_1, CIRCUIT2, EXTPRO_1, SCMFSA6B, SF_MASTR, MSUALG_1, XBOOLE_0, PRE_POLY, AMISTD_2, SCMFSA7B, AFINSQ_1, SCMFSA6C, COMPOS_1, AMISTD_1, TURING_1, RELOC, VALUED_1, SCMPDS_4; 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, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1, AMISTD_2, FUNCOP_1, XXREAL_0, ENUMSET1, NAT_D, PBOOLE, AFINSQ_2, AMISTD_4, SCMFSA_7, COMPOS_2, SCMFSA6A, SF_MASTR, SCMFSA6B, INT_2, PRE_POLY, SCMFSA_M; constructors ENUMSET1, XXREAL_0, REAL_1, SCMFSA_7, SCMFSA6A, SF_MASTR, SCMFSA6B, NAT_D, RELSET_1, PRE_POLY, DOMAIN_1, AFINSQ_2, PARTFUN3, PBOOLE, AMISTD_1, AMISTD_2, AMI_3, MEMSTR_0, SCMFSA_M, FUNCT_7, COMPOS_2; registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6B, ORDINAL1, CARD_1, AFINSQ_1, COMPOS_1, AFINSQ_2, EXTPRO_1, FUNCT_4, STRUCT_0, MEMSTR_0, SCMFSA10, COMPOS_0, SCMFSA_M, COMPOS_2, SCMFSA6C, SCMFSA_4; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve m for Nat; reserve P for Instruction-Sequence of SCM+FSA; theorem :: SCMFSA7B:1 for i being Instruction of SCM+FSA holds (i = halt SCM+FSA implies ( Directed Macro i). 0 = goto 2) & (i <> halt SCM+FSA implies ( Directed Macro i). 0 = i); theorem :: SCMFSA7B:2 for i being Instruction of SCM+FSA holds (Directed Macro i). 1 = goto 2; registration let a be Int-Location, k be Integer; cluster a := k -> initial non empty NAT-defined (the InstructionsF of SCM+FSA)-valued; end; registration let a be Int-Location, k be Integer; cluster a := k -> parahalting; end; theorem :: SCMFSA7B:3 for s being State of SCM+FSA for a being read-write Int-Location, k being Integer holds IExec(a := k,P,s).a = k & (for b being read-write Int-Location st b <> a holds IExec(a := k,P,s).b = s.b) & for f being FinSeq-Location holds IExec(a := k,P,s).f = s.f; registration let f be FinSeq-Location, p be FinSequence of INT; cluster f := p -> initial non empty NAT-defined (the InstructionsF of SCM+FSA)-valued; end; registration let f be FinSeq-Location, p be FinSequence of INT; cluster f := p -> parahalting; end; theorem :: SCMFSA7B:4 for s being State of SCM+FSA, f being FinSeq-Location, p being FinSequence of INT holds IExec(f := p,P,s).f = p & (for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds IExec(f := p,P,s).a = s.a) & for g being FinSeq-Location st g <> f holds IExec(f := p,P,s).g = s.g; definition let i be Instruction of SCM+FSA; let a be Int-Location; pred i refers a means :: SCMFSA7B:def 1 not for b being Int-Location, l being Nat for f being FinSeq-Location holds b := a <> i & AddTo(b,a) <> i & SubFrom(b,a) <> i & MultBy(b,a) <> i & Divide(b,a) <> i & Divide(a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b :=(f,a) <> i & (f,b) := a <> i & (f,a):= b <> i & f :=<0,...,0> a <> i; end; definition let I be preProgram of SCM+FSA; let a be Int-Location; pred I refers a means :: SCMFSA7B:def 2 ex i being Instruction of SCM+FSA st i in rng I & i refers a; end; definition let i be Instruction of SCM+FSA; let a be Int-Location; pred i destroys a means :: SCMFSA7B:def 3 not for b being Int-Location for f being FinSeq-Location holds a := b <> i & AddTo(a,b) <> i & SubFrom(a,b) <> i & MultBy(a,b) <> i & Divide(a,b) <> i & Divide(b,a) <> i & a :=(f,b) <> i & a :=len f <> i; end; definition let I be NAT-defined (the InstructionsF of SCM+FSA)-valued Function; let a be Int-Location; pred I destroys a means :: SCMFSA7B:def 4 ex i being Instruction of SCM+FSA st i in rng I & i destroys a; end; definition let I be NAT-defined (the InstructionsF of SCM+FSA)-valued Function; attr I is good means :: SCMFSA7B:def 5 I does not destroy intloc 0; end; theorem :: SCMFSA7B:5 for a being Int-Location holds halt SCM+FSA does not destroy a; theorem :: SCMFSA7B:6 for a,b,c being Int-Location holds a <> b implies b := c does not destroy a; theorem :: SCMFSA7B:7 for a,b,c being Int-Location holds a <> b implies AddTo(b,c) does not destroy a; theorem :: SCMFSA7B:8 for a,b,c being Int-Location holds a <> b implies SubFrom(b,c) does not destroy a; theorem :: SCMFSA7B:9 for a,b,c being Int-Location holds a <> b implies MultBy(b,c) does not destroy a; theorem :: SCMFSA7B:10 for a,b,c being Int-Location holds a <> b & a <> c implies Divide(b,c) does not destroy a; theorem :: SCMFSA7B:11 for a being Int-Location, l being Nat holds goto l does not destroy a; theorem :: SCMFSA7B:12 for a,b being Int-Location, l being Nat holds b =0_goto l does not destroy a; theorem :: SCMFSA7B:13 for a,b being Int-Location, l being Nat holds b >0_goto l does not destroy a; theorem :: SCMFSA7B:14 for a,b,c being Int-Location, f being FinSeq-Location holds a <> b implies b := (f,c) does not destroy a; theorem :: SCMFSA7B:15 for a,b,c being Int-Location, f being FinSeq-Location holds (f,c):= b does not destroy a; theorem :: SCMFSA7B:16 for a,b being Int-Location, f being FinSeq-Location holds a <> b implies b :=len f does not destroy a; theorem :: SCMFSA7B:17 for a,b being Int-Location, f being FinSeq-Location holds f:=<0,...,0> b does not destroy a; ::$CD definition let I be Program of SCM+FSA; let s be State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; pred I is_halting_on s,P means :: SCMFSA7B:def 7 P +* I halts_on Initialize s; end; ::$CT theorem :: SCMFSA7B:19 for I being Program of SCM+FSA holds I is parahalting iff for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P; theorem :: SCMFSA7B:20 for i being Instruction of SCM+FSA, a being Int-Location, s being State of SCM+FSA st i does not destroy a holds Exec(i,s).a = s.a; theorem :: SCMFSA7B:21 for s being State of SCM+FSA, P being Instruction-Sequence of SCM+FSA, I being really-closed Program of SCM+FSA, a being Int-Location st I does not destroy a :::& I is_closed_on s,P for k being Nat holds Comput(P +* I,Initialize s,k).a = s.a; registration cluster Stop SCM+FSA -> parahalting good; end; registration cluster parahalting good halt-ending unique-halt for Program of SCM+FSA; end; registration cluster really-closed good -> keeping_0 for Program of SCM+FSA; end; theorem :: SCMFSA7B:22 for a being Int-Location, k being Integer holds rng aSeq(a,k) c= {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)}; theorem :: SCMFSA7B:23 for a being Int-Location, k being Integer holds rng (a := k) c= {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)}; registration let a be read-write Int-Location, k be Integer; cluster a := k -> good; end; reserve n for Nat; registration let a be read-write Int-Location, k be Integer; cluster a := k -> really-closed; end; registration let a be read-write Int-Location, k be Integer; cluster a := k -> keeping_0; end;