:: COMPOS_0 semantic presentation

begin


definition
let S be set ;
attrS is standard-ins  means :Def1: :: COMPOS_0:def 1
 ex X being non empty set st S c= [:NAT,(NAT *),(X *):];
end;

:: deftheorem Def1 defines standard-ins COMPOS_0:def_1_:_
 for S being set holds
( S is standard-ins iff ex X being non empty set st S c= [:NAT,(NAT *),(X *):] );

registration
cluster{[0,{},{}]} ->  standard-ins ;
coherence
 {[0,{},{}]} is standard-ins
proof
take  {{}} ; :: according to COMPOS_0:def_1 ::_thesis: {[0,{},{}]} c= [:NAT,(NAT *),({{}} *):]
A1: {{}} c= {{}} * by ZFMISC_1:31, FINSEQ_1:49;
A2: {{}} c= NAT * by ZFMISC_1:31, FINSEQ_1:49;
 {[0,{},{}]} = [:{0},{{}},{{}}:] by MCART_1:35;
hence  {[0,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A1, A2, MCART_1:73; ::_thesis: verum
end;
cluster{[1,{},{}]} ->  standard-ins ;
coherence
 {[1,{},{}]} is standard-ins
proof
take  {{}} ; :: according to COMPOS_0:def_1 ::_thesis: {[1,{},{}]} c= [:NAT,(NAT *),({{}} *):]
A3: {{}} c= {{}} * by ZFMISC_1:31, FINSEQ_1:49;
A4: {{}} c= NAT * by ZFMISC_1:31, FINSEQ_1:49;
 {[1,{},{}]} = [:{1},{{}},{{}}:] by MCART_1:35;
hence  {[1,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A3, A4, MCART_1:73; ::_thesis: verum
end;
end;

notation
let x be set ;
synonym  InsCode x for x `1_3 ;
synonym  JumpPart x for x `2_3 ;
synonym  AddressPart x for x `3_3 ;
end;

registration
cluster non empty standard-ins for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is standard-ins )
proof
take  {[0,{},{}]} ; ::_thesis: ( not {[0,{},{}]} is empty & {[0,{},{}]} is standard-ins )
thus  ( not {[0,{},{}]} is empty & {[0,{},{}]} is standard-ins ) ; ::_thesis: verum
end;
end;

registration
let S be non empty standard-ins set ;
let I be Element of S;
cluster AddressPart I ->  Relation-like Function-like ;
coherence
 ( AddressPart I is Function-like & AddressPart I is Relation-like )
proof
consider X being non empty set  such that
A1: S c= [:NAT,(NAT *),(X *):] by Def1;
 I in S ;
then  AddressPart I in X * by A1, RECDEF_2:2;
hence  ( AddressPart I is Function-like & AddressPart I is Relation-like ) ; ::_thesis: verum
end;
cluster JumpPart I ->  Relation-like Function-like ;
coherence
 ( JumpPart I is Function-like & JumpPart I is Relation-like )
proof
consider X being non empty set  such that
A2: S c= [:NAT,(NAT *),(X *):] by Def1;
 I in S ;
then  JumpPart I in NAT * by A2, RECDEF_2:2;
hence  ( JumpPart I is Function-like & JumpPart I is Relation-like ) ; ::_thesis: verum
end;
end;

registration
let S be non empty standard-ins set ;
let I be Element of S;
cluster AddressPart I ->  FinSequence-like ;
coherence
 AddressPart I is FinSequence-like
proof
consider X being non empty set  such that
A1: S c= [:NAT,(NAT *),(X *):] by Def1;
 I in S ;
then  AddressPart I in X * by A1, RECDEF_2:2;
hence  AddressPart I is FinSequence-like ; ::_thesis: verum
end;
cluster JumpPart I ->  FinSequence-like ;
coherence
 JumpPart I is FinSequence-like
proof
consider X being non empty set  such that
A2: S c= [:NAT,(NAT *),(X *):] by Def1;
 I in S ;
then  JumpPart I in NAT * by A2, RECDEF_2:2;
hence  JumpPart I is FinSequence-like ; ::_thesis: verum
end;
end;

registration
let S be non empty standard-ins set ;
let x be Element of S;
cluster InsCode x ->  natural ;
coherence
 InsCode x is natural
proof
consider X being non empty set  such that
A1: S c= [:NAT,(NAT *),(X *):] by Def1;
 x in S ;
then  x `1_3 in NAT by A1, RECDEF_2:2;
hence  InsCode x is natural ; ::_thesis: verum
end;
end;

registration
cluster standard-ins  ->  Relation-like for set ;
coherence
 for b1 being set st b1 is standard-ins holds
b1 is Relation-like
proof
let S be set ; ::_thesis: ( S is standard-ins implies S is Relation-like )
assume  S is standard-ins ; ::_thesis: S is Relation-like
then  ex X being non empty set st S c= [:NAT,(NAT *),(X *):] by Def1;
hence  S is Relation-like ; ::_thesis: verum
end;
end;

definition
let S be standard-ins set ;
func InsCodes S ->  set  equals :: COMPOS_0:def 2
 proj1_3 S;
correctness
coherence
proj1_3 S is set ;
;
end;

:: deftheorem  defines InsCodes COMPOS_0:def_2_:_
 for S being standard-ins set holds InsCodes S = proj1_3 S;

registration
let S be non empty standard-ins set ;
cluster InsCodes S ->  non empty ;
coherence
 not InsCodes S is empty
proof
 ex X being non empty set st S c= [:NAT,(NAT *),(X *):] by Def1;
then reconsider II = dom S as Relation ;
assume  InsCodes S is empty ; ::_thesis: contradiction
then  II = {} ;
hence  contradiction ; ::_thesis: verum
end;
end;

definition
let S be non empty standard-ins set ;
mode InsType of S is Element of InsCodes S;
end;

definition
let S be non empty standard-ins set ;
let I be Element of S;
:: original: InsCode
redefine func InsCode I ->  InsType of S;
coherence
 InsCode I is InsType of S
proof
consider X being non empty set  such that
A1: S c= [:NAT,(NAT *),(X *):] by Def1;
 I in S ;
then  I = [(I `1_3),(I `2_3),(I `3_3)] by A1, RECDEF_2:3;
then  [(I `1_3),(I `2_3)] in proj1 S by XTUPLE_0:def_12;
hence  InsCode I is InsType of S by XTUPLE_0:def_12; ::_thesis: verum
end;
end;

definition
let S be non empty standard-ins set ;
let T be InsType of S;
func JumpParts T ->  set  equals :: COMPOS_0:def 3
 {  (JumpPart I) where I is Element of S : InsCode I = T  }  ;
coherence
  {  (JumpPart I) where I is Element of S : InsCode I = T  }  is set ;
func AddressParts T ->  set  equals :: COMPOS_0:def 4
 {  (AddressPart I) where I is Element of S : InsCode I = T  }  ;
coherence
  {  (AddressPart I) where I is Element of S : InsCode I = T  }  is set ;
end;

:: deftheorem  defines JumpParts COMPOS_0:def_3_:_
 for S being non empty standard-ins set
for T being InsType of S holds JumpParts T =  {  (JumpPart I) where I is Element of S : InsCode I = T  }  ;

:: deftheorem  defines AddressParts COMPOS_0:def_4_:_
 for S being non empty standard-ins set
for T being InsType of S holds AddressParts T =  {  (AddressPart I) where I is Element of S : InsCode I = T  }  ;

registration
let S be non empty standard-ins set ;
let T be InsType of S;
cluster AddressParts T ->  functional ;
coherence
 AddressParts T is functional
proof
let f be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not f in AddressParts T or f is set )
assume  f in AddressParts T ; ::_thesis: f is set
then  ex I being Element of S st
( f = AddressPart I & InsCode I = T ) ;
hence  f is set ; ::_thesis: verum
end;
cluster JumpParts T ->  non empty functional ;
coherence
 ( not JumpParts T is empty & JumpParts T is functional )
proof
consider y being set  such that
A1: [T,y] in proj1 S by XTUPLE_0:def_12;
consider x being set  such that
A2: [[T,y],x] in S by A1, XTUPLE_0:def_12;
reconsider I = [T,y,x] as Element of S by A2;
 InsCode I = T by RECDEF_2:def_1;
then  JumpPart I in JumpParts T ;
hence  not JumpParts T is empty ; ::_thesis: JumpParts T is functional
let f be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not f in JumpParts T or f is set )
assume  f in JumpParts T ; ::_thesis: f is set
then  ex I being Element of S st
( f = JumpPart I & InsCode I = T ) ;
hence  f is set ; ::_thesis: verum
end;
end;

definition
let S be non empty standard-ins set ;
attrS is homogeneous  means :Def5: :: COMPOS_0:def 5
 for I, J being Element of S st InsCode I = InsCode J holds
dom (JumpPart I) = dom (JumpPart J);
canceled;
attrS is J/A-independent  means :Def7: :: COMPOS_0:def 7
 for T being InsType of S
for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds
for p being set st [T,f1,p] in S holds
[T,f2,p] in S;
end;

:: deftheorem Def5 defines homogeneous COMPOS_0:def_5_:_
 for S being non empty standard-ins set holds
( S is homogeneous iff for I, J being Element of S st InsCode I = InsCode J holds
dom (JumpPart I) = dom (JumpPart J) );

:: deftheorem  COMPOS_0:def_6_:_
canceled;

:: deftheorem Def7 defines J/A-independent COMPOS_0:def_7_:_
 for S being non empty standard-ins set holds
( S is J/A-independent iff for T being InsType of S
for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds
for p being set st [T,f1,p] in S holds
[T,f2,p] in S );

Lm1:  for T being InsType of {[0,{},{}]} holds JumpParts T = {0}
proof
let T be InsType of {[0,{},{}]}; ::_thesis: JumpParts T = {0}
set A =  {  (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T  }  ;
 {0} =  {  (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T  }  c= {0}
let a be set ; ::_thesis: ( a in {0} implies a in  {  (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T  }  )
assume  a in {0} ; ::_thesis: a in  {  (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T  }
then A1: a = 0 by TARSKI:def_1;
A2: InsCodes {[0,{},{}]} = {0} by MCART_1:92;
A3: T = 0 by A2, TARSKI:def_1;
reconsider I = [0,0,0] as Element of {[0,{},{}]} by TARSKI:def_1;
A4: JumpPart I = 0 by RECDEF_2:def_2;
 InsCode I = 0 by RECDEF_2:def_1;
hence  a in  {  (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T  }  by A1, A3, A4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T  }  or a in {0} )
assume  a in  {  (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T  }  ; ::_thesis: a in {0}
then consider I being Element of {[0,{},{}]} such that
A5: ( a = JumpPart I & InsCode I = T ) ;
 I = [0,{},{}] by TARSKI:def_1;
then  a = 0 by A5, RECDEF_2:def_2;
hence  a in {0} by TARSKI:def_1; ::_thesis: verum
end;
hence  JumpParts T = {0} ; ::_thesis: verum
end;

registration
cluster{[0,{},{}]} ->  homogeneous J/A-independent ;
coherence
 ( {[0,{},{}]} is J/A-independent & {[0,{},{}]} is homogeneous )
proof
thus  {[0,{},{}]} is J/A-independent ::_thesis: {[0,{},{}]} is homogeneous
proof
let T be InsType of {[0,{},{}]}; :: according to COMPOS_0:def_7 ::_thesis: for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds
for p being set st [T,f1,p] in {[0,{},{}]} holds
[T,f2,p] in {[0,{},{}]}
let f1, f2 be natural-valued Function; ::_thesis: ( f1 in JumpParts T & dom f1 = dom f2 implies for p being set st [T,f1,p] in {[0,{},{}]} holds
[T,f2,p] in {[0,{},{}]} )
assume that
A1: f1 in JumpParts T and
A2: dom f1 = dom f2 ; ::_thesis: for p being set st [T,f1,p] in {[0,{},{}]} holds
[T,f2,p] in {[0,{},{}]}
let p be set ; ::_thesis: ( [T,f1,p] in {[0,{},{}]} implies [T,f2,p] in {[0,{},{}]} )
A3: f1 in {0} by A1, Lm1;
 ( f1 = 0 & f2 = 0 ) by A3, A2, CARD_3:10;
hence  ( [T,f1,p] in {[0,{},{}]} implies [T,f2,p] in {[0,{},{}]} ) ; ::_thesis: verum
end;
let I, J be Element of {[0,{},{}]}; :: according to COMPOS_0:def_5 ::_thesis: ( InsCode I = InsCode J implies dom (JumpPart I) = dom (JumpPart J) )
assume  InsCode I = InsCode J ; ::_thesis: dom (JumpPart I) = dom (JumpPart J)
 ( I = [0,{},{}] & J = [0,{},{}] ) by TARSKI:def_1;
hence  dom (JumpPart I) = dom (JumpPart J) ; ::_thesis: verum
end;
end;

registration
cluster non empty Relation-like standard-ins homogeneous J/A-independent for set ;
existence
 ex b1 being non empty standard-ins set st
( b1 is J/A-independent & b1 is homogeneous )
proof
take S = {[0,{},{}]}; ::_thesis: ( S is J/A-independent & S is homogeneous )
thus  ( S is J/A-independent & S is homogeneous ) ; ::_thesis: verum
end;
end;

registration
let S be non empty standard-ins homogeneous set ;
let T be InsType of S;
cluster JumpParts T ->  with_common_domain ;
coherence
 JumpParts T is with_common_domain
proof
let f, g be Function; :: according to CARD_3:def_10 ::_thesis: ( not f in JumpParts T or not g in JumpParts T or proj1 f = proj1 g )
assume that
A1: f in JumpParts T and
A2: g in JumpParts T ; ::_thesis: proj1 f = proj1 g
A3: ex I being Element of S st
( f = JumpPart I & InsCode I = T ) by A1;
 ex J being Element of S st
( g = JumpPart J & InsCode J = T ) by A2;
hence  proj1 f = proj1 g by A3, Def5; ::_thesis: verum
end;
end;

registration
let S be non empty standard-ins set ;
let I be Element of S;
cluster JumpPart I ->  NAT -valued for Function;
coherence
 for b1 being Function st b1 = JumpPart I holds
b1 is NAT -valued
proof
let f be Function; ::_thesis: ( f = JumpPart I implies f is NAT -valued )
assume A1: f = JumpPart I ; ::_thesis: f is NAT -valued
consider X being non empty set  such that
A2: S c= [:NAT,(NAT *),(X *):] by Def1;
 I in S ;
then  JumpPart I in NAT * by A2, RECDEF_2:2;
hence  f is NAT -valued by A1, FINSEQ_1:def_11; ::_thesis: verum
end;
end;

Lm2:  for S being non empty standard-ins homogeneous set
for I being Element of S
for x being set st x in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . x c= NAT
proof
let S be non empty standard-ins homogeneous set ; ::_thesis: for I being Element of S
for x being set st x in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . x c= NAT
let I be Element of S; ::_thesis: for x being set st x in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . x c= NAT
let x be set ; ::_thesis: ( x in dom (JumpPart I) implies (product" (JumpParts (InsCode I))) . x c= NAT )
assume A1: x in dom (JumpPart I) ; ::_thesis: (product" (JumpParts (InsCode I))) . x c= NAT
 JumpPart I in JumpParts (InsCode I) ;
then  dom (product" (JumpParts (InsCode I))) = dom (JumpPart I) by CARD_3:100;
then A2: (product" (JumpParts (InsCode I))) . x =  {  (f . x) where f is Element of JumpParts (InsCode I) : verum  }  by A1, CARD_3:74;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (product" (JumpParts (InsCode I))) . x or e in NAT )
assume  e in (product" (JumpParts (InsCode I))) . x ; ::_thesis: e in NAT
then consider f being Element of JumpParts (InsCode I) such that
A3: e = f . x by A2;
 f in JumpParts (InsCode I) ;
then  ex J being Element of S st
( f = JumpPart J & InsCode J = InsCode I ) ;
hence  e in NAT by A3, ORDINAL1:def_12; ::_thesis: verum
end;

Lm3:  for S being non empty standard-ins homogeneous set st S is J/A-independent holds
for I being Element of S
for x being set st x in dom (JumpPart I) holds
NAT c= (product" (JumpParts (InsCode I))) . x
proof
let S be non empty standard-ins homogeneous set ; ::_thesis: ( S is J/A-independent implies for I being Element of S
for x being set st x in dom (JumpPart I) holds
NAT c= (product" (JumpParts (InsCode I))) . x )
assume A1: S is J/A-independent ; ::_thesis: for I being Element of S
for x being set st x in dom (JumpPart I) holds
NAT c= (product" (JumpParts (InsCode I))) . x
consider D0 being non empty set  such that
A2: S c= [:NAT,(NAT *),(D0 *):] by Def1;
let I be Element of S; ::_thesis: for x being set st x in dom (JumpPart I) holds
NAT c= (product" (JumpParts (InsCode I))) . x
let x be set ; ::_thesis: ( x in dom (JumpPart I) implies NAT c= (product" (JumpParts (InsCode I))) . x )
assume A3: x in dom (JumpPart I) ; ::_thesis: NAT c= (product" (JumpParts (InsCode I))) . x
A4: JumpPart I in JumpParts (InsCode I) ;
then  dom (product" (JumpParts (InsCode I))) = dom (JumpPart I) by CARD_3:100;
then A5: (product" (JumpParts (InsCode I))) . x =  {  (f . x) where f is Element of JumpParts (InsCode I) : verum  }  by A3, CARD_3:74;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in NAT or e in (product" (JumpParts (InsCode I))) . x )
assume  e in NAT ; ::_thesis: e in (product" (JumpParts (InsCode I))) . x
then reconsider e = e as Element of NAT ;
set g = (JumpPart I) +* (x,e);
A6: dom ((JumpPart I) +* (x,e)) = dom (JumpPart I) by FUNCT_7:30;
 I in S ;
then  [(InsCode I),(JumpPart I),(AddressPart I)] in S by A2, RECDEF_2:3;
then reconsider J = [(InsCode I),((JumpPart I) +* (x,e)),(AddressPart I)] as Element of S by A4, A1, A6, Def7;
 InsCode J = InsCode I by RECDEF_2:def_1;
then  JumpPart J in JumpParts (InsCode I) ;
then reconsider g = (JumpPart I) +* (x,e) as Element of JumpParts (InsCode I) by RECDEF_2:def_2;
 e = g . x by A3, FUNCT_7:31;
hence  e in (product" (JumpParts (InsCode I))) . x by A5; ::_thesis: verum
end;

theorem Th1: :: COMPOS_0:1
for S being non empty standard-ins set
for I, J being Element of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds
I = J
proof
let S be non empty standard-ins set ; ::_thesis: for I, J being Element of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds
I = J
let I, J be Element of S; ::_thesis: ( InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J implies I = J )
consider X being non empty set  such that
A1: S c= [:NAT,(NAT *),(X *):] by Def1;
A2: I in S ;
 J in S ;
hence  ( InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J implies I = J ) by A2, A1, RECDEF_2:10; ::_thesis: verum
end;

registration
let S be non empty standard-ins homogeneous J/A-independent set ;
let T be InsType of S;
cluster JumpParts T ->  product-like ;
coherence
 JumpParts T is product-like
proof
consider y being set  such that
A1: [T,y] in proj1 S by XTUPLE_0:def_12;
consider z being set  such that
A2: [[T,y],z] in S by A1, XTUPLE_0:def_12;
reconsider I = [T,y,z] as Element of S by A2;
A3: InsCode I = T by RECDEF_2:def_1;
A4: JumpPart I = y by RECDEF_2:def_2;
set f = (dom (JumpPart I)) --> NAT;
A5: dom ((dom (JumpPart I)) --> NAT) = dom (JumpPart I) by FUNCOP_1:13;
 for x being set holds
( x in JumpParts T iff ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y ) ) )
proof
let x be set ; ::_thesis: ( x in JumpParts T iff ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y ) ) )
thus  ( x in JumpParts T implies ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y ) ) ) ::_thesis: ( ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y ) ) implies x in JumpParts T )
proof
assume  x in JumpParts T ; ::_thesis: ex g being Function st
( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y ) )
then consider K being Element of S such that
A6: x = JumpPart K and
A7: InsCode K = T ;
take g = JumpPart K; ::_thesis: ( x = g & dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y ) )
thus  x = g by A6; ::_thesis: ( dom g = dom ((dom (JumpPart I)) --> NAT) & ( for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y ) )
thus A8: dom g = dom ((dom (JumpPart I)) --> NAT) by A7, A3, Def5, A5; ::_thesis: for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y
let y be set ; ::_thesis: ( y in dom ((dom (JumpPart I)) --> NAT) implies g . y in ((dom (JumpPart I)) --> NAT) . y )
assume A9: y in dom ((dom (JumpPart I)) --> NAT) ; ::_thesis: g . y in ((dom (JumpPart I)) --> NAT) . y
then  ((dom (JumpPart I)) --> NAT) . y = NAT by A5, FUNCOP_1:7;
hence  g . y in ((dom (JumpPart I)) --> NAT) . y by A8, A9, FUNCT_1:102; ::_thesis: verum
end;
given g being Function such that A10: x = g and
A11: dom g = dom ((dom (JumpPart I)) --> NAT) and
A12: for y being set st y in dom ((dom (JumpPart I)) --> NAT) holds
g . y in ((dom (JumpPart I)) --> NAT) . y ; ::_thesis: x in JumpParts T
A13: dom g = dom (JumpPart I) by A11, FUNCOP_1:13;
set J = [T,g,z];
A14: y in JumpParts T by A4, A3;
then A15: dom g = dom (product" (JumpParts T)) by A13, A4, CARD_3:100;
A16: for x being set st x in dom (product" (JumpParts T)) holds
g . x in (product" (JumpParts T)) . x
proof
let x be set ; ::_thesis: ( x in dom (product" (JumpParts T)) implies g . x in (product" (JumpParts T)) . x )
assume A17: x in dom (product" (JumpParts T)) ; ::_thesis: g . x in (product" (JumpParts T)) . x
A18: NAT c= (product" (JumpParts (InsCode I))) . x by A17, A15, A13, Lm3;
 ((dom (JumpPart I)) --> NAT) . x = NAT by A15, A13, A17, FUNCOP_1:7;
then  g . x in NAT by A12, A15, A17, A11;
hence  g . x in (product" (JumpParts T)) . x by A3, A18; ::_thesis: verum
end;
A19: g is natural-valued
proof
let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in proj1 g or g . x is natural )
assume A20: x in dom g ; ::_thesis: g . x is natural
then A21: (product" (JumpParts (InsCode I))) . x c= NAT by Lm2, A13;
 g . x in (product" (JumpParts T)) . x by A15, A16, A20;
hence  g . x is natural by A21, A3; ::_thesis: verum
end;
reconsider J = [T,g,z] as Element of S by A14, Def7, A4, A19, A13;
A22: InsCode J = T by RECDEF_2:def_1;
 g = JumpPart J by RECDEF_2:def_2;
hence  x in JumpParts T by A22, A10; ::_thesis: verum
end;
then  JumpParts T = product ((dom (JumpPart I)) --> NAT) by CARD_3:def_5;
hence  JumpParts T is product-like ; ::_thesis: verum
end;
end;

definition
let S be standard-ins set ;
let I be Element of S;
attrI is ins-loc-free  means :Def8: :: COMPOS_0:def 8
 JumpPart I is empty ;
end;

:: deftheorem Def8 defines ins-loc-free COMPOS_0:def_8_:_
 for S being standard-ins set
for I being Element of S holds
( I is ins-loc-free iff JumpPart I is empty );

registration
let S be non empty standard-ins set ;
let I be Element of S;
cluster JumpPart I ->  natural-valued for Function;
coherence
 for b1 being Function st b1 = JumpPart I holds
b1 is natural-valued ;
end;

definition
let S be non empty standard-ins homogeneous J/A-independent set ;
let I be Element of S;
let k be Nat;
func IncAddr (I,k) ->  Element of S means :Def9: :: COMPOS_0:def 9
( InsCode it = InsCode I & AddressPart it = AddressPart I & JumpPart it = k + (JumpPart I) );
existence
 ex b1 being Element of S st
( InsCode b1 = InsCode I & AddressPart b1 = AddressPart I & JumpPart b1 = k + (JumpPart I) )
proof
consider D0 being non empty set  such that
A1: S c= [:NAT,(NAT *),(D0 *):] by Def1;
set p = k + (JumpPart I);
set f = product" (JumpParts (InsCode I));
A2: JumpPart I in JumpParts (InsCode I) ;
A3: JumpParts (InsCode I) = product (product" (JumpParts (InsCode I))) by CARD_3:78;
A4: dom (k + (JumpPart I)) = dom (JumpPart I) by VALUED_1:def_2;
then A5: dom (k + (JumpPart I)) = DOM (JumpParts (InsCode I)) by A2, CARD_3:108
.= dom (product" (JumpParts (InsCode I))) by CARD_3:def_12 ;
 for z being set st z in dom (k + (JumpPart I)) holds
(k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z
proof
let z be set ; ::_thesis: ( z in dom (k + (JumpPart I)) implies (k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z )
assume A6: z in dom (k + (JumpPart I)) ; ::_thesis: (k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z
reconsider z = z as Element of NAT by A6;
A7: (product" (JumpParts (InsCode I))) . z c= NAT by A6, A4, Lm2;
 NAT c= (product" (JumpParts (InsCode I))) . z by A6, A4, Lm3;
then A8: (product" (JumpParts (InsCode I))) . z = NAT by A7, XBOOLE_0:def_10;
reconsider il = (JumpPart I) . z as Element of NAT by ORDINAL1:def_12;
 (k + (JumpPart I)) . z = k + il by A6, VALUED_1:def_2;
hence  (k + (JumpPart I)) . z in (product" (JumpParts (InsCode I))) . z by A8; ::_thesis: verum
end;
then  k + (JumpPart I) in JumpParts (InsCode I) by A3, A5, CARD_3:9;
then consider II being Element of S such that
A9: k + (JumpPart I) = JumpPart II and
 InsCode I = InsCode II ;
A10: JumpPart I in JumpParts (InsCode I) ;
 I in S ;
then  [(InsCode I),(JumpPart I),(AddressPart I)] = I by A1, RECDEF_2:3;
then reconsider IT = [(InsCode I),(JumpPart II),(AddressPart I)] as Element of S by A10, Def7, A4, A9;
take  IT ; ::_thesis: ( InsCode IT = InsCode I & AddressPart IT = AddressPart I & JumpPart IT = k + (JumpPart I) )
thus  InsCode IT = InsCode I by RECDEF_2:def_1; ::_thesis: ( AddressPart IT = AddressPart I & JumpPart IT = k + (JumpPart I) )
thus  AddressPart IT = AddressPart I by RECDEF_2:def_3; ::_thesis: JumpPart IT = k + (JumpPart I)
thus  JumpPart IT = k + (JumpPart I) by A9, RECDEF_2:def_2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of S st InsCode b1 = InsCode I & AddressPart b1 = AddressPart I & JumpPart b1 = k + (JumpPart I) & InsCode b2 = InsCode I & AddressPart b2 = AddressPart I & JumpPart b2 = k + (JumpPart I) holds
b1 = b2 by Th1;
end;

:: deftheorem Def9 defines IncAddr COMPOS_0:def_9_:_
 for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S
for k being Nat
for b4 being Element of S holds
( b4 = IncAddr (I,k) iff ( InsCode b4 = InsCode I & AddressPart b4 = AddressPart I & JumpPart b4 = k + (JumpPart I) ) );

theorem :: COMPOS_0:2
canceled;

theorem :: COMPOS_0:3
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds IncAddr (I,0) = I
proof
let S be non empty standard-ins homogeneous J/A-independent set ; ::_thesis: for I being Element of S holds IncAddr (I,0) = I
let I be Element of S; ::_thesis: IncAddr (I,0) = I
A1: InsCode (IncAddr (I,0)) = InsCode I by Def9;
A2: AddressPart (IncAddr (I,0)) = AddressPart I by Def9;
A3: JumpPart (IncAddr (I,0)) = 0 + (JumpPart I) by Def9;
then A4: dom (JumpPart I) = dom (JumpPart (IncAddr (I,0))) by VALUED_1:def_2;
 for k being Nat st k in dom (JumpPart I) holds
(JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k
proof
let k be Nat; ::_thesis: ( k in dom (JumpPart I) implies (JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k )
assume  k in dom (JumpPart I) ; ::_thesis: (JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k
hence (JumpPart (IncAddr (I,0))) . k = 0 + ((JumpPart I) . k) by A4, A3, VALUED_1:def_2
.= (JumpPart I) . k ;
::_thesis: verum
end;
then  JumpPart (IncAddr (I,0)) = JumpPart I by A4, FINSEQ_1:13;
hence  IncAddr (I,0) = I by A1, A2, Th1; ::_thesis: verum
end;

theorem Th4: :: COMPOS_0:4
for k being Nat
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S st I is ins-loc-free holds
IncAddr (I,k) = I
proof
let k be Nat; ::_thesis: for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S st I is ins-loc-free holds
IncAddr (I,k) = I
let S be non empty standard-ins homogeneous J/A-independent set ; ::_thesis: for I being Element of S st I is ins-loc-free holds
IncAddr (I,k) = I
let I be Element of S; ::_thesis: ( I is ins-loc-free implies IncAddr (I,k) = I )
assume A1: JumpPart I is empty ; :: according to COMPOS_0:def_8 ::_thesis: IncAddr (I,k) = I
set f = IncAddr (I,k);
A2: InsCode (IncAddr (I,k)) = InsCode I by Def9;
A3: AddressPart (IncAddr (I,k)) = AddressPart I by Def9;
A4: JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def9;
 JumpPart (IncAddr (I,k)) = JumpPart I by A1, A4;
hence  IncAddr (I,k) = I by A2, A3, Th1; ::_thesis: verum
end;

theorem :: COMPOS_0:5
for k being Nat
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))
proof
let k be Nat; ::_thesis: for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))
let S be non empty standard-ins homogeneous J/A-independent set ; ::_thesis: for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))
let I be Element of S; ::_thesis: JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))
set A =  {  (JumpPart J) where J is Element of S : InsCode I = InsCode J  }  ;
set B =  {  (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J  }  ;
  {  (JumpPart J) where J is Element of S : InsCode I = InsCode J  }  =  {  (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J  }  c=  {  (JumpPart J) where J is Element of S : InsCode I = InsCode J  }
let a be set ; ::_thesis: ( a in  {  (JumpPart J) where J is Element of S : InsCode I = InsCode J  }  implies a in  {  (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J  }  )
assume  a in  {  (JumpPart J) where J is Element of S : InsCode I = InsCode J  }  ; ::_thesis: a in  {  (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J  }
then consider J being Element of S such that
A1: a = JumpPart J and
A2: InsCode J = InsCode I ;
 InsCode J = InsCode (IncAddr (I,k)) by A2, Def9;
hence  a in  {  (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J  }  by A1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J  }  or a in  {  (JumpPart J) where J is Element of S : InsCode I = InsCode J  }  )
assume  a in  {  (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J  }  ; ::_thesis: a in  {  (JumpPart J) where J is Element of S : InsCode I = InsCode J  }
then consider J being Element of S such that
A3: a = JumpPart J and
A4: InsCode J = InsCode (IncAddr (I,k)) ;
 InsCode J = InsCode I by A4, Def9;
hence  a in  {  (JumpPart J) where J is Element of S : InsCode I = InsCode J  }  by A3; ::_thesis: verum
end;
hence  JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k))) ; ::_thesis: verum
end;

theorem Th6: :: COMPOS_0:6
for S being non empty standard-ins homogeneous J/A-independent set
for I, J being Element of S st ex k being Nat st IncAddr (I,k) = IncAddr (J,k) holds
I = J
proof
let S be non empty standard-ins homogeneous J/A-independent set ; ::_thesis: for I, J being Element of S st ex k being Nat st IncAddr (I,k) = IncAddr (J,k) holds
I = J
let I, J be Element of S; ::_thesis: ( ex k being Nat st IncAddr (I,k) = IncAddr (J,k) implies I = J )
given k being Nat such that A1: IncAddr (I,k) = IncAddr (J,k) ; ::_thesis: I = J
A2: InsCode I = InsCode (IncAddr (I,k)) by Def9
.= InsCode J by A1, Def9 ;
A3: AddressPart I = AddressPart (IncAddr (I,k)) by Def9
.= AddressPart J by A1, Def9 ;
A4: JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def9;
then A5: dom (JumpPart I) = dom (JumpPart (IncAddr (I,k))) by VALUED_1:def_2;
A6: JumpPart (IncAddr (J,k)) = k + (JumpPart J) by Def9;
then A7: dom (JumpPart J) = dom (JumpPart (IncAddr (J,k))) by VALUED_1:def_2;
A8: dom (JumpPart I) = dom (JumpPart J) by A2, Def5;
 for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x = (JumpPart J) . x
proof
let x be set ; ::_thesis: ( x in dom (JumpPart I) implies (JumpPart I) . x = (JumpPart J) . x )
assume A9: x in dom (JumpPart I) ; ::_thesis: (JumpPart I) . x = (JumpPart J) . x
A10: (JumpPart (IncAddr (I,k))) . x = k + ((JumpPart I) . x) by A4, A5, A9, VALUED_1:def_2;
A11: (JumpPart (IncAddr (J,k))) . x = k + ((JumpPart J) . x) by A6, A8, A9, A7, VALUED_1:def_2;
thus  (JumpPart I) . x = (JumpPart J) . x by A1, A10, A11; ::_thesis: verum
end;
then  JumpPart I = JumpPart J by A8, FUNCT_1:2;
hence  I = J by A2, A3, Th1; ::_thesis: verum
end;

theorem :: COMPOS_0:7
for k, m being Nat
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
proof
let k, m be Nat; ::_thesis: for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
let S be non empty standard-ins homogeneous J/A-independent set ; ::_thesis: for I being Element of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
let I be Element of S; ::_thesis: IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
A1: InsCode (IncAddr ((IncAddr (I,k)),m)) = InsCode (IncAddr (I,k)) by Def9
.= InsCode I by Def9
.= InsCode (IncAddr (I,(k + m))) by Def9 ;
A2: AddressPart (IncAddr ((IncAddr (I,k)),m)) = AddressPart (IncAddr (I,k)) by Def9
.= AddressPart I by Def9
.= AddressPart (IncAddr (I,(k + m))) by Def9 ;
A3: JumpPart (IncAddr ((IncAddr (I,k)),m)) = m + (JumpPart (IncAddr (I,k))) by Def9;
A4: JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def9;
A5: JumpPart (IncAddr (I,(k + m))) = (k + m) + (JumpPart I) by Def9;
then A6: dom (JumpPart (IncAddr (I,(k + m)))) = dom (JumpPart I) by VALUED_1:def_2
.= dom (JumpPart (IncAddr (I,k))) by A4, VALUED_1:def_2
.= dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) by A3, VALUED_1:def_2 ;
 for n being set st n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) holds
(JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n
proof
let n be set ; ::_thesis: ( n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) implies (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n )
assume A7: n in dom (JumpPart (IncAddr ((IncAddr (I,k)),m))) ; ::_thesis: (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n
then A8: n in dom (JumpPart (IncAddr (I,k))) by A3, VALUED_1:def_2;
then A9: n in dom (JumpPart I) by A4, VALUED_1:def_2;
A10: (JumpPart (IncAddr (I,k))) . n = k + ((JumpPart I) . n) by A4, A8, VALUED_1:def_2;
A11: (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = m + ((JumpPart (IncAddr (I,k))) . n) by A7, A3, VALUED_1:def_2;
 n in dom (JumpPart (IncAddr (I,(k + m)))) by A5, A9, VALUED_1:def_2;
then  (JumpPart (IncAddr (I,(k + m)))) . n = (k + m) + ((JumpPart I) . n) by A5, VALUED_1:def_2;
hence  (JumpPart (IncAddr ((IncAddr (I,k)),m))) . n = (JumpPart (IncAddr (I,(k + m)))) . n by A11, A10; ::_thesis: verum
end;
then  JumpPart (IncAddr ((IncAddr (I,k)),m)) = JumpPart (IncAddr (I,(k + m))) by A6, FUNCT_1:2;
hence  IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m)) by A1, A2, Th1; ::_thesis: verum
end;

theorem :: COMPOS_0:8
for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x
proof
let S be non empty standard-ins homogeneous J/A-independent set ; ::_thesis: for I being Element of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x
let I be Element of S; ::_thesis: for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x
let x be set ; ::_thesis: ( x in dom (JumpPart I) implies (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x )
assume A1: x in dom (JumpPart I) ; ::_thesis: (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x
A2: JumpPart I in JumpParts (InsCode I) ;
A3: dom (product" (JumpParts (InsCode I))) = DOM (JumpParts (InsCode I)) by CARD_3:def_12
.= dom (JumpPart I) by A2, CARD_3:108 ;
 (JumpPart I) . x in pi ((JumpParts (InsCode I)),x) by A2, CARD_3:def_6;
hence  (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x by A1, A3, CARD_3:def_12; ::_thesis: verum
end;

registration
cluster{[0,{},{}],[1,{},{}]} ->  standard-ins ;
coherence
 {[0,{},{}],[1,{},{}]} is standard-ins
proof
take  {{}} ; :: according to COMPOS_0:def_1 ::_thesis: {[0,{},{}],[1,{},{}]} c= [:NAT,(NAT *),({{}} *):]
A1: {{}} c= {{}} * by ZFMISC_1:31, FINSEQ_1:49;
A2: {{}} c= NAT * by ZFMISC_1:31, FINSEQ_1:49;
 {[0,{},{}]} = [:{0},{{}},{{}}:] by MCART_1:35;
then A3: {[0,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A1, A2, MCART_1:73;
 {[1,{},{}]} = [:{1},{{}},{{}}:] by MCART_1:35;
then A4: {[1,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A1, A2, MCART_1:73;
 {[0,{},{}]} \/ {[1,{},{}]} = {[0,{},{}],[1,0,0]} by ENUMSET1:1;
hence  {[0,{},{}],[1,{},{}]} c= [:NAT,(NAT *),({{}} *):] by A3, A4, XBOOLE_1:8; ::_thesis: verum
end;
end;

theorem Th9: :: COMPOS_0:9
for x being Element of {[0,{},{}],[1,{},{}]} holds JumpPart x = {}
proof
let x be Element of {[0,{},{}],[1,{},{}]}; ::_thesis: JumpPart x = {}
 ( x = [0,{},{}] or x = [1,{},{}] ) by TARSKI:def_2;
hence  JumpPart x = {} by RECDEF_2:def_2; ::_thesis: verum
end;

Lm4:  for T being InsType of {[0,{},{}],[1,{},{}]} holds JumpParts T = {0}
proof
let T be InsType of {[0,{},{}],[1,{},{}]}; ::_thesis: JumpParts T = {0}
set A =  {  (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T  }  ;
 {0} =  {  (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T  }  c= {0}
let a be set ; ::_thesis: ( a in {0} implies a in  {  (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T  }  )
assume  a in {0} ; ::_thesis: a in  {  (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T  }
then A1: a = 0 by TARSKI:def_1;
A2: ( InsCodes {[0,{},{}]} = {0} & InsCodes {[1,{},{}]} = {1} ) by MCART_1:92;
InsCodes {[0,{},{}],[1,{},{}]} = proj1_3 ({[0,{},{}]} \/ {[1,{},{}]}) by ENUMSET1:1
.= (InsCodes {[0,{},{}]}) \/ (InsCodes {[1,{},{}]}) by XTUPLE_0:31 ;
then  ( T in {0} or T in {1} ) by A2, XBOOLE_0:def_3;
then A3: ( T = 0 or T = 1 ) by TARSKI:def_1;
reconsider I = [0,0,0], J = [1,0,0] as Element of {[0,{},{}],[1,{},{}]} by TARSKI:def_2;
A4: ( JumpPart I = 0 & JumpPart J = 0 ) by RECDEF_2:def_2;
 ( InsCode I = 0 & InsCode J = 1 ) by RECDEF_2:def_1;
hence  a in  {  (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T  }  by A1, A3, A4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T  }  or a in {0} )
assume  a in  {  (JumpPart I) where I is Element of {[0,{},{}],[1,{},{}]} : InsCode I = T  }  ; ::_thesis: a in {0}
then consider I being Element of {[0,{},{}],[1,{},{}]} such that
A5: ( a = JumpPart I & InsCode I = T ) ;
 ( I = [0,{},{}] or I = [1,{},{}] ) by TARSKI:def_2;
then  a = 0 by A5, RECDEF_2:def_2;
hence  a in {0} by TARSKI:def_1; ::_thesis: verum
end;
hence  JumpParts T = {0} ; ::_thesis: verum
end;

registration
cluster{[0,{},{}],[1,{},{}]} ->  homogeneous J/A-independent ;
coherence
 ( {[0,{},{}],[1,{},{}]} is J/A-independent & {[0,{},{}],[1,{},{}]} is homogeneous )
proof
set S = {[0,{},{}],[1,{},{}]};
thus  {[0,{},{}],[1,{},{}]} is J/A-independent ::_thesis: {[0,{},{}],[1,{},{}]} is homogeneous
proof
let T be InsType of {[0,{},{}],[1,{},{}]}; :: according to COMPOS_0:def_7 ::_thesis: for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds
for p being set st [T,f1,p] in {[0,{},{}],[1,{},{}]} holds
[T,f2,p] in {[0,{},{}],[1,{},{}]}
let f1, f2 be natural-valued Function; ::_thesis: ( f1 in JumpParts T & dom f1 = dom f2 implies for p being set st [T,f1,p] in {[0,{},{}],[1,{},{}]} holds
[T,f2,p] in {[0,{},{}],[1,{},{}]} )
assume that
A1: f1 in JumpParts T and
A2: dom f1 = dom f2 ; ::_thesis: for p being set st [T,f1,p] in {[0,{},{}],[1,{},{}]} holds
[T,f2,p] in {[0,{},{}],[1,{},{}]}
let p be set ; ::_thesis: ( [T,f1,p] in {[0,{},{}],[1,{},{}]} implies [T,f2,p] in {[0,{},{}],[1,{},{}]} )
A3: f1 in {0} by A1, Lm4;
 ( f1 = 0 & f2 = 0 ) by A3, A2, CARD_3:10;
hence  ( [T,f1,p] in {[0,{},{}],[1,{},{}]} implies [T,f2,p] in {[0,{},{}],[1,{},{}]} ) ; ::_thesis: verum
end;
let I, J be Element of {[0,{},{}],[1,{},{}]}; :: according to COMPOS_0:def_5 ::_thesis: ( InsCode I = InsCode J implies dom (JumpPart I) = dom (JumpPart J) )
assume  InsCode I = InsCode J ; ::_thesis: dom (JumpPart I) = dom (JumpPart J)
 ( JumpPart I = {} & JumpPart J = {} ) by Th9;
hence  dom (JumpPart I) = dom (JumpPart J) ; ::_thesis: verum
end;
end;

theorem :: COMPOS_0:10
for S being non empty standard-ins set
for T being InsType of S ex I being Element of S st InsCode I = T
proof
let S be non empty standard-ins set ; ::_thesis: for T being InsType of S ex I being Element of S st InsCode I = T
let T be InsType of S; ::_thesis: ex I being Element of S st InsCode I = T
consider y being set  such that
A1: [T,y] in proj1 S by XTUPLE_0:def_12;
consider z being set  such that
A2: [[T,y],z] in S by A1, XTUPLE_0:def_12;
reconsider I = [[T,y],z] as Element of S by A2;
take  I ; ::_thesis: InsCode I = T
 I = [T,y,z] ;
hence  InsCode I = T by RECDEF_2:def_1; ::_thesis: verum
end;

theorem :: COMPOS_0:11
for S being non empty standard-ins homogeneous set
for I being Element of S st JumpPart I = {} holds
JumpParts (InsCode I) = {0}
proof
let S be non empty standard-ins homogeneous set ; ::_thesis: for I being Element of S st JumpPart I = {} holds
JumpParts (InsCode I) = {0}
let I be Element of S; ::_thesis: ( JumpPart I = {} implies JumpParts (InsCode I) = {0} )
assume A1: JumpPart I = 0 ; ::_thesis: JumpParts (InsCode I) = {0}
set T = InsCode I;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {0} c= JumpParts (InsCode I)
let a be set ; ::_thesis: ( a in JumpParts (InsCode I) implies a in {0} )
assume  a in JumpParts (InsCode I) ; ::_thesis: a in {0}
then consider II being Element of S such that
A2: a = JumpPart II and
A3: InsCode II = InsCode I ;
 dom (JumpPart II) = dom (JumpPart I) by A3, Def5;
then  a = 0 by A1, A2;
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 (InsCode I) )
assume  a in {0} ; ::_thesis: a in JumpParts (InsCode I)
then  a = 0 by TARSKI:def_1;
hence  a in JumpParts (InsCode I) by A1; ::_thesis: verum
end;

begin

definition
let X be set ;
attrX is with_halt  means :Def10: :: COMPOS_0:def 10
[0,{},{}] in X;
end;

:: deftheorem Def10 defines with_halt COMPOS_0:def_10_:_
 for X being set holds
( X is with_halt iff [0,{},{}] in X );

registration
cluster with_halt  ->  non empty for set ;
coherence
 for b1 being set st b1 is with_halt holds
not b1 is empty by Def10;
end;

registration
cluster{[0,{},{}]} ->  with_halt ;
coherence
 {[0,{},{}]} is with_halt
proof
thus  [0,{},{}] in {[0,{},{}]} by TARSKI:def_1; :: according to COMPOS_0:def_10 ::_thesis: verum
end;
cluster{[0,{},{}],[1,{},{}]} ->  with_halt ;
coherence
 {[0,{},{}],[1,{},{}]} is with_halt
proof
thus  [0,{},{}] in {[0,{},{}],[1,{},{}]} by TARSKI:def_2; :: according to COMPOS_0:def_10 ::_thesis: verum
end;
end;

registration
cluster standard-ins with_halt for set ;
existence
 ex b1 being set st
( b1 is with_halt & b1 is standard-ins )
proof
take S = {[0,{},{}]}; ::_thesis: ( S is with_halt & S is standard-ins )
thus  ( S is with_halt & S is standard-ins ) ; ::_thesis: verum
end;
end;

registration
cluster non empty Relation-like standard-ins homogeneous J/A-independent with_halt for set ;
existence
 ex b1 being standard-ins with_halt set st
( b1 is J/A-independent & b1 is homogeneous )
proof
take S = {[0,{},{}]}; ::_thesis: ( S is J/A-independent & S is homogeneous )
thus  ( S is J/A-independent & S is homogeneous ) ; ::_thesis: verum
end;
end;

definition
let S be with_halt set ;
func halt S ->  Element of S equals :: COMPOS_0:def 11
[0,{},{}];
coherence
 [0,{},{}] is Element of S by Def10;
end;

:: deftheorem  defines halt COMPOS_0:def_11_:_
 for S being with_halt set holds halt S = [0,{},{}];

registration
let S be standard-ins with_halt set ;
cluster halt S ->  ins-loc-free ;
coherence
 halt S is ins-loc-free
proof
thus  JumpPart (halt S) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;

registration
let S be standard-ins with_halt set ;
cluster ins-loc-free for Element of S;
existence
 ex b1 being Element of S st b1 is ins-loc-free
proof
take  halt S ; ::_thesis: halt S is ins-loc-free
thus  halt S is ins-loc-free ; ::_thesis: verum
end;
end;

registration
let S be standard-ins with_halt set ;
let I be ins-loc-free Element of S;
cluster JumpPart I ->  empty ;
coherence
 JumpPart I is empty by Def8;
end;

theorem :: COMPOS_0:12
for k being Nat
for S being non empty standard-ins homogeneous J/A-independent with_halt set
for I being Element of S st IncAddr (I,k) = halt S holds
I = halt S
proof
let k be Nat; ::_thesis: for S being non empty standard-ins homogeneous J/A-independent with_halt set
for I being Element of S st IncAddr (I,k) = halt S holds
I = halt S
let S be non empty standard-ins homogeneous J/A-independent with_halt set ; ::_thesis: for I being Element of S st IncAddr (I,k) = halt S holds
I = halt S
let I be Element of S; ::_thesis: ( IncAddr (I,k) = halt S implies I = halt S )
assume  IncAddr (I,k) = halt S ; ::_thesis: I = halt S
then  IncAddr (I,k) = IncAddr ((halt S),k) by Th4;
hence  I = halt S by Th6; ::_thesis: verum
end;

definition
let S be non empty standard-ins homogeneous J/A-independent with_halt set ;
let i be Element of S;
attri is No-StopCode  means :: COMPOS_0:def 12
i <> halt S;
end;

:: deftheorem  defines No-StopCode COMPOS_0:def_12_:_
 for S being non empty standard-ins homogeneous J/A-independent with_halt set
for i being Element of S holds
( i is No-StopCode iff i <> halt S );

begin

definition
mode Instructions is standard-ins homogeneous J/A-independent with_halt set ;
end;

registration
cluster non empty non trivial Relation-like standard-ins homogeneous J/A-independent with_halt for set ;
existence
 not for b1 being Instructions holds b1 is trivial
proof
take  {[0,{},{}],[1,{},{}]} ; ::_thesis: not {[0,{},{}],[1,{},{}]} is trivial
 [0,{},{}] <> [1,{},{}] by XTUPLE_0:3;
hence  not {[0,{},{}],[1,{},{}]} is trivial by CHAIN_1:3; ::_thesis: verum
end;
end;