Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### The \tt loop and \tt Times Macroinstruction for \SCMFSA

**by****Noriko Asamoto**- Received October 29, 1997
- MML identifier: SCMFSA8C

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_1, SCMFSA_2, BOOLE, SCMFSA8A, SCMFSA6A, CAT_1, FUNCT_4, AMI_3, FUNCT_1, RELAT_1, CARD_1, AMI_5, UNIALG_2, SCMFSA7B, SCM_1, FUNCT_7, RELOC, ARYTM_1, SCMFSA6C, SCMFSA6B, SF_MASTR, SCMFSA_4, FUNCOP_1, SCMFSA8B, AMI_2, SCMFSA8C, CARD_3; notation TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_0, XREAL_0, NAT_1, CQC_LANG, RELAT_1, FUNCT_1, FUNCT_4, FUNCT_7, CARD_1, STRUCT_0, AMI_1, AMI_3, AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCM_1, SF_MASTR, SCMFSA6A, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, BINARITH; constructors ENUMSET1, AMI_5, SCM_1, SCMFSA_5, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA8B, BINARITH, MEMBERED; clusters FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, INT_1, CQC_LANG, NAT_1, FRAENKEL, XREAL_0, MEMBERED; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve m for Nat; definition cluster pseudo-paraclosed Macro-Instruction; end; canceled; theorem :: SCMFSA8C:2 ::T4425 ** n.t for s being State of SCM+FSA,P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s for k being Nat st (for n being Nat st n <= k holds IC (Computation (s +* (P +* Start-At insloc 0))).n in dom P) holds k < pseudo-LifeSpan(s,P); canceled 3; theorem :: SCMFSA8C:6 ::T210837 for f be Function, x be set st x in dom f holds f +* (x .--> f.x) = f; theorem :: SCMFSA8C:7 ::TMP12 for l being Instruction-Location of SCM+FSA holds l + 0 = l; theorem :: SCMFSA8C:8 ::TMP19 for i being Instruction of SCM+FSA holds IncAddr(i,0) = i; theorem :: SCMFSA8C:9 ::TMP13 for P being programmed FinPartState of SCM+FSA holds ProgramPart Relocated(P,0) = P; theorem :: SCMFSA8C:10 ::TMP15' for P,Q being FinPartState of SCM+FSA st P c= Q holds ProgramPart P c= ProgramPart Q; theorem :: SCMFSA8C:11 ::TMP18 for P,Q being programmed FinPartState of SCM+FSA, k being Nat st P c= Q holds Shift(P,k) c= Shift(Q,k); theorem :: SCMFSA8C:12 ::TMP15 for P,Q being FinPartState of SCM+FSA, k being Nat st P c= Q holds ProgramPart Relocated(P,k) c= ProgramPart Relocated(Q,k); theorem :: SCMFSA8C:13 ::TMP16 for I,J being Macro-Instruction, k being Nat st card I <= k & k < card I + card J holds for i being Instruction of SCM+FSA st i = J.insloc (k -' card I) holds (I ';' J).insloc k = IncAddr(i,card I); theorem :: SCMFSA8C:14 ::T22246 ---??? for s being State of SCM+FSA st s.intloc 0 = 1 & IC s = insloc 0 holds Initialize s = s; theorem :: SCMFSA8C:15 ::T200922 for s being State of SCM+FSA holds Initialize Initialize s = Initialize s; theorem :: SCMFSA8C:16 ::TMP6 for s being State of SCM+FSA, I being Macro-Instruction holds s +* (Initialized I +* Start-At insloc 0) = Initialize s +* (I +* Start-At insloc 0); theorem :: SCMFSA8C:17 ::T200938 for s being State of SCM+FSA, I being Macro-Instruction holds IExec(I,s) = IExec(I,Initialize s); theorem :: SCMFSA8C:18 ::T26401 --- ??? for s being State of SCM+FSA, I being Macro-Instruction st s.intloc 0 = 1 holds s +* (I +* Start-At insloc 0) = s +* Initialized I; theorem :: SCMFSA8C:19 ::T24634 --- ??? for I being Macro-Instruction holds I +* Start-At insloc 0 c= Initialized I; theorem :: SCMFSA8C:20 ::TMP10 for l being Instruction-Location of SCM+FSA, I being Macro-Instruction holds l in dom I iff l in dom Initialized I; theorem :: SCMFSA8C:21 for s being State of SCM+FSA, I being Macro-Instruction holds Initialized I is_closed_on s iff I is_closed_on Initialize s; theorem :: SCMFSA8C:22 ::TMP5 for s being State of SCM+FSA, I being Macro-Instruction holds Initialized I is_halting_on s iff I is_halting_on Initialize s; theorem :: SCMFSA8C:23 for I being Macro-Instruction holds (for s being State of SCM+FSA holds I is_halting_on Initialize s) implies Initialized I is halting; theorem :: SCMFSA8C:24 ::TMP3' for I being Macro-Instruction holds (for s being State of SCM+FSA holds Initialized I is_halting_on s) implies Initialized I is halting; theorem :: SCMFSA8C:25 ::TMP9 for I being Macro-Instruction holds ProgramPart Initialized I = I; theorem :: SCMFSA8C:26 ::T18750 for s being State of SCM+FSA, I being Macro-Instruction, l being Instruction-Location of SCM+FSA, x being set holds x in dom I implies I.x = (s +* (I +* Start-At l)).x; theorem :: SCMFSA8C:27 ::T22246' ---??? for s being State of SCM+FSA st s.intloc 0 = 1 holds (Initialize s) | (Int-Locations \/ FinSeq-Locations) = s | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:28 ::T210615 for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location, l being Instruction-Location of SCM+FSA holds (s +* (I +* Start-At l)).a = s.a; theorem :: SCMFSA8C:29 for I being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA holds IC SCM+FSA in dom (I +* Start-At l); theorem :: SCMFSA8C:30 for I being programmed FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA holds (I +* Start-At l).IC SCM+FSA = l; theorem :: SCMFSA8C:31 ::T4633 -- ?? for s being State of SCM+FSA, P being FinPartState of SCM+FSA, l being Instruction-Location of SCM+FSA holds IC (s +* (P +* Start-At l)) = l; theorem :: SCMFSA8C:32 ::T30408 for s being State of SCM+FSA, i being Instruction of SCM+FSA st InsCode i in {0,6,7,8} holds Exec(i,s) | (Int-Locations \/ FinSeq-Locations) = s | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:33 ::T271245 --- ??? for s1,s2 being State of SCM+FSA st s1.intloc 0 = s2.intloc 0 & ((for a being read-write Int-Location holds s1.a = s2.a) & for f being FinSeq-Location holds s1.f = s2.f) holds s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:34 for s being State of SCM+FSA,P being programmed FinPartState of SCM+FSA holds (s +* P) | (Int-Locations \/ FinSeq-Locations) = s | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:35 ::T1643 --- ?? for s,ss being State of SCM+FSA holds (s +* ss | the Instruction-Locations of SCM+FSA) | (Int-Locations \/ FinSeq-Locations) = s | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:36 ::T27643 --- ??? for s being State of SCM+FSA holds (Initialize s) | the Instruction-Locations of SCM+FSA = s | the Instruction-Locations of SCM+FSA; theorem :: SCMFSA8C:37 ::T26530 --- ??? for s,ss being State of SCM+FSA, I being Macro-Instruction holds (ss +* (s | (the Instruction-Locations of SCM+FSA))) | (Int-Locations \/ FinSeq-Locations) = ss | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:38 ::T27500 ue for s being State of SCM+FSA holds IExec(SCM+FSA-Stop,s) = Initialize s +* Start-At insloc 0; theorem :: SCMFSA8C:39 ::T9x for s being State of SCM+FSA,I being Macro-Instruction st I is_closed_on s holds insloc 0 in dom I; theorem :: SCMFSA8C:40 for s being State of SCM+FSA,I being paraclosed Macro-Instruction holds insloc 0 in dom I; theorem :: SCMFSA8C:41 ::Tm1(@BBB8) for i being Instruction of SCM+FSA holds rng Macro i = {i,halt SCM+FSA}; theorem :: SCMFSA8C:42 ::T0x for s1,s2 being State of SCM+FSA,I being Macro-Instruction st I is_closed_on s1 & I +* Start-At insloc 0 c= s1 for n being Nat st ProgramPart Relocated(I,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 :: SCMFSA8C:43 ::T24441 for s1,s2 being State of SCM+FSA,I being Macro-Instruction st I is_closed_on s1 & I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 & s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations) for i being Nat holds IC (Computation s1).i = IC (Computation s2).i & CurInstr (Computation s1).i = CurInstr (Computation s2).i & (Computation s1).i | (Int-Locations \/ FinSeq-Locations) = (Computation s2).i | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:44 ::T24441' for s1,s2 being State of SCM+FSA,I being Macro-Instruction st I is_closed_on s1 & I is_halting_on s1 & I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 & s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations) holds LifeSpan s1 = LifeSpan s2; theorem :: SCMFSA8C:45 ::T27835 for s1,s2 being State of SCM+FSA,I being Macro-Instruction st s1.intloc 0 = 1 & I is_closed_on s1 & I is_halting_on s1 & ((for a being read-write Int-Location holds s1.a = s2.a) & for f being FinSeq-Location holds s1.f = s2.f) holds IExec(I,s1) | (Int-Locations \/ FinSeq-Locations) = IExec(I,s2) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:46 ::T27835' for s1,s2 being State of SCM+FSA,I being Macro-Instruction st s1.intloc 0 = 1 & I is_closed_on s1 & I is_halting_on s1 & s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations) holds IExec(I,s1) | (Int-Locations \/ FinSeq-Locations) = IExec(I,s2) | (Int-Locations \/ FinSeq-Locations); definition let I be Macro-Instruction; cluster Initialized I -> initial; end; theorem :: SCMFSA8C:47 ::TMP8 for s being State of SCM+FSA, I being Macro-Instruction holds Initialized I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s; theorem :: SCMFSA8C:48 for s being State of SCM+FSA, I being Macro-Instruction st I is_pseudo-closed_on Initialize s holds pseudo-LifeSpan(s,Initialized I) = pseudo-LifeSpan(Initialize s,I); theorem :: SCMFSA8C:49 for s being State of SCM+FSA, I being Macro-Instruction st Initialized I is_pseudo-closed_on s holds pseudo-LifeSpan(s,Initialized I) = pseudo-LifeSpan(Initialize s,I); theorem :: SCMFSA8C:50 ::TMP14 for s being State of SCM+FSA, I being initial FinPartState of SCM+FSA st I is_pseudo-closed_on s holds I is_pseudo-closed_on s +* (I +* Start-At insloc 0) & pseudo-LifeSpan(s,I) = pseudo-LifeSpan(s +* (I +* Start-At insloc 0),I); theorem :: SCMFSA8C:51 ::P'115' for s1,s2 being State of SCM+FSA, I being Macro-Instruction st I +* Start-At insloc 0 c= s1 & I is_pseudo-closed_on s1 for n being Nat st ProgramPart Relocated(I,n) c= s2 & IC s2 = insloc n & s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations) holds ((for i being Nat st i < pseudo-LifeSpan(s1,I) holds IncAddr(CurInstr (Computation s1).i,n) = CurInstr (Computation s2).i) & for i being Nat st i <= pseudo-LifeSpan(s1,I) holds IC (Computation s1).i + n = IC (Computation s2).i & (Computation s1).i | (Int-Locations \/ FinSeq-Locations) = (Computation s2).i | (Int-Locations \/ FinSeq-Locations)); theorem :: SCMFSA8C:52 ::TMP11 for s1,s2 being State of SCM+FSA, I being Macro-Instruction st s1 | (Int-Locations \/ FinSeq-Locations) = s2 | (Int-Locations \/ FinSeq-Locations) holds I is_pseudo-closed_on s1 implies I is_pseudo-closed_on s2; theorem :: SCMFSA8C:53 ::T1702 for s being State of SCM+FSA, I being Macro-Instruction st s.intloc 0 = 1 holds I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s; theorem :: SCMFSA8C:54 ::TD2' ** n.t for a being Int-Location, I,J being Macro-Instruction holds insloc 0 in dom if=0(a,I,J) & insloc 1 in dom if=0(a,I,J) & insloc 0 in dom if>0(a,I,J) & insloc 1 in dom if>0(a,I,J); theorem :: SCMFSA8C:55 ::TD2 ** n.t for a being Int-Location, I,J being Macro-Instruction holds if=0(a,I,J).insloc 0 = a =0_goto insloc (card J + 3) & if=0(a,I,J).insloc 1 = goto insloc 2 & if>0(a,I,J).insloc 0 = a >0_goto insloc (card J + 3) & if>0(a,I,J).insloc 1 = goto insloc 2; theorem :: SCMFSA8C:56 ::T6327 ** n.t for a being Int-Location, I,J being Macro-Instruction, n being Nat st n < card I + card J + 3 holds insloc n in dom if=0(a,I,J) & if=0(a,I,J).insloc n <> halt SCM+FSA; theorem :: SCMFSA8C:57 ::T6327' ** n.t for a being Int-Location, I,J being Macro-Instruction, n being Nat st n < card I + card J + 3 holds insloc n in dom if>0(a,I,J) & if>0(a,I,J).insloc n <> halt SCM+FSA; theorem :: SCMFSA8C:58 ::T29502 for s being State of SCM+FSA, I being Macro-Instruction st Directed I is_pseudo-closed_on s holds I ';' SCM+FSA-Stop is_closed_on s & I ';' SCM+FSA-Stop is_halting_on s & LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) = pseudo-LifeSpan(s,Directed I) & (for n being Nat st n < pseudo-LifeSpan(s,Directed I) holds IC (Computation (s +* (I +* Start-At insloc 0))).n = IC (Computation (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))).n) & for n being Nat st n <= pseudo-LifeSpan(s,Directed I) holds (Computation (s +* (I +* Start-At insloc 0))).n | D = (Computation (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))).n | D; theorem :: SCMFSA8C:59 ::T29502' for s being State of SCM+FSA, I being Macro-Instruction st Directed I is_pseudo-closed_on s holds (Result (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))) | D = (Computation (s +* (I +* Start-At insloc 0))). pseudo-LifeSpan(s,Directed I) | D; theorem :: SCMFSA8C:60 for s being State of SCM+FSA, I being Macro-Instruction st s.intloc 0 = 1 & Directed I is_pseudo-closed_on s holds IExec(I ';' SCM+FSA-Stop,s) | D = (Computation (s +* (I +* Start-At insloc 0))). pseudo-LifeSpan(s,Directed I) | D; theorem :: SCMFSA8C:61 ::TMP20 ** n.t for I,J being Macro-Instruction,a being Int-Location holds if=0(a,I,J).insloc (card I + card J + 3) = halt SCM+FSA; theorem :: SCMFSA8C:62 ::TMP20' ** n.t for I,J being Macro-Instruction,a being Int-Location holds if>0(a,I,J).insloc (card I + card J + 3) = halt SCM+FSA; theorem :: SCMFSA8C:63 ::TMP21 ** n.t for I,J being Macro-Instruction,a being Int-Location holds if=0(a,I,J).insloc (card J + 2) = goto insloc (card I + card J + 3); theorem :: SCMFSA8C:64 ::TMP21' ** n.t for I,J being Macro-Instruction,a being Int-Location holds if>0(a,I,J).insloc (card J + 2) = goto insloc (card I + card J + 3); theorem :: SCMFSA8C:65 ::T31139 ** n.t for J being Macro-Instruction,a being Int-Location holds if=0(a,Goto insloc 2,J).insloc (card J + 3) = goto insloc (card J + 5); theorem :: SCMFSA8C:66 ::TMP71 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a = 0 & Directed I is_pseudo-closed_on s holds if=0(a,I,J) is_halting_on s & if=0(a,I,J) is_closed_on s & LifeSpan (s +* (if=0(a,I,J) +* Start-At insloc 0)) = LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) + 1; theorem :: SCMFSA8C:67 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.intloc 0 = 1 & s.a = 0 & Directed I is_pseudo-closed_on s holds IExec(if=0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) = IExec(I ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:68 ::TMP71' for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a > 0 & Directed I is_pseudo-closed_on s holds if>0(a,I,J) is_halting_on s & if>0(a,I,J) is_closed_on s & LifeSpan (s +* (if>0(a,I,J) +* Start-At insloc 0)) = LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) + 1; theorem :: SCMFSA8C:69 ::TMP7' for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.intloc 0 = 1 & s.a > 0 & Directed I is_pseudo-closed_on s holds IExec(if>0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) = IExec(I ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:70 ::TMP171 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a <> 0 & Directed J is_pseudo-closed_on s holds if=0(a,I,J) is_halting_on s & if=0(a,I,J) is_closed_on s & LifeSpan (s +* (if=0(a,I,J) +* Start-At insloc 0)) = LifeSpan (s +* (J ';' SCM+FSA-Stop +* Start-At insloc 0)) + 3; theorem :: SCMFSA8C:71 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.intloc 0 = 1 & s.a <> 0 & Directed J is_pseudo-closed_on s holds IExec(if=0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) = IExec(J ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:72 ::TMP171' for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a <= 0 & Directed J is_pseudo-closed_on s holds if>0(a,I,J) is_halting_on s & if>0(a,I,J) is_closed_on s & LifeSpan (s +* (if>0(a,I,J) +* Start-At insloc 0)) = LifeSpan (s +* (J ';' SCM+FSA-Stop +* Start-At insloc 0)) + 3; theorem :: SCMFSA8C:73 ::TMP17' for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.intloc 0 = 1 & s.a <= 0 & Directed J is_pseudo-closed_on s holds IExec(if>0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) = IExec(J ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:74 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st Directed I is_pseudo-closed_on s & Directed J is_pseudo-closed_on s holds if=0(a,I,J) is_closed_on s & if=0(a,I,J) is_halting_on s; theorem :: SCMFSA8C:75 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st Directed I is_pseudo-closed_on s & Directed J is_pseudo-closed_on s holds if>0(a,I,J) is_closed_on s & if>0(a,I,J) is_halting_on s; theorem :: SCMFSA8C:76 ::TG8' for I being Macro-Instruction, a being Int-Location holds I does_not_destroy a implies Directed I does_not_destroy a; theorem :: SCMFSA8C:77 ::Td1(@BBB8) for i being Instruction of SCM+FSA, a being Int-Location holds i does_not_destroy a implies Macro i does_not_destroy a; theorem :: SCMFSA8C:78 ::R0' for a being Int-Location holds halt SCM+FSA does_not_refer a; theorem :: SCMFSA8C:79 for a,b,c being Int-Location holds a <> b implies AddTo(c,b) does_not_refer a; theorem :: SCMFSA8C:80 for i being Instruction of SCM+FSA, a being Int-Location holds i does_not_refer a implies Macro i does_not_refer a; theorem :: SCMFSA8C:81 ::TG9' for I,J being Macro-Instruction, a being Int-Location holds I does_not_destroy a & J does_not_destroy a implies I ';' J does_not_destroy a; theorem :: SCMFSA8C:82 ::T281220 for J being Macro-Instruction, i being Instruction of SCM+FSA, a being Int-Location st i does_not_destroy a & J does_not_destroy a holds i ';' J does_not_destroy a; theorem :: SCMFSA8C:83 for I being Macro-Instruction, j being Instruction of SCM+FSA, a being Int-Location st I does_not_destroy a & j does_not_destroy a holds I ';' j does_not_destroy a; theorem :: SCMFSA8C:84 for i,j being Instruction of SCM+FSA, a being Int-Location st i does_not_destroy a & j does_not_destroy a holds i ';' j does_not_destroy a; theorem :: SCMFSA8C:85 ::TQ7' for a being Int-Location holds SCM+FSA-Stop does_not_destroy a; theorem :: SCMFSA8C:86 ::T27749 for a being Int-Location, l being Instruction-Location of SCM+FSA holds Goto l does_not_destroy a; theorem :: SCMFSA8C:87 ::T200724' for s being State of SCM+FSA, I being Macro-Instruction st I is_halting_on Initialize s holds (for a being read-write Int-Location holds IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))). (LifeSpan (Initialize s +* (I +* Start-At insloc 0))).a) & for f being FinSeq-Location holds IExec(I,s).f = (Computation (Initialize s +* (I +* Start-At insloc 0))). (LifeSpan (Initialize s +* (I +* Start-At insloc 0))).f; theorem :: SCMFSA8C:88 ::T200724 for s being State of SCM+FSA, I being parahalting Macro-Instruction, a being read-write Int-Location holds IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))). (LifeSpan (Initialize s +* (I +* Start-At insloc 0))).a; theorem :: SCMFSA8C:89 ::TMP29' for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location,k being Nat st I is_closed_on Initialize s & I is_halting_on Initialize s & I does_not_destroy a holds IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).k.a; theorem :: SCMFSA8C:90 ::TMP29 for s being State of SCM+FSA, I being parahalting Macro-Instruction, a being Int-Location,k being Nat st I does_not_destroy a holds IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).k.a; theorem :: SCMFSA8C:91 ::TMP29'' for s being State of SCM+FSA, I being parahalting Macro-Instruction, a being Int-Location st I does_not_destroy a holds IExec(I,s).a = (Initialize s).a; theorem :: SCMFSA8C:92 ::T200724'' for s being State of SCM+FSA, I being keeping_0 Macro-Instruction st I is_halting_on Initialize s holds IExec(I,s).intloc 0 = 1 & for k being Nat holds (Computation (Initialize s +* (I +* Start-At insloc 0))).k.intloc 0 = 1; theorem :: SCMFSA8C:93 ::TQ9 for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location st I does_not_destroy a holds for k being Nat st IC (Computation (s +* (I +* Start-At insloc 0))).k in dom I holds (Computation (s +* (I +* Start-At insloc 0))).(k + 1).a = (Computation (s +* (I +* Start-At insloc 0))).k.a; theorem :: SCMFSA8C:94 ::TQ9' for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location st I does_not_destroy a holds for m being Nat st (for n being Nat st n < m holds IC (Computation (s +* (I +* Start-At insloc 0))).n in dom I) holds for n being Nat st n <= m holds (Computation (s +* (I +* Start-At insloc 0))).n.a = s.a; theorem :: SCMFSA8C:95 ::T210921 for s being State of SCM+FSA, I being good Macro-Instruction for m being Nat st (for n being Nat st n < m holds IC (Computation (s +* (I +* Start-At insloc 0))).n in dom I) holds for n being Nat st n <= m holds (Computation (s +* (I +* Start-At insloc 0))).n.intloc 0 = s.intloc 0; theorem :: SCMFSA8C:96 ::T22842 for s being State of SCM+FSA, I being good Macro-Instruction st I is_halting_on Initialize s & I is_closed_on Initialize s holds IExec(I,s).intloc 0 = 1 & for k being Nat holds (Computation (Initialize s +* (I +* Start-At insloc 0))).k.intloc 0 = 1; theorem :: SCMFSA8C:97 for s being State of SCM+FSA, I being good Macro-Instruction st I is_closed_on s holds for k being Nat holds (Computation (s +* (I +* Start-At insloc 0))).k.intloc 0 = s.intloc 0; theorem :: SCMFSA8C:98 ::TMP27 for s being State of SCM+FSA, I being keeping_0 parahalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a holds (Computation (Initialize s +* (I ';' SubFrom(a,intloc 0) +* Start-At insloc 0))).(LifeSpan (Initialize s +* (I ';' SubFrom(a,intloc 0) +* Start-At insloc 0))).a = s.a - 1; theorem :: SCMFSA8C:99 ::T211205 for i being Instruction of SCM+FSA st i does_not_destroy intloc 0 holds Macro i is good; theorem :: SCMFSA8C:100 ::T13' 6B for s1,s2 being State of SCM+FSA,I being Macro-Instruction st I is_closed_on s1 & I is_halting_on s1 & s1 | D = s2 | D holds for k being Nat holds (Computation (s1 +* (I +* Start-At insloc 0))).k, (Computation (s2 +* (I +* Start-At insloc 0))).k equal_outside the Instruction-Locations of SCM+FSA & CurInstr (Computation (s1 +* (I +* Start-At insloc 0))).k = CurInstr (Computation (s2 +* (I +* Start-At insloc 0))).k; theorem :: SCMFSA8C:101 ::T14' 6B for s1,s2 being State of SCM+FSA,I being Macro-Instruction st I is_closed_on s1 & I is_halting_on s1 & s1 | D = s2 | D holds LifeSpan (s1 +* (I +* Start-At insloc 0)) = LifeSpan (s2 +* (I +* Start-At insloc 0)) & Result (s1 +* (I +* Start-At insloc 0)), Result (s2 +* (I +* Start-At insloc 0)) equal_outside the Instruction-Locations of SCM+FSA; canceled; theorem :: SCMFSA8C:103 ::T3829 for s1,s2 being State of SCM+FSA,I being Macro-Instruction st I is_closed_on s1 & I is_halting_on s1 & I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 & ex k being Nat st (Computation s1).k,s2 equal_outside the Instruction-Locations of SCM+FSA holds Result s1,Result s2 equal_outside the Instruction-Locations of SCM+FSA; begin :: loop definition let I be Macro-Instruction, k be Nat; cluster IncAddr(I,k) -> initial programmed; end; definition let I be Macro-Instruction; canceled 3; func loop I -> halt-free Macro-Instruction equals :: SCMFSA8C:def 4 ::D17 ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc 0)) * I; end; theorem :: SCMFSA8C:104 ::T1 for I being Macro-Instruction holds loop I = Directed(I,insloc 0); theorem :: SCMFSA8C:105 for I being Macro-Instruction, a being Int-Location holds I does_not_destroy a implies loop I does_not_destroy a; definition let I be good Macro-Instruction; cluster loop I -> good; end; theorem :: SCMFSA8C:106 ::SCMFSA6A'14 for I being Macro-Instruction holds dom loop I = dom I; theorem :: SCMFSA8C:107 ::SCMFSA6A'18 for I being Macro-Instruction holds not halt SCM+FSA in rng loop I; theorem :: SCMFSA8C:108 ::SCMFSA6A'54 for I being Macro-Instruction, x being set holds I.x <> halt SCM+FSA implies (loop I).x = I.x; theorem :: SCMFSA8C:109 ::TMP24 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on s & I is_halting_on s for m being Nat st m <= LifeSpan (s +* (I +* Start-At insloc 0)) holds (Computation (s +* (I +* Start-At insloc 0))).m, (Computation(s +* (loop I +* Start-At insloc 0))).m equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA8C:110 ::TMP25 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on s & I is_halting_on s for m being Nat st m < LifeSpan (s +* (I +* Start-At insloc 0)) holds CurInstr (Computation (s +* (I +* Start-At insloc 0))).m = CurInstr (Computation(s +* (loop I +* Start-At insloc 0))).m; theorem :: SCMFSA8C:111 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on s & I is_halting_on s for m being Nat st m <= LifeSpan (s +* (I +* Start-At insloc 0)) holds CurInstr (Computation (s +* (loop I +* Start-At insloc 0))).m <> halt SCM+FSA ; theorem :: SCMFSA8C:112 ::TMP26 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds CurInstr (Computation (s +* (loop I +* Start-At insloc 0))). LifeSpan (s +* (I +* Start-At insloc 0)) = goto insloc 0; theorem :: SCMFSA8C:113 ::MAI1 for s being State of SCM+FSA, I being paraclosed Macro-Instruction st I +* Start-At insloc 0 c= s & s is halting for m being Nat st m <= LifeSpan s holds (Computation s).m,(Computation (s +* loop I)).m equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCMFSA8C:114 for s being State of SCM+FSA, I being parahalting Macro-Instruction st Initialized I c= s holds for k being Nat st k <= LifeSpan s holds CurInstr (Computation (s +* loop I)).k <> halt SCM+FSA; begin :: Times definition let a be Int-Location; let I be Macro-Instruction; func Times(a,I) -> Macro-Instruction equals :: SCMFSA8C:def 5 ::D13 if>0(a,loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)), SCM+FSA-Stop); end; theorem :: SCMFSA8C:115 ::T211147 *** n.t for I being good Macro-Instruction, a being read-write Int-Location holds if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)) is good; theorem :: SCMFSA8C:116 ::T21921 ** n.t for I,J being Macro-Instruction,a being Int-Location holds if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)). insloc (card (I ';' SubFrom(a,intloc 0)) + 3) = goto insloc (card (I ';' SubFrom(a,intloc 0)) + 5); theorem :: SCMFSA8C:117 ::TMP22 for s being State of SCM+FSA, I being good parahalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a & s.intloc 0 = 1 & s.a > 0 holds loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)) is_pseudo-closed_on s; theorem :: SCMFSA8C:118 for s being State of SCM+FSA, I being good parahalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a & s.a > 0 holds Initialized loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)) is_pseudo-closed_on s; theorem :: SCMFSA8C:119 for s being State of SCM+FSA, I being good parahalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a & s.intloc 0 = 1 holds Times(a,I) is_closed_on s & Times(a,I) is_halting_on s; theorem :: SCMFSA8C:120 for I being good parahalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a holds Initialized Times(a,I) is halting; theorem :: SCMFSA8C:121 for I,J being Macro-Instruction, a,c being Int-Location st I does_not_destroy c & J does_not_destroy c holds if=0(a,I,J) does_not_destroy c & if>0(a,I,J) does_not_destroy c; theorem :: SCMFSA8C:122 ::TMP22' for s being State of SCM+FSA, I being good parahalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a & s.intloc 0 = 1 & s.a > 0 holds ex s2 being State of SCM+FSA, k being Nat st s2 = s +* (loop if=0(a,Goto insloc 2, I ';' SubFrom(a,intloc 0)) +* Start-At insloc 0) & k = LifeSpan (s +* (if=0(a,Goto insloc 2, I ';' SubFrom(a,intloc 0)) +* Start-At insloc 0)) + 1 & (Computation s2).k.a = s.a - 1 & (Computation s2).k.intloc 0 = 1 & (for b being read-write Int-Location st b <> a holds (Computation s2).k.b = IExec(I,s).b) & (for f being FinSeq-Location holds (Computation s2).k.f = IExec(I,s).f) & IC (Computation s2).k = insloc 0 & for n being Nat st n <= k holds IC (Computation s2).n in dom loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)); theorem :: SCMFSA8C:123 ::T1 for s being State of SCM+FSA, I being good parahalting Macro-Instruction, a being read-write Int-Location st s.intloc 0 = 1 & s.a <= 0 holds IExec(Times(a,I),s) | (Int-Locations \/ FinSeq-Locations) = s | (Int-Locations \/ FinSeq-Locations); theorem :: SCMFSA8C:124 ::T2 for s being State of SCM+FSA, I being good parahalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a & s.a > 0 holds IExec(I ';' SubFrom(a,intloc 0),s).a = s.a - 1 & IExec(Times(a,I),s) | (Int-Locations \/ FinSeq-Locations) = IExec(Times(a,I),IExec(I ';' SubFrom(a,intloc 0),s)) | (Int-Locations \/ FinSeq-Locations); begin ::example theorem :: SCMFSA8C:125 for s being State of SCM+FSA, a,b,c being read-write Int-Location st a <> b & a <> c & b <> c & s.a >= 0 holds IExec(Times(a,Macro AddTo(b,c)),s).b = s.b + s.c * s.a;

Back to top