:: SCMRINGI semantic presentation

begin


registration
cluster SCM-Instr  ->  non trivial ;
coherence
 not SCM-Instr is trivial
proof
set e = the Element of SCM-Data-Loc ;
 ( 1 in {1,2,3,4,5} & 1 is Element of Segm 9 ) by ENUMSET1:def_3, NAT_1:44;
then  [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in  {  [K,{},<*b,c*>] where K is Element of Segm 9, b, c is Element of SCM-Data-Loc : K in {1,2,3,4,5}  }  ;
then A1: [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr by XBOOLE_0:def_3;
 ( 2 in {1,2,3,4,5} & 2 is Element of Segm 9 ) by ENUMSET1:def_3, NAT_1:44;
then  [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in  {  [K,{},<*b,c*>] where K is Element of Segm 9, b, c is Element of SCM-Data-Loc : K in {1,2,3,4,5}  }  ;
then A2: [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr by XBOOLE_0:def_3;
 [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] <> [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] by XTUPLE_0:3;
hence  not SCM-Instr is trivial by A1, A2, SUBSET_1:def_7; ::_thesis: verum
end;
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
proof
set e1 = the Element of SCM-Data-Loc ;
A1: SCM-Instr S = (({[0,{},{}]} \/  {  [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4}  }  ) \/  {  [6,<*i1*>,{}] where i1 is Element of NAT : verum  }  ) \/ ( {  [7,<*i2*>,<*d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum  }  \/  {  [5,{},<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum  }  ) by XBOOLE_1:4
.= ({[0,{},{}]} \/  {  [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4}  }  ) \/ ( {  [6,<*i1*>,{}] where i1 is Element of NAT : verum  }  \/ ( {  [7,<*i2*>,<*d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum  }  \/  {  [5,{},<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum  }  )) by XBOOLE_1:4
.=  {  [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4}  }  \/ ({[0,{},{}]} \/ ( {  [6,<*i1*>,{}] where i1 is Element of NAT : verum  }  \/ ( {  [7,<*i2*>,<*d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum  }  \/  {  [5,{},<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum  }  ))) by XBOOLE_1:4 ;
 ( 2 in Segm 8 & 2 in {1,2,3,4} ) by ENUMSET1:def_2, NAT_1:44;
then  [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in  {  [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4}  }  ;
then A2: [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr S by A1, XBOOLE_0:def_3;
A3: [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] <> [2,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] by XTUPLE_0:3;
 ( 1 in Segm 8 & 1 in {1,2,3,4} ) by ENUMSET1:def_2, NAT_1:44;
then  [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in  {  [I,{},<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4}  }  ;
then  [1,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr S by A1, XBOOLE_0:def_3;
hence  not SCM-Instr S is trivial by A2, A3, SUBSET_1:def_7; ::_thesis: verum
end;
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 & 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
take  mk ; ::_thesis: ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & mk = f /. 1 )
take  <*mk,ml*> ; ::_thesis: ( <*mk,ml*> = x `3_3 & mk = <*mk,ml*> /. 1 )
thus  ( <*mk,ml*> = x `3_3 & mk = <*mk,ml*> /. 1 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum
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 ;
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 & 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 & b1 = f /. 2 )
proof
take  ml ; ::_thesis: ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & ml = f /. 2 )
take  <*mk,ml*> ; ::_thesis: ( <*mk,ml*> = x `3_3 & ml = <*mk,ml*> /. 2 )
thus  ( <*mk,ml*> = x `3_3 & ml = <*mk,ml*> /. 2 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum
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 /. 2 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & 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 & 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 & 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 & x address_2 = ml )
proof
let I be Element of Segm 8; ::_thesis: 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 & x address_2 = ml )
let S be non empty 1-sorted ; ::_thesis: 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 & x address_2 = ml )
let x be Element of SCM-Instr S; ::_thesis: for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
let mk, ml be Element of SCM-Data-Loc ; ::_thesis: ( x = [I,{},<*mk,ml*>] implies ( x address_1 = mk & x address_2 = ml ) )
assume A1: x = [I,{},<*mk,ml*>] ; ::_thesis: ( x address_1 = mk & x address_2 = ml )
then consider f being FinSequence of SCM-Data-Loc  such that
A2: f = x `3_3 and
A3: x address_1 = f /. 1 by Def2;
 f = <*mk,ml*> by A1, A2, RECDEF_2:def_3;
hence  x address_1 = mk by A3, FINSEQ_4:17; ::_thesis: x address_2 = ml
consider f being FinSequence of SCM-Data-Loc  such that
A4: f = x `3_3 and
A5: x address_2 = f /. 2 by A1, Def3;
 f = <*mk,ml*> by A1, A4, RECDEF_2:def_3;
hence  x address_2 = ml by A5, FINSEQ_4:17; ::_thesis: verum
end;

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 & it = f /. 1 );
existence
 ex b1 being Element of NAT ex f being FinSequence of NAT st
( f = x `2_3 & b1 = f /. 1 )
proof
take  mk ; ::_thesis: ex f being FinSequence of NAT st
( f = x `2_3 & mk = f /. 1 )
take  <*mk*> ; ::_thesis: ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 )
thus  ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st ex f being FinSequence of NAT st
( f = x `2_3 & b1 = f /. 1 ) & ex f being FinSequence of NAT st
( f = x `2_3 & 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 & 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
proof
let I be Element of Segm 8; ::_thesis: 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
let S be non empty 1-sorted ; ::_thesis: for x being Element of SCM-Instr S
for mk being Element of NAT st x = [I,<*mk*>,{}] holds
x jump_address = mk
let x be Element of SCM-Instr S; ::_thesis: for mk being Element of NAT st x = [I,<*mk*>,{}] holds
x jump_address = mk
let mk be Element of NAT ; ::_thesis: ( x = [I,<*mk*>,{}] implies x jump_address = mk )
assume A1: x = [I,<*mk*>,{}] ; ::_thesis: x jump_address = mk
then consider f being FinSequence of NAT  such that
A2: f = x `2_3 and
A3: x jump_address = f /. 1 by Def4;
 f = <*mk*> by A1, A2, RECDEF_2:def_2;
hence  x jump_address = mk by A3, FINSEQ_4:16; ::_thesis: verum
end;

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 & it = <*mk*> /. 1 );
existence
 ex b1, mk being Element of NAT st
( <*mk*> = x `2_3 & b1 = <*mk*> /. 1 )
proof
take  mk ; ::_thesis: ex mk being Element of NAT st
( <*mk*> = x `2_3 & mk = <*mk*> /. 1 )
take  mk ; ::_thesis: ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 )
thus  ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st ex mk being Element of NAT st
( <*mk*> = x `2_3 & b1 = <*mk*> /. 1 ) & ex mk being Element of NAT st
( <*mk*> = x `2_3 & 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 & it = <*ml*> /. 1 );
existence
 ex b1, ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b1 = <*ml*> /. 1 )
proof
take  ml ; ::_thesis: ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & ml = <*ml*> /. 1 )
take  ml ; ::_thesis: ( <*ml*> = x `3_3 & ml = <*ml*> /. 1 )
thus  ( <*ml*> = x `3_3 & ml = <*ml*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b1 = <*ml*> /. 1 ) & ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & 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 & 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 & 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 & x cond_address = ml )
proof
let I be Element of Segm 8; ::_thesis: 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 & x cond_address = ml )
let S be non empty 1-sorted ; ::_thesis: 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 & x cond_address = ml )
let x be Element of SCM-Instr S; ::_thesis: for mk being Element of NAT
for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let mk be Element of NAT ; ::_thesis: for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let ml be Element of SCM-Data-Loc ; ::_thesis: ( x = [I,<*mk*>,<*ml*>] implies ( x cjump_address = mk & x cond_address = ml ) )
assume A1: x = [I,<*mk*>,<*ml*>] ; ::_thesis: ( x cjump_address = mk & x cond_address = ml )
then consider mk9 being Element of NAT  such that
A2: <*mk9*> = x `2_3 and
A3: x cjump_address = <*mk9*> /. 1 by Def5;
 <*mk9*> = <*mk*> by A1, A2, RECDEF_2:def_2;
hence  x cjump_address = mk by A3, FINSEQ_4:16; ::_thesis: x cond_address = ml
consider ml9 being Element of SCM-Data-Loc  such that
A4: <*ml9*> = x `3_3 and
A5: x cond_address = <*ml9*> /. 1 by A1, Def6;
 <*ml9*> = <*ml*> by A1, A4, RECDEF_2:def_3;
hence  x cond_address = ml by A5, FINSEQ_4:16; ::_thesis: verum
end;

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
proof
let y be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not y in proj2 <*d,s*> or y in SCM-Data-Loc \/ the carrier of S )
A1: dom <*d,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
assume  y in rng <*d,s*> ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then consider x being set  such that
A2: x in dom <*d,s*> and
A3: <*d,s*> . x = y by FUNCT_1:def_3;
percases ( x = 1 or x = 2 ) by A2, A1, TARSKI:def_2;
suppose x = 1 ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then  y = d by A3, FINSEQ_1:44;
hence  y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = 2 ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then  y = s by A3, FINSEQ_1:44;
hence  y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
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 & 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 & b1 = f /. 1 )
proof
take  mk ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & mk = f /. 1 )
take  <*mk,r*> ; ::_thesis: ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 )
 ( mk is Element of SCM-Data-Loc \/ the carrier of S & r is Element of SCM-Data-Loc \/ the carrier of S ) by XBOOLE_0:def_3;
hence  ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum
end;
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 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & 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 & 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 & b1 = f /. 2 )
proof
take  r ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & r = f /. 2 )
take  <*mk,r*> ; ::_thesis: ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 )
 ( mk is Element of SCM-Data-Loc \/ the carrier of S & r is Element of SCM-Data-Loc \/ the carrier of S ) by XBOOLE_0:def_3;
hence  ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum
end;
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 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & 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 & 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 & 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 & x const_value = r )
proof
let I be Element of Segm 8; ::_thesis: 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 & x const_value = r )
let S be non empty 1-sorted ; ::_thesis: 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 & x const_value = r )
let x be Element of SCM-Instr S; ::_thesis: for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let mk be Element of SCM-Data-Loc ; ::_thesis: for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let r be Element of S; ::_thesis: ( x = [I,{},<*mk,r*>] implies ( x const_address = mk & x const_value = r ) )
A1: ( mk is Element of SCM-Data-Loc \/ the carrier of S & r is Element of SCM-Data-Loc \/ the carrier of S ) by XBOOLE_0:def_3;
assume A2: x = [I,{},<*mk,r*>] ; ::_thesis: ( x const_address = mk & x const_value = r )
then consider f being FinSequence of SCM-Data-Loc \/ the carrier of S such that
A3: f = x `3_3 and
A4: x const_address = f /. 1 by Def7;
 f = <*mk,r*> by A2, A3, RECDEF_2:def_3;
hence  x const_address = mk by A4, A1, FINSEQ_4:17; ::_thesis: x const_value = r
consider f being FinSequence of SCM-Data-Loc \/ the carrier of S such that
A5: f = x `3_3 and
A6: x const_value = f /. 2 by A2, Def8;
 f = <*mk,r*> by A2, A5, RECDEF_2:def_3;
hence  x const_value = r by A1, A6, FINSEQ_4:17; ::_thesis: verum
end;

theorem Th5: :: SCMRINGI:5
for S being non empty 1-sorted holds SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
proof
let S be non empty 1-sorted ; ::_thesis: SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
set X = proj2 (SCM-Instr S);
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in SCM-Instr S or u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] )
assume A1: u in SCM-Instr S ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
A2: {} in NAT * by FINSEQ_1:49;
percases ( u in (({[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  }  or u in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ) by A1, XBOOLE_0:def_3;
supposeA3: u in (({[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  }  ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
percases ( u in ({[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  }  or u in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ) by A3, XBOOLE_0:def_3;
supposeA4: u in ({[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  }  ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
percases ( u in {[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}  }  or u in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ) by A4, XBOOLE_0:def_3;
supposeA5: u in {[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}  }  ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
percases ( u in {[0,{},{}]} or u 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}  }  ) by A5, XBOOLE_0:def_3;
suppose u in {[0,{},{}]} ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then A6: u = [0,{},{}] by TARSKI:def_1;
then  ( 0 in NAT & {} in proj2 (SCM-Instr S) ) by A1, XTUPLE_0:def_13;
hence  u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A6, A2, MCART_1:69; ::_thesis: verum
end;
suppose u 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}  }  ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc  such that
A7: ( u = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
 ( I in NAT & <*a,b*> in proj2 (SCM-Instr S) ) by A7, A1, XTUPLE_0:def_13;
hence  u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A7, A2, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose u in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then consider i being Element of NAT  such that
A8: u = [6,<*i*>,{}] ;
A9: <*i*> in NAT * by FUNCT_7:18;
 ( 6 in NAT & {} in proj2 (SCM-Instr S) ) by A8, A1, XTUPLE_0:def_13;
hence  u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A8, A9, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose u in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then consider i being Element of NAT , a being Element of SCM-Data-Loc  such that
A10: u = [7,<*i*>,<*a*>] ;
A11: <*i*> in NAT * by FUNCT_7:18;
 ( 7 in NAT & <*a*> in proj2 (SCM-Instr S) ) by A10, A1, XTUPLE_0:def_13;
hence  u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A10, A11, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose u in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ; ::_thesis: u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
then consider a being Element of SCM-Data-Loc , r being Element of S such that
A12: u = [5,{},<*a,r*>] ;
 ( 5 in NAT & <*a,r*> in proj2 (SCM-Instr S) ) by A12, A1, XTUPLE_0:def_13;
hence  u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] by A12, A2, MCART_1:69; ::_thesis: verum
end;
end;
end;

registration
let S be non empty 1-sorted ;
cluster proj2 (SCM-Instr S) ->  FinSequence-membered ;
coherence
 proj2 (SCM-Instr S) is FinSequence-membered
proof
let f be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not f in proj2 (SCM-Instr S) or f is set )
assume  f in proj2 (SCM-Instr S) ; ::_thesis: f is set
then consider y being set  such that
A1: [y,f] in SCM-Instr S by XTUPLE_0:def_13;
set u = [y,f];
percases ( [y,f] in (({[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  }  or [y,f] in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ) by A1, XBOOLE_0:def_3;
supposeA2: [y,f] in (({[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  }  ; ::_thesis: f is set
percases ( [y,f] in ({[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  }  or [y,f] in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ) by A2, XBOOLE_0:def_3;
supposeA3: [y,f] in ({[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  }  ; ::_thesis: f is set
percases ( [y,f] in {[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}  }  or [y,f] in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ) by A3, XBOOLE_0:def_3;
supposeA4: [y,f] in {[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}  }  ; ::_thesis: f is set
percases ( [y,f] in {[0,{},{}]} or [y,f] 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}  }  ) by A4, XBOOLE_0:def_3;
suppose [y,f] in {[0,{},{}]} ; ::_thesis: f is set
then  [y,f] = [0,{},{}] by TARSKI:def_1;
then  f = {} by XTUPLE_0:1;
hence  f is FinSequence ; ::_thesis: verum
end;
suppose [y,f] 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}  }  ; ::_thesis: f is set
then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc  such that
A5: ( [y,f] = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
 f = <*a,b*> by A5, XTUPLE_0:1;
hence  f is FinSequence ; ::_thesis: verum
end;
end;
end;
suppose [y,f] in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ; ::_thesis: f is set
then consider i being Element of NAT  such that
A6: [y,f] = [6,<*i*>,{}] ;
 f = {} by A6, XTUPLE_0:1;
hence  f is FinSequence ; ::_thesis: verum
end;
end;
end;
suppose [y,f] in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ; ::_thesis: f is set
then consider i being Element of NAT , a being Element of SCM-Data-Loc  such that
A7: [y,f] = [7,<*i*>,<*a*>] ;
 f = <*a*> by A7, XTUPLE_0:1;
hence  f is FinSequence ; ::_thesis: verum
end;
end;
end;
suppose [y,f] in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ; ::_thesis: f is set
then consider a being Element of SCM-Data-Loc , r being Element of S such that
A8: [y,f] = [5,{},<*a,r*>] ;
 f = <*a,r*> by A8, XTUPLE_0:1;
hence  f is FinSequence ; ::_thesis: verum
end;
end;
end;
end;

theorem Th6: :: SCMRINGI:6
for S being non empty 1-sorted holds [0,{},{}] in SCM-Instr S
proof
let S be non empty 1-sorted ; ::_thesis: [0,{},{}] in SCM-Instr S
 [0,{},{}] in {[0,{},{}]} by TARSKI:def_1;
then  [0,{},{}] in {[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}  }  by XBOOLE_0:def_3;
then  [0,{},{}] in ({[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  }  by XBOOLE_0:def_3;
then  [0,{},{}] in (({[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  }  by XBOOLE_0:def_3;
hence  [0,{},{}] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th7: :: 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  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  & InsCode x = 6 ) or ( x in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  & InsCode x = 7 ) or ( x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  & InsCode x = 5 ) )
proof
let S be non empty 1-sorted ; ::_thesis: 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  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  & InsCode x = 6 ) or ( x in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  & InsCode x = 7 ) or ( x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  & InsCode x = 5 ) )
let x be Element of SCM-Instr S; ::_thesis: ( ( 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  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  & InsCode x = 6 ) or ( x in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  & InsCode x = 7 ) or ( x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  & InsCode x = 5 ) )
 ( x in (({[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  }  or x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ) by XBOOLE_0:def_3;
then  ( x in ({[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  }  or x in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  or x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ) by XBOOLE_0:def_3;
then  ( x in {[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}  }  or x in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  or x in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  or x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ) by XBOOLE_0:def_3;
percasesthen  ( x in {[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}  }  or x in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  or x in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  or x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ) by XBOOLE_0:def_3;
case x in {[0,{},{}]} ; ::_thesis: InsCode x = 0
then  x = [0,{},{}] by TARSKI:def_1;
hence  InsCode x = 0 by RECDEF_2:def_1; ::_thesis: verum
end;
case 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}  }  ; ::_thesis: ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 )
then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc  such that
A1: x = [I,{},<*a,b*>] and
A2: I in {1,2,3,4} ;
 InsCode x = I by A1, RECDEF_2:def_1;
hence  ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) by A2, ENUMSET1:def_2; ::_thesis: verum
end;
case x in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ; ::_thesis: InsCode x = 6
then  ex i being Element of NAT st x = [6,<*i*>,{}] ;
hence  InsCode x = 6 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ; ::_thesis: InsCode x = 7
then  ex i being Element of NAT ex a being Element of SCM-Data-Loc st x = [7,<*i*>,<*a*>] ;
hence  InsCode x = 7 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  ; ::_thesis: InsCode x = 5
then  ex a being Element of SCM-Data-Loc ex r being Element of S st x = [5,{},<*a,r*>] ;
hence  InsCode x = 5 by RECDEF_2:def_1; ::_thesis: verum
end;
end;
end;

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 & b1 is trivial )
proof
take  the 1 -element strict doubleLoopStr ; ::_thesis: ( the 1 -element strict doubleLoopStr is strict & the 1 -element strict doubleLoopStr is trivial )
thus  ( the 1 -element strict doubleLoopStr is strict & the 1 -element strict doubleLoopStr is trivial ) ; ::_thesis: verum
end;
end;

registration
let R be Ring;
cluster SCM-Instr R ->  non empty standard-ins ;
coherence
 SCM-Instr R is standard-ins
proof
consider X being non empty set  such that
A1: proj2 (SCM-Instr R) c= X * by FINSEQ_1:85;
take  X ; :: according to COMPOS_0:def_1 ::_thesis: SCM-Instr R c= [:NAT,(NAT *),(X *):]
A2: SCM-Instr R c= [:NAT,(NAT *),(proj2 (SCM-Instr R)):] by Th5;
 [:NAT,(NAT *),(proj2 (SCM-Instr R)):] c= [:NAT,(NAT *),(X *):] by A1, MCART_1:73;
hence  SCM-Instr R c= [:NAT,(NAT *),(X *):] by A2, XBOOLE_1:1; ::_thesis: verum
end;
end;

Lm1:  for R being Ring
for i being Element of SCM-Instr R holds InsCode i <= 7
proof
let R be Ring; ::_thesis: for i being Element of SCM-Instr R holds InsCode i <= 7
let i be Element of SCM-Instr R; ::_thesis: InsCode i <= 7
 ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 ) by Th7;
hence  InsCode i <= 7 ; ::_thesis: verum
end;

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 = {}
proof
let S be non empty 1-sorted ; ::_thesis: 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 = {}
let i be Element of SCM-Instr S; ::_thesis: ( ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) implies JumpPart i = {} )
assume  ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) ; ::_thesis: JumpPart i = {}
then  i 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}  }  by Th7;
then  ex I being Element of Segm 8 ex a, b being Element of SCM-Data-Loc st
( i = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
hence  JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;

Lm3:  for S being non empty 1-sorted
for i being Element of SCM-Instr S st InsCode i = 5 holds
JumpPart i = {}
proof
let S be non empty 1-sorted ; ::_thesis: for i being Element of SCM-Instr S st InsCode i = 5 holds
JumpPart i = {}
let i be Element of SCM-Instr S; ::_thesis: ( InsCode i = 5 implies JumpPart i = {} )
assume  InsCode i = 5 ; ::_thesis: JumpPart i = {}
then  i in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum  }  by Th7;
then  ex a being Element of SCM-Data-Loc ex r being Element of S st i = [5,{},<*a,r*>] ;
hence  JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;

Lm4:  for R being Ring
for I being Element of SCM-Instr R st InsCode I = 6 holds
dom (JumpPart I) = Seg 1
proof
let R be Ring; ::_thesis: for I being Element of SCM-Instr R st InsCode I = 6 holds
dom (JumpPart I) = Seg 1
let I be Element of SCM-Instr R; ::_thesis: ( InsCode I = 6 implies dom (JumpPart I) = Seg 1 )
assume  InsCode I = 6 ; ::_thesis: dom (JumpPart I) = Seg 1
then  I in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  by Th7;
then consider i being Element of NAT  such that
A1: I = [6,<*i*>,{}] ;
 JumpPart I = <*i*> by A1, RECDEF_2:def_2;
hence  dom (JumpPart I) = Seg 1 by FINSEQ_1:38; ::_thesis: verum
end;

Lm5:  for R being Ring
for I being Element of SCM-Instr R st InsCode I = 7 holds
dom (JumpPart I) = Seg 1
proof
let R be Ring; ::_thesis: for I being Element of SCM-Instr R st InsCode I = 7 holds
dom (JumpPart I) = Seg 1
let I be Element of SCM-Instr R; ::_thesis: ( InsCode I = 7 implies dom (JumpPart I) = Seg 1 )
assume  InsCode I = 7 ; ::_thesis: dom (JumpPart I) = Seg 1
then  I in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  by Th7;
then consider i being Element of NAT , a being Element of SCM-Data-Loc  such that
A1: I = [7,<*i*>,<*a*>] ;
 JumpPart I = <*i*> by A1, RECDEF_2:def_2;
hence  dom (JumpPart I) = Seg 1 by FINSEQ_1:38; ::_thesis: verum
end;

registration
let R be Ring;
cluster SCM-Instr R ->  non empty homogeneous ;
coherence
 SCM-Instr R is homogeneous
proof
let i, j be Element of SCM-Instr R; :: according to COMPOS_0:def_5 ::_thesis: ( not InsCode i = InsCode j or dom (i `2_3) = dom (j `2_3) )
assume A1: InsCode i = InsCode j ; ::_thesis: dom (i `2_3) = dom (j `2_3)
 InsCode i <= 7 by Lm1;
percasesthen  ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 ) by NAT_1:31;
suppose InsCode i = 0 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( i in {[0,{},{}]} & j in {[0,{},{}]} ) by A1, Th7;
then  ( i = [0,{},{}] & j = [0,{},{}] ) by TARSKI:def_1;
hence  dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm2;
hence  dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose InsCode i = 5 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm3;
hence  dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose InsCode i = 6 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm4;
hence  dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm5;
hence  dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
end;
end;
end;


registration
let R be Ring;
cluster SCM-Instr R ->  non empty J/A-independent ;
coherence
 SCM-Instr R is J/A-independent
proof
let T be InsType of (SCM-Instr R); :: according to COMPOS_0:def_7 ::_thesis: for b1, b2 being set holds
( not b1 in JumpParts T or not proj1 b1 = proj1 b2 or for b3 being set holds
( not [T,b1,b3] in SCM-Instr R or [T,b2,b3] in SCM-Instr R ) )
let f1, f2 be natural-valued Function; ::_thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b1 being set holds
( not [T,f1,b1] in SCM-Instr R or [T,f2,b1] in SCM-Instr R ) )
assume that
A1: f1 in JumpParts T and
A2: dom f1 = dom f2 ; ::_thesis: for b1 being set holds
( not [T,f1,b1] in SCM-Instr R or [T,f2,b1] in SCM-Instr R )
let p be set ; ::_thesis: ( not [T,f1,p] in SCM-Instr R or [T,f2,p] in SCM-Instr R )
assume A3: [T,f1,p] in SCM-Instr R ; ::_thesis: [T,f2,p] in SCM-Instr R
reconsider II = [T,f1,p] as Element of SCM-Instr R by A3;
A4: InsCode II = T by RECDEF_2:def_1;
 InsCode II <= 7 by Lm1;
percasesthen  ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by A4, NAT_1:31;
suppose T = 0 ; ::_thesis: [T,f2,p] in SCM-Instr R
then  II in {[0,{},{}]} by A4, Th7;
then  II = [0,{},{}] by TARSKI:def_1;
then  JumpPart II = {} by RECDEF_2:def_2;
then A5: JumpParts T = {0} by A4, COMPOS_0:11;
 f1 = 0 by A5, A1, TARSKI:def_1;
then  f1 = f2 by A2;
hence  [T,f2,p] in SCM-Instr R by A3; ::_thesis: verum
end;
suppose ( T = 1 or T = 2 or T = 3 or T = 4 ) ; ::_thesis: [T,f2,p] in SCM-Instr R
then  II 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}  }  by A4, Th7;
then  ex I being Element of Segm 8 ex a, b being Element of SCM-Data-Loc st
( II = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
then  JumpPart II = {} by RECDEF_2:def_2;
then A6: JumpParts T = {0} by A4, COMPOS_0:11;
 f1 = 0 by A6, A1, TARSKI:def_1;
then  f1 = f2 by A2;
hence  [T,f2,p] in SCM-Instr R by A3; ::_thesis: verum
end;
suppose T = 5 ; ::_thesis: [T,f2,p] in SCM-Instr R
then  II in  {  [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum  }  by A4, Th7;
then  ex a being Element of SCM-Data-Loc ex r being Element of R st II = [5,{},<*a,r*>] ;
then  JumpPart II = {} by RECDEF_2:def_2;
then A7: JumpParts T = {0} by A4, COMPOS_0:11;
 f1 = 0 by A7, A1, TARSKI:def_1;
then  f1 = f2 by A2;
hence  [T,f2,p] in SCM-Instr R by A3; ::_thesis: verum
end;
supposeA8: T = 6 ; ::_thesis: [T,f2,p] in SCM-Instr R
reconsider J = [T,f1,p] as Element of SCM-Instr R by A3;
 InsCode J = 6 by A8, RECDEF_2:def_1;
then  J in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  by Th7;
then consider i1 being Element of NAT  such that
A9: J = [6,<*i1*>,{}] ;
A10: p = {} by A9, XTUPLE_0:3;
 f1 = <*i1*> by A9, XTUPLE_0:3;
then A11: dom f2 = {1} by A2, FINSEQ_1:2, FINSEQ_1:38;
reconsider l = f2 . 1 as Element of NAT by ORDINAL1:def_12;
set I = [T,f2,{}];
A12: [T,f2,{}] = [6,<*l*>,{}] by A8, A11, FINSEQ_1:2, FINSEQ_1:def_8;
 [6,<*l*>,{}] in  {  [6,<*n*>,{}] where n is Element of NAT : verum  }  ;
then  [6,<*l*>,{}] in ({[0,{},{}]} \/  {  [H,{},<*a,b*>] where H is Element of Segm 8, a, b is Element of SCM-Data-Loc : H in {1,2,3,4}  }  ) \/  {  [6,<*n*>,{}] where n is Element of NAT : verum  }  by XBOOLE_0:def_3;
then  [6,<*l*>,{}] in (({[0,{},{}]} \/  {  [H,{},<*a,b*>] where H is Element of Segm 8, a, b is Element of SCM-Data-Loc : H in {1,2,3,4}  }  ) \/  {  [6,<*n*>,{}] where n is Element of NAT : verum  }  ) \/  {  [7,<*n*>,<*a*>] where n is Element of NAT , a is Element of SCM-Data-Loc : verum  }  by XBOOLE_0:def_3;
then  [6,<*l*>,{}] in SCM-Instr R by XBOOLE_0:def_3;
then reconsider I = [T,f2,{}] as Element of SCM-Instr R by A12;
 f2 = JumpPart I by RECDEF_2:def_2;
hence  [T,f2,p] in SCM-Instr R by A10; ::_thesis: verum
end;
supposeA13: T = 7 ; ::_thesis: [T,f2,p] in SCM-Instr R
reconsider J = [T,f1,p] as Element of SCM-Instr R by A3;
 InsCode J = T by RECDEF_2:def_1;
then  J in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  by A13, Th7;
then consider i1 being Element of NAT , a being Element of SCM-Data-Loc  such that
A14: J = [7,<*i1*>,<*a*>] ;
A15: p = <*a*> by A14, XTUPLE_0:3;
 f1 = <*i1*> by A14, XTUPLE_0:3;
then A16: dom f2 = {1} by A2, FINSEQ_1:2, FINSEQ_1:38;
reconsider l = f2 . 1 as Element of NAT by ORDINAL1:def_12;
set I = [T,f2,p];
A17: [T,f2,p] = [T,<*l*>,<*a*>] by A15, A16, FINSEQ_1:2, FINSEQ_1:def_8;
 [(InsCode [T,f2,p]),<*l*>,<*a*>] in  {  [7,<*n*>,<*c*>] where n is Element of NAT , c is Element of SCM-Data-Loc : verum  }  by A13;
then  [(InsCode [T,f2,p]),<*l*>,<*a*>] in (({[0,{},{}]} \/  {  [H,{},<*a7,b7*>] where H is Element of Segm 8, a7, b7 is Element of SCM-Data-Loc : H in {1,2,3,4}  }  ) \/  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ) \/  {  [7,<*i*>,<*a7*>] where i is Element of NAT , a7 is Element of SCM-Data-Loc : verum  }  by XBOOLE_0:def_3;
then  [(InsCode [T,f2,p]),<*l*>,<*a*>] in ((({[0,{},{}]} \/  {  [H,{},<*a7,b7*>] where H is Element of Segm 8, a7, b7 is Element of SCM-Data-Loc : H in {1,2,3,4}  }  ) \/  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ) \/  {  [7,<*i*>,<*a7*>] where i is Element of NAT , a7 is Element of SCM-Data-Loc : verum  }  ) \/  {  [5,{},<*a7,r7*>] where a7 is Element of SCM-Data-Loc , r7 is Element of R : verum  }  by XBOOLE_0:def_3;
then  [(InsCode [T,f2,p]),<*l*>,<*a*>] in SCM-Instr R ;
then reconsider I = [T,f2,p] as Element of SCM-Instr R by A17;
 InsCode I = T by RECDEF_2:def_1;
then  I in  {  [7,<*i2*>,<*b*>] where i2 is Element of NAT , b is Element of SCM-Data-Loc : verum  }  by A13, Th7;
then consider i2 being Element of NAT , b being Element of SCM-Data-Loc  such that
A18: I = [7,<*i2*>,<*b*>] ;
7 = InsCode I by A18, RECDEF_2:def_1
.= T by RECDEF_2:def_1 ;
then A19: I = [T,<*i2*>,<*b*>] by A18;
thus  [T,f2,p] in SCM-Instr R by A19; ::_thesis: verum
end;
end;
end;
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
proof
let S be non empty 1-sorted ; ::_thesis: 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
let x be set ; ::_thesis: for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let d1, d2 be Element of SCM-Data-Loc ; ::_thesis: ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )
reconsider D1 = d1, D2 = d2 as Element of SCM-Data-Loc ;
assume A1: x in {1,2,3,4} ; ::_thesis: [x,{},<*d1,d2*>] in SCM-Instr S
then  ( x = 1 or x = 2 or x = 3 or x = 4 ) by ENUMSET1:def_2;
then reconsider x = x as Element of Segm 8 by NAT_1:44;
 [x,{},<*D1,D2*>] 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}  }  by A1;
then  [x,{},<*D1,D2*>] in {[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}  }  by XBOOLE_0:def_3;
then  [x,{},<*D1,D2*>] in ({[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  }  by XBOOLE_0:def_3;
then  [x,{},<*D1,D2*>] in (({[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  }  by XBOOLE_0:def_3;
hence  [x,{},<*d1,d2*>] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;

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
proof
let S be non empty 1-sorted ; ::_thesis: for t being Element of S
for d1 being Element of SCM-Data-Loc holds [5,{},<*d1,t*>] in SCM-Instr S
let t be Element of S; ::_thesis: for d1 being Element of SCM-Data-Loc holds [5,{},<*d1,t*>] in SCM-Instr S
let d1 be Element of SCM-Data-Loc ; ::_thesis: [5,{},<*d1,t*>] in SCM-Instr S
reconsider D1 = d1 as Element of SCM-Data-Loc ;
 [5,{},<*D1,t*>] in  {  [5,{},<*i,a*>] where i is Element of SCM-Data-Loc , a is Element of S : verum  }  ;
hence  [5,{},<*d1,t*>] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: SCMRINGI:10
for S being non empty 1-sorted
for i1 being Element of NAT holds [6,<*i1*>,{}] in SCM-Instr S
proof
let S be non empty 1-sorted ; ::_thesis: for i1 being Element of NAT holds [6,<*i1*>,{}] in SCM-Instr S
let i1 be Element of NAT ; ::_thesis: [6,<*i1*>,{}] in SCM-Instr S
reconsider I1 = i1 as Element of NAT ;
 [6,<*I1*>,{}] in  {  [6,<*i*>,{}] where i is Element of NAT : verum  }  ;
then  [6,<*I1*>,{}] in ({[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  }  by XBOOLE_0:def_3;
then  [6,<*I1*>,{}] in (({[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  }  by XBOOLE_0:def_3;
hence  [6,<*i1*>,{}] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;

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
proof
let S be non empty 1-sorted ; ::_thesis: for d1 being Element of SCM-Data-Loc
for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S
let d1 be Element of SCM-Data-Loc ; ::_thesis: for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S
let i1 be Element of NAT ; ::_thesis: [7,<*i1*>,<*d1*>] in SCM-Instr S
reconsider D1 = d1 as Element of SCM-Data-Loc ;
reconsider I1 = i1 as Element of NAT ;
 [7,<*I1*>,<*D1*>] in  {  [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum  }  ;
then  [7,<*I1*>,<*D1*>] in (({[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  }  by XBOOLE_0:def_3;
hence  [7,<*i1*>,<*d1*>] in SCM-Instr S by XBOOLE_0:def_3; ::_thesis: verum
end;

registration
let S be non empty 1-sorted ;
cluster SCM-Instr S ->  non empty with_halt ;
coherence
 SCM-Instr S is with_halt
proof
thus  [0,{},{}] in SCM-Instr S by Th6; :: according to COMPOS_0:def_10 ::_thesis: verum
end;
end;