The abstract of the Mizar article:

On the Instructions of SCM

by

Artur Kornilowicz

Received May 8, 2001

MML identifier: AMI_6

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_3, AMI_1, ORDINAL2, ARYTM, AMI_2, CAT_1, BOOLE, FUNCT_7,
      FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, FINSEQ_1, GR_CY_1, AMISTD_2,
      MCART_1, AMI_5, AMISTD_1, SETFAM_1, REALSET1, TARSKI, SGRAPH1, GOBOARD5,
      FRECHET, ARYTM_1, NAT_1, INT_1, UNIALG_1, CARD_5, CARD_3, RELOC;
 notation TARSKI, XBOOLE_0, SUBSET_1, MCART_1, SETFAM_1, RELAT_1, FUNCT_1,
      FUNCT_2, REALSET1, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, INT_1,
      NAT_1, CQC_LANG, FINSEQ_1, FUNCT_4, STRUCT_0, GR_CY_1, CARD_3, FUNCT_7,
      AMI_1, AMI_2, AMI_3, AMI_5, AMISTD_1, AMISTD_2;
 constructors AMI_5, AMISTD_2, DOMAIN_1, NAT_1, FUNCT_7, PRALG_2, MEMBERED;
 clusters AMI_1, RELSET_1, SCMRING1, TEX_2, AMISTD_2, RELAT_1, FUNCT_1, NAT_1,
      CQC_LANG, FINSEQ_1, XBOOLE_0, INT_1, AMI_3, FRAENKEL, AMI_5, MEMBERED,
      ORDINAL2;
 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 the Instruction-Locations of SCM;

theorem :: AMI_6:2
 SCM-Data-Loc <> the Instruction-Locations of SCM;

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

theorem :: AMI_6:4
 i1 <> i2 implies Next i1 <> Next i2;

theorem :: AMI_6:5
 s1,s2 equal_outside the Instruction-Locations of SCM implies s1.a = s2.a;

theorem :: AMI_6:6
 for N being with_non-empty_elements set,
     S being realistic IC-Ins-separated definite
       (non empty non void AMI-Struct over N),
     t, u being State of S,
     il being Instruction-Location of S,
     e being Element of ObjectKind IC S,
     I being Element of ObjectKind il
  st e = il & u = t+*((IC S, il)-->(e, I))
  holds
    u.il = I &
    IC u = il &
    IC Following u = Exec(u.IC u, u).IC S;

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

theorem :: AMI_6:8
 AddressPart (a:=b) = <*a,b*>;

theorem :: AMI_6:9
 AddressPart AddTo(a,b) = <*a,b*>;

theorem :: AMI_6:10
 AddressPart SubFrom(a,b) = <*a,b*>;

theorem :: AMI_6:11
 AddressPart MultBy(a,b) = <*a,b*>;

theorem :: AMI_6:12
 AddressPart Divide(a,b) = <*a,b*>;

theorem :: AMI_6:13
 AddressPart goto i1 = <*i1*>;

theorem :: AMI_6:14
 AddressPart (a=0_goto i1) = <*i1,a*>;

theorem :: AMI_6:15
 AddressPart (a>0_goto i1) = <*i1,a*>;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: AMI_6:35
 (PA AddressParts InsCode goto i1).1 = the Instruction-Locations of SCM;

theorem :: AMI_6:36
 (PA AddressParts InsCode (a =0_goto i1)).1 =
   the Instruction-Locations of SCM;

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

theorem :: AMI_6:38
 (PA AddressParts InsCode (a >0_goto i1)).1 =
   the Instruction-Locations of SCM;

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

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

definition
 cluster JUMP halt SCM -> empty;
end;

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

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

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

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

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

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

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

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

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

definition 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};

definition 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};

definition 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};

definition 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 Function of NAT, the Instruction-Locations of SCM
   st for k being Nat holds f.k = il.k holds
  f is bijective &
  for k being Nat holds f.(k+1) in SUCC (f.k) &
   for j being Nat st f.j in SUCC (f.k) holds k <= j;

definition
 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;

definition
 cluster InsCode halt SCM -> jump-only;
end;

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

definition let i1;
 cluster InsCode goto i1 -> jump-only;
end;

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

definition let a, i1;
 cluster InsCode (a =0_goto i1) -> jump-only;

 cluster InsCode (a >0_goto i1) -> jump-only;
end;

definition 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;

definition let a, b;
 cluster InsCode (a:=b) -> non jump-only;

 cluster InsCode AddTo(a,b) -> non jump-only;

 cluster InsCode SubFrom(a,b) -> non jump-only;

 cluster InsCode MultBy(a,b) -> non jump-only;

 cluster InsCode Divide(a,b) -> non jump-only;
end;

definition 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;

definition
 cluster SCM -> homogeneous with_explicit_jumps without_implicit_jumps;
end;

definition
 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);

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