:: Development of Terminology for {\bf SCM}
::  by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-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, INT_1, FINSEQ_1, SUBSET_1, FSM_1, AMI_3, PARTFUN1,
      AMI_1, EXTPRO_1, RELAT_1, FUNCT_1, CIRCUIT2, MSUALG_1, ARYTM_3, XXREAL_0,
      CARD_1, TARSKI, AFINSQ_1, ORDINAL4, GRAPHSP, ARYTM_1, SCM_1, STRUCT_0,
      RECDEF_2, FUNCT_4, CAT_1, GOBRD13, MEMSTR_0, NAT_1;
 notations TARSKI, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
      INT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, XXREAL_0, AFINSQ_1, FUNCT_4,
      RECDEF_2, STRUCT_0, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_3;
 constructors AMI_3, RELSET_1, PRE_POLY, XTUPLE_0;
 registrations ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1, AMI_3, AFINSQ_1,
      RELAT_1, PBOOLE, FINSEQ_1, STRUCT_0, VALUED_0, FUNCT_4, COMPOS_0,
      XTUPLE_0, MEMSTR_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

registration let i1 be Integer;
 cluster <%i1%> -> INT-valued;
 let i2 be Integer;
 cluster <%i1,i2%> -> INT-valued;
 let i3 be Integer;
 cluster <%i1,i2,i3%> -> INT-valued;
 let i4 be Integer;
 cluster <%i1,i2,i3,i4%> -> INT-valued;
end;

definition
  let D be XFinSequence of INT;
  mode State-consisting of D -> State of SCM means
:: SCM_1:def 1

   for k being Element of NAT st k < len D holds it.dl.k = D.k;
end;

registration
  let D be XFinSequence of INT, il be Element of NAT;
 cluster il-started for State-consisting of D;
end;

theorem :: SCM_1:1
  for i1, i2, i3, i4 being Integer, il being Element of NAT,
 s being il-started State-consisting of <%i1,i2,i3,i4%>
holds
  s.dl.0 = i1 & s.dl.1 = i2 & s.dl.2 = i3 & s.dl.3 = i4;

theorem :: SCM_1:2
  for i1, i2 being Integer, il being Element of NAT,
  s being il-started State-consisting of <%i1,i2%> holds
   s.dl.0 = i1 & s.dl.1 = i2;

theorem :: SCM_1:3
  for I1, I2 being Instruction of SCM
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
   st <%I1%>^<%I2%> c= F
   holds F.0 = I1 & F.1 = I2;

reserve F for total
  NAT-defined (the InstructionsF of SCM)-valued Function;

theorem :: SCM_1:4
  for k, n being Element of NAT, s being State of SCM,
    a, b being Data-Location st
  IC Comput(F,s,k) = n & F.n = a := b
 holds IC Comput(F,s,k+1) = n+1 &
  Comput(F,s,k+1).a = Comput(F,s,k).b &
  for d being Data-Location st d <> a
   holds Comput(F,s,k+1).d = Comput(F,s,k).d;

theorem :: SCM_1:5
  for k, n being Element of NAT, s being State of SCM, a, b being
  Data-Location st IC Comput(F,s,k) = n & F.n = AddTo(a,b)
  holds IC Comput(F,s,k+1) = n+1 &
    Comput(F,s,k+1).a = Comput(F,s,k).a+
Comput(F,s,k).b & for d being Data-Location st d <> a holds Comput
(F,s,k+
  1).d = Comput(F,s,k).d;

theorem :: SCM_1:6
  for k, n being Element of NAT, s being State of SCM, a, b being
  Data-Location st IC Comput(F,s,k) = n & F.n = SubFrom(a,b)
   holds IC Comput(F,s,k+1) = n+1 &
   Comput(F,s,k+1).a =
Comput(F,s,k).a-
Comput(F,s,k).b & for d being Data-Location st d <> a holds Comput
(F,s,k+
  1).d = Comput(F,s,k).d;

theorem :: SCM_1:7
  for k, n being Element of NAT, s being State of SCM, a, b being
  Data-Location st IC Comput(F,s,k) = n & F.n = MultBy(a,b) holds
IC
  Comput(F,s,k+1) = (n+1) & Comput(F,s,k+1).a =
Comput(F,s,k).a*
Comput(F,s,k).b & for d being Data-Location st d <> a holds Comput
(F,s,k+
  1).d = Comput(F,s,k).d;

theorem :: SCM_1:8
  for k, n being Element of NAT, s being State of SCM, a, b being
Data-Location st IC Comput(F,s,k) = n & F.n = Divide(a,b) & a<>b
holds
  IC Comput(F,s,k+1) = (n+1) & Comput(F,s,k+1).a =
Comput(F,s,k).a
  div Comput(F,s,k).b & Comput(F,s,k+1).b = Comput(
F,s,k).a mod
  Comput(F,s,k).b & for d being Data-Location st d <> a & d <> b
holds
  Comput(F,s,k+1).d = Comput(F,s,k).d;

theorem :: SCM_1:9
  for k, n being Element of NAT, s being State of SCM, il being
  Element of NAT st IC Comput(F,s,k) = n &
   F.n = SCM-goto il
holds IC Comput(F,s,k+1) = il & for d being Data-Location holds
   Comput(F,s,k+1).d = Comput(F,s,k).d;

theorem :: SCM_1:10
  for k, n being Nat, s being State of SCM, a being
  Data-Location, il being Element of NAT st IC Comput(F,s,k) =
  n & F.n = a =0_goto il holds ( Comput(F,s,k).a = 0 implies IC
Comput(F,s,k+1) = il) & ( Comput(F,s,k).a <>0 implies
IC Comput(F,s,k+
  1) = (n+1)) & for d being Data-Location holds Comput(F,s,k+1).d
=
  Comput(F,s,k).d;

theorem :: SCM_1:11
  for k, n being Element of NAT, s being State of SCM, a being
  Data-Location, il being Element of NAT st IC Comput(F,s,k) =
  n & F.n = a >0_goto il holds ( Comput(F,s,k).a > 0 implies IC
Comput(F,s,k+1) = il) & ( Comput(F,s,k).a <= 0
implies IC Comput(F,s,k
  +1) = (n+1)) & for d being Data-Location holds Comput(F,s,k+1).d
=
  Comput(F,s,k).d;

theorem :: SCM_1:12
  (halt SCM)`1_3 = 0 &
  (for a, b being Data-Location holds (a := b)`1_3 = 1) &
  (for a, b being Data-Location holds (AddTo(a,b))`1_3 = 2) &
  (for a, b being Data-Location holds (SubFrom(a,b))`1_3 = 3) &
  (for a, b being Data-Location holds (MultBy(a,b))`1_3 = 4) &
  (for a, b being Data-Location holds (Divide(a,b))`1_3 = 5) &
  (for i being Element of NAT holds (SCM-goto i)`1_3 = 6) &
  (for a being Data-Location, i being Element of NAT
   holds (a =0_goto i)`1_3 = 7) &
  for a being Data-Location, i being Element of NAT holds
   (a >0_goto i)`1_3 = 8;

theorem :: SCM_1:13
  for i1, i2, i3, i4 being Integer,
  s being State of SCM st s.dl.0 = i1 & s.dl.1 = i2 & s.dl.2 = i3 & s.dl.3 = i4
   holds s is State-consisting of <%i1,i2,i3,i4%>;

:: Empty program

theorem :: SCM_1:14
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%halt SCM%> c= F
  for s being 0-started State-consisting of <*>INT
   holds F halts_on s & LifeSpan(F,s) = 0 & Result(F,s) = s;

:: Assignment

theorem :: SCM_1:15
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%dl.0 := dl.1%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      s being 0-started State-consisting of <%i1,i2%>
   holds F halts_on s & LifeSpan(F,s) = 1 & (Result(F,s)).dl.0 = i2 &
  for d being Data-Location st d<>dl.0
   holds (Result(F,s)).d = s.d;

:: Adding two integers

theorem :: SCM_1:16
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%AddTo(dl.0,dl.1)%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      s being 0-started State-consisting of <%i1,i2%>
  holds F halts_on s & LifeSpan(F,s) = 1 & (Result(F,s)).dl.0 = i1 + i2 &
  for d being Data-Location st d<>dl.0 holds Result(F,s).d = s.d;

:: Subtracting two integers

theorem :: SCM_1:17
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%SubFrom(dl.0,dl.1)%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      s being 0-started State-consisting of <%i1,i2%>
    holds F halts_on s
 & LifeSpan(F,s) = 1 &
 (Result(F,s)).dl.0 = i1 - i2 & for d being Data-Location
st d<>dl.0 holds
  (Result(F,s)).d = s.d;

:: Multiplying two integers

theorem :: SCM_1:18
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%MultBy(dl.0,dl.1)%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
     s being 0-started State-consisting of <%i1,i2%>
  holds F halts_on s & LifeSpan(F,s) = 1 & (Result(F,s)).dl.0 = i1 * i2 &
   for d being Data-Location st d<>dl.0 holds (Result(F,s)).d = s.d;

:: Dividing two integers

theorem :: SCM_1:19
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%Divide(dl.0,dl.1)%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
    s being 0-started State-consisting of  <%i1,i2%>
   holds F halts_on s
 & LifeSpan(F,s)
  = 1 & (Result(F,s)).dl.0 = i1 div i2 & (Result(F,s)
).dl.1 = i1 mod i2 & for d being
  Data-Location st d<>dl.0 & d<>dl.1 holds (Result(F,s)).d = s.d;

:: Unconditional jump

theorem :: SCM_1:20
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%SCM-goto 1%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      s being 0-started State-consisting of <%i1,i2%>
    holds F halts_on s &
 LifeSpan(F,s) = 1 & for d
  being Data-Location holds (Result(F,s)).d = s.d;

:: Jump at zero

theorem :: SCM_1:21
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%dl.0=0_goto 1%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      s being 0-started State-consisting of <%i1,i2%>
    holds F halts_on s
 & LifeSpan(F,s) = 1
  & for d being Data-Location holds (Result(F,s)).d = s.d;

:: Jump at greater than zero

theorem :: SCM_1:22
  for F being total
   NAT-defined (the InstructionsF of SCM)-valued Function
    st <%dl.0>0_goto 1%>^<%halt SCM%> c= F
  for i1, i2 being Integer,
      s being 0-started State-consisting of <%i1,i2%>
    holds F halts_on s
 & LifeSpan(F,s) = 1
  & for d being Data-Location holds (Result(F,s)).d = s.d;

theorem :: SCM_1:23
 for s being State of SCM holds s is State-consisting of <*>INT;