:: The Instructions for SCM+FSA Computer
:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received February 3, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users


definition
func SCM+FSA-Data*-Loc -> set equals :: SCMFSA_I:def 1
INT \ NAT;
coherence
INT \ NAT is set ;
end;

:: deftheorem defines SCM+FSA-Data*-Loc SCMFSA_I:def 1 :
SCM+FSA-Data*-Loc = INT \ NAT;

registration
cluster SCM+FSA-Data*-Loc -> non empty ;
coherence
not SCM+FSA-Data*-Loc is empty
proof end;
end;

definition
func SCM+FSA-Instr -> non empty set equals :: SCMFSA_I:def 2
(SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;
coherence
(SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } is non empty set ;
end;

:: deftheorem defines SCM+FSA-Instr SCMFSA_I:def 2 :
SCM+FSA-Instr = (SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;

theorem Th1: :: SCMFSA_I:1
SCM-Instr c= SCM+FSA-Instr
proof end;

Lm1: SCM+FSA-Instr c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
proof end;

registration
cluster proj2 SCM+FSA-Instr -> FinSequence-membered ;
coherence
proj2 SCM+FSA-Instr is FinSequence-membered
proof end;
end;

registration
cluster SCM+FSA-Instr -> non empty standard-ins ;
coherence
( SCM+FSA-Instr is standard-ins & not SCM+FSA-Instr is empty )
proof end;
end;

theorem Th2: :: SCMFSA_I:2
for I being Element of SCM+FSA-Instr st I `1_3 <= 8 holds
I in SCM-Instr
proof end;

theorem Th3: :: SCMFSA_I:3
[0,{},{}] in SCM+FSA-Instr by Th1, SCM_INST:1;

theorem Th4: :: SCMFSA_I:4
for x being set
for b, c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds
[x,{},<*c,f,b*>] in SCM+FSA-Instr
proof end;

theorem Th5: :: SCMFSA_I:5
for x being set
for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds
[x,{},<*c,f*>] in SCM+FSA-Instr
proof end;

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc , b being Element of SCM-Data-Loc , J being Element of Segm 13 such that A1: x = [J,{},<*c,f,b*>] ;
func x int_addr1 -> Element of SCM-Data-Loc means :: SCMFSA_I:def 3
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & it = c );
existence
ex b1, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = c ) by A1;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = c ) holds
b1 = b2
proof end;
func x int_addr2 -> Element of SCM-Data-Loc means :: SCMFSA_I:def 4
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & it = b );
existence
ex b1, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = b ) by A1;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = b ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = b ) holds
b1 = b2;
proof end;
func x coll_addr1 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_I:def 5
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & it = f );
existence
ex b1 being Element of SCM+FSA-Data*-Loc ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = f ) by A1;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = f ) holds
b1 = b2;
proof end;
end;

:: deftheorem defines int_addr1 SCMFSA_I:def 3 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x int_addr1 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = c ) );

:: deftheorem defines int_addr2 SCMFSA_I:def 4 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x int_addr2 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = b ) );

:: deftheorem defines coll_addr1 SCMFSA_I:def 5 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f,b*>] holds
for b2 being Element of SCM+FSA-Data*-Loc holds
( b2 = x coll_addr1 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = f ) );

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM-Data-Loc such that A1: x = [13,{},<*c*>] ;
func x int_addr -> Element of SCM-Data-Loc means :: SCMFSA_I:def 6
 ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & it = c );
existence
ex b1, c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & b1 = c ) by A1;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & b1 = c ) & ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & b2 = c ) holds
b1 = b2
proof end;
end;

:: deftheorem defines int_addr SCMFSA_I:def 6 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc st x = [13,{},<*c*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x int_addr iff ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & b2 = c ) );

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc , J being Element of Segm 13 such that A1: x = [J,{},<*c,f*>] ;
func x int_addr3 -> Element of SCM-Data-Loc means :: SCMFSA_I:def 7
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & it = c );
existence
ex b1, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = c ) by A1;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = c ) holds
b1 = b2
proof end;
func x coll_addr2 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_I:def 8
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & it = f );
existence
ex b1 being Element of SCM+FSA-Data*-Loc ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = f ) by A1;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = f ) holds
b1 = b2;
proof end;
end;

:: deftheorem defines int_addr3 SCMFSA_I:def 7 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x int_addr3 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = c ) );

:: deftheorem defines coll_addr2 SCMFSA_I:def 8 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex J being Element of Segm 13 st x = [J,{},<*c,f*>] holds
for b2 being Element of SCM+FSA-Data*-Loc holds
( b2 = x coll_addr2 iff ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = f ) );

theorem :: SCMFSA_I:6
SCM+FSA-Instr c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by Lm1;

theorem Th7: :: SCMFSA_I:7
for x being Element of SCM+FSA-Instr holds
( ( x in SCM-Instr & not not InsCode x = 0 & ... & not InsCode x = 8 ) or ( x in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } & ( InsCode x = 9 or InsCode x = 10 ) ) or ( x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } & ( InsCode x = 11 or InsCode x = 12 ) ) )
proof end;

Lm2: for i being Element of SCM+FSA-Instr holds InsCode i <= 12
proof end;

Lm3: for i being Element of SCM+FSA-Instr st ( InsCode i = 9 or InsCode i = 10 ) holds
JumpPart i = {}
proof end;

Lm4: for i being Element of SCM+FSA-Instr st ( InsCode i = 11 or InsCode i = 12 ) holds
JumpPart i = {}
proof end;

registration
cluster SCM+FSA-Instr -> non empty homogeneous ;
coherence
SCM+FSA-Instr is homogeneous
proof end;
end;

Lm5: for i being Element of SCM+FSA-Instr
for ii being Element of SCM-Instr st i = ii holds
JumpParts (InsCode i) = JumpParts (InsCode ii)
proof end;

theorem Th8: :: SCMFSA_I:8
for T being InsType of SCM+FSA-Instr st ( T = 9 or T = 10 ) holds
JumpParts T = {{}}
proof end;

theorem Th9: :: SCMFSA_I:9
for T being InsType of SCM+FSA-Instr st ( T = 11 or T = 12 ) holds
JumpParts T = {{}}
proof end;

registration
cluster SCM+FSA-Instr -> non empty J/A-independent ;
coherence
SCM+FSA-Instr is J/A-independent
proof end;
end;

registration
cluster SCM+FSA-Instr -> non empty with_halt ;
coherence
SCM+FSA-Instr is with_halt by Th3;
end;