:: The Construction of { \bf SCM } over Ring
::  by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998-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, CARD_1, AMI_2, XBOOLE_0, STRUCT_0, ZFMISC_1,
      RELAT_1, FINSEQ_1, FUNCSDOM, FUNCT_1, AMI_1, PARTFUN1, TARSKI, SCMRING1,
      RECDEF_2, ALGSTR_0, UNIALG_1, AMISTD_2, VALUED_0, COMPOS_0, XXREAL_0,
      NAT_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1,
      FUNCT_1, PARTFUN1, VALUED_0, ORDINAL1, CARD_1, RECDEF_2, XXREAL_0,
      NUMBERS, STRUCT_0, ALGSTR_0, VECTSP_1, MCART_1, FINSEQ_1, FINSEQ_4,
      COMPOS_0, SCM_INST;
 constructors FINSEQ_4, REALSET2, FINSEQ_2, COMPOS_1, SCM_INST, VALUED_0,
      XTUPLE_0;
 registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSEQ_1, STRUCT_0, CARD_1, GCD_1,
      FUNCT_1, ALGSTR_0, ALGSTR_1, COMPOS_0, SCM_INST, XXREAL_0, VALUED_0,
      XTUPLE_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE;


begin  :: The construction of { \bf SCM } over ring

reserve i, j, k for Nat,
  I for Element of Segm 8,
  i1, i2 for Nat,
  d1, d2, d3, d4 for Element of SCM-Data-Loc,
  S for non empty 1-sorted;

registration
  cluster SCM-Instr -> non trivial;
end;

definition
  let S be non empty 1-sorted;
  func SCM-Instr S -> non empty set equals
:: SCMRINGI:def 1
  { [0,{},{}] }
   \/ { [I,{},<*a,b*>] where I is Element of Segm 8,
    a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } }
   \/ (the set of all  [6,<*i*>,{}] where i is Nat)
   \/ (the set of all
 [7,<*i*>,<*a*>] where i is Nat,a is Element of SCM-Data-Loc)
 \/ (the set of all  [5,{},<*a,r*>] where a is
  Element of SCM-Data-Loc, r is Element of S);
end;

registration
  let S be non empty 1-sorted;
  cluster SCM-Instr S -> non trivial;
end;

reserve G for non empty 1-sorted;

definition
  let S be non empty 1-sorted, x be Element of SCM-Instr S;
  given mk, ml being Element of SCM-Data-Loc, I such that
 x = [I,{},<*mk,ml*>];
  func x address_1 -> Element of SCM-Data-Loc means
:: SCMRINGI:def 2

  ex f being
  FinSequence of SCM-Data-Loc st f = x`3_3 & it = f/.1;
  func x address_2 -> Element of SCM-Data-Loc means
:: SCMRINGI:def 3

  ex f being
  FinSequence of SCM-Data-Loc st f = x`3_3 & it = f/.2;
end;

theorem :: SCMRINGI:1
  for x being Element of SCM-Instr S, mk, ml being Element of
SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds x address_1 = mk & x address_2 = ml;

definition
  let R be non empty 1-sorted, x be Element of SCM-Instr R;
  given mk being Element of NAT, I such that
 x = [I,<*mk*>,{}];
  func x jump_address -> Element of NAT means
:: SCMRINGI:def 4

  ex f being FinSequence of
  NAT st f = x`2_3 & it = f/.1;
end;

theorem :: SCMRINGI:2
  for x being Element of SCM-Instr S, mk being Nat
   st x = [ I,<*mk*>,{}] holds x jump_address = mk;

definition
  let S be non empty 1-sorted, x be Element of SCM-Instr S;
  given mk being Element of NAT, ml being Element of SCM-Data-Loc, I such that
 x = [I,<*mk*>,<*ml*>];
  func x cjump_address -> Element of NAT means
:: SCMRINGI:def 5

  ex mk being Element of NAT st <*mk*> = x`2_3 & it = <*mk*>/.1;
  func x cond_address -> Element of SCM-Data-Loc means
:: SCMRINGI:def 6

  ex ml being Element of SCM-Data-Loc st <*ml*> = x`3_3 & it = <*ml*>/.1;
end;

theorem :: SCMRINGI:3
  for x being Element of SCM-Instr S, mk being Element of NAT, ml being
  Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>]
   holds x cjump_address = mk & x
  cond_address = ml;

definition
  let S be non empty 1-sorted, d be Element of SCM-Data-Loc, s be Element of S;
  redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S;
end;

definition
  let S be non empty 1-sorted, x be Element of SCM-Instr S;
  given mk being Element of SCM-Data-Loc, r being Element of S, I such that
 x = [I,{},<*mk,r*>];
  func x const_address -> Element of SCM-Data-Loc means
:: SCMRINGI:def 7

  ex f being
  FinSequence of SCM-Data-Loc \/ the carrier of S st f = x`3_3 & it = f/.1;
  func x const_value -> Element of S means
:: SCMRINGI:def 8

  ex f being FinSequence of
  SCM-Data-Loc \/ the carrier of S st f = x`3_3 & it = f/.2;
end;

theorem :: SCMRINGI:4
  for x being Element of SCM-Instr S, mk being Element of SCM-Data-Loc,
  r being Element of S st x = [I,{},<*mk,r*>] holds x const_address = mk & x
  const_value = r;

theorem :: SCMRINGI:5
 for S being non empty 1-sorted
  holds  SCM-Instr S c= [:NAT,NAT*,proj2 SCM-Instr S:];

registration let S be non empty 1-sorted;
 cluster proj2 SCM-Instr S -> FinSequence-membered;
end;

theorem :: SCMRINGI:6
  [0,{},{}] in SCM-Instr S;

theorem :: SCMRINGI:7
  for S being non empty 1-sorted
  for x being Element of SCM-Instr S holds
  x in { [0,{},{}] } & InsCode x = 0 or
  x in { [I,{},<*a,b*>] where I is Element of Segm 8,
    a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } }
     & (InsCode x = 1 or InsCode x = 2 or InsCode x = 3
         or InsCode x = 4) or
  x in the set of all  [6,<*i*>,{}] where i is Nat
        & InsCode x = 6 or
  x in the set of all  [7,<*i*>,<*a*>]
       where i is Nat,a is Element of SCM-Data-Loc
    & InsCode x = 7 or
  x in the set of all  [5,{},<*a,r*>] where a is
  Element of SCM-Data-Loc, r is Element of S
    & InsCode x = 5;

begin :: from SCMRING2

reserve I for Element of Segm 8,
  S for non empty 1-sorted,
  t for Element of S,
  x for set,
  k for Nat;

registration
  cluster strict trivial for Ring;
end;

registration
  let R be Ring;
 cluster SCM-Instr R -> standard-ins;
end;

registration
  let R be Ring;
 cluster SCM-Instr R -> homogeneous;
end;

 reserve R for Ring, T for InsType of SCM-Instr R;

registration
  let R be Ring;
  cluster SCM-Instr R -> J/A-independent;
end;

reserve R for Ring,
  r for Element of R,
  a, b, c, d1, d2 for Element of SCM-Data-Loc;
reserve i1 for Nat;

theorem :: SCMRINGI:8
  x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S;

theorem :: SCMRINGI:9
  [5,{},<*d1,t*>] in SCM-Instr S;

theorem :: SCMRINGI:10
  [6,<*i1*>,{}] in SCM-Instr S;

theorem :: SCMRINGI:11
  [7,<*i1*>,<*d1*>] in SCM-Instr S;

registration let S;
 cluster SCM-Instr S -> with_halt;
end;