:: 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;