:: SCMFSA_I semantic presentation

begin


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

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

registration
cluster SCM+FSA-Data*-Loc  ->  non empty ;
coherence
 not SCM+FSA-Data*-Loc is empty
proof
 not INT c= NAT by NUMBERS:17, NUMBERS:27, XBOOLE_0:def_10;
hence  not SCM+FSA-Data*-Loc is empty by XBOOLE_1:37; ::_thesis: verum
end;
end;


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

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

theorem Th1: :: SCMFSA_I:1
SCM-Instr c= SCM+FSA-Instr
proof
A1: SCM-Instr c= SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  by XBOOLE_1:7;
 SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  c= (SCM-Instr \/  {  [J1,{},<*c2,f2,b2*>] where J1 is Element of Segm 13, c2, b2 is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J1 in {9,10}  }  ) \/  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  by XBOOLE_1:7;
then A2: SCM-Instr c= (SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) \/  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  by A1, XBOOLE_1:1;
thus  SCM-Instr c= SCM+FSA-Instr by A2; ::_thesis: verum
end;

Lm1:  SCM+FSA-Instr c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SCM+FSA-Instr or x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] )
assume A1: x in SCM+FSA-Instr ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
percases ( x in (SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) \/  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  or x in  {  [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum  }  ) by A1;
supposeA2: x in (SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) \/  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
percases ( x in SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  or x in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ) by A2, XBOOLE_0:def_3;
supposeA3: x in SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
percases ( x in SCM-Instr or x in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) by A3, XBOOLE_0:def_3;
suppose x in SCM-Instr ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
then A4: x in [:NAT,(NAT *),(proj2 SCM-Instr):] by SCM_INST:8;
 proj2 SCM-Instr c= proj2 SCM+FSA-Instr by Th1, XTUPLE_0:9;
then  [:NAT,(NAT *),(proj2 SCM-Instr):] c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by MCART_1:73;
hence  x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by A4; ::_thesis: verum
end;
suppose x in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
then consider J being Element of Segm 13, c, b being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc  such that
A5: ( x = [J,{},<*c,f,b*>] & J in {9,10} ) ;
A6: {} in NAT * by FINSEQ_1:49;
 ( J in NAT & <*c,f,b*> in proj2 SCM+FSA-Instr ) by A1, A5, XTUPLE_0:def_13;
hence  x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by A5, A6, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose x in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
then consider K being Element of Segm 13, c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc  such that
A7: ( x = [K,{},<*c1,f1*>] & K in {11,12} ) ;
A8: {} in NAT * by FINSEQ_1:49;
 ( K in NAT & <*c1,f1*> in proj2 SCM+FSA-Instr ) by A1, A7, XTUPLE_0:def_13;
hence  x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by A7, A8, MCART_1:69; ::_thesis: verum
end;
end;
end;
suppose x in  {  [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum  }  ; ::_thesis: x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
then consider b1 being Element of SCM-Data-Loc  such that
A9: x = [13,{},<*b1*>] ;
A10: {} in NAT * by FINSEQ_1:49;
 for K being Element of Segm 13 holds
( K in NAT & <*b1*> in proj2 SCM+FSA-Instr ) by A1, A9, XTUPLE_0:def_13;
hence  x in [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by A9, A10, MCART_1:69; ::_thesis: verum
end;
end;
end;

registration
cluster proj2 SCM+FSA-Instr ->  FinSequence-membered ;
coherence
 proj2 SCM+FSA-Instr is FinSequence-membered
proof
let f be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not f in proj2 SCM+FSA-Instr or f is set )
assume  f in proj2 SCM+FSA-Instr ; ::_thesis: f is set
then consider y being set  such that
A1: [y,f] in SCM+FSA-Instr by XTUPLE_0:def_13;
set x = [y,f];
percases ( [y,f] in (SCM-Instr \/  {  [J,{},<*c,f2,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) \/  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  or [y,f] in  {  [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum  }  ) by A1;
supposeA2: [y,f] in (SCM-Instr \/  {  [J,{},<*c,f2,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) \/  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ; ::_thesis: f is set
percases ( [y,f] in SCM-Instr \/  {  [J,{},<*c,f1,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  or [y,f] in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ) by A2, XBOOLE_0:def_3;
supposeA3: [y,f] in SCM-Instr \/  {  [J,{},<*c,f1,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ; ::_thesis: f is set
percases ( [y,f] in SCM-Instr or [y,f] in  {  [J,{},<*c,f1,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) by A3, XBOOLE_0:def_3;
suppose [y,f] in SCM-Instr ; ::_thesis: f is set
then  f in proj2 SCM-Instr by XTUPLE_0:def_13;
hence  f is FinSequence ; ::_thesis: verum
end;
suppose [y,f] in  {  [J,{},<*c,f1,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ; ::_thesis: f is set
then consider J being Element of Segm 13, c, b being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc  such that
A4: ( [y,f] = [J,{},<*c,f1,b*>] & J in {9,10} ) ;
 f = <*c,f1,b*> by A4, XTUPLE_0:1;
hence  f is FinSequence ; ::_thesis: verum
end;
end;
end;
suppose [y,f] in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ; ::_thesis: f is set
then consider K being Element of Segm 13, c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc  such that
A5: ( [y,f] = [K,{},<*c1,f1*>] & K in {11,12} ) ;
 f = <*c1,f1*> by A5, XTUPLE_0:1;
hence  f is FinSequence ; ::_thesis: verum
end;
end;
end;
suppose [y,f] in  {  [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum  }  ; ::_thesis: f is set
then consider b1 being Element of SCM-Data-Loc  such that
A6: [y,f] = [13,{},<*b1*>] ;
 f = <*b1*> by A6, XTUPLE_0:1;
hence  f is FinSequence ; ::_thesis: verum
end;
end;
end;
end;

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

theorem Th2: :: SCMFSA_I:2
for I being Element of SCM+FSA-Instr st I `1_3 <= 8 holds
I in SCM-Instr
proof
let I be Element of SCM+FSA-Instr ; ::_thesis: ( I `1_3 <= 8 implies I in SCM-Instr )
assume A1: I `1_3 <= 8 ; ::_thesis: I in SCM-Instr
A2: now__::_thesis:_not_I_in__{__[K,{},<*c1,f1*>]_where_K_is_Element_of_Segm_13,_c1_is_Element_of_SCM-Data-Loc_,_f1_is_Element_of_SCM+FSA-Data*-Loc_:_K_in_{11,12}__}_
assume  I in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ; ::_thesis: contradiction
then consider K being Element of Segm 13, c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc  such that
A3: I = [K,{},<*c,f*>] and
A4: K in {11,12} ;
 I `1_3 = K by A3, RECDEF_2:def_1;
then  ( I `1_3 = 11 or I `1_3 = 12 ) by A4, TARSKI:def_2;
hence  contradiction by A1; ::_thesis: verum
end;
A5: now__::_thesis:_not_I_in__{__[J,{},<*c,f,b*>]_where_J_is_Element_of_Segm_13,_c,_b_is_Element_of_SCM-Data-Loc_,_f_is_Element_of_SCM+FSA-Data*-Loc_:_J_in_{9,10}__}_
assume  I in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ; ::_thesis: contradiction
then consider J being Element of Segm 13, c, b being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc  such that
A6: I = [J,{},<*c,f,b*>] and
A7: J in {9,10} ;
 I `1_3 = J by A6, RECDEF_2:def_1;
then  ( I `1_3 = 9 or I `1_3 = 10 ) by A7, TARSKI:def_2;
hence  contradiction by A1; ::_thesis: verum
end;
A8: now__::_thesis:_not_I_in__{__[13,{},<*b1*>]_where_b1_is_Element_of_SCM-Data-Loc_:_verum__}_
assume  I in  {  [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum  }  ; ::_thesis: contradiction
then consider b1 being Element of SCM-Data-Loc  such that
A9: I = [13,{},<*b1*>] ;
 I `1_3 = 13 by A9, RECDEF_2:def_1;
hence  contradiction by A1; ::_thesis: verum
end;
 ( I in SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  or I in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  or I in  {  [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum  }  ) by XBOOLE_0:def_3;
hence  I in SCM-Instr by A2, A5, A8, XBOOLE_0:def_3; ::_thesis: verum
end;

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

theorem Th4: :: SCMFSA_I:4
for x being set
for c, b being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds
[x,{},<*c,f,b*>] in SCM+FSA-Instr
proof
let x be set ; ::_thesis: for c, b being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds
[x,{},<*c,f,b*>] in SCM+FSA-Instr
let c, b be Element of SCM-Data-Loc ; ::_thesis: for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds
[x,{},<*c,f,b*>] in SCM+FSA-Instr
let f be Element of SCM+FSA-Data*-Loc ; ::_thesis: ( x in {9,10} implies [x,{},<*c,f,b*>] in SCM+FSA-Instr )
assume A1: x in {9,10} ; ::_thesis: [x,{},<*c,f,b*>] in SCM+FSA-Instr
then  ( x = 9 or x = 10 ) by TARSKI:def_2;
then reconsider x = x as Element of Segm 13 by NAT_1:44;
 [x,{},<*c,f,b*>] in  {  [K,{},<*c1,f1,b1*>] where K is Element of Segm 13, c1, b1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {9,10}  }  by A1;
then  [x,{},<*c,f,b*>] in SCM-Instr \/  {  [J,{},<*c1,f1,b1*>] where J is Element of Segm 13, c1, b1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  by XBOOLE_0:def_3;
then  [x,{},<*c,f,b*>] in (SCM-Instr \/  {  [J,{},<*c1,f1,b1*>] where J is Element of Segm 13, c1, b1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) \/  {  [K,{},<*c2,f2*>] where K is Element of Segm 13, c2 is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  by XBOOLE_0:def_3;
hence  [x,{},<*c,f,b*>] in SCM+FSA-Instr ; ::_thesis: verum
end;

theorem Th5: :: SCMFSA_I:5
for x being set
for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds
[x,{},<*c,f*>] in SCM+FSA-Instr
proof
let x be set ; ::_thesis: for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds
[x,{},<*c,f*>] in SCM+FSA-Instr
let c be Element of SCM-Data-Loc ; ::_thesis: for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds
[x,{},<*c,f*>] in SCM+FSA-Instr
let f be Element of SCM+FSA-Data*-Loc ; ::_thesis: ( x in {11,12} implies [x,{},<*c,f*>] in SCM+FSA-Instr )
assume A1: x in {11,12} ; ::_thesis: [x,{},<*c,f*>] in SCM+FSA-Instr
then  ( x = 11 or x = 12 ) by TARSKI:def_2;
then reconsider x = x as Element of Segm 13 by NAT_1:44;
 [x,{},<*c,f*>] in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  by A1;
then  [x,{},<*c,f*>] in (SCM-Instr \/  {  [J,{},<*c2,f2,b*>] where J is Element of Segm 13, c2, b is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) \/  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  by XBOOLE_0:def_3;
then  [x,{},<*c,f*>] in (SCM-Instr \/  {  [J,{},<*c2,f2,b*>] where J is Element of Segm 13, c2, b is Element of SCM-Data-Loc , f2 is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ) \/  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ;
hence  [x,{},<*c,f*>] in SCM+FSA-Instr ; ::_thesis: verum
end;

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc , b being Element of SCM-Data-Loc , J being Element of Segm 13 such that A1: x = [J,{},<*c,f,b*>] ;
funcx int_addr1  ->  Element of SCM-Data-Loc  means :: SCMFSA_I:def 3
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & it = c );
existence
 ex b1, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = c )
proof
take  c ; ::_thesis: ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & c = c )
take  c ; ::_thesis: ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & c = c )
take  f ; ::_thesis: ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & c = c )
take  b ; ::_thesis: ( <*c,f,b*> = x `3_3 & c = c )
thus  ( <*c,f,b*> = x `3_3 & c = c ) by A1, RECDEF_2:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = c ) holds
b1 = b2
proof
let a1, a2 be Element of SCM-Data-Loc ; ::_thesis: ( ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & a1 = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & a2 = c ) implies a1 = a2 )
given c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc , b1 being Element of SCM-Data-Loc  such that A2: <*c1,f1,b1*> = x `3_3 and
A3: a1 = c1 ; ::_thesis: ( for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc
for b being Element of SCM-Data-Loc holds
( not <*c,f,b*> = x `3_3 or not a2 = c ) or a1 = a2 )
given c2 being Element of SCM-Data-Loc , f2 being Element of SCM+FSA-Data*-Loc , b2 being Element of SCM-Data-Loc  such that A4: ( <*c2,f2,b2*> = x `3_3 & a2 = c2 ) ; ::_thesis: a1 = a2
thus a1 = <*c1,f1,b1*> . 1 by A3, FINSEQ_1:45
.= a2 by A2, A4, FINSEQ_1:45 ; ::_thesis: verum
end;
funcx int_addr2  ->  Element of SCM-Data-Loc  means :: SCMFSA_I:def 4
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & it = b );
existence
 ex b1, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = b )
proof
take  b ; ::_thesis: ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b = b )
take  c ; ::_thesis: ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b = b )
take  f ; ::_thesis: ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b = b )
take  b ; ::_thesis: ( <*c,f,b*> = x `3_3 & b = b )
thus  ( <*c,f,b*> = x `3_3 & b = b ) by A1, RECDEF_2:def_3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = b ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = b ) holds
b1 = b2;
proof
let a1, a2 be Element of SCM-Data-Loc ; ::_thesis: ( ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & a1 = b ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & a2 = b ) implies a1 = a2 )
given c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc , b1 being Element of SCM-Data-Loc  such that A5: <*c1,f1,b1*> = x `3_3 and
A6: a1 = b1 ; ::_thesis: ( for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc
for b being Element of SCM-Data-Loc holds
( not <*c,f,b*> = x `3_3 or not a2 = b ) or a1 = a2 )
given c2 being Element of SCM-Data-Loc , f2 being Element of SCM+FSA-Data*-Loc , b2 being Element of SCM-Data-Loc  such that A7: ( <*c2,f2,b2*> = x `3_3 & a2 = b2 ) ; ::_thesis: a1 = a2
thus a1 = <*c1,f1,b1*> . 3 by A6, FINSEQ_1:45
.= a2 by A5, A7, FINSEQ_1:45 ; ::_thesis: verum
end;
funcx coll_addr1  ->  Element of SCM+FSA-Data*-Loc  means :: SCMFSA_I:def 5
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & it = f );
existence
 ex b1 being Element of SCM+FSA-Data*-Loc ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = f )
proof
take  f ; ::_thesis: ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & f = f )
take  c ; ::_thesis: ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & f = f )
take  f ; ::_thesis: ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & f = f )
take  b ; ::_thesis: ( <*c,f,b*> = x `3_3 & f = f )
thus  ( <*c,f,b*> = x `3_3 & f = f ) by A1, RECDEF_2:def_3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b1 = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & b2 = f ) holds
b1 = b2;
proof
let a1, a2 be Element of SCM+FSA-Data*-Loc ; ::_thesis: ( ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & a1 = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM-Data-Loc st
( <*c,f,b*> = x `3_3 & a2 = f ) implies a1 = a2 )
given c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc , b1 being Element of SCM-Data-Loc  such that A8: <*c1,f1,b1*> = x `3_3 and
A9: a1 = f1 ; ::_thesis: ( for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc
for b being Element of SCM-Data-Loc holds
( not <*c,f,b*> = x `3_3 or not a2 = f ) or a1 = a2 )
given c2 being Element of SCM-Data-Loc , f2 being Element of SCM+FSA-Data*-Loc , b2 being Element of SCM-Data-Loc  such that A10: ( <*c2,f2,b2*> = x `3_3 & a2 = f2 ) ; ::_thesis: a1 = a2
thus a1 = <*c1,f1,b1*> . 2 by A9, FINSEQ_1:45
.= a2 by A8, A10, FINSEQ_1:45 ; ::_thesis: verum
end;
end;

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

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

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

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM-Data-Loc  such that A1: x = [13,{},<*c*>] ;
funcx int_addr  ->  Element of SCM-Data-Loc  means :: SCMFSA_I:def 6
 ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & it = c );
existence
 ex b1, c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & b1 = c )
proof
take  c ; ::_thesis: ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & c = c )
take  c ; ::_thesis: ( <*c*> = x `3_3 & c = c )
thus  ( <*c*> = x `3_3 & c = c ) by A1, RECDEF_2:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & b1 = c ) & ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & b2 = c ) holds
b1 = b2
proof
let a1, a2 be Element of SCM-Data-Loc ; ::_thesis: ( ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & a1 = c ) & ex c being Element of SCM-Data-Loc st
( <*c*> = x `3_3 & a2 = c ) implies a1 = a2 )
given c1 being Element of SCM-Data-Loc  such that A2: <*c1*> = x `3_3 and
A3: a1 = c1 ; ::_thesis: ( for c being Element of SCM-Data-Loc holds
( not <*c*> = x `3_3 or not a2 = c ) or a1 = a2 )
given c2 being Element of SCM-Data-Loc  such that A4: ( <*c2*> = x `3_3 & a2 = c2 ) ; ::_thesis: a1 = a2
thus a1 = <*c1*> /. 1 by A3, FINSEQ_4:16
.= a2 by A2, A4, FINSEQ_4:16 ; ::_thesis: verum
end;
end;

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

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc , J being Element of Segm 13 such that A1: x = [J,{},<*c,f*>] ;
funcx int_addr3  ->  Element of SCM-Data-Loc  means :: SCMFSA_I:def 7
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & it = c );
existence
 ex b1, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = c )
proof
take  c ; ::_thesis: ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & c = c )
take  c ; ::_thesis: ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & c = c )
take  f ; ::_thesis: ( <*c,f*> = x `3_3 & c = c )
thus  ( <*c,f*> = x `3_3 & c = c ) by A1, RECDEF_2:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of SCM-Data-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = c ) holds
b1 = b2
proof
let a1, a2 be Element of SCM-Data-Loc ; ::_thesis: ( ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & a1 = c ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & a2 = c ) implies a1 = a2 )
given c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc  such that A2: <*c1,f1*> = x `3_3 and
A3: a1 = c1 ; ::_thesis: ( for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc holds
( not <*c,f*> = x `3_3 or not a2 = c ) or a1 = a2 )
given c2 being Element of SCM-Data-Loc , f2 being Element of SCM+FSA-Data*-Loc  such that A4: ( <*c2,f2*> = x `3_3 & a2 = c2 ) ; ::_thesis: a1 = a2
thus a1 = <*c1,f1*> . 1 by A3, FINSEQ_1:44
.= a2 by A2, A4, FINSEQ_1:44 ; ::_thesis: verum
end;
funcx coll_addr2  ->  Element of SCM+FSA-Data*-Loc  means :: SCMFSA_I:def 8
 ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & it = f );
existence
 ex b1 being Element of SCM+FSA-Data*-Loc ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = f )
proof
take  f ; ::_thesis: ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & f = f )
take  c ; ::_thesis: ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & f = f )
take  f ; ::_thesis: ( <*c,f*> = x `3_3 & f = f )
thus  ( <*c,f*> = x `3_3 & f = f ) by A1, RECDEF_2:def_3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b1 = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = f ) holds
b1 = b2;
proof
let a1, a2 be Element of SCM+FSA-Data*-Loc ; ::_thesis: ( ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & a1 = f ) & ex c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & a2 = f ) implies a1 = a2 )
given c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc  such that A5: <*c1,f1*> = x `3_3 and
A6: a1 = f1 ; ::_thesis: ( for c being Element of SCM-Data-Loc
for f being Element of SCM+FSA-Data*-Loc holds
( not <*c,f*> = x `3_3 or not a2 = f ) or a1 = a2 )
given c2 being Element of SCM-Data-Loc , f2 being Element of SCM+FSA-Data*-Loc  such that A7: ( <*c2,f2*> = x `3_3 & a2 = f2 ) ; ::_thesis: a1 = a2
thus a1 = <*c1,f1*> . 2 by A6, FINSEQ_1:44
.= a2 by A5, A7, FINSEQ_1:44 ; ::_thesis: verum
end;
end;

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

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

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

theorem Th7: :: SCMFSA_I:7
for x being Element of SCM+FSA-Instr holds
( ( x in SCM-Instr & ( InsCode x = 0 or InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  & ( InsCode x = 9 or InsCode x = 10 ) ) or ( x in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  & ( InsCode x = 11 or InsCode x = 12 ) ) )
proof
let x be Element of SCM+FSA-Instr ; ::_thesis: ( ( x in SCM-Instr & ( InsCode x = 0 or InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  & ( InsCode x = 9 or InsCode x = 10 ) ) or ( x in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  & ( InsCode x = 11 or InsCode x = 12 ) ) )
 ( x in SCM-Instr \/  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  or x in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ) by XBOOLE_0:def_3;
percasesthen  ( x in SCM-Instr or x in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  or x in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ) by XBOOLE_0:def_3;
case x in SCM-Instr ; ::_thesis: ( InsCode x = 0 or InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 )
then  InsCode x <= 8 by SCM_INST:10;
hence  ( InsCode x = 0 or InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) by NAT_1:32; ::_thesis: verum
end;
case x in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  ; ::_thesis: ( InsCode x = 9 or InsCode x = 10 )
then consider J being Element of Segm 13, c, b being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc  such that
A1: x = [J,{},<*c,f,b*>] and
A2: J in {9,10} ;
 InsCode x = J by A1, RECDEF_2:def_1;
hence  ( InsCode x = 9 or InsCode x = 10 ) by A2, TARSKI:def_2; ::_thesis: verum
end;
case x in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  ; ::_thesis: ( InsCode x = 11 or InsCode x = 12 )
then consider K being Element of Segm 13, c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc  such that
A3: x = [K,{},<*c1,f1*>] and
A4: K in {11,12} ;
 InsCode x = K by A3, RECDEF_2:def_1;
hence  ( InsCode x = 11 or InsCode x = 12 ) by A4, TARSKI:def_2; ::_thesis: verum
end;
end;
end;

Lm2:  for i being Element of SCM+FSA-Instr holds InsCode i <= 12
proof
let i be Element of SCM+FSA-Instr ; ::_thesis: InsCode i <= 12
 ( 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 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by Th7;
hence  InsCode i <= 12 ; ::_thesis: verum
end;

Lm3:  for i being Element of SCM+FSA-Instr st ( InsCode i = 9 or InsCode i = 10 ) holds
JumpPart i = {}
proof
let i be Element of SCM+FSA-Instr ; ::_thesis: ( ( InsCode i = 9 or InsCode i = 10 ) implies JumpPart i = {} )
assume  ( InsCode i = 9 or InsCode i = 10 ) ; ::_thesis: JumpPart i = {}
then  i in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  by Th7;
then  ex J being Element of Segm 13 ex c, b being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( i = [J,{},<*c,f,b*>] & J in {9,10} ) ;
hence  JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;

Lm4:  for i being Element of SCM+FSA-Instr st ( InsCode i = 11 or InsCode i = 12 ) holds
JumpPart i = {}
proof
let i be Element of SCM+FSA-Instr ; ::_thesis: ( ( InsCode i = 11 or InsCode i = 12 ) implies JumpPart i = {} )
assume  ( InsCode i = 11 or InsCode i = 12 ) ; ::_thesis: JumpPart i = {}
then  i in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  by Th7;
then  ex K being Element of Segm 13 ex c1 being Element of SCM-Data-Loc ex f1 being Element of SCM+FSA-Data*-Loc st
( i = [K,{},<*c1,f1*>] & K in {11,12} ) ;
hence  JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum
end;

registration
cluster SCM+FSA-Instr  ->  non empty homogeneous ;
coherence
 SCM+FSA-Instr is homogeneous
proof
let i, j be Element of SCM+FSA-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 <= 12 by Lm2;
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 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by NAT_1:36;
suppose ( 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 or InsCode i = 8 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( i in SCM-Instr & j in SCM-Instr ) by A1, Th7;
hence  dom (i `2_3) = dom (j `2_3) by A1, COMPOS_0:def_5; ::_thesis: verum
end;
suppose ( InsCode i = 9 or InsCode i = 10 ) ; ::_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 = 11 or InsCode i = 12 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3)
then  ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm4;
hence  dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum
end;
end;
end;
end;

Lm5:  for i being Element of SCM+FSA-Instr
for ii being Element of SCM-Instr st i = ii holds
JumpParts (InsCode i) = JumpParts (InsCode ii)
proof
let i be Element of SCM+FSA-Instr ; ::_thesis: for ii being Element of SCM-Instr st i = ii holds
JumpParts (InsCode i) = JumpParts (InsCode ii)
let ii be Element of SCM-Instr ; ::_thesis: ( i = ii implies JumpParts (InsCode i) = JumpParts (InsCode ii) )
assume A1: i = ii ; ::_thesis: JumpParts (InsCode i) = JumpParts (InsCode ii)
thus  JumpParts (InsCode i) c= JumpParts (InsCode ii) :: according to XBOOLE_0:def_10 ::_thesis: JumpParts (InsCode ii) c= JumpParts (InsCode i)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in JumpParts (InsCode i) or e in JumpParts (InsCode ii) )
assume  e in JumpParts (InsCode i) ; ::_thesis: e in JumpParts (InsCode ii)
then consider I being Element of SCM+FSA-Instr  such that
A2: e = JumpPart I and
A3: InsCode I = InsCode i ;
 InsCode I <= 8 by A1, A3, SCM_INST:10;
then reconsider II = I as Element of SCM-Instr by Th2;
 InsCode II = InsCode ii by A1, A3;
hence  e in JumpParts (InsCode ii) by A2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in JumpParts (InsCode ii) or e in JumpParts (InsCode i) )
assume  e in JumpParts (InsCode ii) ; ::_thesis: e in JumpParts (InsCode i)
then consider II being Element of SCM-Instr  such that
A4: e = JumpPart II and
A5: InsCode II = InsCode ii ;
A6: SCM-Instr c= SCM+FSA-Instr by Th1;
 II in SCM-Instr ;
then  II in SCM+FSA-Instr by A6;
then reconsider I = II as Element of SCM+FSA-Instr ;
 InsCode I = InsCode i by A1, A5;
hence  e in JumpParts (InsCode i) by A4; ::_thesis: verum
end;

theorem Th8: :: SCMFSA_I:8
for T being InsType of SCM+FSA-Instr st ( T = 9 or T = 10 ) holds
JumpParts T = {{}}
proof
let T be InsType of SCM+FSA-Instr; ::_thesis: ( ( T = 9 or T = 10 ) implies JumpParts T = {{}} )
assume A1: ( T = 9 or T = 10 ) ; ::_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+FSA-Instr  such that
A2: x = JumpPart I and
A3: InsCode I = T ;
 I in  {  [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10}  }  by A1, A3, Th7;
then consider J being Element of Segm 13, c, b being Element of SCM-Data-Loc , f being Element of SCM+FSA-Data*-Loc  such that
A4: ( I = [J,{},<*c,f,b*>] & J in {9,10} ) ;
 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 ;
set f = the Element of SCM+FSA-Data*-Loc ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
 T in {9,10} by A1, TARSKI:def_2;
then A5: [T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc , the Element of SCM-Data-Loc *>] in SCM+FSA-Instr by Th4;
assume  x in {{}} ; ::_thesis: x in JumpParts T
then  x = {} by TARSKI:def_1;
then A6: x = JumpPart [T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc , the Element of SCM-Data-Loc *>] ;
 InsCode [T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc , the Element of SCM-Data-Loc *>] = T ;
hence  x in JumpParts T by A6, A5; ::_thesis: verum
end;

theorem Th9: :: SCMFSA_I:9
for T being InsType of SCM+FSA-Instr st ( T = 11 or T = 12 ) holds
JumpParts T = {{}}
proof
let T be InsType of SCM+FSA-Instr; ::_thesis: ( ( T = 11 or T = 12 ) implies JumpParts T = {{}} )
assume A1: ( T = 11 or T = 12 ) ; ::_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+FSA-Instr  such that
A2: x = JumpPart I and
A3: InsCode I = T ;
 I in  {  [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12}  }  by A1, A3, Th7;
then consider K being Element of Segm 13, c1 being Element of SCM-Data-Loc , f1 being Element of SCM+FSA-Data*-Loc  such that
A4: ( I = [K,{},<*c1,f1*>] & K in {11,12} ) ;
 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 ;
set f = the Element of SCM+FSA-Data*-Loc ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T )
 T in {11,12} by A1, TARSKI:def_2;
then A5: [T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc *>] in SCM+FSA-Instr by Th5;
assume  x in {{}} ; ::_thesis: x in JumpParts T
then  x = {} by TARSKI:def_1;
then A6: x = JumpPart [T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc *>] ;
 InsCode [T,{},<* the Element of SCM-Data-Loc , the Element of SCM+FSA-Data*-Loc *>] = T ;
hence  x in JumpParts T by A6, A5; ::_thesis: verum
end;

registration
cluster SCM+FSA-Instr  ->  non empty J/A-independent ;
coherence
 SCM+FSA-Instr is J/A-independent
proof
let T be InsType of SCM+FSA-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+FSA-Instr or [T,b2,b3] in SCM+FSA-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+FSA-Instr or [T,f2,b1] in SCM+FSA-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+FSA-Instr or [T,f2,b1] in SCM+FSA-Instr )
let p be set ; ::_thesis: ( not [T,f1,p] in SCM+FSA-Instr or [T,f2,p] in SCM+FSA-Instr )
assume A3: [T,f1,p] in SCM+FSA-Instr ; ::_thesis: [T,f2,p] in SCM+FSA-Instr
A4: T = InsCode [T,f1,p] ;
reconsider II = [T,f1,p] as Element of SCM+FSA-Instr by A3;
 InsCode II <= 12 by Lm2;
percasesthen  ( InsCode II = 0 or InsCode II = 1 or InsCode II = 2 or InsCode II = 3 or InsCode II = 4 or InsCode II = 5 or InsCode II = 6 or InsCode II = 7 or InsCode II = 8 or T = 9 or T = 10 or T = 11 or T = 12 ) by A4, NAT_1:36;
suppose ( InsCode II = 0 or InsCode II = 1 or InsCode II = 2 or InsCode II = 3 or InsCode II = 4 or InsCode II = 5 or InsCode II = 6 or InsCode II = 7 or InsCode II = 8 ) ; ::_thesis: [T,f2,p] in SCM+FSA-Instr
then A5: InsCode II <= 8 ;
then reconsider ii = II as Element of SCM-Instr by Th2;
A6: T = InsCode ii by A4;
then  T in InsCodes SCM-Instr ;
then reconsider t = T as InsType of SCM-Instr ;
A7: [t,f1,p] in SCM-Instr by A5, Th2;
 JumpParts t = JumpParts T by A6, Lm5;
then  [t,f2,p] in SCM-Instr by A1, A2, A7, COMPOS_0:def_7;
then  [T,f2,p] in SCM-Instr ;
hence  [T,f2,p] in SCM+FSA-Instr by Th1; ::_thesis: verum
end;
suppose ( T = 9 or T = 10 or T = 11 or T = 12 ) ; ::_thesis: [T,f2,p] in SCM+FSA-Instr
then  JumpParts T = {0} by Th8, Th9;
then  f1 = 0 by A1, TARSKI:def_1;
then  f1 = f2 by A2;
hence  [T,f2,p] in SCM+FSA-Instr by A3; ::_thesis: verum
end;
end;
end;
end;

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