The Mizar abstract of SCMPDS

Journal of Formalized Mathematics
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;
The abstract of the Mizar article:

Computation of Two Consecutive Program Blocks for SCMPDS
