:: SCM_INST semantic presentation

begin


notation
synonym  SCM-Halt for  {} ;
end;

definition
:: original: SCM-Halt
redefine func SCM-Halt  ->  Element of Segm 9;
correctness
coherence
SCM-Halt is Element of Segm 9;
by NAT_1:44;
end;

definition
func SCM-Data-Loc  ->  set  equals :: SCM_INST:def 1
[:{1},NAT:];
coherence
 [:{1},NAT:] is set ;
end;

:: deftheorem  defines SCM-Data-Loc SCM_INST:def_1_:_
 SCM-Data-Loc = [:{1},NAT:];

registration
cluster SCM-Data-Loc  ->  non empty ;
coherence
 not SCM-Data-Loc is empty ;
end;


definition
func SCM-Instr  ->  non empty set  equals :: SCM_INST:def 2
(({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ) \/  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ;
coherence
 (({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ) \/  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  is non empty set ;
end;

:: deftheorem  defines SCM-Instr SCM_INST:def_2_:_
 SCM-Instr = (({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ) \/  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ;

theorem Th1: :: SCM_INST:1
[0,{},{}] in SCM-Instr
proof
 [0,{},{}] in {[SCM-Halt,{},{}]} by TARSKI:def_1;
then  [0,{},{}] in {[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  by XBOOLE_0:def_3;
then  [0,{},{}] in ({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  by XBOOLE_0:def_3;
hence  [0,{},{}] in SCM-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;

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

theorem Th2: :: SCM_INST:2
for a2 being Element of NAT holds [6,<*a2*>,{}] in SCM-Instr
proof
let a2 be Element of NAT ; ::_thesis: [6,<*a2*>,{}] in SCM-Instr
reconsider x = 6 as Element of Segm 9 by NAT_1:44;
 [x,<*a2*>,{}] in  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ;
then  [x,<*a2*>,{}] in {[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  by XBOOLE_0:def_3;
then  [x,<*a2*>,{}] in ({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  by XBOOLE_0:def_3;
hence  [6,<*a2*>,{}] in SCM-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th3: :: SCM_INST:3
for x being set
for a2 being Element of NAT
for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr
proof
let x be set ; ::_thesis: for a2 being Element of NAT
for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr
let a2 be Element of NAT ; ::_thesis: for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr
let b2 be Element of SCM-Data-Loc ; ::_thesis: ( x in {7,8} implies [x,<*a2*>,<*b2*>] in SCM-Instr )
assume A1: x in {7,8} ; ::_thesis: [x,<*a2*>,<*b2*>] in SCM-Instr
then  ( x = 7 or x = 8 ) by TARSKI:def_2;
then reconsider x = x as Element of Segm 9 by NAT_1:44;
 [x,<*a2*>,<*b2*>] in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  by A1;
then  [x,<*a2*>,<*b2*>] in ({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  by XBOOLE_0:def_3;
hence  [x,<*a2*>,<*b2*>] in SCM-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th4: :: SCM_INST:4
for x being set
for b1, c1 being Element of SCM-Data-Loc st x in {1,2,3,4,5} holds
[x,{},<*b1,c1*>] in SCM-Instr
proof
let x be set ; ::_thesis: for b1, c1 being Element of SCM-Data-Loc st x in {1,2,3,4,5} holds
[x,{},<*b1,c1*>] in SCM-Instr
let b1, c1 be Element of SCM-Data-Loc ; ::_thesis: ( x in {1,2,3,4,5} implies [x,{},<*b1,c1*>] in SCM-Instr )
assume A1: x in {1,2,3,4,5} ; ::_thesis: [x,{},<*b1,c1*>] in SCM-Instr
then  ( x = 1 or x = 2 or x = 3 or x = 4 or x = 5 ) by ENUMSET1:def_3;
then reconsider x = x as Element of Segm 9 by NAT_1:44;
 [x,{},<*b1,c1*>] in  {  [J,{},<*b,c*>] where J is Element of Segm 9, b, c is Element of SCM-Data-Loc : J in {1,2,3,4,5}  }  by A1;
hence  [x,{},<*b1,c1*>] in SCM-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;

definition
let x be Element of SCM-Instr ;
given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,{},<*mk,ml*>] ;
funcx address_1  ->  Element of SCM-Data-Loc  means :Def3: :: SCM_INST:def 3
 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 :Def4: :: SCM_INST:def 4
 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;
correctness
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 Def3 defines address_1 SCM_INST:def_3_:_
 for x being Element of SCM-Instr st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,{},<*mk,ml*>] 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 ) );

:: deftheorem Def4 defines address_2 SCM_INST:def_4_:_
 for x being Element of SCM-Instr st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x address_2 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 2 ) );

theorem :: SCM_INST:5
for x being Element of SCM-Instr
for mk, ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
proof
let x be Element of SCM-Instr ; ::_thesis: for mk, ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
let mk, ml be Element of SCM-Data-Loc ; ::_thesis: for I being Element of Segm 9 st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )
let I be Element of Segm 9; ::_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 Def3;
 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, Def4;
 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 x be Element of SCM-Instr ;
given mk being Element of NAT , I being Element of Segm 9 such that A1: x = [I,<*mk*>,{}] ;
funcx jump_address  ->  Element of NAT  means :Def5: :: SCM_INST:def 5
 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;
correctness
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 Def5 defines jump_address SCM_INST:def_5_:_
 for x being Element of SCM-Instr st ex mk being Element of NAT ex I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
for b2 being Element of NAT holds
( b2 = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 & b2 = f /. 1 ) );

theorem :: SCM_INST:6
for x being Element of SCM-Instr
for mk being Element of NAT
for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
proof
let x be Element of SCM-Instr ; ::_thesis: for mk being Element of NAT
for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
let mk be Element of NAT ; ::_thesis: for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
let I be Element of Segm 9; ::_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 Def5;
 f = <*mk*> by A1, A2, RECDEF_2:def_2;
hence  x jump_address = mk by A3, FINSEQ_4:16; ::_thesis: verum
end;

definition
let x be Element of SCM-Instr ;
given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 9 such that A1: x = [I,<*mk*>,<*ml*>] ;
funcx cjump_address  ->  Element of NAT  means :Def6: :: SCM_INST:def 6
 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;
correctness
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 :Def7: :: SCM_INST:def 7
 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;
correctness
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 Def6 defines cjump_address SCM_INST:def_6_:_
 for x being Element of SCM-Instr st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b2 being Element of NAT holds
( b2 = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 & b2 = <*mk*> /. 1 ) );

:: deftheorem Def7 defines cond_address SCM_INST:def_7_:_
 for x being Element of SCM-Instr st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b2 = <*ml*> /. 1 ) );

theorem :: SCM_INST:7
for x being Element of SCM-Instr
for mk being Element of NAT
for ml being Element of SCM-Data-Loc
for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
proof
let x be Element of SCM-Instr ; ::_thesis: for mk being Element of NAT
for ml being Element of SCM-Data-Loc
for I being Element of Segm 9 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
for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let ml be Element of SCM-Data-Loc ; ::_thesis: for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let I be Element of Segm 9; ::_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 Def6;
 <*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, Def7;
 <*ml9*> = <*ml*> by A1, A4, RECDEF_2:def_3;
hence  x cond_address = ml by A5, FINSEQ_4:16; ::_thesis: verum
end;

theorem Th8: :: SCM_INST:8
SCM-Instr c= [:NAT,(NAT *),(proj2 SCM-Instr):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SCM-Instr or x in [:NAT,(NAT *),(proj2 SCM-Instr):] )
assume A1: x in SCM-Instr ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
percases ( x in ({[SCM-Halt,{},{}]} \/  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  or x in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ) by A1, XBOOLE_0:def_3;
supposeA2: x in ({[SCM-Halt,{},{}]} \/  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
percases ( x in {[SCM-Halt,{},{}]} \/  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  or x in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ) by A2, XBOOLE_0:def_3;
supposeA3: x in {[SCM-Halt,{},{}]} \/  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
A4: SCM-Halt = 0 ;
percases ( x in {[SCM-Halt,{},{}]} or x in  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ) by A3, XBOOLE_0:def_3;
suppose x in {[SCM-Halt,{},{}]} ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then A5: x = [SCM-Halt,{},{}] by TARSKI:def_1;
then  ( SCM-Halt in NAT & {} in NAT * & {} in proj2 SCM-Instr ) by A1, A4, FINSEQ_1:49, XTUPLE_0:def_13;
hence  x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A5, DOMAIN_1:3; ::_thesis: verum
end;
suppose x in  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider J being Element of Segm 9, a being Element of NAT  such that
A6: ( x = [J,<*a*>,{}] & J = 6 ) ;
 ( J in NAT & <*a*> in NAT * & {} in proj2 SCM-Instr ) by A1, A6, FUNCT_7:18, XTUPLE_0:def_13;
hence  x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A6, DOMAIN_1:3; ::_thesis: verum
end;
end;
end;
suppose x in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc  such that
A7: ( x = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
 ( K in NAT & <*a1*> in NAT * & <*b1*> in proj2 SCM-Instr ) by A1, A7, FUNCT_7:18, XTUPLE_0:def_13;
hence  x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A7, DOMAIN_1:3; ::_thesis: verum
end;
end;
end;
suppose x in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider I being Element of Segm 9, b, c being Element of SCM-Data-Loc  such that
A8: ( x = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
 ( I in NAT & {} in NAT * & <*b,c*> in proj2 SCM-Instr ) by A1, A8, FINSEQ_1:49, XTUPLE_0:def_13;
hence  x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A8, DOMAIN_1:3; ::_thesis: verum
end;
end;
end;

registration
cluster proj2 SCM-Instr ->  FinSequence-membered ;
coherence
 proj2 SCM-Instr is FinSequence-membered
proof
let f be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not f in proj2 SCM-Instr or f is set )
assume  f in proj2 SCM-Instr ; ::_thesis: f is set
then consider y being set  such that
A1: [y,f] in SCM-Instr by XTUPLE_0:def_13;
set x = [y,f];
percases ( [y,f] in ({[SCM-Halt,{},{}]} \/  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  or [y,f] in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ) by A1, XBOOLE_0:def_3;
supposeA2: [y,f] in ({[SCM-Halt,{},{}]} \/  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ; ::_thesis: f is set
percases ( [y,f] in {[SCM-Halt,{},{}]} \/  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  or [y,f] in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ) by A2, XBOOLE_0:def_3;
supposeA3: [y,f] in {[SCM-Halt,{},{}]} \/  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ; ::_thesis: f is set
percases ( [y,f] in {[SCM-Halt,{},{}]} or [y,f] in  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ) by A3, XBOOLE_0:def_3;
suppose [y,f] in {[SCM-Halt,{},{}]} ; ::_thesis: f is set
then  [y,f] = [SCM-Halt,{},{}] by TARSKI:def_1;
hence  f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
suppose [y,f] in  {  [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Element of NAT : J = 6  }  ; ::_thesis: f is set
then  ex J being Element of Segm 9 ex a being Element of NAT st
( [y,f] = [J,<*a*>,{}] & J = 6 ) ;
hence  f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
suppose [y,f] in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ; ::_thesis: f is set
then  ex K being Element of Segm 9 ex a1 being Element of NAT ex b1 being Element of SCM-Data-Loc st
( [y,f] = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
hence  f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
suppose [y,f] in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ; ::_thesis: f is set
then  ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st
( [y,f] = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
hence  f is FinSequence by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
end;

theorem Th9: :: SCM_INST:9
for x being Element of SCM-Instr holds
( ( x in {[SCM-Halt,{},{}]} & InsCode x = 0 ) or ( x in  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  & InsCode x = 6 ) or ( x in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  & ( InsCode x = 7 or InsCode x = 8 ) ) or ( x in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) ) )
proof
let x be Element of SCM-Instr ; ::_thesis: ( ( x in {[SCM-Halt,{},{}]} & InsCode x = 0 ) or ( x in  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  & InsCode x = 6 ) or ( x in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  & ( InsCode x = 7 or InsCode x = 8 ) ) or ( x in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) ) )
 ( x in ({[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ) \/  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  or x in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ) by XBOOLE_0:def_3;
then  ( x in {[SCM-Halt,{},{}]} \/  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  or x in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  or x in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ) by XBOOLE_0:def_3;
percasesthen  ( x in {[SCM-Halt,{},{}]} or x in  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  or x in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  or x in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ) by XBOOLE_0:def_3;
case x in {[SCM-Halt,{},{}]} ; ::_thesis: InsCode x = 0
then  x = [SCM-Halt,{},{}] by TARSKI:def_1;
hence  InsCode x = 0 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in  {  [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6  }  ; ::_thesis: InsCode x = 6
then  ex J being Element of Segm 9 ex a being Element of NAT st
( x = [J,<*a*>,{}] & J = 6 ) ;
hence  InsCode x = 6 by RECDEF_2:def_1; ::_thesis: verum
end;
case x in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  ; ::_thesis: ( InsCode x = 7 or InsCode x = 8 )
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc  such that
A1: x = [K,<*a1*>,<*b1*>] and
A2: K in {7,8} ;
 InsCode x = K by A1, RECDEF_2:def_1;
hence  ( InsCode x = 7 or InsCode x = 8 ) by A2, TARSKI:def_2; ::_thesis: verum
end;
case x in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  ; ::_thesis: ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 )
then consider I being Element of Segm 9, b, c being Element of SCM-Data-Loc  such that
A3: x = [I,{},<*b,c*>] and
A4: I in {1,2,3,4,5} ;
 InsCode x = I by A3, RECDEF_2:def_1;
hence  ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) by A4, ENUMSET1:def_3; ::_thesis: verum
end;
end;
end;

begin


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


theorem Th10: :: SCM_INST:10
for l being Element of SCM-Instr holds InsCode l <= 8
proof
let l be Element of SCM-Instr ; ::_thesis: InsCode l <= 8
 ( InsCode l = 0 or InsCode l = 1 or InsCode l = 2 or InsCode l = 3 or InsCode l = 4 or InsCode l = 5 or InsCode l = 6 or InsCode l = 7 or InsCode l = 8 ) by Th9;
hence  InsCode l <= 8 ; ::_thesis: verum
end;

Lm1:  for i being Element of SCM-Instr st ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) holds
JumpPart i = {}
proof
let i be Element of SCM-Instr ; ::_thesis: ( ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) implies JumpPart i = {} )
assume  ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) ; ::_thesis: JumpPart i = {}
then  i in  {  [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5}  }  by Th9;
then  ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st
( i = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
hence  JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;

Lm2:  for i being Element of SCM-Instr st ( InsCode i = 7 or InsCode i = 8 ) holds
dom (JumpPart i) = Seg 1
proof
let i be Element of SCM-Instr ; ::_thesis: ( ( InsCode i = 7 or InsCode i = 8 ) implies dom (JumpPart i) = Seg 1 )
assume  ( InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: dom (JumpPart i) = Seg 1
then  i in  {  [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8}  }  by Th9;
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc  such that
A1: i = [K,<*a1*>,<*b1*>] and
 K in {7,8} ;
 JumpPart i = <*a1*> by A1, RECDEF_2:def_2;
hence  dom (JumpPart i) = Seg 1 by FINSEQ_1:38; ::_thesis: verum
end;

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

registration
cluster SCM-Instr  ->  non empty homogeneous ;
coherence
 SCM-Instr is homogeneous
proof
let i, j be Element of SCM-Instr ; :: 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 <= 8 by Th10;
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 = 7 or InsCode i = 8 or InsCode i = 6 ) by NAT_1:32;
suppose InsCode i = 0 ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( i in {[SCM-Halt,{},{}]} & j in {[SCM-Halt,{},{}]} ) by A1, Th9;
then  ( i = [SCM-Halt,{},{}] & j = [SCM-Halt,{},{}] ) 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 or InsCode i = 5 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm1;
hence  dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
suppose ( InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm2;
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, Lm3;
hence  dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
end;
end;
end;

Lm4:  for T being InsType of SCM-Instr holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
proof
let T be InsType of SCM-Instr; ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
consider y being set  such that
A1: [T,y] in proj1 SCM-Instr by XTUPLE_0:def_12;
consider x being set  such that
A2: [[T,y],x] in SCM-Instr by A1, XTUPLE_0:def_12;
reconsider I = [T,y,x] as Element of SCM-Instr by A2;
 T = InsCode I by RECDEF_2:def_1;
hence  ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) by Th10, NAT_1:32; ::_thesis: verum
end;

  Lm5:  for T being InsType of SCM-Instr st T = 0 holds
JumpParts T = {0}
proof
let T be InsType of SCM-Instr; ::_thesis: ( T = 0 implies JumpParts T = {0} )
assume A1: T = 0 ; ::_thesis: JumpParts T = {0}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {0} c= JumpParts T
let a be set ; ::_thesis: ( a in JumpParts T implies a in {0} )
assume  a in JumpParts T ; ::_thesis: a in {0}
then consider I being Element of SCM-Instr  such that
A2: a = JumpPart I and
A3: InsCode I = T ;
 I in {[SCM-Halt,{},{}]} by A1, A3, Th9;
then  I = [SCM-Halt,{},{}] by TARSKI:def_1;
then  a = 0 by A2, RECDEF_2:def_2;
hence  a in {0} by TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {0} or a in JumpParts T )
assume  a in {0} ; ::_thesis: a in JumpParts T
then A4: a = 0 by TARSKI:def_1;
A5: JumpPart [SCM-Halt,{},{}] = {} ;
A6: InsCode [SCM-Halt,{},{}] = SCM-Halt ;
 [SCM-Halt,{},{}] in SCM-Instr by Th1;
hence  a in JumpParts T by A1, A4, A5, A6; ::_thesis: verum
end;

Lm6:  for T being InsType of SCM-Instr st ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) holds
JumpParts T = {{}}
proof
let T be InsType of SCM-Instr; ::_thesis: ( ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) implies JumpParts T = {{}} )
assume A1: ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) ; ::_thesis: JumpParts T = {{}}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T
let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} )
assume  x in JumpParts T ; ::_thesis: x in {{}}
then consider I being Element of SCM-Instr  such that
A2: x = JumpPart I and
A3: InsCode I = T ;
 I in  {  [J,{},<*b,c*>] where J is Element of Segm 9, b, c is Element of SCM-Data-Loc : J in {1,2,3,4,5}  }  by A1, A3, Th9;
then consider J being Element of Segm 9, b, c being Element of SCM-Data-Loc  such that
A4: I = [J,{},<*b,c*>] and
 J in {1,2,3,4,5} ;
 x = {} by A2, A4, RECDEF_2:def_2;
hence  x in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set a = the Element of SCM-Data-Loc ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
assume  x in {{}} ; ::_thesis: x in JumpParts T
then A5: x = {} by TARSKI:def_1;
A6: JumpPart [T,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] = {} ;
A7: InsCode [T,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] = T ;
 T in {1,2,3,4,5} by A1, ENUMSET1:def_3;
then  [T,{},<* the Element of SCM-Data-Loc , the Element of SCM-Data-Loc *>] in SCM-Instr by Th4;
hence  x in JumpParts T by A5, A6, A7; ::_thesis: verum
end;

registration
cluster SCM-Instr  ->  non empty J/A-independent ;
coherence
 SCM-Instr is J/A-independent
proof
let T be InsType of SCM-Instr; :: 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 or [T,b2,b3] in SCM-Instr ) )
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 or [T,f2,b1] in SCM-Instr ) )
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 or [T,f2,b1] in SCM-Instr )
let p be set ; ::_thesis: ( not [T,f1,p] in SCM-Instr or [T,f2,p] in SCM-Instr )
assume A3: [T,f1,p] in SCM-Instr ; ::_thesis: [T,f2,p] in SCM-Instr
percases ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) by Lm4;
suppose T = 0 ; ::_thesis: [T,f2,p] in SCM-Instr
then  JumpParts T = {0} by Lm5;
then  f1 = 0 by A1, TARSKI:def_1;
then  f1 = f2 by A2;
hence  [T,f2,p] in SCM-Instr by A3; ::_thesis: verum
end;
suppose ( T = 1 or T = 2 or T = 3 or T = 4 or T = 5 ) ; ::_thesis: [T,f2,p] in SCM-Instr
then A4: JumpParts T = {0} by Lm6;
 f1 = 0 by A4, A1, TARSKI:def_1;
then  f1 = f2 by A2;
hence  [T,f2,p] in SCM-Instr by A3; ::_thesis: verum
end;
supposeA5: T = 6 ; ::_thesis: [T,f2,p] in SCM-Instr
reconsider J = [T,f1,p] as Element of SCM-Instr by A3;
 InsCode J = 6 by A5, RECDEF_2:def_1;
then  J in  {  [K,<*i1*>,{}] where K is Element of Segm 9, i1 is Element of NAT : K = 6  }  by Th9;
then consider K being Element of Segm 9, i1 being Element of NAT  such that
A6: ( J = [K,<*i1*>,{}] & K = 6 ) ;
A7: p = {} by A6, XTUPLE_0:3;
 f1 = <*i1*> by A6, XTUPLE_0:3;
then A8: 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,{}];
 [T,f2,{}] = [6,<*l*>,{}] by A5, A8, FINSEQ_1:2, FINSEQ_1:def_8;
then reconsider I = [T,f2,{}] as Element of SCM-Instr by Th2;
 f2 = JumpPart I by RECDEF_2:def_2;
hence  [T,f2,p] in SCM-Instr by A7; ::_thesis: verum
end;
supposeA9: ( T = 7 or T = 8 ) ; ::_thesis: [T,f2,p] in SCM-Instr
reconsider J = [T,f1,p] as Element of SCM-Instr by A3;
 InsCode J = T by RECDEF_2:def_1;
then  J in  {  [K,<*i1*>,<*a*>] where K is Element of Segm 9, i1 is Element of NAT , a is Element of SCM-Data-Loc : K in {7,8}  }  by A9, Th9;
then consider K being Element of Segm 9, i1 being Element of NAT , a being Element of SCM-Data-Loc  such that
A10: J = [K,<*i1*>,<*a*>] and
 K in {7,8} ;
A11: p = <*a*> by A10, XTUPLE_0:3;
 f1 = <*i1*> by A10, XTUPLE_0:3;
then A12: 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];
A13: T in {7,8} by A9, TARSKI:def_2;
 [T,f2,p] = [T,<*l*>,<*a*>] by A11, A12, FINSEQ_1:2, FINSEQ_1:def_8;
then reconsider I = [T,f2,p] as Element of SCM-Instr by A13, Th3;
 InsCode I = T by RECDEF_2:def_1;
then  I in  {  [L,<*i2*>,<*b*>] where L is Element of Segm 9, i2 is Element of NAT , b is Element of SCM-Data-Loc : L in {7,8}  }  by A9, Th9;
then consider L being Element of Segm 9, i2 being Element of NAT , b being Element of SCM-Data-Loc  such that
A14: I = [L,<*i2*>,<*b*>] and
 L in {7,8} ;
L = InsCode I by A14, RECDEF_2:def_1
.= T by RECDEF_2:def_1 ;
then A15: I = [T,<*i2*>,<*b*>] by A14;
thus  [T,f2,p] in SCM-Instr by A15; ::_thesis: verum
end;
end;
end;
end;

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