The Mizar abstract of SCMRING3

Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users
The abstract of the Mizar article:: The Properties of Instructions of SCM over Ring
by
Artur Kornilowicz
Received April 14, 2000
MML identifier: SCMRING3
[ Mizar article, MML identifier index ]
environ

 vocabulary AMI_3, SCMFSA7B, FUNCSDOM, AMI_1, ORDINAL2, ARYTM, INT_1, FINSET_1,
      INT_3, AMI_2, GR_CY_1, TARSKI, BOOLE, FUNCT_1, FUNCOP_1, CAT_1, FUNCT_7,
      RELAT_1, AMI_5, MCART_1, FINSEQ_1, AMISTD_2, AMISTD_1, FUNCT_4, SETFAM_1,
      REALSET1, RLVECT_1, SGRAPH1, GOBOARD5, ARYTM_1, VECTSP_1, FRECHET,
      UNIALG_1, CARD_5, CARD_3, RELOC;
 notation TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, MCART_1, SETFAM_1, RELAT_1,
      FUNCT_1, FUNCT_2, STRUCT_0, FUNCSDOM, REALSET1, ORDINAL1, ORDINAL2,
      NUMBERS, XCMPLX_0, XREAL_0, NAT_1, RLVECT_1, CQC_LANG, FINSEQ_1, FUNCT_4,
      GR_CY_1, CARD_3, FUNCT_7, VECTSP_1, GROUP_1, AMI_1, AMI_2, AMI_3, AMI_5,
      SCMRING1, SCMRING2, INT_3, AMISTD_1, AMISTD_2;
 constructors AMI_5, AMISTD_2, DOMAIN_1, NAT_1, SCMRING2, FUNCT_7, PRALG_2,
      INT_3, GCD_1, ALGSTR_2, MEMBERED;
 clusters AMI_1, RELSET_1, SCMRING1, SCMRING2, STRUCT_0, TEX_2, AMISTD_2,
      RELAT_1, FUNCT_1, CQC_LANG, FINSEQ_1, INT_1, INT_3, WAYBEL12, XBOOLE_0,
      REVROT_1, AMI_3, NAT_1, VECTSP_1, FRAENKEL, MEMBERED;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

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

definition
 cluster INT -> infinite;
end;

definition
 cluster INT.Ring -> infinite good;
end;

definition
 cluster strict infinite 1-sorted;
end;

definition
 cluster strict infinite good Ring;
end;

theorem :: SCMRING3:1
 ObjectKind a = the carrier of R;

definition
 let R be good Ring;
 let la, lb be Data-Location of R;
 let a, b be Element of R;
 redefine func (la,lb) --> (a,b) -> FinPartState of SCM R;
end;

theorem :: SCMRING3:2
 not a in the Instruction-Locations of SCM R;

theorem :: SCMRING3:3
 a <> IC SCM R;

theorem :: SCMRING3:4
 SCM-Data-Loc <> the Instruction-Locations of SCM R;

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

theorem :: SCMRING3:6
 i1 <> i2 implies Next i1 <> Next i2;

theorem :: SCMRING3:7
 s1,s2 equal_outside the Instruction-Locations of SCM R implies s1.a = s2.a;

theorem :: SCMRING3:8
 InsCode halt SCM R = 0;

theorem :: SCMRING3:9
 InsCode (a:=b) = 1;

theorem :: SCMRING3:10
 InsCode AddTo(a,b) = 2;

theorem :: SCMRING3:11
 InsCode SubFrom(a,b) = 3;

theorem :: SCMRING3:12
 InsCode MultBy(a,b) = 4;

theorem :: SCMRING3:13
 InsCode (a:=r) = 5;

theorem :: SCMRING3:14
 InsCode goto i1 = 6;

theorem :: SCMRING3:15
 InsCode (a=0_goto i1) = 7;

theorem :: SCMRING3:16
 InsCode I = 0 implies I = halt SCM R;

theorem :: SCMRING3:17
 InsCode I = 1 implies ex a, b st I = a:=b;

theorem :: SCMRING3:18
 InsCode I = 2 implies ex a, b st I = AddTo(a,b);

theorem :: SCMRING3:19
 InsCode I = 3 implies ex a, b st I = SubFrom(a,b);

theorem :: SCMRING3:20
 InsCode I = 4 implies ex a, b st I = MultBy(a,b);

theorem :: SCMRING3:21
 InsCode I = 5 implies ex a, r st I = a:=r;

theorem :: SCMRING3:22
 InsCode I = 6 implies ex i2 st I = goto i2;

theorem :: SCMRING3:23
 InsCode I = 7 implies ex a, i1 st I = a=0_goto i1;

theorem :: SCMRING3:24
 AddressPart halt SCM R = {};

theorem :: SCMRING3:25
 AddressPart (a:=b) = <*a,b*>;

theorem :: SCMRING3:26
 AddressPart AddTo(a,b) = <*a,b*>;

theorem :: SCMRING3:27
 AddressPart SubFrom(a,b) = <*a,b*>;

theorem :: SCMRING3:28
 AddressPart MultBy(a,b) = <*a,b*>;

theorem :: SCMRING3:29
 AddressPart (a:=r) = <*a,r*>;

theorem :: SCMRING3:30
 AddressPart goto i1 = <*i1*>;

theorem :: SCMRING3:31
 AddressPart (a=0_goto i1) = <*i1,a*>;

theorem :: SCMRING3:32
 T = 0 implies AddressParts T = {0};

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

theorem :: SCMRING3:33
 T = 1 implies dom PA AddressParts T = {1,2};

theorem :: SCMRING3:34
 T = 2 implies dom PA AddressParts T = {1,2};

theorem :: SCMRING3:35
 T = 3 implies dom PA AddressParts T = {1,2};

theorem :: SCMRING3:36
 T = 4 implies dom PA AddressParts T = {1,2};

theorem :: SCMRING3:37
 T = 5 implies dom PA AddressParts T = {1,2};

theorem :: SCMRING3:38
 T = 6 implies dom PA AddressParts T = {1};

theorem :: SCMRING3:39
 T = 7 implies dom PA AddressParts T = {1,2};

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

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

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

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

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

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

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

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

theorem :: SCMRING3:48
 (PA AddressParts InsCode (a:=r)).1 = SCM-Data-Loc;

theorem :: SCMRING3:49
 (PA AddressParts InsCode (a:=r)).2 = the carrier of R;

theorem :: SCMRING3:50
 (PA AddressParts InsCode goto i1).1 = the Instruction-Locations of SCM R;

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

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

theorem :: SCMRING3:53
 NIC(halt SCM R, il) = {il};

definition let R;
 cluster JUMP halt SCM R -> empty;
end;

theorem :: SCMRING3:54
 NIC(a := b, il) = {Next il};

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

theorem :: SCMRING3:55
 NIC(AddTo(a,b), il) = {Next il};

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

theorem :: SCMRING3:56
 NIC(SubFrom(a,b), il) = {Next il};

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

theorem :: SCMRING3:57
 NIC(MultBy(a,b), il) = {Next il};

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

theorem :: SCMRING3:58
 NIC(a := r, il) = {Next il};

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

theorem :: SCMRING3:59
 NIC(goto i1, il) = {i1};

theorem :: SCMRING3:60
 JUMP goto i1 = {i1};

definition let R, i1;
 cluster JUMP goto i1 -> non empty trivial;
end;

theorem :: SCMRING3:61
 i1 in NIC(a=0_goto i1, il) & NIC(a=0_goto i1, il) c= {i1, Next il};

theorem :: SCMRING3:62
  for R being non trivial good Ring,
      a being Data-Location of R,
      il, i1 being Instruction-Location of SCM R
  holds NIC(a=0_goto i1, il) = {i1, Next il};

theorem :: SCMRING3:63
 JUMP (a=0_goto i1) = {i1};

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

theorem :: SCMRING3:64
 SUCC il = {il, Next il};

theorem :: SCMRING3:65
 for f being Function of NAT, the Instruction-Locations of SCM R
   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 let R;
 cluster SCM R -> standard;
end;

theorem :: SCMRING3:66
 il.(SCM R,k) = il.k;

theorem :: SCMRING3:67
 Next il.(SCM R,k) = il.(SCM R,k+1);

theorem :: SCMRING3:68
 Next il = NextLoc il;

definition let R be good Ring, k be Nat;
 func dl.(R,k) -> Data-Location of R equals
:: SCMRING3:def 1
  dl.k;
end;

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

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

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

definition let R, i1;
 cluster goto i1 -> jump-only;
end;

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

definition let R, a, i1;
 cluster a =0_goto i1 -> jump-only;
end;

reserve S for non trivial good Ring,
        p, q for Data-Location of S,
        w for Element of S;

definition let S, p, q;
 cluster InsCode (p:=q) -> non jump-only;
end;

definition let S, p, q;
 cluster p:=q -> non jump-only;
end;

definition let S, p, q;
 cluster InsCode AddTo(p,q) -> non jump-only;
end;

definition let S, p, q;
 cluster AddTo(p, q) -> non jump-only;
end;

definition let S, p, q;
 cluster InsCode SubFrom(p,q) -> non jump-only;
end;

definition let S, p, q;
 cluster SubFrom(p, q) -> non jump-only;
end;

definition let S, p, q;
 cluster InsCode MultBy(p,q) -> non jump-only;
end;

definition let S, p, q;
 cluster MultBy(p, q) -> non jump-only;
end;

definition let S, p, w;
 cluster InsCode (p:=w) -> non jump-only;
end;

definition let S, p, w;
 cluster p:=w -> non jump-only;
end;

definition let R, a, b;
 cluster a:=b -> sequential;
end;

definition let R, a, b;
 cluster AddTo(a,b) -> sequential;
end;

definition let R, a, b;
 cluster SubFrom(a,b) -> sequential;
end;

definition let R, a, b;
 cluster MultBy(a,b) -> sequential;
end;

definition let R, a, r;
 cluster a:=r -> sequential;
end;

definition let R, i1;
 cluster goto i1 -> non sequential;
end;

definition let R, a, i1;
 cluster a =0_goto i1 -> non sequential;
end;

definition let R, i1;
 cluster goto i1 -> non ins-loc-free;
end;

definition let R, a, i1;
 cluster a =0_goto i1 -> non ins-loc-free;
end;

definition let R;
 cluster SCM R -> homogeneous with_explicit_jumps without_implicit_jumps;
end;

definition let R;
 cluster SCM R -> regular;
end;

theorem :: SCMRING3:69
 IncAddr(goto i1,k) = goto il.(SCM R, locnum i1 + k);

theorem :: SCMRING3:70
 IncAddr(a=0_goto i1,k) = a=0_goto il.(SCM R, locnum i1 + k);

definition let R;
 cluster SCM R -> IC-good Exec-preserving;
end;
The abstract of the Mizar article:

The Properties of Instructions of SCM over Ring
