Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### Initialization Halting Concepts and Their Basic Properties of \SCMFSA

**by****Jing-Chao Chen, and****Yatsuka Nakamura**- Received June 17, 1998
- MML identifier: SCM_HALT

- [ Mizar article, MML identifier index ]

environ vocabulary SCMFSA6A, AMI_1, SCMFSA_2, FUNCT_1, RELAT_1, CAT_1, FUNCT_4, AMI_3, BOOLE, FUNCOP_1, SCMFSA6B, FUNCT_7, SF_MASTR, FINSEQ_1, INT_1, AMI_5, RELOC, SCM_1, CARD_1, SCMFSA6C, SCMFSA7B, SCMFSA_4, UNIALG_2, SCMFSA8B, ARYTM_1, SCMFSA8C, SCMFSA8A, SCM_HALT, CARD_3; notation TARSKI, XBOOLE_0, ENUMSET1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, RELAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_7, STRUCT_0, AMI_1, AMI_3, AMI_5, SCMFSA_2, CQC_LANG, CARD_1, SCM_1, SCMFSA_4, SCMFSA6B, SCMFSA_5, SCMFSA6A, SF_MASTR, SCMFSA8A, SCMFSA8B, SCMFSA8C, SCMFSA7B, BINARITH, SCMFSA_3, SCMFSA6C; constructors SCM_1, AMI_5, SCMFSA_3, SCMFSA_5, SF_MASTR, SCMFSA6A, SCMFSA6B, SCMFSA6C, SETWISEO, SCMFSA8A, SCMFSA8B, SCMFSA8C, BINARITH; clusters FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, INT_1, SCMFSA6A, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8C, SCMFSA6B, SCMFSA_9, CQC_LANG, NAT_1, FRAENKEL, XREAL_0, XBOOLE_0, ORDINAL2, NUMBERS; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve m,n for Nat, I for Macro-Instruction, s,s1,s2 for State of SCM+FSA, a for Int-Location, f for FinSeq-Location; definition let I be Macro-Instruction; attr I is InitClosed means :: SCM_HALT:def 1 for s being State of SCM+FSA, n being Nat st Initialized I c= s holds IC (Computation s).n in dom I; attr I is InitHalting means :: SCM_HALT:def 2 Initialized I is halting; attr I is keepInt0_1 means :: SCM_HALT:def 3 ::def5 for s being State of SCM+FSA st Initialized I c= s for k being Nat holds ((Computation s).k).intloc 0 = 1; end; theorem :: SCM_HALT:1 ::TM001 for x being set,i,m,n being Nat st x in dom (((intloc i) .--> m) +* Start-At insloc n) holds x=intloc i or x=IC SCM+FSA; theorem :: SCM_HALT:2 ::TM002 for I being Macro-Instruction,i,m,n being Nat holds dom I misses dom (((intloc i) .--> m) +* Start-At insloc n); theorem :: SCM_HALT:3 ::I_iS Initialized I = I +* (((intloc 0) .--> 1) +* Start-At insloc 0); theorem :: SCM_HALT:4 Macro halt SCM+FSA is InitHalting; definition cluster InitHalting Macro-Instruction; end; theorem :: SCM_HALT:5 ::TM006=HA2,HA,SCMFSA6B:19 for I being InitHalting Macro-Instruction st Initialized I c= s holds s is halting; theorem :: SCM_HALT:6 ::TM007 I +* Start-At insloc 0 c= Initialized I; theorem :: SCM_HALT:7 ::int0_1 for I being Macro-Instruction,s being State of SCM+FSA st Initialized I c= s holds s.intloc 0 =1; definition cluster paraclosed -> InitClosed Macro-Instruction; end; definition cluster parahalting -> InitHalting Macro-Instruction; end; definition cluster InitHalting -> InitClosed Macro-Instruction; cluster keepInt0_1 -> InitClosed Macro-Instruction; cluster keeping_0 -> keepInt0_1 Macro-Instruction; end; theorem :: SCM_HALT:8 ::TM008=SCMFSA6B:22 for I being InitHalting Macro-Instruction, a being read-write Int-Location holds not a in UsedIntLoc I implies (IExec(I, s)).a = s.a; theorem :: SCM_HALT:9 ::TM010=SCMFSA6B:23 for I being InitHalting Macro-Instruction,f being FinSeq-Location holds not f in UsedInt*Loc I implies (IExec(I, s)).f = s.f; definition let I be InitHalting Macro-Instruction; cluster Initialized I -> halting; end; definition cluster InitHalting -> non empty Macro-Instruction; end; theorem :: SCM_HALT:10 ::TM012=SCMFSA6B:25 for I being InitHalting Macro-Instruction holds dom I <> {}; theorem :: SCM_HALT:11 ::TM014=SCMFSA6B:26 for I being InitHalting Macro-Instruction holds insloc 0 in dom I; theorem :: SCM_HALT:12 ::TM016=SCMFSA6B:27 ::T0 for J being InitHalting Macro-Instruction st Initialized J 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 :: SCM_HALT:13 ::TM018=MacroAt0: Initialized I c= s implies I c= s; theorem :: SCM_HALT:14 :: TM020=SCMFSA6B:28 ::T13 for I being InitHalting Macro-Instruction st Initialized I c= s1 & Initialized I 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 :: SCM_HALT:15 ::TM022=SCMFSA6B:29 ::T14 for I being InitHalting Macro-Instruction st Initialized I c= s1 & Initialized I 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 :: SCM_HALT:16 Macro halt SCM+FSA is keeping_0; definition cluster keeping_0 InitHalting Macro-Instruction; end; definition cluster keepInt0_1 InitHalting Macro-Instruction; end; theorem :: SCM_HALT:17 ::TM026=SCMFSA6B:35 for I being keepInt0_1 InitHalting Macro-Instruction holds IExec(I, s).intloc 0 = 1; theorem :: SCM_HALT:18 ::TM028=MAI1: for I being InitClosed Macro-Instruction, J being Macro-Instruction st Initialized I 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 :: SCM_HALT:19 ::TM030=IScommute: for i,m,n being Nat holds s+*I+*(((intloc i) .--> m) +* Start-At insloc n) = s+*(((intloc i) .--> m) +* Start-At insloc n)+* I; theorem :: SCM_HALT:20 ::TM031: ((intloc 0) .--> 1) +* Start-At insloc 0 c= s implies Initialized I c= s +* (I +* (((intloc 0) .--> 1) +* Start-At insloc 0)) & s +* (I +* (((intloc 0) .--> 1) +* Start-At insloc 0)) = s +* I & s +* (I +* (((intloc 0) .--> 1) +* Start-At insloc 0)) +* Directed I = s +* Directed I; theorem :: SCM_HALT:21 ::TM032=Lemma01 for I being InitClosed Macro-Instruction st s +*I is halting & Directed I c= s & ((intloc 0) .--> 1) +* Start-At insloc 0 c= s holds IC (Computation s).(LifeSpan (s +*I) + 1) = insloc card I; theorem :: SCM_HALT:22 ::TM034=Lemma02 for I being InitClosed Macro-Instruction st s +*I is halting & Directed I c= s & ((intloc 0) .--> 1) +* 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 :: SCM_HALT:23 ::TM036=Lemma0 for I being InitHalting 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 :: SCM_HALT:24 ::TM038=Keep2 for I being InitClosed Macro-Instruction st s +* Initialized I is halting for J being Macro-Instruction, k being Nat st k <= LifeSpan (s +* Initialized I ) holds (Computation (s +* Initialized I)).k, (Computation (s +* Initialized (I ';' J))).k equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCM_HALT:25 ::TM040=Th1: for I being keepInt0_1 InitHalting Macro-Instruction, J being InitHalting Macro-Instruction, s being State of SCM+FSA st Initialized (I ';' J) c= s holds IC (Computation s).(LifeSpan (s +* I) + 1) = insloc card I & (Computation s).(LifeSpan (s +* I) + 1) | (Int-Locations \/ FinSeq-Locations) = ((Computation (s +* I)).(LifeSpan (s +* I)) +* Initialized J) | (Int-Locations \/ FinSeq-Locations) & ProgramPart Relocated(J,card I) c= (Computation s).(LifeSpan (s +* I) + 1) & (Computation s).(LifeSpan (s +* I) + 1).intloc 0 = 1 & s is halting & LifeSpan s = LifeSpan (s +* I) + 1 + LifeSpan (Result (s +* I) +* Initialized J) & (J is keeping_0 implies (Result s).intloc 0 = 1); definition let I be keepInt0_1 InitHalting Macro-Instruction, J be InitHalting Macro-Instruction; cluster I ';' J -> InitHalting; end; theorem :: SCM_HALT:26 ::TM042=Keep3 for I being keepInt0_1 Macro-Instruction st s +* I is halting for J being InitClosed Macro-Instruction st Initialized (I ';' J) c= s for k being Nat holds (Computation (Result(s +*I) +* Initialized J )).k +* Start-At (IC (Computation (Result(s +*I) +* Initialized J )).k + card I), (Computation (s +* (I ';' J))).(LifeSpan (s +* I)+1+k) equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCM_HALT:27 ::Keep1 for I being keepInt0_1 Macro-Instruction st not s +* Initialized I is halting for J being Macro-Instruction, k being Nat holds (Computation (s +* Initialized I)).k, (Computation (s +* Initialized (I ';' J))).k equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCM_HALT:28 ::TM044=T22 for I being keepInt0_1 InitHalting Macro-Instruction, J being InitHalting Macro-Instruction holds LifeSpan (s +* Initialized (I ';' J)) = LifeSpan (s +* Initialized I) + 1 + LifeSpan (Result (s +* Initialized I) +* Initialized J); theorem :: SCM_HALT:29 ::TM046 for I being keepInt0_1 InitHalting Macro-Instruction, J being InitHalting Macro-Instruction holds IExec(I ';' J,s) = IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I); definition let i be parahalting Instruction of SCM+FSA; cluster Macro i -> InitHalting; end; definition let i be parahalting Instruction of SCM+FSA, J be parahalting Macro-Instruction; cluster i ';' J -> InitHalting; end; definition let i be keeping_0 parahalting Instruction of SCM+FSA, J be InitHalting Macro-Instruction; cluster i ';' J -> InitHalting; end; definition let I, J be keepInt0_1 Macro-Instruction; cluster I ';' J -> keepInt0_1; end; definition let j be keeping_0 parahalting Instruction of SCM+FSA, I be keepInt0_1 InitHalting Macro-Instruction; cluster I ';' j -> InitHalting keepInt0_1; end; definition let i be keeping_0 parahalting Instruction of SCM+FSA, J be keepInt0_1 InitHalting Macro-Instruction; cluster i ';' J -> InitHalting keepInt0_1; end; definition let j be parahalting Instruction of SCM+FSA, I be parahalting Macro-Instruction; cluster I ';' j -> InitHalting; end; definition let i,j be parahalting Instruction of SCM+FSA; cluster i ';' j -> InitHalting; end; theorem :: SCM_HALT:30 ::TM048 for I being keepInt0_1 InitHalting Macro-Instruction, J being InitHalting Macro-Instruction holds IExec(I ';' J, s).a = IExec(J,IExec(I,s)).a; theorem :: SCM_HALT:31 ::TM050 for I being keepInt0_1 InitHalting Macro-Instruction, J being InitHalting Macro-Instruction holds IExec(I ';' J, s).f = IExec(J,IExec(I,s)).f; theorem :: SCM_HALT:32 for I be keepInt0_1 InitHalting Macro-Instruction,s be State of SCM+FSA holds (Initialize IExec(I,s)) | (Int-Locations \/ FinSeq-Locations) = IExec(I,s) | (Int-Locations \/ FinSeq-Locations); theorem :: SCM_HALT:33 ::TM051=miI: for I being keepInt0_1 InitHalting Macro-Instruction, j being parahalting Instruction of SCM+FSA holds IExec(I ';' j, s).a = Exec(j, IExec(I, s)).a; theorem :: SCM_HALT:34 ::TM053=miF for I being keepInt0_1 InitHalting Macro-Instruction, j being parahalting Instruction of SCM+FSA holds IExec(I ';' j, s).f = Exec(j, IExec(I, s)).f; definition let I be Macro-Instruction; let s be State of SCM+FSA; pred I is_closed_onInit s means :: SCM_HALT:def 4 ::def3=D18 for k being Nat holds IC (Computation (s +* Initialized I )).k in dom I; pred I is_halting_onInit s means :: SCM_HALT:def 5 ::def4=D18' s +* Initialized I is halting; end; theorem :: SCM_HALT:35 ::TM052=TQ6 for I being Macro-Instruction holds I is InitClosed iff for s being State of SCM+FSA holds I is_closed_onInit s; theorem :: SCM_HALT:36 ::TM054=*TQ6' for I being Macro-Instruction holds I is InitHalting iff for s being State of SCM+FSA holds I is_halting_onInit s; theorem :: SCM_HALT:37 ::TM055=TQ9''(SCMFSA7B) for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location st I does_not_destroy a & I is_closed_onInit s & Initialized I c= s holds for k being Nat holds (Computation s).k.a = s.a; definition cluster InitHalting good Macro-Instruction; end; definition cluster InitClosed good -> keepInt0_1 Macro-Instruction; end; definition cluster SCM+FSA-Stop -> InitHalting good; end; theorem :: SCM_HALT:38 ::TM056=TG25 for s being State of SCM+FSA, i being keeping_0 parahalting Instruction of SCM+FSA, J being InitHalting Macro-Instruction, a being Int-Location holds IExec(i ';' J,s).a = IExec(J,Exec(i,Initialize s)).a; theorem :: SCM_HALT:39 ::TM058=TG26 for s being State of SCM+FSA, i being keeping_0 parahalting Instruction of SCM+FSA, J being InitHalting Macro-Instruction, f being FinSeq-Location holds IExec(i ';' J,s).f = IExec(J,Exec(i,Initialize s)).f; theorem :: SCM_HALT:40 ::TM060 for s being State of SCM+FSA, I being Macro-Instruction holds I is_closed_onInit s iff I is_closed_on Initialize s; theorem :: SCM_HALT:41 ::TM062 for s being State of SCM+FSA, I being Macro-Instruction holds I is_halting_onInit s iff I is_halting_on Initialize s; theorem :: SCM_HALT:42 ::TM064(SCMFSA8C:17) for I be Macro-Instruction, s be State of SCM+FSA holds IExec(I,s) = IExec(I,Initialize s); theorem :: SCM_HALT:43 ::ThIF0_1' for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a = 0 & I is_closed_onInit s & I is_halting_onInit s holds if=0(a,I,J) is_closed_onInit s & if=0(a,I,J) is_halting_onInit s; theorem :: SCM_HALT:44 ::ThIF0_1(@BBB8) for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a = 0 & I is_closed_onInit s & I is_halting_onInit s holds IExec(if=0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + 3); theorem :: SCM_HALT:45 ::ThIF0_2' for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a <> 0 & J is_closed_onInit s & J is_halting_onInit s holds if=0(a,I,J) is_closed_onInit s & if=0(a,I,J) is_halting_onInit s; theorem :: SCM_HALT:46 ::ThIF0_2 for I,J being Macro-Instruction, a being read-write Int-Location holds for s being State of SCM+FSA st s.a <> 0 & J is_closed_onInit s & J is_halting_onInit s holds IExec(if=0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + 3) ; theorem :: SCM_HALT:47 ::=ThIF0 for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction, a being read-write Int-Location holds if=0(a,I,J) is InitHalting & (s.a = 0 implies IExec(if=0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + 3)) & (s.a <> 0 implies IExec(if=0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + 3)); theorem :: SCM_HALT:48 ::ThIF0' for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction, a being read-write Int-Location holds IC IExec(if=0(a,I,J),s) = insloc (card I + card J + 3) & (s.a = 0 implies ((for d being Int-Location holds IExec(if=0(a,I,J),s).d = IExec(I,s).d) & for f being FinSeq-Location holds IExec(if=0(a,I,J),s).f = IExec(I,s).f)) & (s.a <> 0 implies ((for d being Int-Location holds IExec(if=0(a,I,J),s).d = IExec(J,s).d) & for f being FinSeq-Location holds IExec(if=0(a,I,J),s).f = IExec(J,s).f)); theorem :: SCM_HALT:49 ::ThIFg0_1' for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a > 0 & I is_closed_onInit s & I is_halting_onInit s holds if>0(a,I,J) is_closed_onInit s & if>0(a,I,J) is_halting_onInit s; theorem :: SCM_HALT:50 ::ThIFg0_1 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a > 0 & I is_closed_onInit s & I is_halting_onInit s holds IExec(if>0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + 3); theorem :: SCM_HALT:51 ::ThIFg0_2' for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a <= 0 & J is_closed_onInit s & J is_halting_onInit s holds if>0(a,I,J) is_closed_onInit s & if>0(a,I,J) is_halting_onInit s; theorem :: SCM_HALT:52 ::ThIFg0_2 for I,J being Macro-Instruction, a being read-write Int-Location holds for s being State of SCM+FSA st s.a <= 0 & J is_closed_onInit s & J is_halting_onInit s holds IExec(if>0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + 3); theorem :: SCM_HALT:53 ::ThIFg0 for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction, a being read-write Int-Location holds if>0(a,I,J) is InitHalting & (s.a > 0 implies IExec(if>0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + 3)) & (s.a <= 0 implies IExec(if>0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + 3)); theorem :: SCM_HALT:54 ::ThIFg0' for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction, a being read-write Int-Location holds IC IExec(if>0(a,I,J),s) = insloc (card I + card J + 3) & (s.a > 0 implies ((for d being Int-Location holds IExec(if>0(a,I,J),s).d = IExec(I,s).d) & for f being FinSeq-Location holds IExec(if>0(a,I,J),s).f = IExec(I,s).f)) & (s.a <= 0 implies ((for d being Int-Location holds IExec(if>0(a,I,J),s).d = IExec(J,s).d) & for f being FinSeq-Location holds IExec(if>0(a,I,J),s).f = IExec(J,s).f)); theorem :: SCM_HALT:55 ::ThIFl0_1 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a < 0 & I is_closed_onInit s & I is_halting_onInit s holds IExec(if<0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + card J + 7); theorem :: SCM_HALT:56 ::ThIFl0_2 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a = 0 & J is_closed_onInit s & J is_halting_onInit s holds IExec(if<0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + card J + 7); theorem :: SCM_HALT:57 ::ThIFl0_3 for s being State of SCM+FSA, I,J being Macro-Instruction, a being read-write Int-Location st s.a > 0 & J is_closed_onInit s & J is_halting_onInit s holds IExec(if<0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + card J + 7); theorem :: SCM_HALT:58 ::ThIFl0 for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction, a being read-write Int-Location holds (if<0(a,I,J) is InitHalting & (s.a < 0 implies IExec(if<0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + card J + 7)) & (s.a >= 0 implies IExec(if<0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + card J + 7))); definition let I,J be InitHalting Macro-Instruction; let a be read-write Int-Location; cluster if=0(a,I,J) -> InitHalting; cluster if>0(a,I,J) -> InitHalting; cluster if<0(a,I,J) -> InitHalting; end; theorem :: SCM_HALT:59 ::TM202 for I being Macro-Instruction holds I is InitHalting iff for s being State of SCM+FSA holds I is_halting_on Initialize s; theorem :: SCM_HALT:60 ::TM204 for I being Macro-Instruction holds I is InitClosed iff for s being State of SCM+FSA holds I is_closed_on Initialize s; theorem :: SCM_HALT:61 ::TM206=T200724 for s being State of SCM+FSA, I being InitHalting 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 :: SCM_HALT:62 ::TM208=TMP29 for s being State of SCM+FSA, I being InitHalting 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 :: SCM_HALT:63 ::TM209=TMP29'' for s being State of SCM+FSA, I being InitHalting Macro-Instruction, a being Int-Location st I does_not_destroy a holds IExec(I,s).a = (Initialize s).a; theorem :: SCM_HALT:64 ::TM210=TMP27 for s be State of SCM+FSA,I be keepInt0_1 InitHalting 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 :: SCM_HALT:65 ::MAI1 for s being State of SCM+FSA, I being InitClosed Macro-Instruction st Initialized I 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 :: SCM_HALT:66 for s being State of SCM+FSA, I being InitHalting 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; theorem :: SCM_HALT:67 ::I_SI I c= s +* Initialized I; theorem :: SCM_HALT:68 ::TMP24 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_onInit s & I is_halting_onInit s for m being Nat st m <= LifeSpan (s +* Initialized I) holds (Computation (s +* Initialized I)).m, (Computation(s +* Initialized (loop I))).m equal_outside the Instruction-Locations of SCM+FSA; theorem :: SCM_HALT:69 ::TMP25 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_onInit s & I is_halting_onInit s for m being Nat st m < LifeSpan (s +* Initialized I) holds CurInstr (Computation (s +* Initialized I)).m = CurInstr (Computation(s +* Initialized(loop I))).m; theorem :: SCM_HALT:70 ::InsLoc for l being Instruction-Location of SCM+FSA holds not l in dom (((intloc 0) .--> 1) +* Start-At insloc 0); theorem :: SCM_HALT:71 ::_TMP23 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_onInit s & I is_halting_onInit s holds (CurInstr (Computation (s +* Initialized (loop I))). LifeSpan (s +* Initialized I) = goto insloc 0 & for m being Nat st m <= LifeSpan (s +* Initialized I) holds CurInstr (Computation (s +* Initialized (loop I))).m <> halt SCM+FSA); theorem :: SCM_HALT:72 ::TMP26 for s being State of SCM+FSA, I being Macro-Instruction st I is_closed_onInit s & I is_halting_onInit s holds CurInstr (Computation (s +* Initialized loop I)). LifeSpan (s +* Initialized I) = goto insloc 0; theorem :: SCM_HALT:73 ::TMP22 for s being State of SCM+FSA, I being good InitHalting 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 :: SCM_HALT:74 for s being State of SCM+FSA, I being good InitHalting 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 :: SCM_HALT:75 for s being State of SCM+FSA, I being good InitHalting 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 :: SCM_HALT:76 ::Itime for I being good InitHalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a holds Initialized Times(a,I) is halting; definition let a be read-write Int-Location,I be good Macro-Instruction; cluster Times(a,I) -> good; end; theorem :: SCM_HALT:77 ::TMP22' for s being State of SCM+FSA, I being good InitHalting Macro-Instruction, a being read-write Int-Location st I does_not_destroy a & s.a > 0 holds ex s2 being State of SCM+FSA, k being Nat st s2 = s +* Initialized (loop if=0(a,Goto insloc 2, I ';' SubFrom(a,intloc 0))) & k = LifeSpan (s +* Initialized (if=0(a,Goto insloc 2, I ';' SubFrom(a,intloc 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 :: SCM_HALT:78 ::T1 for s being State of SCM+FSA, I being good InitHalting 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 :: SCM_HALT:79 ::T2 for s being State of SCM+FSA, I being good InitHalting 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); theorem :: SCM_HALT:80 ::T03 for s be State of SCM+FSA, I be good InitHalting Macro-Instruction, f be FinSeq-Location,a be read-write Int-Location st s.a <= 0 holds IExec(Times(a,I),s).f=s.f; theorem :: SCM_HALT:81 ::T04 for s be State of SCM+FSA, I be good InitHalting Macro-Instruction, b be Int-Location,a be read-write Int-Location st s.a <= 0 holds IExec(Times(a,I),s).b=(Initialize s).b; theorem :: SCM_HALT:82 ::T05 for s be State of SCM+FSA, I be good InitHalting Macro-Instruction, f be FinSeq-Location,a be read-write Int-Location st I does_not_destroy a & s.a > 0 holds IExec(Times(a,I),s).f =IExec(Times(a,I),IExec(I ';' SubFrom(a,intloc 0),s)).f; theorem :: SCM_HALT:83 ::T06 for s be State of SCM+FSA, I be good InitHalting Macro-Instruction, b be Int-Location,a be read-write Int-Location st I does_not_destroy a & s.a > 0 holds IExec(Times(a,I),s).b =IExec(Times(a,I),IExec(I ';' SubFrom(a,intloc 0),s)).b; definition let i be Instruction of SCM+FSA; attr i is good means :: SCM_HALT:def 6 ::defB1 i does_not_destroy intloc 0; end; definition cluster parahalting good Instruction of SCM+FSA; end; definition let i be good Instruction of SCM+FSA, J be good Macro-Instruction; cluster i ';' J -> good; cluster J ';' i -> good; end; definition let i,j be good Instruction of SCM+FSA; cluster i ';' j -> good; end; definition let a be read-write Int-Location,b be Int-Location; cluster a := b -> good; cluster SubFrom(a,b) -> good; end; definition let a be read-write Int-Location,b be Int-Location,f be FinSeq-Location; cluster a:=(f,b) -> good; end; definition let a,b be Int-Location,f be FinSeq-Location; cluster (f,a):=b -> good; end; definition let a be read-write Int-Location,f be FinSeq-Location; cluster a:=len f -> good; end; definition let n be Nat; cluster intloc (n+1) -> read-write; end;

Back to top