:: On the Instructions of { \bf SCM }
::  by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001 Association of Mizar Users

environ

 vocabularies AMI_3, AMI_1, ORDINAL2, ARYTM, AMI_2, CAT_1, BOOLE, FUNCT_7,
      FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, FINSEQ_1, AMISTD_2, AMI_5, AMISTD_1,
      SETFAM_1, REALSET1, TARSKI, SGRAPH1, GOBOARD5, FRECHET, ARYTM_1, NAT_1,
      UNIALG_1, CARD_5, CARD_3, RELOC;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2,
      REALSET1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, FUNCOP_1, FINSEQ_1,
      FUNCT_4, XXREAL_0, STRUCT_0, CARD_3, FUNCT_7, AMI_1, AMI_2, AMI_3,
      AMISTD_1, AMISTD_2, SCMNORM;
 constructors XXREAL_0, NAT_1, NAT_D, REALSET1, AMI_5, AMISTD_2;
 registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FRAENKEL, NUMBERS, XREAL_0, NAT_1, INT_1, FINSEQ_1, CARD_3, AMI_1, AMI_3,
      AMI_5, SCMRING1, AMISTD_2, REALSET1;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

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

theorem :: AMI_6:1
  not a in NAT;

theorem :: AMI_6:2
  SCM-Data-Loc <> NAT;

theorem :: AMI_6:3
  for o being Object of SCM holds o = IC SCM or o in NAT or o is Data-Location;

canceled;

theorem :: AMI_6:5
  s1,s2 equal_outside NAT implies s1.a = s2.a;

canceled;

theorem :: AMI_6:7
  AddressPart halt SCM = {};

canceled 8;

theorem :: AMI_6:16
  T = 0 implies AddressParts T = {0};

registration
  let T;
  cluster AddressParts T -> non empty;
end;

theorem :: AMI_6:17
  T = 1 implies dom product" AddressParts T = {1,2};

theorem :: AMI_6:18
  T = 2 implies dom product" AddressParts T = {1,2};

theorem :: AMI_6:19
  T = 3 implies dom product" AddressParts T = {1,2};

theorem :: AMI_6:20
  T = 4 implies dom product" AddressParts T = {1,2};

theorem :: AMI_6:21
  T = 5 implies dom product" AddressParts T = {1,2};

theorem :: AMI_6:22
  T = 6 implies dom product" AddressParts T = {1};

theorem :: AMI_6:23
  T = 7 implies dom product" AddressParts T = {1,2};

theorem :: AMI_6:24
  T = 8 implies dom product" AddressParts T = {1,2};

theorem :: AMI_6:25
  (product" AddressParts InsCode (a:=b)).1 = SCM-Data-Loc;

theorem :: AMI_6:26
  (product" AddressParts InsCode (a:=b)).2 = SCM-Data-Loc;

theorem :: AMI_6:27
  (product" AddressParts InsCode AddTo(a,b)).1 = SCM-Data-Loc;

theorem :: AMI_6:28
  (product" AddressParts InsCode AddTo(a,b)).2 = SCM-Data-Loc;

theorem :: AMI_6:29
  (product" AddressParts InsCode SubFrom(a,b)).1 = SCM-Data-Loc;

theorem :: AMI_6:30
  (product" AddressParts InsCode SubFrom(a,b)).2 = SCM-Data-Loc;

theorem :: AMI_6:31
  (product" AddressParts InsCode MultBy(a,b)).1 = SCM-Data-Loc;

theorem :: AMI_6:32
  (product" AddressParts InsCode MultBy(a,b)).2 = SCM-Data-Loc;

theorem :: AMI_6:33
  (product" AddressParts InsCode Divide(a,b)).1 = SCM-Data-Loc;

theorem :: AMI_6:34
  (product" AddressParts InsCode Divide(a,b)).2 = SCM-Data-Loc;

theorem :: AMI_6:35
  (product" AddressParts InsCode goto i1).1 = NAT;

theorem :: AMI_6:36
  (product" AddressParts InsCode (a =0_goto i1)).1 = NAT;

theorem :: AMI_6:37
  (product" AddressParts InsCode (a =0_goto i1)).2 = SCM-Data-Loc;

theorem :: AMI_6:38
  (product" AddressParts InsCode (a >0_goto i1)).1 = NAT;

theorem :: AMI_6:39
  (product" AddressParts InsCode (a >0_goto i1)).2 = SCM-Data-Loc;

theorem :: AMI_6:40
  NIC(halt SCM, il) = {il};

registration
  cluster JUMP halt SCM -> empty;
end;

theorem :: AMI_6:41
  NIC(a := b, il) = {Next il};

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

theorem :: AMI_6:42
  NIC(AddTo(a,b), il) = {Next il};

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

theorem :: AMI_6:43
  NIC(SubFrom(a,b), il) = {Next il};

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

theorem :: AMI_6:44
  NIC(MultBy(a,b), il) = {Next il};

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

theorem :: AMI_6:45
  NIC(Divide(a,b), il) = {Next il};

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

theorem :: AMI_6:46
  NIC(goto i1, il) = {i1};

theorem :: AMI_6:47
  JUMP goto i1 = {i1};

registration
  let i1;
  cluster JUMP goto i1 -> non empty trivial;
end;

theorem :: AMI_6:48
  NIC(a=0_goto i1, il) = {i1, Next il};

theorem :: AMI_6:49
  JUMP (a=0_goto i1) = {i1};

registration
  let a, i1;
  cluster JUMP (a =0_goto i1) -> non empty trivial;
end;

theorem :: AMI_6:50
  NIC(a>0_goto i1, il) = {i1, Next il};

theorem :: AMI_6:51
  JUMP (a>0_goto i1) = {i1};

registration
  let a, i1;
  cluster JUMP (a >0_goto i1) -> non empty trivial;
end;

theorem :: AMI_6:52
  SUCC il = {il, Next il};

theorem :: AMI_6:53
  for f being IL-Function of NAT, SCM
  st for k being Element of NAT holds f.k = il.k holds f is bijective &
  for k being Element of NAT holds f.(k+1) in SUCC (f.k) &
  for j being Element of NAT st f.j in SUCC (f.k) holds k <= j;

registration
  cluster SCM -> standard;
end;

theorem :: AMI_6:54
  il.(SCM,k) = il.k;

theorem :: AMI_6:55
  Next il.(SCM,k) = il.(SCM,k+1);

theorem :: AMI_6:56
  Next il = NextLoc il;

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

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

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

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

registration
  let a, i1;
  cluster InsCode (a =0_goto i1) -> jump-only InsType of SCM;
  cluster InsCode (a >0_goto i1) -> jump-only InsType 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 InsType of SCM;
  cluster InsCode AddTo(a,b) -> non jump-only InsType of SCM;
  cluster InsCode SubFrom(a,b) -> non jump-only InsType of SCM;
  cluster InsCode MultBy(a,b) -> non jump-only InsType of SCM;
  cluster InsCode Divide(a,b) -> non jump-only InsType of SCM;
end;

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

registration
  cluster SCM -> homogeneous with_explicit_jumps without_implicit_jumps;
end;

registration
  cluster SCM -> regular;
end;

theorem :: AMI_6:57
  IncAddr(goto i1,k) = goto il.(SCM, locnum i1 + k);

theorem :: AMI_6:58
  IncAddr(a=0_goto i1,k) = a=0_goto il.(SCM, locnum i1 + k);

theorem :: AMI_6:59
  IncAddr(a>0_goto i1,k) = a>0_goto il.(SCM, locnum i1 + k);

registration
  cluster SCM -> IC-good Exec-preserving;
end;