Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Jing-Chao Chen
- Received June 15, 1999
- MML identifier: SCMPDS_1
- [
Mizar article,
MML identifier index
]
environ
vocabulary GR_CY_1, AMI_2, INT_1, FINSEQ_1, FUNCT_1, RELAT_1, TARSKI, BOOLE,
NAT_1, CARD_3, AMI_1, FUNCT_4, CAT_1, ABSVALUE, ARYTM_1, MCART_1,
CQC_LANG, FUNCT_2, FUNCT_5, SCMPDS_1, FINSEQ_4;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
FUNCT_2, GR_CY_1, MCART_1, NUMBERS, XCMPLX_0, XREAL_0, CARD_3, INT_1,
NAT_1, FINSEQ_1, FRAENKEL, FINSEQ_4, CQC_LANG, FUNCT_4, CAT_2, AMI_2,
GROUP_1;
constructors AMI_1, AMI_2, CAT_2, DOMAIN_1, FINSEQ_4, NAT_1, MEMBERED;
clusters AMI_1, AMI_2, CQC_LANG, INT_1, FINSEQ_1, RELSET_1, XBOOLE_0, NAT_1,
FRAENKEL, MEMBERED, ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve x1,x2,x3,x4,x5 for set,
i, j, k for Nat,
I,I2,I3,I4 for Element of Segm 14,
i1 for Element of SCM-Instr-Loc,
d1,d2,d3,d4,d5 for Element of SCM-Data-Loc,
k1,k2 for Integer;
definition let x1,x2,x3,x4 be set;
func <*x1,x2,x3,x4*> -> set equals
:: SCMPDS_1:def 1
<*x1,x2,x3*>^<*x4*>;
let x5 be set;
func <*x1,x2,x3,x4,x5*> -> set equals
:: SCMPDS_1:def 2
<*x1,x2,x3*>^<*x4,x5*>;
end;
definition let x1,x2,x3,x4 be set;
cluster <*x1,x2,x3,x4*> -> Function-like Relation-like;
let x5 be set;
cluster <*x1,x2,x3,x4,x5*> -> Function-like Relation-like;
end;
definition let x1,x2,x3,x4 be set;
cluster <*x1,x2,x3,x4*> -> FinSequence-like;
let x5 be set;
cluster <*x1,x2,x3,x4,x5*> -> FinSequence-like;
end;
definition let D be non empty set,x1,x2,x3,x4 be Element of D;
redefine func <* x1,x2,x3,x4*> -> FinSequence of D;
end;
definition let D be non empty set,x1,x2,x3,x4,x5 be Element of D;
redefine func <*x1,x2,x3,x4,x5*> -> FinSequence of D;
end;
theorem :: SCMPDS_1:1
<*x1,x2,x3,x4*>=<*x1,x2,x3*>^<*x4*> &
<*x1,x2,x3,x4*>=<*x1,x2*>^<*x3,x4*> &
<*x1,x2,x3,x4*>=<*x1*>^<*x2,x3,x4*> &
<*x1,x2,x3,x4*>=<*x1*>^<*x2*>^<*x3*>^<*x4*>;
theorem :: SCMPDS_1:2
<*x1,x2,x3,x4,x5*>=<*x1,x2,x3*>^<*x4,x5*> &
<*x1,x2,x3,x4,x5*>=<*x1,x2,x3,x4*>^<*x5*> &
<*x1,x2,x3,x4,x5*>=<*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*> &
<*x1,x2,x3,x4,x5*>=<*x1,x2*>^<*x3,x4,x5*> &
<*x1,x2,x3,x4,x5*>=<*x1*>^<*x2,x3,x4,x5*>;
reserve ND for non empty set;
reserve y1,y2,y3,y4,y5 for Element of ND;
reserve p for FinSequence;
theorem :: SCMPDS_1:3
p = <*x1,x2,x3,x4*> iff len p = 4 & p.1 = x1 & p.2 = x2
& p.3=x3 & p.4= x4;
theorem :: SCMPDS_1:4
dom<*x1,x2,x3,x4*> = Seg(4);
theorem :: SCMPDS_1:5
p = <*x1,x2,x3,x4,x5*> iff len p = 5 & p.1 = x1 & p.2 = x2
& p.3=x3 & p.4= x4 & p.5= x5;
theorem :: SCMPDS_1:6
dom<*x1,x2,x3,x4,x5*> = Seg(5);
theorem :: SCMPDS_1:7
<*y1,y2,y3,y4*>/.1 = y1 & <*y1,y2,y3,y4*>/.2 = y2
& <*y1,y2,y3,y4*>/.3 = y3 & <*y1,y2,y3,y4*>/.4=y4;
theorem :: SCMPDS_1:8
<*y1,y2,y3,y4,y5*>/.1 = y1 & <*y1,y2,y3,y4,y5*>/.2 = y2
& <*y1,y2,y3,y4,y5*>/.3 = y3 &
<*y1,y2,y3,y4,y5*>/.4=y4 & <*y1,y2,y3,y4,y5*>/.5=y5;
theorem :: SCMPDS_1:9
for k be Integer holds k in union {INT} \/ NAT;
theorem :: SCMPDS_1:10
for k be Integer holds k in SCM-Data-Loc \/ INT;
theorem :: SCMPDS_1:11
for d be Element of SCM-Data-Loc holds d in SCM-Data-Loc \/ INT;
begin :: The construction of SCM with Push-Down Stack
:: [0,goto L]
:: [1,return sp<-sp+0,count<-(sp)+2]
:: [2,a:=c(constant)]
:: [3,saveIC (a,k)]
:: [4,if(a,k)<>0 goto L ]
:: [5,if(a,k)<=0 goto L ]
:: [6,if(a,k)>=0 goto L ]
:: [7,(a,k):=c(constant) ]
:: [8,(a,k1)+k2]
:: [9, (a1,k1)+(a2,k2)]
:: [10,(a1,k1)-(a2,k2)]
:: [11,(a1,k1)*(a2,k2)]
:: [12,(a1,k1)/(a2,k2)]
:: [13,(a1,k1):=(a2,k2)]
definition
func SCMPDS-Instr ->
Subset of [: Segm 14, (union {INT} \/ NAT)* :] equals
:: SCMPDS_1:def 3
{ [0,<*l*>] where l is Element of INT: not contradiction} \/
{ [1,<*sp*>] where sp is Element of SCM-Data-Loc:not contradiction} \/
{ [I,<*v,c*>] where I is Element of Segm 14,v is Element of SCM-Data-Loc,
c is Element of INT: I in {2,3} } \/
{ [I,<*v,c1,c2*>] where I is Element of Segm 14,
v is Element of SCM-Data-Loc,
c1,c2 is Element of INT: I in {4,5,6,7,8} } \/
{ [I,<*v1,v2,c1,c2*>] where I is Element of Segm 14,
v1,v2 is Element of SCM-Data-Loc,
c1,c2 is Element of INT: I in {9,10,11,12,13} };
end;
canceled;
theorem :: SCMPDS_1:13
[0,<*0*>] in SCMPDS-Instr;
definition
cluster SCMPDS-Instr -> non empty;
end;
theorem :: SCMPDS_1:14
k= 0 or (ex j st k = 2*j+1) or (ex j st k = 2*j+2);
theorem :: SCMPDS_1:15
k = 0 implies not (ex j st k = 2*j+1) & not (ex j st k = 2*j+2);
theorem :: SCMPDS_1:16
((ex j st k = 2*j+1) implies k<>0 & not (ex j st k = 2*j+2)) &
((ex j st k = 2*j+2) implies k<>0 & not (ex j st k = 2*j+1));
definition
func SCMPDS-OK ->
Function of NAT, { INT } \/ { SCMPDS-Instr, SCM-Instr-Loc } means
:: SCMPDS_1:def 4
it.0 = SCM-Instr-Loc &
for k being Nat holds
it.(2*k+1) = INT & it.(2*k+2) = SCMPDS-Instr;
end;
definition
mode SCMPDS-State is Element of product SCMPDS-OK;
end;
theorem :: SCMPDS_1:17
SCM-Instr-Loc <> SCMPDS-Instr & SCMPDS-Instr <> INT;
theorem :: SCMPDS_1:18
SCMPDS-OK.i = SCM-Instr-Loc iff i = 0;
theorem :: SCMPDS_1:19
SCMPDS-OK.i = INT iff ex k st i = 2*k+1;
theorem :: SCMPDS_1:20
SCMPDS-OK.i = SCMPDS-Instr iff ex k st i = 2*k+2;
theorem :: SCMPDS_1:21
SCMPDS-OK.d1 = INT;
theorem :: SCMPDS_1:22
SCMPDS-OK.i1 = SCMPDS-Instr;
theorem :: SCMPDS_1:23
pi(product SCMPDS-OK,0) = SCM-Instr-Loc;
theorem :: SCMPDS_1:24
pi(product SCMPDS-OK,d1) = INT;
theorem :: SCMPDS_1:25
pi(product SCMPDS-OK,i1) = SCMPDS-Instr;
definition let s be SCMPDS-State;
func IC s -> Element of SCM-Instr-Loc equals
:: SCMPDS_1:def 5
s.0;
end;
definition let s be SCMPDS-State,
u be Element of SCM-Instr-Loc;
func SCM-Chg(s,u) -> SCMPDS-State equals
:: SCMPDS_1:def 6
s +* (0 .--> u);
end;
theorem :: SCMPDS_1:26
for s being SCMPDS-State, u being Element of SCM-Instr-Loc
holds SCM-Chg(s,u).0 = u;
theorem :: SCMPDS_1:27
for s being SCMPDS-State, u being Element of SCM-Instr-Loc,
mk being Element of SCM-Data-Loc
holds SCM-Chg(s,u).mk = s.mk;
theorem :: SCMPDS_1:28
for s being SCMPDS-State,
u, v being Element of SCM-Instr-Loc
holds SCM-Chg(s,u).v = s.v;
definition let s be SCMPDS-State,
t be Element of SCM-Data-Loc,
u be Integer;
func SCM-Chg(s,t,u) -> SCMPDS-State equals
:: SCMPDS_1:def 7
s +* (t .--> u);
end;
theorem :: SCMPDS_1:29
for s being SCMPDS-State, t being Element of SCM-Data-Loc,
u being Integer
holds SCM-Chg(s,t,u).0 = s.0;
theorem :: SCMPDS_1:30
for s being SCMPDS-State, t being Element of SCM-Data-Loc,
u being Integer
holds SCM-Chg(s,t,u).t = u;
theorem :: SCMPDS_1:31
for s being SCMPDS-State, t being Element of SCM-Data-Loc,
u being Integer,
mk being Element of SCM-Data-Loc st mk <> t
holds SCM-Chg(s,t,u).mk = s.mk;
theorem :: SCMPDS_1:32
for s being SCMPDS-State, t being Element of SCM-Data-Loc,
u being Integer,
v being Element of SCM-Instr-Loc
holds SCM-Chg(s,t,u).v = s.v;
definition let s be SCMPDS-State,
a be Element of SCM-Data-Loc;
redefine func s.a -> Integer;
end;
definition let s be SCMPDS-State,
a be Element of SCM-Data-Loc,
n be Integer;
func Address_Add(s,a,n) -> Element of SCM-Data-Loc equals
:: SCMPDS_1:def 8
2*abs(s.a+n)+1;
end;
definition let s be SCMPDS-State,
n be Integer;
func jump_address(s,n) -> Element of SCM-Instr-Loc equals
:: SCMPDS_1:def 9
abs(((IC s) qua Nat )-2+2*n)+2;
end;
definition let d be Element of SCM-Data-Loc,
s be Integer;
redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT;
end;
definition let x be Element of SCMPDS-Instr;
given mk be Element of SCM-Data-Loc, I such that
x = [ I, <*mk*>];
func x address_1 -> Element of SCM-Data-Loc means
:: SCMPDS_1:def 10
ex f being FinSequence of SCM-Data-Loc st f = x`2 & it = f/.1;
end;
theorem :: SCMPDS_1:33
for x being Element of SCMPDS-Instr, mk being Element of SCM-Data-Loc
st x = [ I, <*mk*>] holds
x address_1 = mk;
definition let x be Element of SCMPDS-Instr;
given r being Integer, I such that
x = [ I, <*r*>];
func x const_INT -> Integer means
:: SCMPDS_1:def 11
ex f being FinSequence of INT st f = x`2 & it = f/.1;
end;
theorem :: SCMPDS_1:34
for x being Element of SCMPDS-Instr, k being Integer
st x = [ I, <*k*>] holds
x const_INT = k;
definition let x be Element of SCMPDS-Instr;
given mk being Element of SCM-Data-Loc, r being Integer,
I such that
x = [ I, <*mk, r*>];
func x P21address -> Element of SCM-Data-Loc means
:: SCMPDS_1:def 12
ex f being FinSequence of SCM-Data-Loc \/ INT
st f = x`2 & it = f/.1;
func x P22const -> Integer means
:: SCMPDS_1:def 13
ex f being FinSequence of SCM-Data-Loc \/ INT
st f = x`2 & it = f/.2;
end;
theorem :: SCMPDS_1:35
for x being Element of SCMPDS-Instr, mk being Element of SCM-Data-Loc,
r being Integer st x = [ I, <*mk, r*>] holds
x P21address = mk & x P22const = r;
definition let x be Element of SCMPDS-Instr;
given m1 being Element of SCM-Data-Loc,k1,k2 be Integer,I such that
x = [I, <*m1,k1,k2*>];
func x P31address -> Element of SCM-Data-Loc means
:: SCMPDS_1:def 14
ex f being FinSequence of (SCM-Data-Loc \/ INT) st
f = x`2 & it = f/.1;
func x P32const -> Integer means
:: SCMPDS_1:def 15
ex f being FinSequence of (SCM-Data-Loc \/ INT) st
f = x`2 & it = f/.2;
func x P33const -> Integer means
:: SCMPDS_1:def 16
ex f being FinSequence of (SCM-Data-Loc \/ INT) st
f = x`2 & it = f/.3;
end;
theorem :: SCMPDS_1:36
for x being Element of SCMPDS-Instr, d1 being Element of SCM-Data-Loc,
k1,k2 being Integer st x = [ I, <*d1,k1,k2*>] holds
x P31address = d1 & x P32const = k1 & x P33const = k2;
definition let x be Element of SCMPDS-Instr;
given m1,m2 being Element of SCM-Data-Loc,k1,k2 be Integer,I such that
x = [ I, <*m1,m2,k1,k2*>];
func x P41address -> Element of SCM-Data-Loc means
:: SCMPDS_1:def 17
ex f being FinSequence of (SCM-Data-Loc \/ INT) st
f = x`2 & it = f/.1;
func x P42address -> Element of SCM-Data-Loc means
:: SCMPDS_1:def 18
ex f being FinSequence of (SCM-Data-Loc \/ INT) st
f = x`2 & it = f/.2;
func x P43const -> Integer means
:: SCMPDS_1:def 19
ex f being FinSequence of (SCM-Data-Loc \/ INT) st
f = x`2 & it = f/.3;
func x P44const -> Integer means
:: SCMPDS_1:def 20
ex f being FinSequence of (SCM-Data-Loc \/ INT) st
f = x`2 & it = f/.4;
end;
theorem :: SCMPDS_1:37
for x being Element of SCMPDS-Instr, d1,d2 being Element of SCM-Data-Loc,
k1,k2 being Integer st x = [ I, <*d1,d2,k1,k2*>] holds
x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2;
definition let s be SCMPDS-State,
a be Element of SCM-Data-Loc;
func PopInstrLoc(s,a) -> Element of SCM-Instr-Loc equals
:: SCMPDS_1:def 21
2*(abs(s.a) div 2)+4;
end;
:: RetSP: Return Stack Pointer
:: RetIC: Return Instruction-Counter
definition
func RetSP -> Nat equals
:: SCMPDS_1:def 22
0;
func RetIC -> Nat equals
:: SCMPDS_1:def 23
1;
end;
definition let x be Element of SCMPDS-Instr,
s be SCMPDS-State;
func SCM-Exec-Res (x,s) -> SCMPDS-State equals
:: SCMPDS_1:def 24
SCM-Chg(s, jump_address(s,x const_INT ))
if ex k1 st x = [ 0, <*k1*>],
SCM-Chg(SCM-Chg(s, x P21address, x P22const), Next IC s)
if ex d1,k1 st x = [ 2, <*d1, k1*>],
SCM-Chg(SCM-Chg(s, Address_Add(s,x P21address,x P22const),
IC s qua Nat),Next IC s)
if ex d1,k1 st x = [ 3, <*d1, k1*>],
SCM-Chg(SCM-Chg(s, x address_1,s.Address_Add(s,x address_1,RetSP)),
PopInstrLoc(s,Address_Add(s,x address_1,RetIC)) )
if ex d1 st x = [ 1, <*d1*>],
SCM-Chg(s, IFEQ(s.Address_Add(s,x P31address,x P32const), 0,
Next IC s,jump_address(s,x P33const )))
if ex d1,k1,k2 st x = [ 4, <*d1,k1,k2*>],
SCM-Chg(s, IFGT(s.Address_Add(s,x P31address,x P32const), 0,
Next IC s,jump_address(s,x P33const )))
if ex d1,k1,k2 st x = [ 5, <*d1,k1,k2*>],
SCM-Chg(s, IFGT(0, s.Address_Add(s,x P31address,x P32const),
Next IC s,jump_address(s,x P33const )))
if ex d1,k1,k2 st x = [ 6, <*d1,k1,k2*>],
SCM-Chg(SCM-Chg(s, Address_Add(s,x P31address,x P32const),
x P33const), Next IC s)
if ex d1,k1,k2 st x = [ 7, <*d1,k1,k2*>],
SCM-Chg(SCM-Chg(s, Address_Add(s,x P31address,x P32const),
s.Address_Add(s,x P31address,x P32const)+ (x P33const)), Next IC s)
if ex d1,k1,k2 st x = [ 8, <*d1,k1,k2*>],
SCM-Chg(SCM-Chg(s, Address_Add(s,x P41address,x P43const),
s.Address_Add(s,x P41address,x P43const)+
s.Address_Add(s,x P42address,x P44const)),Next IC s)
if ex d1,d2,k1,k2 st x = [ 9, <*d1,d2,k1,k2*>],
SCM-Chg(SCM-Chg(s, Address_Add(s,x P41address,x P43const),
s.Address_Add(s,x P41address,x P43const) -
s.Address_Add(s,x P42address,x P44const)),Next IC s)
if ex d1,d2,k1,k2 st x = [ 10, <*d1,d2,k1,k2*>],
SCM-Chg(SCM-Chg(s, Address_Add(s,x P41address,x P43const),
s.Address_Add(s,x P41address,x P43const) *
s.Address_Add(s,x P42address,x P44const)),Next IC s)
if ex d1,d2,k1,k2 st x = [ 11, <*d1,d2,k1,k2*>],
SCM-Chg(SCM-Chg(s, Address_Add(s,x P41address,x P43const),
s.Address_Add(s,x P42address,x P44const)), Next IC s)
if ex d1,d2,k1,k2 st x = [13, <*d1,d2,k1,k2*>],
SCM-Chg(SCM-Chg(
SCM-Chg(s,Address_Add(s,x P41address,x P43const),
s.Address_Add(s,x P41address,x P43const) div
s.Address_Add(s,x P42address,x P44const)),
Address_Add(s,x P42address,x P44const),
s.Address_Add(s,x P41address,x P43const) mod
s.Address_Add(s,x P42address,x P44const)), Next IC s)
if ex d1,d2,k1,k2 st x = [12, <*d1,d2,k1,k2*>]
otherwise s;
end;
definition
let f be Function of SCMPDS-Instr, Funcs(product SCMPDS-OK,
product SCMPDS-OK ), x be Element of SCMPDS-Instr;
cluster f.x -> Function-like Relation-like;
end;
definition
func SCMPDS-Exec ->
Function of SCMPDS-Instr, Funcs(product SCMPDS-OK, product SCMPDS-OK)
means
:: SCMPDS_1:def 25
for x being Element of SCMPDS-Instr, y being SCMPDS-State holds
(it.x).y = SCM-Exec-Res (x,y);
end;
Back to top