Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### Computation of Two Consecutive Program Blocks for SCMPDS

**by****Jing-Chao Chen**- Received June 15, 1999
- MML identifier: SCMPDS_5

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_3, SCMPDS_2, AMI_1, INT_1, SCMPDS_4, FUNCT_1, RELAT_1, SCMFSA_7, SCMPDS_3, CAT_1, RELOC, CARD_1, SCMFSA6A, FUNCT_4, BOOLE, SCMFSA6B, FUNCT_7, SCM_1, AMI_2, AMI_5, SCMPDS_1, ABSVALUE, NAT_1, ARYTM_1, SCMPDS_5; notation TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_4, INT_1, NAT_1, STRUCT_0, AMI_1, AMI_2, AMI_3, AMI_5, FUNCT_7, SCMPDS_1, SCMPDS_2, GROUP_1, SCMPDS_3, CARD_1, SCMPDS_4, SCM_1; constructors DOMAIN_1, NAT_1, AMI_5, SCMPDS_1, SCMFSA_4, SCMPDS_4, SCM_1, MEMBERED; clusters AMI_1, INT_1, FUNCT_1, SCMPDS_2, PRELAMB, SCMFSA_4, SCMPDS_4, FRAENKEL, MEMBERED; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve x for set, m,n for Nat, a,b,c for Int_position, i for Instruction of SCMPDS, s,s1,s2 for State of SCMPDS, k1,k2 for Integer, loc,l1 for Instruction-Location of SCMPDS, I,J for Program-block, N for with_non-empty_elements set; theorem :: SCMPDS_5:1 :: S6B15 for S being halting IC-Ins-separated definite (non empty non void AMI-Struct over N), s being State of S st s = Following s holds for n holds (Computation s).n = s; theorem :: SCMPDS_5:2 x in dom Load i iff x = inspos 0; theorem :: SCMPDS_5:3 :: Stp loc in dom (stop I) & (stop I).loc <> halt SCMPDS implies loc in dom I; theorem :: SCMPDS_5:4 :: PDS4_72 dom Load i = {inspos 0} & (Load i).(inspos 0)=i; theorem :: SCMPDS_5:5 inspos 0 in dom Load i; theorem :: SCMPDS_5:6 :: PDS4_74 card Load i = 1; theorem :: SCMPDS_5:7 ::CardsI card stop I = card I + 1; theorem :: SCMPDS_5:8 card stop Load i = 2; theorem :: SCMPDS_5:9 ::PDS4_75 inspos 0 in dom stop (Load i) & inspos 1 in dom stop (Load i); theorem :: SCMPDS_5:10 (stop Load i).inspos 0=i & (stop Load i).inspos 1=halt SCMPDS; theorem :: SCMPDS_5:11 ::SCMFSA6B_32 x in dom (stop Load i) iff x=inspos 0 or x=inspos 1; theorem :: SCMPDS_5:12 dom (stop Load i)={inspos 0,inspos 1}; theorem :: SCMPDS_5:13 inspos 0 in dom (Initialized stop Load i) & inspos 1 in dom (Initialized stop Load i) & (Initialized stop Load i).inspos 0=i & (Initialized stop Load i).inspos 1=halt SCMPDS; theorem :: SCMPDS_5:14 for I,J being Program-block holds Initialized stop (I ';' J) = (I ';' (J ';' SCMPDS-Stop)) +* Start-At inspos 0; theorem :: SCMPDS_5:15 for I,J being Program-block holds Initialized I c= Initialized stop (I ';' J); theorem :: SCMPDS_5:16 dom stop I c= dom stop (I ';' J); theorem :: SCMPDS_5:17 :: SCMPDS_4:42,T6A40 for I,J being Program-block holds Initialized stop I +* Initialized stop (I ';' J) = Initialized stop (I ';' J); theorem :: SCMPDS_5:18 Initialized I c= s implies IC s = inspos 0; theorem :: SCMPDS_5:19 (s +* Initialized I).a = s.a; theorem :: SCMPDS_5:20 ::T13 for I being parahalting Program-block st Initialized stop I c= s1 & Initialized stop I c= s2 & s1,s2 equal_outside the Instruction-Locations of SCMPDS holds for k being Nat holds (Computation s1).k, (Computation s2).k equal_outside the Instruction-Locations of SCMPDS & CurInstr (Computation s1).k = CurInstr (Computation s2).k; theorem :: SCMPDS_5:21 ::T14 for I being parahalting Program-block st Initialized stop I c= s1 & Initialized stop I c= s2 & s1,s2 equal_outside the Instruction-Locations of SCMPDS holds LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside the Instruction-Locations of SCMPDS; theorem :: SCMPDS_5:22 ::T27 for I being Program-block holds IC IExec(I,s) = IC Result (s +* Initialized stop I); theorem :: SCMPDS_5:23 for I being parahalting Program-block, J being Program-block st Initialized stop I c= s for m st m <= LifeSpan s holds (Computation s).m,(Computation(s+*(I ';' J))).m equal_outside the Instruction-Locations of SCMPDS; theorem :: SCMPDS_5:24 for I being parahalting Program-block, J being Program-block st Initialized stop I c= s for m st m <= LifeSpan s holds (Computation s).m,(Computation(s+*Initialized stop (I ';' J))).m equal_outside the Instruction-Locations of SCMPDS; begin :: Non halting instrutions and parahalting instrutions definition let i be Instruction of SCMPDS; attr i is No-StopCode means :: SCMPDS_5:def 1 i <> halt SCMPDS; end; definition let i be Instruction of SCMPDS; attr i is parahalting means :: SCMPDS_5:def 2 Load i is parahalting; end; definition cluster No-StopCode shiftable parahalting Instruction of SCMPDS; end; theorem :: SCMPDS_5:25 k1 <>0 implies goto k1 is No-StopCode; definition let a; cluster return a -> No-StopCode; end; definition let a,k1; cluster a := k1 -> No-StopCode; cluster saveIC(a,k1) -> No-StopCode; end; definition let a,k1,k2; cluster (a,k1)<>0_goto k2 -> No-StopCode; cluster (a,k1)<=0_goto k2 -> No-StopCode; cluster (a,k1)>=0_goto k2 -> No-StopCode; cluster (a,k1) := k2 -> No-StopCode; end; definition let a,k1,k2; cluster AddTo(a,k1,k2) -> No-StopCode; end; definition let a,b,k1,k2; cluster AddTo(a,k1,b,k2) -> No-StopCode; cluster SubFrom(a,k1,b,k2) -> No-StopCode; cluster MultBy(a,k1,b,k2) -> No-StopCode; cluster Divide(a,k1,b,k2) -> No-StopCode; cluster (a,k1) := (b,k2) -> No-StopCode; end; definition cluster halt SCMPDS -> parahalting; end; definition let i be parahalting Instruction of SCMPDS; cluster Load i -> parahalting; end; definition let a,k1; cluster a := k1 -> parahalting; end; definition let a,k1,k2; cluster (a,k1) := k2 -> parahalting; cluster AddTo(a,k1,k2) -> parahalting; end; definition let a,b,k1,k2; cluster AddTo(a,k1,b,k2) -> parahalting; cluster SubFrom(a,k1,b,k2) -> parahalting; cluster MultBy(a,k1,b,k2) -> parahalting; cluster Divide(a,k1,b,k2) -> parahalting; cluster (a,k1) := (b,k2) -> parahalting; end; theorem :: SCMPDS_5:26 InsCode i =1 implies i is not parahalting; definition let IT be FinPartState of SCMPDS; attr IT is No-StopCode means :: SCMPDS_5:def 3 for x being Instruction-Location of SCMPDS st x in dom IT holds IT.x <> halt SCMPDS; end; definition cluster parahalting shiftable No-StopCode Program-block; end; definition let I,J be No-StopCode Program-block; cluster I ';' J -> No-StopCode; end; definition let i be No-StopCode Instruction of SCMPDS; cluster Load i -> No-StopCode; end; definition let i be No-StopCode Instruction of SCMPDS, J be No-StopCode Program-block; cluster i ';' J -> No-StopCode; end; definition let I be No-StopCode Program-block, j be No-StopCode Instruction of SCMPDS; cluster I ';' j -> No-StopCode; end; definition let i,j be No-StopCode Instruction of SCMPDS; cluster i ';' j -> No-StopCode; end; theorem :: SCMPDS_5:27 ::Th37 for I being parahalting No-StopCode Program-block st Initialized (stop I) c= s holds IC (Computation s).LifeSpan (s +* Initialized stop(I)) = inspos card I; theorem :: SCMPDS_5:28 for I being parahalting Program-block,k be Nat st k < LifeSpan (s +* Initialized stop(I)) holds IC (Computation (s +* Initialized stop(I))).k in dom I; theorem :: SCMPDS_5:29 for I being parahalting Program-block,k be Nat st Initialized I c= s & k <= LifeSpan (s +* Initialized stop(I)) holds (Computation s).k,(Computation (s +* Initialized stop(I))).k equal_outside the Instruction-Locations of SCMPDS; theorem :: SCMPDS_5:30 :: Th37,Lemma01 for I being parahalting No-StopCode Program-block st Initialized I c= s holds IC (Computation s).LifeSpan (s +* Initialized stop(I)) = inspos card I; theorem :: SCMPDS_5:31 ::Th37 end for I being parahalting Program-block st Initialized I c= s holds CurInstr (Computation s).LifeSpan (s +* Initialized stop(I)) = halt SCMPDS or IC (Computation s).LifeSpan (s +* Initialized stop(I)) = inspos card I; theorem :: SCMPDS_5:32 :: Th39 for I being parahalting No-StopCode Program-block,k being Nat st Initialized I c= s & k < LifeSpan (s +* Initialized stop(I)) holds CurInstr (Computation s).k <> halt SCMPDS; theorem :: SCMPDS_5:33 ::Th40 for I being parahalting Program-block,J being Program-block, k being Nat st k <= LifeSpan (s +* Initialized stop(I)) holds (Computation (s +* Initialized stop I )).k, (Computation (s +* ((I ';' J) +* Start-At inspos 0))).k equal_outside the Instruction-Locations of SCMPDS; theorem :: SCMPDS_5:34 ::Th41B for I being parahalting Program-block,J being Program-block, k being Nat st k <= LifeSpan (s +* Initialized stop(I)) holds (Computation (s +* Initialized stop I )).k, (Computation (s +* Initialized stop (I ';' J))).k equal_outside the Instruction-Locations of SCMPDS; definition let I be parahalting Program-block, J be parahalting shiftable Program-block; cluster I ';' J -> parahalting; end; definition let i be parahalting Instruction of SCMPDS, J be parahalting shiftable Program-block; cluster i ';' J -> parahalting; end; definition let I be parahalting Program-block, j be parahalting shiftable Instruction of SCMPDS; cluster I ';' j -> parahalting; end; definition let i be parahalting Instruction of SCMPDS, j be parahalting shiftable Instruction of SCMPDS; cluster i ';' j -> parahalting; end; theorem :: SCMPDS_5:35 :: SF4_28 for s,s1 being State of SCMPDS, J being parahalting shiftable Program-block st s=(Computation (s1+*Initialized stop J)).m holds Exec(CurInstr s ,s +* Start-At (IC s + n)) = Following(s) +* Start-At (IC Following(s) + n); begin :: Computation of two consecutive program blocks theorem :: SCMPDS_5:36 ::Th42 for I being parahalting No-StopCode Program-block,J being parahalting shiftable Program-block,k being Nat st Initialized stop (I ';' J) c= s holds (Computation (Result(s +*Initialized stop I) +* Initialized stop J )).k +* Start-At (IC (Computation (Result(s +*Initialized stop I) +* Initialized stop J )).k + card I), (Computation (s +* Initialized stop (I ';' J))). (LifeSpan (s +* Initialized stop I)+k) equal_outside the Instruction-Locations of SCMPDS; theorem :: SCMPDS_5:37 ::Th43 for I being parahalting No-StopCode Program-block,J being parahalting shiftable Program-block holds LifeSpan (s +* Initialized stop (I ';' J)) = LifeSpan (s +* Initialized stop I) + LifeSpan (Result (s +* Initialized stop I) +* Initialized stop J); theorem :: SCMPDS_5:38 for I being parahalting No-StopCode Program-block,J being parahalting shiftable Program-block holds IExec(I ';' J,s) = IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I); theorem :: SCMPDS_5:39 for I being parahalting No-StopCode Program-block,J being parahalting shiftable Program-block holds IExec(I ';' J, s).a = IExec(J,IExec(I,s)).a; begin :: Computation of the program consisting of a instruction and a block definition let s be State of SCMPDS; func Initialized s -> State of SCMPDS equals :: SCMPDS_5:def 4 s +* Start-At(inspos 0); end; theorem :: SCMPDS_5:40 ::Th3c IC Initialized s = inspos 0 & (Initialized s).a = s.a & (Initialized s).loc = s.loc; theorem :: SCMPDS_5:41 ::Th4c s1, s2 equal_outside the Instruction-Locations of SCMPDS iff s1 | (SCM-Data-Loc \/ {IC SCMPDS}) = s2 | (SCM-Data-Loc \/ {IC SCMPDS}); canceled; theorem :: SCMPDS_5:43 ::Th5c s1 | SCM-Data-Loc = s2 | SCM-Data-Loc & InsCode i <> 3 implies Exec (i, s1) | SCM-Data-Loc = Exec (i, s2) | SCM-Data-Loc; theorem :: SCMPDS_5:44 ::Th5c for i being shiftable Instruction of SCMPDS holds (s1 | SCM-Data-Loc = s2 | SCM-Data-Loc implies Exec (i, s1) | SCM-Data-Loc = Exec (i, s2) | SCM-Data-Loc); theorem :: SCMPDS_5:45 ::Th6c for i being parahalting Instruction of SCMPDS holds Exec(i, Initialized s) = IExec(Load i, s); theorem :: SCMPDS_5:46 ::Th7c for I being parahalting No-StopCode Program-block,j being parahalting shiftable Instruction of SCMPDS holds IExec(I ';' j, s).a = Exec(j, IExec(I, s)).a; theorem :: SCMPDS_5:47 ::Th9c for i being No-StopCode parahalting Instruction of SCMPDS, j being shiftable parahalting Instruction of SCMPDS holds IExec(i ';' j, s).a = Exec(j, Exec(i, Initialized s)).a;

Back to top