Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Conditional Branch Macro Instructions of \SCMFSA. Part I

**by****Noriko Asamoto**- Received August 27, 1996
- MML identifier: SCMFSA8A

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_3, AMI_1, SCMFSA_2, BOOLE, FUNCT_1, RELAT_1, FUNCT_4, SCM_1, FUNCT_7, SCMFSA6A, SCMFSA6B, SCMFSA6C, CAT_1, SF_MASTR, SCMFSA_4, CARD_1, SCMFSA7B, AMI_5, RELOC, SCMFSA_7, FINSEQ_1, UNIALG_2, SCMFSA8A, CARD_3; notation TARSKI, XBOOLE_0, XREAL_0, NAT_1, CQC_LANG, RELAT_1, FUNCT_1, FUNCT_4, FUNCT_7, CARD_1, FINSEQ_1, STRUCT_0, AMI_1, AMI_3, AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA_7, SCM_1, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B; constructors AMI_5, SCMFSA_5, SCM_1, SCMFSA6A, SCMFSA6B, BINARITH, SCMFSA6C, SCMFSA_7, SCMFSA7B, SF_MASTR, MEMBERED; clusters RELSET_1, FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, SCMFSA6A, SF_MASTR, SCMFSA7B, INT_1, CQC_LANG, FRAENKEL, MEMBERED; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve m for Nat; canceled; theorem :: SCMFSA8A:2 ::Lemma11 for f,g being Function, D being set holds dom g misses D implies (f +* g) | D = f | D; theorem :: SCMFSA8A:3 ::T50 for s being State of SCM+FSA holds dom (s | the Instruction-Locations of SCM+FSA) = the Instruction-Locations of SCM+FSA; theorem :: SCMFSA8A:4 ::PRE8'103 for s being State of SCM+FSA st s is halting for k being Nat st LifeSpan s <= k holds CurInstr (Computation s).k = halt SCM+FSA; theorem :: SCMFSA8A:5 ::TQ53 for s being State of SCM+FSA st s is halting for k being Nat st LifeSpan s <= k holds IC (Computation s).k = IC (Computation s).LifeSpan s; theorem :: SCMFSA8A:6 ::T51(@BBB8) for s1,s2 being State of SCM+FSA holds s1,s2 equal_outside the Instruction-Locations of SCM+FSA iff IC s1 = IC s2 & s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8A:7 ::T27' for s being State of SCM+FSA, I being Macro-Instruction holds IC IExec(I,s) = IC Result (s +* Initialized I); theorem :: SCMFSA8A:8 ::TI8 for s being State of SCM+FSA, I being Macro-Instruction holds Initialize s +* Initialized I = s +* Initialized I; theorem :: SCMFSA8A:9 ::TG13 for I being Macro-Instruction, l being Instruction-Location of SCM+FSA holds I c= I +* Start-At l; theorem :: SCMFSA8A:10 ::T52(@BBB8) for s being State of SCM+FSA, l being Instruction-Location of SCM+FSA holds s | (Int-Locations \/ FinSeq-Locations) = (s +* Start-At l) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8A:11 ::T52' for s being State of SCM+FSA, I being Macro-Instruction, l being Instruction-Location of SCM+FSA holds s | (Int-Locations \/ FinSeq-Locations) = (s +* (I +* Start-At l)) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8A:12 ::T53(@BBB8) for s being State of SCM+FSA, l being Instruction-Location of SCM+FSA holds dom (s | the Instruction-Locations of SCM+FSA) misses dom Start-At l; theorem :: SCMFSA8A:13 ::TI2 for s being State of SCM+FSA, I being Macro-Instruction holds s +* Initialized I = Initialize s +* (I +* Start-At insloc 0); theorem :: SCMFSA8A:14 ::TG14 <> T23 for s being State of SCM+FSA, I1,I2 being Macro-Instruction, l being Instruction-Location of SCM+FSA holds s +* (I1 +* Start-At l), s +* (I2 +* Start-At l) equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA8A:15 ::T40(@BBB8) dom SCM+FSA-Stop = {insloc 0}; theorem :: SCMFSA8A:16 ::T41(@BBB8) insloc 0 in dom SCM+FSA-Stop & SCM+FSA-Stop.insloc 0 = halt SCM+FSA; theorem :: SCMFSA8A:17 ::T20(@BBB8) card SCM+FSA-Stop = 1; definition let P be programmed FinPartState of SCM+FSA; let l be Instruction-Location of SCM+FSA; func Directed(P,l) -> programmed FinPartState of SCM+FSA equals :: SCMFSA8A:def 1 ::D7 ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto l)) * P; end; theorem :: SCMFSA8A:18 ::T38 for I being programmed FinPartState of SCM+FSA holds Directed I = Directed(I,insloc card I); definition let P be programmed FinPartState of SCM+FSA; let l be Instruction-Location of SCM+FSA; cluster Directed(P,l) -> halt-free; end; definition let P be programmed FinPartState of SCM+FSA; cluster Directed P -> halt-free; end; theorem :: SCMFSA8A:19 ::T21 for P being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA holds dom Directed(P,l) = dom P; theorem :: SCMFSA8A:20 ::T72' for P being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA holds Directed(P,l) = P +* ((halt SCM+FSA .--> goto l) * P); theorem :: SCMFSA8A:21 ::T39' for P being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA, x being set st x in dom P holds (P.x = halt SCM+FSA implies Directed(P,l).x = goto l) & (P.x <> halt SCM+FSA implies Directed(P,l).x = P.x); theorem :: SCMFSA8A:22 ::TQ60 <> T4 for i being Instruction of SCM+FSA, a being Int-Location, n being Nat holds i does_not_destroy a implies IncAddr(i,n) does_not_destroy a; theorem :: SCMFSA8A:23 ::TQ59' for P being programmed FinPartState of SCM+FSA, n being Nat, a being Int-Location holds P does_not_destroy a implies ProgramPart Relocated(P,n) does_not_destroy a ; theorem :: SCMFSA8A:24 ::TQ59 <> T7 for P being good programmed FinPartState of SCM+FSA, n being Nat holds ProgramPart Relocated(P,n) is good; theorem :: SCMFSA8A:25 ::TQ58' for I,J being programmed FinPartState of SCM+FSA, a being Int-Location holds I does_not_destroy a & J does_not_destroy a implies I +* J does_not_destroy a; theorem :: SCMFSA8A:26 ::TQ58 for I,J being good programmed FinPartState of SCM+FSA holds I +* J is good; theorem :: SCMFSA8A:27 ::TG8 for I being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA, a being Int-Location holds I does_not_destroy a implies Directed(I,l) does_not_destroy a; definition let I be good programmed FinPartState of SCM+FSA; let l be Instruction-Location of SCM+FSA; cluster Directed(I,l) -> good; end; definition let I be good Macro-Instruction; cluster Directed I -> good; end; definition let I be Macro-Instruction, l be Instruction-Location of SCM+FSA; cluster Directed(I,l) -> initial; end; definition let I,J be good Macro-Instruction; cluster I ';' J -> good; end; definition let l be Instruction-Location of SCM+FSA; func Goto l -> halt-free good Macro-Instruction equals :: SCMFSA8A:def 2 ::D1 insloc 0 .--> goto l; end; definition let s be State of SCM+FSA; let P be initial FinPartState of SCM+FSA; pred P is_pseudo-closed_on s means :: SCMFSA8A:def 3 ::DQ1 ex k being Nat st IC (Computation (s +* (P +* Start-At insloc 0))).k = insloc card ProgramPart P & for n being Nat st n < k holds IC (Computation (s +* (P +* Start-At insloc 0))).n in dom P; end; definition let P be initial FinPartState of SCM+FSA; attr P is pseudo-paraclosed means :: SCMFSA8A:def 4 ::D2 for s being State of SCM+FSA holds P is_pseudo-closed_on s; end; definition cluster pseudo-paraclosed Macro-Instruction; end; definition let s be State of SCM+FSA, P be initial FinPartState of SCM+FSA such that P is_pseudo-closed_on s; func pseudo-LifeSpan(s,P) -> Nat means :: SCMFSA8A:def 5 ::DQ3 IC (Computation (s +* (P +* Start-At insloc 0))).it = insloc card ProgramPart P & for n being Nat st not IC (Computation (s +* (P +* Start-At insloc 0))).n in dom P holds it <= n; end; theorem :: SCMFSA8A:28 ::TQ51 for I,J being Macro-Instruction, x being set holds x in dom I implies (I ';' J).x = (Directed I).x; theorem :: SCMFSA8A:29 ::T31(@BBB8) for l being Instruction-Location of SCM+FSA holds card Goto l = 1; theorem :: SCMFSA8A:30 ::T39 for P being programmed FinPartState of SCM+FSA, x being set st x in dom P holds (P.x = halt SCM+FSA implies (Directed P).x = goto insloc card P) & (P.x <> halt SCM+FSA implies (Directed P).x = P.x); theorem :: SCMFSA8A:31 ::TQ3 for s being State of SCM+FSA, P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds for n being Nat st n < pseudo-LifeSpan(s,P) holds IC ((Computation (s +* (P +* Start-At insloc 0))).n) in dom P & CurInstr ((Computation (s +* (P +* Start-At insloc 0))).n) <> halt SCM+FSA; theorem :: SCMFSA8A:32 ::BBBB'54' for s being State of SCM+FSA, I,J being Macro-Instruction st I is_pseudo-closed_on s for k being Nat st k <= pseudo-LifeSpan(s,I) 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 :: SCMFSA8A:33 ::TT4 for I being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA holds card Directed(I,l) = card I; theorem :: SCMFSA8A:34 ::TQ1 for I being Macro-Instruction holds card Directed I = card I; theorem :: SCMFSA8A:35 ::TQ21' for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds for k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) holds ((Computation (s +* (I +* Start-At insloc 0))).k, (Computation (s +* (Directed I +* Start-At insloc 0))).k equal_outside the Instruction-Locations of SCM+FSA & CurInstr (Computation (s +* (Directed I +* Start-At insloc 0))).k <> halt SCM+FSA); theorem :: SCMFSA8A:36 ::TQ4''(Lemma0)'' for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds IC (Computation (s +* (Directed I +* Start-At insloc 0))). (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) = insloc card I & (Computation (s +* (I +* Start-At insloc 0))). (LifeSpan (s +* (I +* Start-At insloc 0))) | (Int-Locations \/ FinSeq-Locations) = (Computation (s +* (Directed I +* Start-At insloc 0))). (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8A:37 ::TQ18 for s being State of SCM+FSA, I being Macro-Instruction holds I is_closed_on s & I is_halting_on s implies Directed I is_pseudo-closed_on s; theorem :: SCMFSA8A:38 ::TQ18' for s being State of SCM+FSA, I being Macro-Instruction holds I is_closed_on s & I is_halting_on s implies pseudo-LifeSpan(s,Directed I) = LifeSpan (s +* (I +* Start-At insloc 0)) + 1; theorem :: SCMFSA8A:39 ::T35' for I being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA holds I is halt-free implies Directed(I,l) = I; theorem :: SCMFSA8A:40 ::T35 for I being Macro-Instruction holds I is halt-free implies Directed I = I; theorem :: SCMFSA8A:41 ::TT8' for I,J being Macro-Instruction holds Directed I ';' J = I ';' J; theorem :: SCMFSA8A:42 ::TR1' for s being State of SCM+FSA, I,J being Macro-Instruction st I is_closed_on s & I is_halting_on s holds (for k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) holds IC (Computation (s +* (Directed I +* Start-At insloc 0))).k = IC (Computation (s +* ((I ';' J) +* Start-At insloc 0))).k & CurInstr (Computation (s +* (Directed I +* Start-At insloc 0))).k = CurInstr (Computation (s +* ((I ';' J) +* Start-At insloc 0))).k) & (Computation (s +* (Directed I +* Start-At insloc 0))). (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) | (Int-Locations \/ FinSeq-Locations) = (Computation (s +* ((I ';' J) +* Start-At insloc 0))). (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) | (Int-Locations \/ FinSeq-Locations) & IC (Computation (s +* (Directed I +* Start-At insloc 0))). (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) = IC (Computation (s +* ((I ';' J) +* Start-At insloc 0))). (LifeSpan (s +* (I +* Start-At insloc 0)) + 1); theorem :: SCMFSA8A:43 ::TR1 for s being State of SCM+FSA, I,J being Macro-Instruction st I is_closed_on Initialize s & I is_halting_on Initialize s holds (for k being Nat st k <= LifeSpan (s +* Initialized I) holds IC (Computation (s +* Initialized Directed I)).k = IC (Computation (s +* Initialized (I ';' J))).k & CurInstr (Computation (s +* Initialized Directed I)).k = CurInstr (Computation (s +* Initialized (I ';' J))).k) & (Computation (s +* Initialized Directed I)). (LifeSpan (s +* Initialized I) + 1) | (Int-Locations \/ FinSeq-Locations) = (Computation (s +* Initialized (I ';' J))). (LifeSpan (s +* Initialized I) + 1) | (Int-Locations \/ FinSeq-Locations) & IC (Computation (s +* Initialized Directed I)). (LifeSpan (s +* Initialized I) + 1) = IC (Computation (s +* Initialized (I ';' J))). (LifeSpan (s +* Initialized I) + 1); theorem :: SCMFSA8A:44 ::TQ21 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on Initialize s & I is_halting_on Initialize s holds for k being Nat st k <= LifeSpan (s +* Initialized I) holds ((Computation (s +* Initialized I)).k, (Computation (s +* Initialized Directed I)).k equal_outside the Instruction-Locations of SCM+FSA & CurInstr (Computation (s +* Initialized Directed I)).k <> halt SCM+FSA); theorem :: SCMFSA8A:45 ::TQ4'(Lemma0)' for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on Initialize s & I is_halting_on Initialize s holds IC (Computation (s +* Initialized Directed I)). (LifeSpan (s +* Initialized I) + 1) = insloc card I & (Computation (s +* Initialized I)).(LifeSpan (s +* Initialized I)) | (Int-Locations \/ FinSeq-Locations) = (Computation (s +* Initialized Directed I)). (LifeSpan (s +* Initialized I) + 1) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8A:46 ::TI9' <> _T22'' for I being Macro-Instruction, s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds I ';' SCM+FSA-Stop is_closed_on s & I ';' SCM+FSA-Stop is_halting_on s; theorem :: SCMFSA8A:47 ::TB61'(TB61'@BBB8) for l being Instruction-Location of SCM+FSA holds insloc 0 in dom Goto l & (Goto l).insloc 0 = goto l; theorem :: SCMFSA8A:48 ::T70 for N being with_non-empty_elements set, S being definite (non empty non void AMI-Struct over N), I being programmed FinPartState of S, x being set holds x in dom I implies I.x is Instruction of S; theorem :: SCMFSA8A:49 ::T71 for I being programmed FinPartState of SCM+FSA, x being set, k being Nat holds x in dom ProgramPart Relocated(I,k) implies (ProgramPart Relocated(I,k)).x = Relocated(I,k).x; theorem :: SCMFSA8A:50 ::T12 for I being programmed FinPartState of SCM+FSA, k being Nat holds ProgramPart Relocated(Directed I,k) = Directed(ProgramPart Relocated(I,k),insloc (card I + k)); theorem :: SCMFSA8A:51 ::T37 for I,J being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA holds Directed(I +* J,l) = Directed(I,l) +* Directed(J,l); theorem :: SCMFSA8A:52 ::TQ52 for I,J being Macro-Instruction holds Directed (I ';' J) = I ';' Directed J; theorem :: SCMFSA8A:53 for I being Macro-Instruction, s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds IC (Computation (s +* Initialized (I ';' SCM+FSA-Stop))). (LifeSpan (s +* Initialized I) + 1) = insloc card I; theorem :: SCMFSA8A:54 for I being Macro-Instruction, s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds (Computation (s +* Initialized I)).(LifeSpan (s +* Initialized I)) | (Int-Locations \/ FinSeq-Locations) = (Computation (s +* Initialized (I ';' SCM+FSA-Stop))). (LifeSpan (s +* Initialized I) + 1) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8A:55 ::TI9 <> _T22' for I being Macro-Instruction, s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds s +* Initialized (I ';' SCM+FSA-Stop) is halting; theorem :: SCMFSA8A:56 for I being Macro-Instruction, s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds LifeSpan (s +* Initialized (I ';' SCM+FSA-Stop)) = LifeSpan (s +* Initialized I) + 1; theorem :: SCMFSA8A:57 ::TA24'(@BBB8) for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on Initialize s & I is_halting_on Initialize s holds IExec(I ';' SCM+FSA-Stop,s) = IExec(I,s) +* Start-At insloc card I; theorem :: SCMFSA8A:58 ::TI10 <> T62''(@BBB8) for I,J being Macro-Instruction,s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop is_closed_on s & I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop is_halting_on s; theorem :: SCMFSA8A:59 for I,J being Macro-Instruction, s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds s +* (I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop +* Start-At insloc 0) is halting; theorem :: SCMFSA8A:60 for I,J being Macro-Instruction, s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds s +* Initialized (I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop) is halting; theorem :: SCMFSA8A:61 ::T63'(@BBB8) for I,J being Macro-Instruction, s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds IC IExec(I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop,s) = insloc (card I + card J + 1); theorem :: SCMFSA8A:62 ::T64'(@BBB8) for I,J being Macro-Instruction, s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds IExec(I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop,s) = IExec(I,s) +* Start-At insloc (card I + card J + 1);

Back to top