The Mizar abstract of SCMFSA6A

Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users
The abstract of the Mizar article:: On the Compositions of Macro Instructions. Part I
by
Andrzej Trybulec,
Yatsuka Nakamura, and
Noriko Asamoto
Received June 20, 1996
MML identifier: SCMFSA6A
[ Mizar article, MML identifier index ]
environ

 vocabulary FUNCT_1, RELAT_1, FUNCT_4, FUNCT_7, BOOLE, CAT_1, AMI_3, AMI_1,
      SCMFSA_2, CARD_1, FUNCOP_1, FINSET_1, TARSKI, AMI_5, RELOC, INT_1, AMI_2,
      ARYTM_1, NAT_1, ABSVALUE, FINSEQ_1, FINSEQ_2, SCMFSA6A, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      NAT_1, INT_1, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
      FINSEQ_4, CARD_1, CQC_LANG, FINSET_1, FUNCT_4, STRUCT_0, AMI_1, AMI_3,
      AMI_5, FUNCT_7, SCMFSA_2, SCMFSA_4, SCMFSA_5;
 constructors SCMFSA_4, WELLORD2, SCMFSA_5, NAT_1, AMI_5, ENUMSET1, FUNCT_7,
      RELOC, FINSEQ_4, MEMBERED;
 clusters XBOOLE_0, AMI_1, SCMFSA_2, FUNCT_1, FINSET_1, PRELAMB, FUNCT_7,
      SCMFSA_4, RELSET_1, INT_1, FRAENKEL, MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

theorem :: SCMFSA6A:1
   for f,g being Function, x,y being set st g c= f & not x in dom g
  holds g c= f+*(x,y);

theorem :: SCMFSA6A:2
   for f,g being Function, A being set st f|A = g|A &
  f,g equal_outside A holds f = g;

theorem :: SCMFSA6A:3
   for f being Function, a,b,A being set st a in A
  holds f,f+*(a,b) equal_outside A;

theorem :: SCMFSA6A:4
 for f being Function, a,b,A being set holds
  a in A or (f+*(a,b))|A = f|A;

theorem :: SCMFSA6A:5
   for f,g being Function, a,b,A being set st f|A = g|A
   holds (f+*(a,b))|A = (g+*(a,b))|A;

theorem :: SCMFSA6A:6
   for f,g,h being Function st f c= h & g c= h
  holds f +* g c= h;

theorem :: SCMFSA6A:7
   for a,b being set, f being Function holds
  a.-->b c= f iff a in dom f & f.a = b;

theorem :: SCMFSA6A:8  ::Lemma12
 for f being Function, A being set holds
     dom (f | (dom f \ A)) = dom f \ A;

theorem :: SCMFSA6A:9  ::LemmaD
 for f,g being Function, D being set st D c= dom f & D c= dom g holds
     f | D = g | D iff for x being set st x in D holds f.x = g.x;

theorem :: SCMFSA6A:10  ::Lemma14
 for f being Function, D being set holds
     f | D = f | (dom f /\ D);

theorem :: SCMFSA6A:11  ::Lemma7
   for f,g,h being Function, A being set holds
     f, g equal_outside A implies f +* h, g +* h equal_outside A;

theorem :: SCMFSA6A:12  ::Lemma7'
   for f,g,h being Function, A being set holds
     f, g equal_outside A implies h +* f, h +* g equal_outside A;

theorem :: SCMFSA6A:13
   for f,g,h being Function
 holds f +* h = g +* h iff f,g equal_outside dom h;

begin

definition
 mode Macro-Instruction is initial programmed FinPartState of SCM+FSA;
end;

reserve l, m, n for Nat,
        i,j,k for Instruction of SCM+FSA,
        I,J,K for Macro-Instruction;

definition let I be programmed FinPartState of SCM+FSA;
 func Directed I -> programmed FinPartState of SCM+FSA equals
:: SCMFSA6A:def 1
 ((id the Instructions of SCM+FSA) +*
         (halt SCM+FSA .--> goto insloc card I))*I;
end;

theorem :: SCMFSA6A:14
 dom Directed I = dom I;

definition let I be Macro-Instruction;
 cluster Directed I -> initial;
end;

definition let i;
 func Macro i -> Macro-Instruction equals
:: SCMFSA6A:def 2
  (insloc 0,insloc 1) --> (i,halt SCM+FSA);
end;

definition let i;
 cluster Macro i -> non empty;
end;

theorem :: SCMFSA6A:15
 for P being Macro-Instruction, n holds
  n < card P iff insloc n in dom P;

definition let I be initial FinPartState of SCM+FSA;
 cluster ProgramPart I -> initial;
end;

theorem :: SCMFSA6A:16
 dom I misses dom ProgramPart Relocated(J, card I);

theorem :: SCMFSA6A:17
for I being programmed FinPartState of SCM+FSA
 holds card ProgramPart Relocated(I, m) = card I;

theorem :: SCMFSA6A:18
 not halt SCM+FSA in rng Directed I;

theorem :: SCMFSA6A:19
 ProgramPart Relocated(Directed I, m) =
   ((id the Instructions of SCM+FSA) +*
     (halt SCM+FSA .--> goto insloc(m + card I)))*
          ProgramPart Relocated(I, m);

theorem :: SCMFSA6A:20
for I,J being FinPartState of SCM+FSA holds
 ProgramPart(I +* J) = ProgramPart I +* ProgramPart J;

theorem :: SCMFSA6A:21
for I,J being FinPartState of SCM+FSA holds
 ProgramPart Relocated(I +* J, n) =
    ProgramPart Relocated(I,n) +* ProgramPart Relocated(J,n);

theorem :: SCMFSA6A:22
  ProgramPart Relocated(ProgramPart Relocated(I, m), n)
          = ProgramPart Relocated(I, m + n);

reserve a,b for Int-Location, f for FinSeq-Location,
        s,s1,s2 for State of SCM+FSA;

definition let I be FinPartState of SCM+FSA;
 func Initialized I -> FinPartState of SCM+FSA equals
:: SCMFSA6A:def 3
 I +* ((intloc 0) .--> 1) +* Start-At(insloc 0);
end;

theorem :: SCMFSA6A:23
 InsCode i in {0,6,7,8} or Exec(i,s).IC SCM+FSA = Next IC s;

theorem :: SCMFSA6A:24
 IC SCM+FSA in dom Initialized I;

theorem :: SCMFSA6A:25
   IC Initialized I = insloc 0;

theorem :: SCMFSA6A:26
 I c= Initialized I;

theorem :: SCMFSA6A:27
   for N being set, A being AMI-Struct over N, s being State of A,
     I being programmed FinPartState of A holds
 s,s+*I equal_outside the Instruction-Locations of A;

theorem :: SCMFSA6A:28
 for s1,s2 being State of SCM+FSA
       st IC s1 = IC s2 &
      (for a being Int-Location holds s1.a = s2.a) &
       for f being FinSeq-Location holds s1.f = s2.f
  holds s1,s2 equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:29
 for N being with_non-empty_elements set,
     S being realistic IC-Ins-separated definite
       (non empty non void AMI-Struct over N),
     s1, s2 being State of S holds
 s1,s2 equal_outside the Instruction-Locations of S implies
   IC s1 = IC s2;

theorem :: SCMFSA6A:30
 s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies
  for a being Int-Location holds s1.a = s2.a;

theorem :: SCMFSA6A:31
 s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies
  for f being FinSeq-Location holds s1.f = s2.f;

theorem :: SCMFSA6A:32
   s1,s2 equal_outside the Instruction-Locations of SCM+FSA implies
  Exec(i,s1),Exec(i,s2) equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:33
   (Initialized I)|the Instruction-Locations of SCM+FSA = I;

scheme SCMFSAEx{ F(set) -> Element of the Instructions of SCM+FSA,
                 G(set) -> Integer, H(set) -> FinSequence of INT,
                 I() -> Instruction-Location of SCM+FSA }:
 ex S being State of SCM+FSA st IC S = I() &
  for i being Nat holds
    S.insloc i = F(i) & S.intloc i = G(i) & S.fsloc i = H(i);

theorem :: SCMFSA6A:34  ::T12
  for s being State of SCM+FSA holds
     dom s = Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/
         the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:35  ::T12'
   for s being State of SCM+FSA, x being set st x in dom s holds
     x is Int-Location or x is FinSeq-Location or
     x = IC SCM+FSA or x is Instruction-Location of SCM+FSA;

theorem :: SCMFSA6A:36  ::T29
   for s1,s2 being State of SCM+FSA holds
     (for l being Instruction-Location of SCM+FSA holds s1.l = s2.l)
 iff s1 | the Instruction-Locations of SCM+FSA =
     s2 | the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:37  ::T32
   for i being Instruction-Location of SCM+FSA holds
     not i in Int-Locations \/ FinSeq-Locations &
     not IC SCM+FSA in Int-Locations \/ FinSeq-Locations;

theorem :: SCMFSA6A:38  ::T28
 for s1,s2 being State of SCM+FSA holds
     ((for a being Int-Location holds s1.a = s2.a) &
     for f being FinSeq-Location holds s1.f = s2.f)
 iff s1 | (Int-Locations \/ FinSeq-Locations) =
     s2 | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6A:39  ::T19
   for s1,s2 being State of SCM+FSA st
     s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
     s1 | (Int-Locations \/ FinSeq-Locations) =
     s2 | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6A:40  ::T21
   for s,ss being State of SCM+FSA, A being set holds
     (ss +* s | A) | A = s | A;

theorem :: SCMFSA6A:41  ::Lemma
   for s1,s2 being State of SCM+FSA, n being Nat,
     i being Instruction of SCM+FSA holds
     IC s1 + n = IC s2 &
     s1 | (Int-Locations \/ FinSeq-Locations) =
     s2 | (Int-Locations \/ FinSeq-Locations)
 implies
     IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) &
     Exec(i,s1) | (Int-Locations \/ FinSeq-Locations) =
     Exec(IncAddr(i,n),s2) | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA6A:42  ::T18
   for I,J being Macro-Instruction holds
     I,J equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA6A:43  ::T3
 for I being Macro-Instruction holds
     dom Initialized I = dom I \/ {intloc 0} \/ {IC SCM+FSA};

theorem :: SCMFSA6A:44  ::T2
 for I being Macro-Instruction, x being set st x in dom Initialized I holds
     x in dom I or x = intloc 0 or x = IC SCM+FSA;

theorem :: SCMFSA6A:45  ::T3'
 for I being Macro-Instruction holds intloc 0 in dom Initialized I;

theorem :: SCMFSA6A:46  ::T5
 for I being Macro-Instruction holds
     (Initialized I).intloc 0 = 1 & (Initialized I).IC SCM+FSA = insloc 0;

theorem :: SCMFSA6A:47  ::T7
 for I being Macro-Instruction holds
     not intloc 0 in dom I & not IC SCM+FSA in dom I;

theorem :: SCMFSA6A:48  ::T36
 for I being Macro-Instruction, a being Int-Location st a <> intloc 0 holds
     not a in dom Initialized I;

theorem :: SCMFSA6A:49  ::T37
 for I being Macro-Instruction, f being FinSeq-Location holds
     not f in dom Initialized I;

theorem :: SCMFSA6A:50  ::T8
 for I being Macro-Instruction, x being set st x in dom I holds
     I.x = (Initialized I).x;

theorem :: SCMFSA6A:51  ::T10'
 for I,J being Macro-Instruction
 for s being State of SCM+FSA st Initialized J c= s holds
     s +* Initialized I = s +* I;

theorem :: SCMFSA6A:52  ::T10
   for I,J being Macro-Instruction
 for s being State of SCM+FSA st Initialized J c= s holds
     Initialized I c= s +* I;

theorem :: SCMFSA6A:53  ::T23
   for I,J being Macro-Instruction
 for s being State of SCM+FSA holds
     s +* Initialized I, s +* Initialized J
         equal_outside the Instruction-Locations of SCM+FSA;

begin :: The composition of macroinstructions

definition let I,J be Macro-Instruction;
 func I ';' J -> Macro-Instruction equals
:: SCMFSA6A:def 4
  Directed I +* ProgramPart Relocated(J, card I);
end;

theorem :: SCMFSA6A:54
   for I,J being Macro-Instruction, l being Instruction-Location of SCM+FSA
  st l in dom I & I.l <> halt SCM+FSA
 holds (I ';' J).l = I.l;

theorem :: SCMFSA6A:55  ::T16
   for I,J being Macro-Instruction holds
     Directed I c= I ';' J;

theorem :: SCMFSA6A:56  ::T4
 for I,J being Macro-Instruction holds
     dom I c= dom (I ';' J);

theorem :: SCMFSA6A:57  ::T6
   for I,J being Macro-Instruction holds
     I +* (I ';' J) = (I ';' J);

theorem :: SCMFSA6A:58  ::T1
   for I,J being Macro-Instruction holds
     Initialized I +* (I ';' J) = Initialized (I ';' J);


begin :: The compostion of instruction and macroinstructions

definition let i, J;
 func i ';' J -> Macro-Instruction equals
:: SCMFSA6A:def 5
  Macro i ';' J;
end;

definition let I, j;
 func I ';' j -> Macro-Instruction equals
:: SCMFSA6A:def 6
  I ';' Macro j;
end;

definition let i,j;
 func i ';' j -> Macro-Instruction equals
:: SCMFSA6A:def 7
  Macro i ';' Macro j;
end;

theorem :: SCMFSA6A:59
 i ';' j = Macro i ';' j;

theorem :: SCMFSA6A:60
 i ';' j = i ';' Macro j;

theorem :: SCMFSA6A:61
 card(I ';' J) = card I + card J;

theorem :: SCMFSA6A:62
 I ';' J ';' K = I ';' (J ';' K);

theorem :: SCMFSA6A:63
 I ';' J ';' k = I ';' (J ';' k);

theorem :: SCMFSA6A:64
   I ';' j ';' K = I ';' (j ';' K);

theorem :: SCMFSA6A:65
   I ';' j ';' k = I ';' (j ';' k);

theorem :: SCMFSA6A:66
 i ';' J ';' K = i ';' (J ';' K);

theorem :: SCMFSA6A:67
   i ';' J ';' k = i ';' (J ';' k);

theorem :: SCMFSA6A:68
 i ';' j ';' K = i ';' (j ';' K);

theorem :: SCMFSA6A:69
   i ';' j ';' k = i ';' (j ';' k);
The abstract of the Mizar article:

On the Compositions of Macro Instructions. Part I
