:: On the Instructions of { \bf SCM }
::  by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001-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, AMI_3, AMI_1, FSM_1, ORDINAL1, CAT_1, XBOOLE_0, FUNCT_1,
      RELAT_1, FINSEQ_1, CARD_1, AMISTD_2, GRAPHSP, CARD_3, AMISTD_1, SUBSET_1,
      CIRCUIT2, FUNCT_4, FUNCOP_1, SETFAM_1, XXREAL_0, TARSKI, ARYTM_3,
      GOBOARD5, FRECHET, ARYTM_1, INT_1, PARTFUN1, NAT_1, COMPOS_1, GOBRD13,
      MEMSTR_0;
 notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, FUNCOP_1, PARTFUN1, FINSEQ_1,
      FUNCT_4, XXREAL_0, VALUED_1, CARD_3, FUNCT_7, MEMSTR_0, COMPOS_0,
      COMPOS_1, EXTPRO_1, AMI_3, AMISTD_1, AMISTD_2;
 constructors NAT_D, AMI_3, AMISTD_2, RELSET_1, AMISTD_1, PRE_POLY, FUNCT_7,
      DOMAIN_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, NAT_1,
      INT_1, FINSEQ_1, CARD_3, AMI_3, AMISTD_2, FUNCT_4, VALUED_0, EXTPRO_1,
      FUNCT_7, PRE_POLY, MEMSTR_0, CARD_1, COMPOS_0, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

reserve a, b, d1, d2 for Data-Location,
  il, i1, i2 for Nat,
  I for Instruction of SCM,
  s, s1, s2 for State of SCM,
  T for InsType of the InstructionsF of SCM,
  k,k1 for Nat;

theorem :: AMI_6:1
 T = 0 or ... or T = 8;

theorem :: AMI_6:2
  JumpPart halt SCM = {};

theorem :: AMI_6:3
  T = 0 implies JumpParts T = {0};

theorem :: AMI_6:4
  T = 1 implies JumpParts T = {{}};

theorem :: AMI_6:5
  T = 2 implies JumpParts T = {{}};

theorem :: AMI_6:6
  T = 3 implies JumpParts T = {{}};

theorem :: AMI_6:7
  T = 4 implies JumpParts T = {{}};

theorem :: AMI_6:8
  T = 5 implies JumpParts T = {{}};

theorem :: AMI_6:9
  T = 6 implies dom product" JumpParts T = {1};

theorem :: AMI_6:10
  T = 7 implies dom product" JumpParts T = {1};

theorem :: AMI_6:11
  T = 8 implies dom product" JumpParts T = {1};

theorem :: AMI_6:12
  (product" JumpParts InsCode SCM-goto k1).1 = NAT;

theorem :: AMI_6:13
  (product" JumpParts InsCode (a =0_goto k1)).1 = NAT;

theorem :: AMI_6:14
  (product" JumpParts InsCode (a >0_goto k1)).1 = NAT;

registration
  cluster JUMP halt SCM -> empty;
end;

registration
  let a, b;
  cluster a:=b -> sequential;
  cluster AddTo(a,b) -> sequential;
  cluster SubFrom(a,b) -> sequential;
  cluster MultBy(a,b) -> sequential;
  cluster Divide(a,b) -> sequential;
end;

registration
  let a, b;
  cluster JUMP (a := b) -> empty;
end;

registration
  let a, b;
  cluster JUMP AddTo(a, b) -> empty;
end;

registration
  let a, b;
  cluster JUMP SubFrom(a, b) -> empty;
end;

registration
  let a, b;
  cluster JUMP MultBy(a,b) -> empty;
end;

registration
  let a, b;
  cluster JUMP Divide(a,b) -> empty;
end;

theorem :: AMI_6:15
  NIC(SCM-goto k, il) = {k};

theorem :: AMI_6:16
  JUMP SCM-goto k = {k};

registration
  let i1;
  cluster JUMP SCM-goto i1 -> 1-element;
end;

theorem :: AMI_6:17
  NIC(a=0_goto k, il) = {k, il+1};

theorem :: AMI_6:18
  JUMP (a=0_goto k) = {k};

registration
  let a, i1;
  cluster JUMP (a =0_goto i1) -> 1-element;
end;

theorem :: AMI_6:19
  NIC(a>0_goto k, il) = {k, il+1};

theorem :: AMI_6:20
  JUMP (a>0_goto k) = {k};

registration
  let a, i1;
  cluster JUMP (a >0_goto i1) -> 1-element;
end;

theorem :: AMI_6:21
  SUCC(il,SCM) = {il, il+1};

theorem :: AMI_6:22
for k being Nat holds k+1 in SUCC(k,SCM) &
 for j being Nat st j in SUCC(k,SCM) holds k <= j;

registration
  cluster SCM -> standard;
end;

registration
  cluster InsCode halt SCM -> jump-only
   for InsType of the InstructionsF of SCM;
end;

registration
  cluster halt SCM -> jump-only;
end;

registration
  let i1;
  cluster InsCode SCM-goto i1 -> jump-only
  for InsType of the InstructionsF of SCM;
end;

registration
  let i1;
  cluster SCM-goto i1 -> jump-only non sequential non ins-loc-free;
end;

registration
  let a, i1;
  cluster InsCode (a =0_goto i1) -> jump-only
  for InsType of the InstructionsF of SCM;
  cluster InsCode (a >0_goto i1) -> jump-only
  for InsType of the InstructionsF of SCM;
end;

registration
  let a, i1;
  cluster a =0_goto i1 -> jump-only non sequential non ins-loc-free;
  cluster a >0_goto i1 -> jump-only non sequential non ins-loc-free;
end;

registration
  let a, b;
  cluster InsCode (a:=b) -> non jump-only
  for InsType of the InstructionsF of SCM;
  cluster InsCode AddTo(a,b) -> non jump-only
  for InsType of the InstructionsF of SCM;
  cluster InsCode SubFrom(a,b) -> non jump-only
  for InsType of the InstructionsF of SCM;
  cluster InsCode MultBy(a,b) -> non jump-only
  for InsType of the InstructionsF of SCM;
  cluster InsCode Divide(a,b) -> non jump-only
  for InsType of the InstructionsF of SCM;
end;

registration
  let a, b;
  cluster a:=b -> non jump-only;
  cluster AddTo(a,b) -> non jump-only;
  cluster SubFrom(a,b) -> non jump-only;
  cluster MultBy(a,b) -> non jump-only;
  cluster Divide(a,b) -> non jump-only;
end;

registration
  cluster SCM -> with_explicit_jumps;
end;

theorem :: AMI_6:23
  IncAddr(SCM-goto i1,k) = SCM-goto(i1+k);

theorem :: AMI_6:24
  IncAddr(a=0_goto i1,k) = a=0_goto(i1+k);

theorem :: AMI_6:25
  IncAddr(a>0_goto i1,k) = a>0_goto(i1+k);

registration
  cluster SCM -> IC-relocable;
end;