Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### On the Composition of Macro Instructions. Part II

**by****Noriko Asamoto,****Yatsuka Nakamura,****Piotr Rudnicki, and****Andrzej Trybulec**- Received July 22, 1996
- MML identifier: SCMFSA6B

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, FUNCT_4, BOOLE, AMI_1, SCMFSA_2, SCMFSA6A, AMI_3, CAT_1, SCM_1, INT_1, FUNCOP_1, FUNCT_7, SF_MASTR, AMI_5, FINSEQ_1, RELOC, CARD_1, SCMFSA6B, CARD_3; notation TARSKI, XBOOLE_0, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, CARD_1, CQC_LANG, FUNCT_4, STRUCT_0, AMI_1, AMI_3, SCM_1, AMI_5, FUNCT_7, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A, SF_MASTR; constructors SCM_1, SCMFSA6A, SF_MASTR, FUNCT_7, SCMFSA_5, AMI_5, NAT_1, MEMBERED; clusters AMI_1, SCMFSA_2, FUNCT_1, SCMFSA_4, INT_1, SCMFSA6A, SF_MASTR, CQC_LANG, RELSET_1, FRAENKEL, XREAL_0, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin canceled 2; theorem :: SCMFSA6B:3 for f, g being Function, A being set st A /\ dom f c= A /\ dom g holds (f+*g|A)|A = g|A; begin reserve m, n for Nat, x for set, i for Instruction of SCM+FSA, I for Macro-Instruction, a for Int-Location, f for FinSeq-Location, l, l1 for Instruction-Location of SCM+FSA, s,s1,s2 for State of SCM+FSA; theorem :: SCMFSA6B:4 Start-At insloc 0 c= Initialized I; theorem :: SCMFSA6B:5 I +* Start-At insloc n c= s implies I c= s; theorem :: SCMFSA6B:6 (I +* Start-At insloc n)|the Instruction-Locations of SCM+FSA = I; theorem :: SCMFSA6B:7 x in dom I implies I.x = (I +* Start-At insloc n).x; theorem :: SCMFSA6B:8 Initialized I c= s implies I +* Start-At insloc 0 c= s; theorem :: SCMFSA6B:9 not a in dom Start-At l; theorem :: SCMFSA6B:10 not f in dom Start-At l; theorem :: SCMFSA6B:11 not l1 in dom Start-At l; theorem :: SCMFSA6B:12 not a in dom (I+*Start-At l); theorem :: SCMFSA6B:13 not f in dom (I+*Start-At l); theorem :: SCMFSA6B:14 s+*I+*Start-At insloc 0 = s+*Start-At insloc 0+*I; begin :: General theory reserve N for non empty with_non-empty_elements set; theorem :: SCMFSA6B:15 s = Following s implies for n holds (Computation s).n = s; theorem :: SCMFSA6B:16 for S being halting IC-Ins-separated definite (non empty non void AMI-Struct over N), s being State of S st s is halting holds Result s = (Computation s).LifeSpan s; definition let N; let S be IC-Ins-separated definite (non empty non void AMI-Struct over N); let s be State of S, l be Instruction-Location of S, i be Instruction of S; redefine func s+*(l,i) -> State of S; end; definition let s be State of SCM+FSA, li be Int-Location, k be Integer; redefine func s+*(li,k) -> State of SCM+FSA; end; theorem :: SCMFSA6B:17 for S being steady-programmed IC-Ins-separated definite (non empty non void AMI-Struct over N) for s being State of S, n holds s|the Instruction-Locations of S = ((Computation s).n)|the Instruction-Locations of S; begin definition let I be Macro-Instruction, s be State of SCM+FSA; func IExec(I,s) -> State of SCM+FSA equals :: SCMFSA6B:def 1 Result(s+*Initialized I) +* s|the Instruction-Locations of SCM+FSA; end; definition let I be Macro-Instruction; attr I is paraclosed means :: SCMFSA6B:def 2 for s being State of SCM+FSA, n being Nat st I +* Start-At insloc 0 c= s holds IC (Computation s).n in dom I; attr I is parahalting means :: SCMFSA6B:def 3 I +* Start-At insloc 0 is halting; attr I is keeping_0 means :: SCMFSA6B:def 4 ::Lkeep for s being State of SCM+FSA st I +* Start-At insloc 0 c= s for k being Nat holds ((Computation s).k).intloc 0 = s.intloc 0; end; definition cluster parahalting Macro-Instruction; end; theorem :: SCMFSA6B:18 for I being parahalting Macro-Instruction st I +* Start-At insloc 0 c= s holds s is halting; theorem :: SCMFSA6B:19 for I being parahalting Macro-Instruction st Initialized I c= s holds s is halting; definition let I be parahalting Macro-Instruction; cluster Initialized I -> halting; end; theorem :: SCMFSA6B:20 s2 +*(IC s2, goto IC s2) is not halting; theorem :: SCMFSA6B:21 s1,s2 equal_outside the Instruction-Locations of SCM+FSA & I c= s1 & I c= s2 & (for m st m < n holds IC((Computation s2).m) in dom I) implies for m st m <= n holds (Computation s1).m, (Computation s2 ).m equal_outside the Instruction-Locations of SCM+FSA; definition cluster parahalting -> paraclosed Macro-Instruction; cluster keeping_0 -> paraclosed Macro-Instruction; end; theorem :: SCMFSA6B:22 for I being parahalting Macro-Instruction, a being read-write Int-Location holds not a in UsedIntLoc I implies (IExec(I, s)).a = s.a; theorem :: SCMFSA6B:23 for I being parahalting Macro-Instruction holds not f in UsedInt*Loc I implies (IExec(I, s)).f = s.f; theorem :: SCMFSA6B:24 IC s = l & s.l = goto l implies s is not halting; definition cluster parahalting -> non empty Macro-Instruction; end; theorem :: SCMFSA6B:25 ::T9' for I being parahalting Macro-Instruction holds dom I <> {}; theorem :: SCMFSA6B:26 ::T9 for I being parahalting Macro-Instruction holds insloc 0 in dom I; theorem :: SCMFSA6B:27 ::T0 for J being parahalting Macro-Instruction st J +* Start-At insloc 0 c= s1 for n being Nat st ProgramPart Relocated(J,n) c= s2 & IC s2 = insloc n & s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations) for i being Nat holds IC (Computation s1).i + n = IC (Computation s2).i & IncAddr(CurInstr ((Computation s1).i),n) = CurInstr ((Computation s2).i) & (Computation s1).i | (Int-Locations \/ FinSeq-Locations) = (Computation s2).i | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA6B:28 ::T13 for I being parahalting Macro-Instruction st I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 & s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds for k being Nat holds (Computation s1).k, (Computation s2).k equal_outside the Instruction-Locations of SCM+FSA & CurInstr (Computation s1).k = CurInstr (Computation s2).k; theorem :: SCMFSA6B:29 ::T14 for I being parahalting Macro-Instruction st I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 & s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA6B:30 ::T27 for I being parahalting Macro-Instruction holds IC IExec(I,s) = IC Result (s +* Initialized I); theorem :: SCMFSA6B:31 for I being non empty Macro-Instruction holds insloc 0 in dom I & insloc 0 in dom Initialized I & insloc 0 in dom (I +* Start-At insloc 0); theorem :: SCMFSA6B:32 x in dom Macro i iff x = insloc 0 or x = insloc 1; theorem :: SCMFSA6B:33 (Macro i).(insloc 0) = i & (Macro i).(insloc 1) = halt SCM+FSA & (Initialized Macro i).insloc 0 = i & (Initialized Macro i).insloc 1 = halt SCM+FSA & ((Macro i) +* Start-At insloc 0).insloc 0 = i; theorem :: SCMFSA6B:34 Initialized I c= s implies IC s = insloc 0; definition cluster keeping_0 parahalting Macro-Instruction; end; theorem :: SCMFSA6B:35 for I being keeping_0 parahalting Macro-Instruction holds IExec(I, s).intloc 0 = 1; begin :: The composition of macroinstructions theorem :: SCMFSA6B:36 for I being paraclosed Macro-Instruction, J being Macro-Instruction st I +* Start-At insloc 0 c= s & s is halting for m st m <= LifeSpan s holds (Computation s).m,(Computation(s+*(I ';' J))).m equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA6B:37 ::Lemma01 for I being paraclosed Macro-Instruction st s +*I is halting & Directed I c= s & Start-At insloc 0 c= s holds IC (Computation s).(LifeSpan (s +*I) + 1) = insloc card I; theorem :: SCMFSA6B:38 ::Lemma02 for I being paraclosed Macro-Instruction st s +*I is halting & Directed I c= s & Start-At insloc 0 c= s holds (Computation s).(LifeSpan (s +*I)) | (Int-Locations \/ FinSeq-Locations) = (Computation s).(LifeSpan (s +*I) + 1) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA6B:39 ::Lemma0 for I being parahalting Macro-Instruction st Initialized I c= s holds for k being Nat st k <= LifeSpan s holds CurInstr (Computation (s +* Directed I)).k <> halt SCM+FSA; theorem :: SCMFSA6B:40 for I being paraclosed Macro-Instruction st s +* (I +* Start-At insloc 0) is halting for J being Macro-Instruction, k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) holds (Computation (s +* (I +* Start-At insloc 0))).k, (Computation (s +* ((I ';' J) +* Start-At insloc 0))).k equal_outside the Instruction-Locations of SCM+FSA; definition let I, J be parahalting Macro-Instruction; cluster I ';' J -> parahalting; end; theorem :: SCMFSA6B:41 for I being keeping_0 Macro-Instruction st not s +* (I +* Start-At insloc 0) is halting for J being Macro-Instruction, k being Nat holds (Computation (s +* (I +* Start-At insloc 0))).k, (Computation (s +* ((I ';' J) +* Start-At insloc 0))).k equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA6B:42 for I being keeping_0 Macro-Instruction st s +* I is halting for J being paraclosed Macro-Instruction st (I ';' J) +* Start-At insloc 0 c= s for k being Nat holds (Computation (Result(s +*I) +* (J +* Start-At insloc 0))).k +* Start-At (IC (Computation ((Result(s +*I)) +* (J +* Start-At insloc 0))).k + card I), (Computation (s +* (I ';' J))). (LifeSpan (s +* I)+1+k) equal_outside the Instruction-Locations of SCM+FSA; definition let I, J be keeping_0 Macro-Instruction; cluster I ';' J -> keeping_0; end; theorem :: SCMFSA6B:43 ::T22 for I being keeping_0 parahalting Macro-Instruction, J being parahalting Macro-Instruction holds LifeSpan (s +* Initialized (I ';' J)) = LifeSpan (s +* Initialized I) + 1 + LifeSpan (Result (s +* Initialized I) +* Initialized J); theorem :: SCMFSA6B:44 for I being keeping_0 parahalting Macro-Instruction, J being parahalting Macro-Instruction holds IExec(I ';' J,s) = IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I);

Back to top