:: The Construction of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

registration
cluster SCM-Instr  ->  non trivial ;
coherence
 not SCM-Instr is trivial
proofend;
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}  }  ) \/  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ) \/  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ) \/  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ;
coherence
 ((({[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}  }  ) \/  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ) \/  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ) \/  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  is non empty set ;
end;

:: deftheorem  defines SCM-Instr SCMRINGI:def_1_:_
 for S being non empty 1-sorted holds SCM-Instr S = ((({[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}  }  ) \/  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ) \/  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ) \/  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ;

registration
let S be non empty 1-sorted ;
cluster SCM-Instr S ->  non empty non trivial ;
coherence
 not SCM-Instr S is trivial
proofend;
end;

definition
let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,{},<*mk,ml*>] ;
funcx address_1  ->  Element of SCM-Data-Loc  means :Def2: :: SCMRINGI:def 2
 ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; 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 &amp; b1 = f /. 1 )
proofend;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b1 = f /. 1 ) &amp; ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b2 = f /. 1 ) holds
b1 = b2 ;
funcx address_2  ->  Element of SCM-Data-Loc  means :Def3: :: SCMRINGI:def 3
 ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; it = f /. 2 );
existence
 ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b1 = f /. 2 )
proofend;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b1 = f /. 2 ) &amp; ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b2 = f /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines address_1 SCMRINGI:def_2_:_
 for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b3 = f /. 1 ) );

:: deftheorem Def3 defines address_2 SCMRINGI:def_3_:_
 for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = x address_2 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 &amp; b3 = f /. 2 ) );

theorem :: SCMRINGI:1
for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk &amp; x address_2 = ml )
proofend;

definition
let R be non empty 1-sorted ;
let x be Element of SCM-Instr R;
given mk being Element of NAT , I being Element of Segm 8 such that A1: x = [I,<*mk*>,{}] ;
funcx jump_address  ->  Element of NAT  means :Def4: :: SCMRINGI:def 4
 ex f being FinSequence of NAT st
( f = x `2_3 &amp; it = f /. 1 );
existence
 ex b1 being Element of NAT ex f being FinSequence of NAT st
( f = x `2_3 &amp; b1 = f /. 1 )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex f being FinSequence of NAT st
( f = x `2_3 &amp; b1 = f /. 1 ) &amp; ex f being FinSequence of NAT st
( f = x `2_3 &amp; b2 = f /. 1 ) holds
b1 = b2 ;
end;

:: deftheorem Def4 defines jump_address SCMRINGI:def_4_:_
 for R being non empty 1-sorted
for x being Element of SCM-Instr R st ex mk being Element of NAT ex I being Element of Segm 8 st x = [I,<*mk*>,{}] holds
for b3 being Element of NAT holds
( b3 = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 &amp; b3 = f /. 1 ) );

theorem :: SCMRINGI:2
for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT st x = [I,<*mk*>,{}] holds
x jump_address = mk
proofend;

definition
let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,<*mk*>,<*ml*>] ;
funcx cjump_address  ->  Element of NAT  means :Def5: :: SCMRINGI:def 5
 ex mk being Element of NAT st
( <*mk*> = x `2_3 &amp; it = <*mk*> /. 1 );
existence
 ex b1, mk being Element of NAT st
( <*mk*> = x `2_3 &amp; b1 = <*mk*> /. 1 )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex mk being Element of NAT st
( <*mk*> = x `2_3 &amp; b1 = <*mk*> /. 1 ) &amp; ex mk being Element of NAT st
( <*mk*> = x `2_3 &amp; b2 = <*mk*> /. 1 ) holds
b1 = b2 ;
funcx cond_address  ->  Element of SCM-Data-Loc  means :Def6: :: SCMRINGI:def 6
 ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 &amp; it = <*ml*> /. 1 );
existence
 ex b1, ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 &amp; b1 = <*ml*> /. 1 )
proofend;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 &amp; b1 = <*ml*> /. 1 ) &amp; ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 &amp; b2 = <*ml*> /. 1 ) holds
b1 = b2 ;
end;

:: deftheorem Def5 defines cjump_address SCMRINGI:def_5_:_
 for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds
for b3 being Element of NAT holds
( b3 = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 &amp; b3 = <*mk*> /. 1 ) );

:: deftheorem Def6 defines cond_address SCMRINGI:def_6_:_
 for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 &amp; b3 = <*ml*> /. 1 ) );

theorem :: SCMRINGI:3
for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT
for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk &amp; x cond_address = ml )
proofend;

definition
let S be non empty 1-sorted ;
let d be Element of SCM-Data-Loc ;
let s be Element of S;
:: original:<*
redefine func<*d,s*> ->  FinSequence of SCM-Data-Loc \/ the carrier of S;
coherence
 <*d,s*> is FinSequence of SCM-Data-Loc \/ the carrier of S
proofend;
end;

definition
let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk being Element of SCM-Data-Loc , r being Element of S, I being Element of Segm 8 such that A1: x = [I,{},<*mk,r*>] ;
funcx const_address  ->  Element of SCM-Data-Loc  means :Def7: :: SCMRINGI:def 7
 ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; it = f /. 1 );
existence
 ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; b1 = f /. 1 )
proofend;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; b1 = f /. 1 ) &amp; ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; b2 = f /. 1 ) holds
b1 = b2 ;
funcx const_value  ->  Element of S means :Def8: :: SCMRINGI:def 8
 ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; it = f /. 2 );
existence
 ex b1 being Element of S ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; b1 = f /. 2 )
proofend;
uniqueness
 for b1, b2 being Element of S st ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; b1 = f /. 2 ) &amp; ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; b2 = f /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def7 defines const_address SCMRINGI:def_7_:_
 for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = x const_address iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; b3 = f /. 1 ) );

:: deftheorem Def8 defines const_value SCMRINGI:def_8_:_
 for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds
for b3 being Element of S holds
( b3 = x const_value iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 &amp; b3 = f /. 2 ) );

theorem :: SCMRINGI:4
for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk &amp; x const_value = r )
proofend;

theorem Th5: :: SCMRINGI:5
for S being non empty 1-sorted holds SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
proofend;

registration
let S be non empty 1-sorted ;
cluster proj2 (SCM-Instr S) ->  FinSequence-membered ;
coherence
 proj2 (SCM-Instr S) is FinSequence-membered
proofend;
end;

theorem Th6: :: SCMRINGI:6
for S being non empty 1-sorted holds [0,{},{}] in SCM-Instr S
proofend;

theorem Th7: :: SCMRINGI:7
for S being non empty 1-sorted
for x being Element of SCM-Instr S holds
( ( x in {[0,{},{}]} &amp; 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}  }  &amp; ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) ) or ( x in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  &amp; InsCode x = 6 ) or ( x in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  &amp; InsCode x = 7 ) or ( x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  &amp; InsCode x = 5 ) )
proofend;

begin

registration
cluster non empty trivial right_complementable strict V92() V93() V94() V103() V110() V111() for doubleLoopStr ;
existence
 ex b1 being Ring st
( b1 is strict &amp; b1 is trivial )
proofend;
end;

registration
let R be Ring;
cluster SCM-Instr R ->  non empty standard-ins ;
coherence
 SCM-Instr R is standard-ins
proofend;
end;

Lm1:  for R being Ring
for i being Element of SCM-Instr R holds InsCode i <= 7
proofend;

Lm2:  for S being non empty 1-sorted
for i being Element of SCM-Instr S st ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) holds
JumpPart i = {}
proofend;

Lm3:  for S being non empty 1-sorted
for i being Element of SCM-Instr S st InsCode i = 5 holds
JumpPart i = {}
proofend;

Lm4:  for R being Ring
for I being Element of SCM-Instr R st InsCode I = 6 holds
dom (JumpPart I) = Seg 1
proofend;

Lm5:  for R being Ring
for I being Element of SCM-Instr R st InsCode I = 7 holds
dom (JumpPart I) = Seg 1
proofend;

registration
let R be Ring;
cluster SCM-Instr R ->  non empty homogeneous ;
coherence
 SCM-Instr R is homogeneous
proofend;
end;

registration
let R be Ring;
cluster SCM-Instr R ->  non empty J/A-independent ;
coherence
 SCM-Instr R is J/A-independent
proofend;
end;

theorem :: SCMRINGI:8
for S being non empty 1-sorted
for x being set
for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
proofend;

theorem :: SCMRINGI:9
for S being non empty 1-sorted
for t being Element of S
for d1 being Element of SCM-Data-Loc holds [5,{},<*d1,t*>] in SCM-Instr S
proofend;

theorem :: SCMRINGI:10
for S being non empty 1-sorted
for i1 being Element of NAT holds [6,<*i1*>,{}] in SCM-Instr S
proofend;

theorem :: SCMRINGI:11
for S being non empty 1-sorted
for d1 being Element of SCM-Data-Loc
for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S
proofend;

registration
let S be non empty 1-sorted ;
cluster SCM-Instr S ->  non empty with_halt ;
coherence
 SCM-Instr S is with_halt
proofend;
end;