:: An Extension of { \bf SCM }
::  by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received February 3, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, AMI_2, XBOOLE_0, TARSKI, CARD_1, FINSEQ_1,
      ZFMISC_1, RELAT_1, AMI_1, ORDINAL1, XXREAL_0, FUNCT_1, FUNCOP_1, FUNCT_4,
      INT_1, CARD_3, PBOOLE, NAT_1, PARTFUN1, COMPLEX1, FINSEQ_2, FUNCT_2,
      FUNCT_5, SCMFSA_1, GROUP_9, RECDEF_2, AFINSQ_1, ARYTM_3;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
      CARD_1, NUMBERS, INT_2, PBOOLE, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      BINOP_1, XCMPLX_0, INT_1, AFINSQ_1, FINSEQ_1, FUNCT_4, FUNCT_5, FINSEQ_2,
      CARD_3, FUNCOP_1, FUNCT_7, XXREAL_0, RECDEF_2, MEMSTR_0, SCM_INST, AMI_2,
      SCMFSA_I;
 constructors INT_2, FUNCT_5, RELSET_1, FUNCT_7, PRE_POLY, AMI_3, SCMFSA_I,
      BINOP_1, XTUPLE_0, XFAMILY;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, INT_1, FINSEQ_1,
      CARD_3, AMI_2, RELAT_1, FINSET_1, CARD_1, CARD_2, RELSET_1, FUNCT_2,
      AFINSQ_1, COMPOS_0, SCM_INST, SCMFSA_I;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin

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

notation
  synonym SCM+FSA-Data-Loc for SCM-Data-Loc;
end;

definition
::$CD
  func SCM+FSA-Memory -> set equals
:: SCMFSA_1:def 2
  SCM-Memory \/ SCM+FSA-Data*-Loc;
end;

registration
  cluster SCM+FSA-Memory -> non empty;
end;

theorem :: SCMFSA_1:1
  SCM-Memory c= SCM+FSA-Memory;

definition
  redefine func SCM+FSA-Data-Loc -> Subset of SCM+FSA-Memory;
end;

definition
  redefine func SCM+FSA-Data*-Loc -> Subset of SCM+FSA-Memory;
end;

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

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

definition
::$CD
  func SCM+FSA-OK -> Function of SCM+FSA-Memory, Segm 3 equals
:: SCMFSA_1:def 4
   (SCM+FSA-Memory --> 2) +* SCM-OK;
end;

::$CT 3

theorem :: SCMFSA_1:5
  NAT in SCM+FSA-Memory;

::$CT 2

theorem :: SCMFSA_1:8
  SCM+FSA-Memory = {NAT} \/ SCM+FSA-Data-Loc \/ SCM+FSA-Data*-Loc;

definition
 func SCM*-VAL -> ManySortedSet of Segm 3 equals
:: SCMFSA_1:def 5
  <%NAT,INT,INT*%>;
end;

theorem :: SCMFSA_1:9
  (SCM*-VAL*SCM+FSA-OK).NAT = NAT;

theorem :: SCMFSA_1:10
  (SCM*-VAL*SCM+FSA-OK).b = INT;

theorem :: SCMFSA_1:11
  (SCM*-VAL*SCM+FSA-OK).f = INT*;

registration
 cluster (SCM*-VAL*SCM+FSA-OK) -> non-empty;
end;

definition
  mode SCM+FSA-State is Element of product(SCM*-VAL*SCM+FSA-OK);
end;

::$CT 5

theorem :: SCMFSA_1:17
  for s being SCM+FSA-State, I being Element of SCM-Instr holds s|
  SCM-Memory is SCM-State;

theorem :: SCMFSA_1:18
  for s being SCM+FSA-State, s1 being SCM-State
   holds s +* s1 is SCM+FSA-State;

definition
  let s be SCM+FSA-State, u be Nat;
  func SCM+FSA-Chg(s,u) -> SCM+FSA-State equals
:: SCMFSA_1:def 6
  s +* (NAT .--> 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 7
  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 8
  s +* (t .--> u);
end;

registration
  let s be SCM+FSA-State, a be Element of SCM+FSA-Data-Loc;
  cluster 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
::$CD 6
  let s be SCM+FSA-State;
  func IC(s) -> Element of NAT equals
:: SCMFSA_1:def 15
  s.NAT;
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 16
    ex x9 being Element of SCM-Instr, s9 being SCM-State st
     x = x9 & s9 = s|SCM-Memory &
     it = s +* SCM-Exec-Res(x9,s9)
              if x`1_3 <= 8,
    ex i being Integer, k st
     k = |.s.(x int_addr2).| & i = (s.(x coll_addr1))/.k &
        it = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr1,i),IC s + 1)
              if x`1_3 = 9,
    ex f being FinSequence of INT,k st
     k = |.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),IC s + 1)
              if x`1_3 = 10,
    it =
     SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr3,len(s.(x coll_addr2))),IC s + 1)
              if x`1_3 = 11,
    ex f being FinSequence of INT,k st
     k = |.s.(x int_addr3).| & f = k |-> 0 &
     it = SCM+FSA-Chg(SCM+FSA-Chg(s,x coll_addr2,f),IC s + 1)
              if x`1_3 = 12,
    ex i being Integer st
     i = 1 &
     it = SCM+FSA-Chg(SCM+FSA-Chg(s,x int_addr,i),IC s + 1)
              if x`1_3 = 13
    otherwise it = s;
end;

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

theorem :: SCMFSA_1:19
  for s being SCM+FSA-State, u being Nat holds SCM+FSA-Chg(s,
  u).NAT = u;

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

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

theorem :: SCMFSA_1:22
  for s being SCM+FSA-State, u,v being Nat
   holds SCM+FSA-Chg(s,u).v = s.v;

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

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).t = u;

theorem :: SCMFSA_1:25
  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:26
  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:27
  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:28
  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:29
  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:30
  SCM+FSA-Data*-Loc misses SCM-Memory;

::$CT

theorem :: SCMFSA_1:32
  dom(SCM*-VAL*SCM+FSA-OK) = SCM+FSA-Memory;

theorem :: SCMFSA_1:33
 for s being SCM+FSA-State holds dom s = SCM+FSA-Memory;