:: The Construction of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998-2016 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, SUBSET_1, CARD_1, AMI_2, XBOOLE_0, STRUCT_0, ZFMISC_1,
RELAT_1, FINSEQ_1, FUNCSDOM, FUNCT_1, AMI_1, PARTFUN1, TARSKI, SCMRING1,
RECDEF_2, ALGSTR_0, UNIALG_1, AMISTD_2, VALUED_0, COMPOS_0, XXREAL_0,
NAT_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1,
FUNCT_1, PARTFUN1, VALUED_0, ORDINAL1, CARD_1, RECDEF_2, XXREAL_0,
NUMBERS, STRUCT_0, ALGSTR_0, VECTSP_1, MCART_1, FINSEQ_1, FINSEQ_4,
COMPOS_0, SCM_INST;
constructors FINSEQ_4, REALSET2, FINSEQ_2, COMPOS_1, SCM_INST, VALUED_0,
XTUPLE_0;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSEQ_1, STRUCT_0, CARD_1, GCD_1,
FUNCT_1, ALGSTR_0, ALGSTR_1, COMPOS_0, SCM_INST, XXREAL_0, VALUED_0,
XTUPLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE;
begin :: The construction of { \bf SCM } over ring
reserve i, j, k for Nat,
I for Element of Segm 8,
i1, i2 for Nat,
d1, d2, d3, d4 for Element of SCM-Data-Loc,
S for non empty 1-sorted;
registration
cluster SCM-Instr -> non trivial;
end;
definition
let S be non empty 1-sorted;
func SCM-Instr S -> non empty set equals
:: SCMRINGI:def 1
{ [0,{},{}] }
\/ { [I,{},<*a,b*>] where I is Element of Segm 8,
a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } }
\/ (the set of all [6,<*i*>,{}] where i is Nat)
\/ (the set of all
[7,<*i*>,<*a*>] where i is Nat,a is Element of SCM-Data-Loc)
\/ (the set of all [5,{},<*a,r*>] where a is
Element of SCM-Data-Loc, r is Element of S);
end;
registration
let S be non empty 1-sorted;
cluster SCM-Instr S -> non trivial;
end;
reserve G for non empty 1-sorted;
definition
let S be non empty 1-sorted, x be Element of SCM-Instr S;
given mk, ml being Element of SCM-Data-Loc, I such that
x = [I,{},<*mk,ml*>];
func x address_1 -> Element of SCM-Data-Loc means
:: SCMRINGI:def 2
ex f being
FinSequence of SCM-Data-Loc st f = x`3_3 & it = f/.1;
func x address_2 -> Element of SCM-Data-Loc means
:: SCMRINGI:def 3
ex f being
FinSequence of SCM-Data-Loc st f = x`3_3 & it = f/.2;
end;
theorem :: SCMRINGI:1
for x being Element of SCM-Instr S, mk, ml being Element of
SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds x address_1 = mk & x address_2 = ml;
definition
let R be non empty 1-sorted, x be Element of SCM-Instr R;
given mk being Element of NAT, I such that
x = [I,<*mk*>,{}];
func x jump_address -> Element of NAT means
:: SCMRINGI:def 4
ex f being FinSequence of
NAT st f = x`2_3 & it = f/.1;
end;
theorem :: SCMRINGI:2
for x being Element of SCM-Instr S, mk being Nat
st x = [ I,<*mk*>,{}] holds x jump_address = mk;
definition
let S be non empty 1-sorted, x be Element of SCM-Instr S;
given mk being Element of NAT, ml being Element of SCM-Data-Loc, I such that
x = [I,<*mk*>,<*ml*>];
func x cjump_address -> Element of NAT means
:: SCMRINGI:def 5
ex mk being Element of NAT st <*mk*> = x`2_3 & it = <*mk*>/.1;
func x cond_address -> Element of SCM-Data-Loc means
:: SCMRINGI:def 6
ex ml being Element of SCM-Data-Loc st <*ml*> = x`3_3 & it = <*ml*>/.1;
end;
theorem :: SCMRINGI:3
for x being Element of SCM-Instr S, mk being Element of NAT, ml being
Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>]
holds x cjump_address = mk & x
cond_address = ml;
definition
let S be non empty 1-sorted, d be Element of SCM-Data-Loc, s be Element of S;
redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S;
end;
definition
let S be non empty 1-sorted, x be Element of SCM-Instr S;
given mk being Element of SCM-Data-Loc, r being Element of S, I such that
x = [I,{},<*mk,r*>];
func x const_address -> Element of SCM-Data-Loc means
:: SCMRINGI:def 7
ex f being
FinSequence of SCM-Data-Loc \/ the carrier of S st f = x`3_3 & it = f/.1;
func x const_value -> Element of S means
:: SCMRINGI:def 8
ex f being FinSequence of
SCM-Data-Loc \/ the carrier of S st f = x`3_3 & it = f/.2;
end;
theorem :: SCMRINGI:4
for x being Element of SCM-Instr S, mk being Element of SCM-Data-Loc,
r being Element of S st x = [I,{},<*mk,r*>] holds x const_address = mk & x
const_value = r;
theorem :: SCMRINGI:5
for S being non empty 1-sorted
holds SCM-Instr S c= [:NAT,NAT*,proj2 SCM-Instr S:];
registration let S be non empty 1-sorted;
cluster proj2 SCM-Instr S -> FinSequence-membered;
end;
theorem :: SCMRINGI:6
[0,{},{}] in SCM-Instr S;
theorem :: SCMRINGI:7
for S being non empty 1-sorted
for x being Element of SCM-Instr S holds
x in { [0,{},{}] } & InsCode x = 0 or
x in { [I,{},<*a,b*>] where I is Element of Segm 8,
a, b is Element of SCM-Data-Loc: I in { 1,2,3,4 } }
& (InsCode x = 1 or InsCode x = 2 or InsCode x = 3
or InsCode x = 4) or
x in the set of all [6,<*i*>,{}] where i is Nat
& InsCode x = 6 or
x in the set of all [7,<*i*>,<*a*>]
where i is Nat,a is Element of SCM-Data-Loc
& InsCode x = 7 or
x in the set of all [5,{},<*a,r*>] where a is
Element of SCM-Data-Loc, r is Element of S
& InsCode x = 5;
begin :: from SCMRING2
reserve I for Element of Segm 8,
S for non empty 1-sorted,
t for Element of S,
x for set,
k for Nat;
registration
cluster strict trivial for Ring;
end;
registration
let R be Ring;
cluster SCM-Instr R -> standard-ins;
end;
registration
let R be Ring;
cluster SCM-Instr R -> homogeneous;
end;
reserve R for Ring, T for InsType of SCM-Instr R;
registration
let R be Ring;
cluster SCM-Instr R -> J/A-independent;
end;
reserve R for Ring,
r for Element of R,
a, b, c, d1, d2 for Element of SCM-Data-Loc;
reserve i1 for Nat;
theorem :: SCMRINGI:8
x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S;
theorem :: SCMRINGI:9
[5,{},<*d1,t*>] in SCM-Instr S;
theorem :: SCMRINGI:10
[6,<*i1*>,{}] in SCM-Instr S;
theorem :: SCMRINGI:11
[7,<*i1*>,<*d1*>] in SCM-Instr S;
registration let S;
cluster SCM-Instr S -> with_halt;
end;