The Mizar abstract of SCMFSA

Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users
The abstract of the Mizar article:: An Extension of \bf SCM
by
Andrzej Trybulec,
Yatsuka Nakamura, and
Piotr Rudnicki
Received February 3, 1996
MML identifier: SCMFSA_1
[ Mizar article, MML identifier index ]
environ

 vocabulary INT_1, AMI_2, BOOLE, GR_CY_1, TARSKI, FINSEQ_1, AMI_5, MCART_1,
      FUNCT_1, FUNCOP_1, FUNCT_4, CAT_1, RELAT_1, AMI_3, AMI_1, ORDINAL2,
      CARD_3, ZF_REFLE, PBOOLE, ABSVALUE, FINSEQ_2, FUNCT_2, FUNCT_5, SCMFSA_1,
      FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, ORDINAL1, NUMBERS,
      XREAL_0, NAT_1, MCART_1, ABSVALUE, PBOOLE, RELAT_1, FUNCT_1, FUNCT_2,
      FRAENKEL, FUNCOP_1, INT_1, FINSEQ_1, FUNCT_4, CAT_2, FINSOP_1, CARD_3,
      GR_CY_1, CQC_LANG, FINSEQ_4, AMI_1, AMI_2, AMI_3, FUNCT_7;
 constructors DOMAIN_1, CAT_2, NAT_1, FINSOP_1, FUNCT_7, AMI_2, AMI_3,
      FINSEQ_4, MEMBERED;
 clusters NUMBERS, SUBSET_1, FUNCT_1, INT_1, AMI_1, RELSET_1, AMI_3, PBOOLE,
      FINSEQ_1, AMI_2, FUNCOP_1, CQC_LANG, ARYTM_3, XBOOLE_0, FRAENKEL,
      ZFMISC_1, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

 reserve x,y,z for set,
         k for Nat;

definition
 func SCM+FSA-Data-Loc -> Subset of INT equals
:: SCMFSA_1:def 1
  SCM-Data-Loc;
 func SCM+FSA-Data*-Loc -> Subset of INT equals
:: SCMFSA_1:def 2
  INT \ NAT;
 func SCM+FSA-Instr-Loc -> Subset of INT equals
:: SCMFSA_1:def 3
  SCM-Instr-Loc;
end;

definition
 cluster SCM+FSA-Data*-Loc -> non empty;
 cluster SCM+FSA-Data-Loc -> non empty;
 cluster SCM+FSA-Instr-Loc -> non empty;
end;

reserve J,K for Element of Segm 13,
        a for Element of SCM+FSA-Instr-Loc,
        b,b1,b2,c,c1,c2 for Element of SCM+FSA-Data-Loc,
        f,f1,f2 for Element of SCM+FSA-Data*-Loc;

definition
 func SCM+FSA-Instr -> Subset of [: Segm 13, (union {INT,INT*} \/ INT)* :]
 equals
:: SCMFSA_1:def 4
 SCM-Instr \/ { [J,<*c,f,b*>] : J in {9,10} } \/
                { [K,<*c1,f1*>] : K in {11,12} };
end;

canceled;

theorem :: SCMFSA_1:2
 SCM-Instr c= SCM+FSA-Instr;

definition
 cluster SCM+FSA-Instr -> non empty;
end;

definition
 let I be Element of SCM+FSA-Instr;
 func InsCode I -> Nat equals
:: SCMFSA_1:def 5
 I `1;
end;

theorem :: SCMFSA_1:3
 for I being Element of SCM+FSA-Instr st InsCode I <= 8
  holds I in SCM-Instr;

theorem :: SCMFSA_1:4
   [0,{}] in SCM+FSA-Instr;

definition
 func SCM+FSA-OK ->
  Function of INT, {INT,INT*} \/ { SCM+FSA-Instr, SCM+FSA-Instr-Loc } equals
:: SCMFSA_1:def 6
 (INT --> INT*) +* SCM-OK +*
              ((SCM-Instr.-->SCM+FSA-Instr)*(SCM-OK|SCM-Instr-Loc));
end;

canceled;

theorem :: SCMFSA_1:6
   x in {9,10} implies [x,<*c,f,b*>] in SCM+FSA-Instr;

theorem :: SCMFSA_1:7
   x in {11,12} implies [x,<*c,f*>] in SCM+FSA-Instr;

theorem :: SCMFSA_1:8
 INT = {0} \/ SCM+FSA-Data-Loc \/ SCM+FSA-Data*-Loc \/ SCM+FSA-Instr-Loc;

theorem :: SCMFSA_1:9
 SCM+FSA-OK.0 = SCM+FSA-Instr-Loc;

theorem :: SCMFSA_1:10
 SCM+FSA-OK.b = INT;

theorem :: SCMFSA_1:11
 SCM+FSA-OK.a = SCM+FSA-Instr;

theorem :: SCMFSA_1:12
 SCM+FSA-OK.f = INT*;

theorem :: SCMFSA_1:13
   SCM+FSA-Instr-Loc <> INT & SCM+FSA-Instr <> INT &
   SCM+FSA-Instr-Loc <> SCM+FSA-Instr &
   SCM+FSA-Instr-Loc <> INT* & SCM+FSA-Instr <> INT*;

theorem :: SCMFSA_1:14
   for i being Integer st SCM+FSA-OK.i = SCM+FSA-Instr-Loc
  holds i = 0;

theorem :: SCMFSA_1:15
   for i being Integer st SCM+FSA-OK.i = INT
  holds i in SCM+FSA-Data-Loc;

theorem :: SCMFSA_1:16
   for i being Integer st SCM+FSA-OK.i = SCM+FSA-Instr
  holds i in SCM+FSA-Instr-Loc;

theorem :: SCMFSA_1:17
   for i being Integer st SCM+FSA-OK.i = INT*
  holds i in SCM+FSA-Data*-Loc;

definition
 mode SCM+FSA-State is Element of product SCM+FSA-OK;
end;

theorem :: SCMFSA_1:18
 for s being SCM+FSA-State, I being Element of SCM-Instr
  holds s|NAT +* (SCM-Instr-Loc --> I) is SCM-State;

theorem :: SCMFSA_1:19
 for s being SCM+FSA-State, s' being SCM-State
  holds s +* s' +* s|SCM+FSA-Instr-Loc is SCM+FSA-State;



definition let s be SCM+FSA-State, u be Element of SCM+FSA-Instr-Loc;
 func SCM+FSA-Chg(s,u) -> SCM+FSA-State equals
:: SCMFSA_1:def 7
  s +* (0 .--> u);
end;

definition
 let s be SCM+FSA-State, t be Element of SCM+FSA-Data-Loc, u be Integer;
 func SCM+FSA-Chg(s,t,u) -> SCM+FSA-State equals
:: SCMFSA_1:def 8
  s +* (t .--> u);
end;

definition
 let s be SCM+FSA-State, t be Element of SCM+FSA-Data*-Loc,
     u be FinSequence of INT;
 func SCM+FSA-Chg(s,t,u) -> SCM+FSA-State equals
:: SCMFSA_1:def 9
  s +* (t .--> u);
end;

definition let s be SCM+FSA-State, a be Element of SCM+FSA-Data-Loc;
 redefine
  func s.a -> Integer;
end;

definition let s be SCM+FSA-State, a be Element of SCM+FSA-Data*-Loc;
 redefine
  func s.a -> FinSequence of INT;
end;

definition let x be Element of SCM+FSA-Instr;
 given c,f,b,J such that
 x = [ J, <*c,f,b*>];
 func x int_addr1 -> Element of SCM+FSA-Data-Loc means
:: SCMFSA_1:def 10
     ex c,f,b st <*c,f,b*> = x`2 & it = c;
 func x int_addr2 -> Element of SCM+FSA-Data-Loc means
:: SCMFSA_1:def 11
     ex c,f,b st <*c,f,b*> = x`2 & it = b;
 func x coll_addr1 -> Element of SCM+FSA-Data*-Loc means
:: SCMFSA_1:def 12
     ex c,f,b st <*c,f,b*> = x`2 & it = f;
end;

definition let x be Element of SCM+FSA-Instr;
 given c,f,J such that
 x = [ J, <*c,f*>];
 func x int_addr3 -> Element of SCM+FSA-Data-Loc means
:: SCMFSA_1:def 13
     ex c,f st <*c,f*> = x`2 & it = c;
 func x coll_addr2 -> Element of SCM+FSA-Data*-Loc means
:: SCMFSA_1:def 14
    ex c,f st <*c,f*> = x`2 & it = f;
end;

definition let l be Element of SCM+FSA-Instr-Loc;
 func Next l -> Element of SCM+FSA-Instr-Loc means
:: SCMFSA_1:def 15
     ex L being Element of SCM-Instr-Loc st L = l & it = Next L;
end;

definition let s be SCM+FSA-State;
 func IC(s) -> Element of SCM+FSA-Instr-Loc equals
:: SCMFSA_1:def 16
     s.0;
end;

definition let x be Element of SCM+FSA-Instr, s be SCM+FSA-State;
 func SCM+FSA-Exec-Res(x,s) -> SCM+FSA-State means
:: SCMFSA_1:def 17
     ex x' being Element of SCM-Instr, s' being SCM-State st
    x = x' & s' = s|NAT +* (SCM-Instr-Loc --> x')
           & it = s +* SCM-Exec-Res(x',s') +* s|SCM+FSA-Instr-Loc
      if InsCode x <= 8,
 ex i being Integer, k st k = abs(s.(x int_addr2)) & i = (s.(x coll_addr1))/.k
   & it = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr1,i),Next IC s)
    if InsCode x = 9,
    ex f being FinSequence of INT,k st k = abs(s.(x int_addr2)) &
     f = s.(x coll_addr1)+*(k,s.(x int_addr1)) &
     it = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr1,f),Next IC s)
    if InsCode x = 10,
  it = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr3,len(s.(x coll_addr2))),Next IC s)
    if InsCode x = 11,
  ex f being FinSequence of INT,k st k = abs(s.(x int_addr3)) & f = k |-> 0
    & it = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr2,f),Next IC s)
    if InsCode x = 12
     otherwise it = s;
end;

definition
 func SCM+FSA-Exec ->
  Function of SCM+FSA-Instr, Funcs(product SCM+FSA-OK, product SCM+FSA-OK)
         means
:: SCMFSA_1:def 18
    for x being Element of SCM+FSA-Instr, y being SCM+FSA-State holds
    (it.x qua Element of Funcs(product SCM+FSA-OK, product SCM+FSA-OK)).y =
    SCM+FSA-Exec-Res(x,y);
end;

theorem :: SCMFSA_1:20
   for s being SCM+FSA-State, u being Element of SCM+FSA-Instr-Loc
  holds SCM+FSA-Chg(s,u).0 = u;

theorem :: SCMFSA_1:21
   for s being SCM+FSA-State, u being Element of SCM+FSA-Instr-Loc,
     mk being Element of SCM+FSA-Data-Loc
  holds SCM+FSA-Chg(s,u).mk = s.mk;

theorem :: SCMFSA_1:22
   for s being SCM+FSA-State, u being Element of SCM+FSA-Instr-Loc,
     p being Element of SCM+FSA-Data*-Loc
  holds SCM+FSA-Chg(s,u).p = s.p;

theorem :: SCMFSA_1:23
   for s being SCM+FSA-State, u,v being Element of SCM+FSA-Instr-Loc
  holds SCM+FSA-Chg(s,u).v = s.v;

theorem :: SCMFSA_1:24
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data-Loc, u being Integer
  holds SCM+FSA-Chg(s,t,u).0 = s.0;

theorem :: SCMFSA_1:25
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data-Loc, u being Integer
  holds SCM+FSA-Chg(s,t,u).t = u;

theorem :: SCMFSA_1:26
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data-Loc, u being Integer,
     mk being Element of SCM+FSA-Data-Loc st mk <> t
  holds SCM+FSA-Chg(s,t,u).mk = s.mk;

theorem :: SCMFSA_1:27
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data-Loc, u being Integer,
     f being Element of SCM+FSA-Data*-Loc
  holds SCM+FSA-Chg(s,t,u).f = s.f;

theorem :: SCMFSA_1:28
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data-Loc, u being Integer,
     v being Element of SCM+FSA-Instr-Loc
  holds SCM+FSA-Chg(s,t,u).v = s.v;

theorem :: SCMFSA_1:29
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data*-Loc, u being FinSequence of INT
  holds SCM+FSA-Chg(s,t,u).t = u;

theorem :: SCMFSA_1:30
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data*-Loc, u being FinSequence of INT,
     mk being Element of SCM+FSA-Data*-Loc st mk <> t
  holds SCM+FSA-Chg(s,t,u).mk = s.mk;

theorem :: SCMFSA_1:31
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data*-Loc, u being FinSequence of INT,
     a being Element of SCM+FSA-Data-Loc
  holds SCM+FSA-Chg(s,t,u).a = s.a;

theorem :: SCMFSA_1:32
   for s being SCM+FSA-State,
     t being Element of SCM+FSA-Data*-Loc, u being FinSequence of INT,
     v being Element of SCM+FSA-Instr-Loc
  holds SCM+FSA-Chg(s,t,u).v = s.v;
The abstract of the Mizar article:

An Extension of \bf SCM
