Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### On the Compositions of Macro Instructions. Part I

**by****Andrzej Trybulec,****Yatsuka Nakamura, and****Noriko Asamoto**- Received June 20, 1996
- MML identifier: SCMFSA6A

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, FUNCT_4, FUNCT_7, BOOLE, CAT_1, AMI_3, AMI_1, SCMFSA_2, CARD_1, FUNCOP_1, FINSET_1, TARSKI, AMI_5, RELOC, INT_1, AMI_2, ARYTM_1, NAT_1, ABSVALUE, FINSEQ_1, FINSEQ_2, SCMFSA6A, FINSEQ_4; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, CQC_LANG, FINSET_1, FUNCT_4, STRUCT_0, AMI_1, AMI_3, AMI_5, FUNCT_7, SCMFSA_2, SCMFSA_4, SCMFSA_5; constructors SCMFSA_4, WELLORD2, SCMFSA_5, NAT_1, AMI_5, ENUMSET1, FUNCT_7, RELOC, FINSEQ_4, MEMBERED; clusters XBOOLE_0, AMI_1, SCMFSA_2, FUNCT_1, FINSET_1, PRELAMB, FUNCT_7, SCMFSA_4, RELSET_1, INT_1, FRAENKEL, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries theorem :: SCMFSA6A:1 for f,g being Function, x,y being set st g c= f & not x in dom g holds g c= f+*(x,y); theorem :: SCMFSA6A:2 for f,g being Function, A being set st f|A = g|A & f,g equal_outside A holds f = g; theorem :: SCMFSA6A:3 for f being Function, a,b,A being set st a in A holds f,f+*(a,b) equal_outside A; theorem :: SCMFSA6A:4 for f being Function, a,b,A being set holds a in A or (f+*(a,b))|A = f|A; theorem :: SCMFSA6A:5 for f,g being Function, a,b,A being set st f|A = g|A holds (f+*(a,b))|A = (g+*(a,b))|A; theorem :: SCMFSA6A:6 for f,g,h being Function st f c= h & g c= h holds f +* g c= h; theorem :: SCMFSA6A:7 for a,b being set, f being Function holds a.-->b c= f iff a in dom f & f.a = b; theorem :: SCMFSA6A:8 ::Lemma12 for f being Function, A being set holds dom (f | (dom f \ A)) = dom f \ A; theorem :: SCMFSA6A:9 ::LemmaD for f,g being Function, D being set st D c= dom f & D c= dom g holds f | D = g | D iff for x being set st x in D holds f.x = g.x; theorem :: SCMFSA6A:10 ::Lemma14 for f being Function, D being set holds f | D = f | (dom f /\ D); theorem :: SCMFSA6A:11 ::Lemma7 for f,g,h being Function, A being set holds f, g equal_outside A implies f +* h, g +* h equal_outside A; theorem :: SCMFSA6A:12 ::Lemma7' for f,g,h being Function, A being set holds f, g equal_outside A implies h +* f, h +* g equal_outside A; theorem :: SCMFSA6A:13 for f,g,h being Function holds f +* h = g +* h iff f,g equal_outside dom h; begin definition mode Macro-Instruction is initial programmed FinPartState of SCM+FSA; end; reserve l, m, n for Nat, i,j,k for Instruction of SCM+FSA, I,J,K for Macro-Instruction; definition let I be programmed FinPartState of SCM+FSA; func Directed I -> programmed FinPartState of SCM+FSA equals :: SCMFSA6A:def 1 ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc card I))*I; end; theorem :: SCMFSA6A:14 dom Directed I = dom I; definition let I be Macro-Instruction; cluster Directed I -> initial; end; definition let i; func Macro i -> Macro-Instruction equals :: SCMFSA6A:def 2 (insloc 0,insloc 1) --> (i,halt SCM+FSA); end; definition let i; cluster Macro i -> non empty; end; theorem :: SCMFSA6A:15 for P being Macro-Instruction, n holds n < card P iff insloc n in dom P; definition let I be initial FinPartState of SCM+FSA; cluster ProgramPart I -> initial; end; theorem :: SCMFSA6A:16 dom I misses dom ProgramPart Relocated(J, card I); theorem :: SCMFSA6A:17 for I being programmed FinPartState of SCM+FSA holds card ProgramPart Relocated(I, m) = card I; theorem :: SCMFSA6A:18 not halt SCM+FSA in rng Directed I; theorem :: SCMFSA6A:19 ProgramPart Relocated(Directed I, m) = ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc(m + card I)))* ProgramPart Relocated(I, m); theorem :: SCMFSA6A:20 for I,J being FinPartState of SCM+FSA holds ProgramPart(I +* J) = ProgramPart I +* ProgramPart J; theorem :: SCMFSA6A:21 for I,J being FinPartState of SCM+FSA holds ProgramPart Relocated(I +* J, n) = ProgramPart Relocated(I,n) +* ProgramPart Relocated(J,n); theorem :: SCMFSA6A:22 ProgramPart Relocated(ProgramPart Relocated(I, m), n) = ProgramPart Relocated(I, m + n); reserve a,b for Int-Location, f for FinSeq-Location, s,s1,s2 for State of SCM+FSA; definition let I be FinPartState of SCM+FSA; func Initialized I -> FinPartState of SCM+FSA equals :: SCMFSA6A:def 3 I +* ((intloc 0) .--> 1) +* Start-At(insloc 0); end; theorem :: SCMFSA6A:23 InsCode i in {0,6,7,8} or Exec(i,s).IC SCM+FSA = Next IC s; theorem :: SCMFSA6A:24 IC SCM+FSA in dom Initialized I; theorem :: SCMFSA6A:25 IC Initialized I = insloc 0; theorem :: SCMFSA6A:26 I c= Initialized I; theorem :: SCMFSA6A:27 for N being set, A being AMI-Struct over N, s being State of A, I being programmed FinPartState of A holds s,s+*I equal_outside the Instruction-Locations of A; theorem :: SCMFSA6A:28 for s1,s2 being State of SCM+FSA st IC s1 = IC s2 & (for a being Int-Location holds s1.a = s2.a) & for f being FinSeq-Location holds s1.f = s2.f holds s1,s2 equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA6A:29 for N being with_non-empty_elements set, S being realistic IC-Ins-separated definite (non empty non void AMI-Struct over N), s1, s2 being State of S holds s1,s2 equal_outside the Instruction-Locations of S implies IC s1 = IC s2; theorem :: SCMFSA6A:30 s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies for a being Int-Location holds s1.a = s2.a; theorem :: SCMFSA6A:31 s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies for f being FinSeq-Location holds s1.f = s2.f; theorem :: SCMFSA6A:32 s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies Exec(i,s1),Exec(i,s2) equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA6A:33 (Initialized I)|the Instruction-Locations of SCM+FSA = I; scheme SCMFSAEx{ F(set) -> Element of the Instructions of SCM+FSA, G(set) -> Integer, H(set) -> FinSequence of INT, I() -> Instruction-Location of SCM+FSA }: ex S being State of SCM+FSA st IC S = I() & for i being Nat holds S.insloc i = F(i) & S.intloc i = G(i) & S.fsloc i = H(i); theorem :: SCMFSA6A:34 ::T12 for s being State of SCM+FSA holds dom s = Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/ the Instruction-Locations of SCM+FSA; theorem :: SCMFSA6A:35 ::T12' for s being State of SCM+FSA, x being set st x in dom s holds x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Instruction-Location of SCM+FSA; theorem :: SCMFSA6A:36 ::T29 for s1,s2 being State of SCM+FSA holds (for l being Instruction-Location of SCM+FSA holds s1.l = s2.l) iff s1 | the Instruction-Locations of SCM+FSA = s2 | the Instruction-Locations of SCM+FSA; theorem :: SCMFSA6A:37 ::T32 for i being Instruction-Location of SCM+FSA holds not i in Int-Locations \/ FinSeq-Locations & not IC SCM+FSA in Int-Locations \/ FinSeq-Locations; theorem :: SCMFSA6A:38 ::T28 for s1,s2 being State of SCM+FSA holds ((for a being Int-Location holds s1.a = s2.a) & for f being FinSeq-Location holds s1.f = s2.f) iff s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA6A:39 ::T19 for s1,s2 being State of SCM+FSA st s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA6A:40 ::T21 for s,ss being State of SCM+FSA, A being set holds (ss +* s | A) | A = s | A; theorem :: SCMFSA6A:41 ::Lemma for s1,s2 being State of SCM+FSA, n being Nat, i being Instruction of SCM+FSA holds IC s1 + n = IC s2 & s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations) implies IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) & Exec(i,s1) | (Int-Locations \/ FinSeq-Locations) = Exec(IncAddr(i,n),s2) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA6A:42 ::T18 for I,J being Macro-Instruction holds I,J equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA6A:43 ::T3 for I being Macro-Instruction holds dom Initialized I = dom I \/ {intloc 0} \/ {IC SCM+FSA}; theorem :: SCMFSA6A:44 ::T2 for I being Macro-Instruction, x being set st x in dom Initialized I holds x in dom I or x = intloc 0 or x = IC SCM+FSA; theorem :: SCMFSA6A:45 ::T3' for I being Macro-Instruction holds intloc 0 in dom Initialized I; theorem :: SCMFSA6A:46 ::T5 for I being Macro-Instruction holds (Initialized I).intloc 0 = 1 & (Initialized I).IC SCM+FSA = insloc 0; theorem :: SCMFSA6A:47 ::T7 for I being Macro-Instruction holds not intloc 0 in dom I & not IC SCM+FSA in dom I; theorem :: SCMFSA6A:48 ::T36 for I being Macro-Instruction, a being Int-Location st a <> intloc 0 holds not a in dom Initialized I; theorem :: SCMFSA6A:49 ::T37 for I being Macro-Instruction, f being FinSeq-Location holds not f in dom Initialized I; theorem :: SCMFSA6A:50 ::T8 for I being Macro-Instruction, x being set st x in dom I holds I.x = (Initialized I).x; theorem :: SCMFSA6A:51 ::T10' for I,J being Macro-Instruction for s being State of SCM+FSA st Initialized J c= s holds s +* Initialized I = s +* I; theorem :: SCMFSA6A:52 ::T10 for I,J being Macro-Instruction for s being State of SCM+FSA st Initialized J c= s holds Initialized I c= s +* I; theorem :: SCMFSA6A:53 ::T23 for I,J being Macro-Instruction for s being State of SCM+FSA holds s +* Initialized I, s +* Initialized J equal_outside the Instruction-Locations of SCM+FSA; begin :: The composition of macroinstructions definition let I,J be Macro-Instruction; func I ';' J -> Macro-Instruction equals :: SCMFSA6A:def 4 Directed I +* ProgramPart Relocated(J, card I); end; theorem :: SCMFSA6A:54 for I,J being Macro-Instruction, l being Instruction-Location of SCM+FSA st l in dom I & I.l <> halt SCM+FSA holds (I ';' J).l = I.l; theorem :: SCMFSA6A:55 ::T16 for I,J being Macro-Instruction holds Directed I c= I ';' J; theorem :: SCMFSA6A:56 ::T4 for I,J being Macro-Instruction holds dom I c= dom (I ';' J); theorem :: SCMFSA6A:57 ::T6 for I,J being Macro-Instruction holds I +* (I ';' J) = (I ';' J); theorem :: SCMFSA6A:58 ::T1 for I,J being Macro-Instruction holds Initialized I +* (I ';' J) = Initialized (I ';' J); begin :: The compostion of instruction and macroinstructions definition let i, J; func i ';' J -> Macro-Instruction equals :: SCMFSA6A:def 5 Macro i ';' J; end; definition let I, j; func I ';' j -> Macro-Instruction equals :: SCMFSA6A:def 6 I ';' Macro j; end; definition let i,j; func i ';' j -> Macro-Instruction equals :: SCMFSA6A:def 7 Macro i ';' Macro j; end; theorem :: SCMFSA6A:59 i ';' j = Macro i ';' j; theorem :: SCMFSA6A:60 i ';' j = i ';' Macro j; theorem :: SCMFSA6A:61 card(I ';' J) = card I + card J; theorem :: SCMFSA6A:62 I ';' J ';' K = I ';' (J ';' K); theorem :: SCMFSA6A:63 I ';' J ';' k = I ';' (J ';' k); theorem :: SCMFSA6A:64 I ';' j ';' K = I ';' (j ';' K); theorem :: SCMFSA6A:65 I ';' j ';' k = I ';' (j ';' k); theorem :: SCMFSA6A:66 i ';' J ';' K = i ';' (J ';' K); theorem :: SCMFSA6A:67 i ';' J ';' k = i ';' (J ';' k); theorem :: SCMFSA6A:68 i ';' j ';' K = i ';' (j ';' K); theorem :: SCMFSA6A:69 i ';' j ';' k = i ';' (j ';' k);

Back to top