:: The Instructions for the SCMPDS computer
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem Th1: :: SCMPDS_I:1
for k being Integer holds k in SCM-Data-Loc \/ INT
proof end;

begin

:: [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 -> set equals :: SCMPDS_I:def 1
(((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;
coherence
(((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } is set ;
end;

:: deftheorem defines SCMPDS-Instr SCMPDS_I:def 1 :
SCMPDS-Instr = (((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, 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 15, 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 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ;

Lm1: [0,{},{}] in SCMPDS-Instr
proof end;

theorem :: SCMPDS_I:2
[14,{},<*0*>] in SCMPDS-Instr
proof end;

registration
cluster SCMPDS-Instr -> non empty ;
coherence
not SCMPDS-Instr is empty ;
end;

definition
let d be Element of SCM-Data-Loc ;
let s be Integer;
:: original: <*
redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ INT;
coherence
<*d,s*> is FinSequence of SCM-Data-Loc \/ INT
proof end;
end;

definition
let x be Element of SCMPDS-Instr ;
given mk being Element of SCM-Data-Loc , I being Element of Segm 15 such that A1: x = [I,{},<*mk*>] ;
func x address_1 -> Element of SCM-Data-Loc means :Def2: :: SCMPDS_I:def 2
 ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines address_1 SCMPDS_I:def 2 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex I being Element of Segm 15 st x = [I,{},<*mk*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 1 ) );

theorem :: SCMPDS_I:3
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds
x address_1 = mk
proof end;

definition
let x be Element of SCMPDS-Instr ;
given r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*r*>] ;
func x const_INT -> Integer means :Def3: :: SCMPDS_I:def 3
 ex f being FinSequence of INT st
( f = x `3_3 & it = f /. 1 );
existence
ex b1 being Integer ex f being FinSequence of INT st
( f = x `3_3 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
end;

:: deftheorem Def3 defines const_INT SCMPDS_I:def 3 :
for x being Element of SCMPDS-Instr st ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*r*>] holds
for b2 being Integer holds
( b2 = x const_INT iff ex f being FinSequence of INT st
( f = x `3_3 & b2 = f /. 1 ) );

theorem :: SCMPDS_I:4
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for k being Integer st x = [I,{},<*k*>] holds
x const_INT = k
proof end;

definition
let x be Element of SCMPDS-Instr ;
given mk being Element of SCM-Data-Loc , r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*mk,r*>] ;
func x P21address -> Element of SCM-Data-Loc means :Def4: :: SCMPDS_I:def 4
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
func x P22const -> Integer means :Def5: :: SCMPDS_I:def 5
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def4 defines P21address SCMPDS_I:def 4 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*mk,r*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P21address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );

:: deftheorem Def5 defines P22const SCMPDS_I:def 5 :
for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*mk,r*>] holds
for b2 being Integer holds
( b2 = x P22const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );

theorem :: SCMPDS_I:5
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc
for r being Integer st x = [I,{},<*mk,r*>] holds
( x P21address = mk & x P22const = r )
proof end;

definition
let x be Element of SCMPDS-Instr ;
given m1 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,k1,k2*>] ;
func x P31address -> Element of SCM-Data-Loc means :Def6: :: SCMPDS_I:def 6
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
func x P32const -> Integer means :Def7: :: SCMPDS_I:def 7
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 2 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2 ;
func x P33const -> Integer means :Def8: :: SCMPDS_I:def 8
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) holds
b1 = b2 ;
end;

:: deftheorem Def6 defines P31address SCMPDS_I:def 6 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P31address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );

:: deftheorem Def7 defines P32const SCMPDS_I:def 7 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P32const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );

:: deftheorem Def8 defines P33const SCMPDS_I:def 8 :
for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P33const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) );

theorem :: SCMPDS_I:6
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
proof end;

definition
let x be Element of SCMPDS-Instr ;
given m1, m2 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,m2,k1,k2*>] ;
func x P41address -> Element of SCM-Data-Loc means :Def9: :: SCMPDS_I:def 9
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) holds
b1 = b2 ;
func x P42address -> Element of SCM-Data-Loc means :Def10: :: SCMPDS_I:def 10
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) holds
b1 = b2 ;
func x P43const -> Integer means :Def11: :: SCMPDS_I:def 11
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 3 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) holds
b1 = b2 ;
func x P44const -> Integer means :Def12: :: SCMPDS_I:def 12
 ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & it = f /. 4 );
existence
ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 4 )
proof end;
uniqueness
for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b1 = f /. 4 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 4 ) holds
b1 = b2 ;
end;

:: deftheorem Def9 defines P41address SCMPDS_I:def 9 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P41address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 1 ) );

:: deftheorem Def10 defines P42address SCMPDS_I:def 10 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x P42address iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 2 ) );

:: deftheorem Def11 defines P43const SCMPDS_I:def 11 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P43const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 3 ) );

:: deftheorem Def12 defines P44const SCMPDS_I:def 12 :
for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds
for b2 being Integer holds
( b2 = x P44const iff ex f being FinSequence of SCM-Data-Loc \/ INT st
( f = x `3_3 & b2 = f /. 4 ) );

theorem :: SCMPDS_I:7
for I being Element of Segm 15
for x being Element of SCMPDS-Instr
for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
proof end;

:: RetSP: Return Stack Pointer
:: RetIC: Return Instruction-Counter
definition
func RetSP -> Element of NAT equals :: SCMPDS_I:def 13
 0 ;
coherence
0 is Element of NAT ;
func RetIC -> Element of NAT equals :: SCMPDS_I:def 14
1;
coherence
1 is Element of NAT ;
end;

:: deftheorem defines RetSP SCMPDS_I:def 13 :
RetSP = 0 ;

:: deftheorem defines RetIC SCMPDS_I:def 14 :
RetIC = 1;

theorem Th8: :: SCMPDS_I:8
for x being Element of SCMPDS-Instr holds
( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [14,{},<*l*>] where l is Element of INT : verum } & InsCode x = 14 ) or ( x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } & InsCode x = 1 ) or ( x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } & ( InsCode x = 2 or InsCode x = 3 ) ) or ( x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } & ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } & ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) ) )
proof end;

begin

registration
cluster proj2 SCMPDS-Instr -> FinSequence-membered ;
coherence
proj2 SCMPDS-Instr is FinSequence-membered
proof end;
end;

registration
cluster SCMPDS-Instr -> standard-ins ;
coherence
SCMPDS-Instr is standard-ins
proof end;
end;

Lm2: for l being Element of SCMPDS-Instr holds InsCode l <= 14
proof end;

Lm3: for i being Element of SCMPDS-Instr st InsCode i = 0 holds
JumpPart i = {}
proof end;

Lm4: for i being Element of SCMPDS-Instr st InsCode i = 14 holds
JumpPart i = {}
proof end;

Lm5: for i being Element of SCMPDS-Instr st InsCode i = 1 holds
JumpPart i = {}
proof end;

Lm6: for i being Element of SCMPDS-Instr st ( InsCode i = 2 or InsCode i = 3 ) holds
JumpPart i = {}
proof end;

Lm7: for i being Element of SCMPDS-Instr st ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) holds
JumpPart i = {}
proof end;

Lm8: for i being Element of SCMPDS-Instr st ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) holds
JumpPart i = {}
proof end;

registration
cluster SCMPDS-Instr -> homogeneous ;
coherence
SCMPDS-Instr is homogeneous
proof end;
end;

registration
cluster SCMPDS-Instr -> J/A-independent ;
coherence
SCMPDS-Instr is J/A-independent
proof end;
end;

registration
cluster SCMPDS-Instr -> with_halt ;
coherence
SCMPDS-Instr is with_halt
proof end;
end;