:: NECKLA_2 semantic presentation

theorem Th1: :: NECKLA_2:1

for b₁ being Universe
for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
for b₄ being Relation of b₂,b₃ holds b₄ in b₁

proof end;

theorem Th2: :: NECKLA_2:2

the InternalRel of (Necklace 4) = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}

proof end;

registration

let c₁ be natural number ;
cluster -> finite Element of Rank a₁;
coherence

proof end;

end;

theorem Th3: :: NECKLA_2:3

for b₁ being set st b₁ in FinSETS holds
b₁ is finite

proof end;

registration

cluster -> finite Element of FinSETS ;
coherence by Th3;

end;

registration

cluster ordinal finite -> natural set ;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
attr a₁ is N-free means :Def1: :: NECKLA_2:def 1
not a₁ embeds Necklace 4;

end;

:: deftheorem Def1 defines N-free NECKLA_2:def 1 :

registration

cluster non empty strict finite N-free RelStr ;
existence

proof end;

end;

definition

let c₁, c₂ be RelStr ;
func union_of c₁,c₂ -> strict RelStr means :Def2: :: NECKLA_2:def 2
( the carrier of a₃ = the carrier of a₁ \/ the carrier of a₂ & the InternalRel of a₃ = the InternalRel of a₁ \/ the InternalRel of a₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines union_of NECKLA_2:def 2 :

definition

let c₁, c₂ be RelStr ;
func sum_of c₁,c₂ -> strict RelStr means :Def3: :: NECKLA_2:def 3
( the carrier of a₃ = the carrier of a₁ \/ the carrier of a₂ & the InternalRel of a₃ = ((the InternalRel of a₁ \/ the InternalRel of a₂) \/ [:the carrier of a₁,the carrier of a₂:]) \/ [:the carrier of a₂,the carrier of a₁:] );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines sum_of NECKLA_2:def 3 :

definition

func fin_RelStr -> set means :Def4: :: NECKLA_2:def 4
for b₁ being set holds
( b₁ in a₁ iff ex b₂ being strict RelStr st
( b₁ = b₂ & the carrier of b₂ in FinSETS ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines fin_RelStr NECKLA_2:def 4 :

registration

cluster fin_RelStr -> non empty ;
correctness

proof end;

end;

definition

func fin_RelStr_sp -> Subset of fin_RelStr means :Def5: :: NECKLA_2:def 5
( ( for b₁ being strict RelStr st not the carrier of b₁ is empty & the carrier of b₁ is trivial & the carrier of b₁ in FinSETS holds
b₁ in a₁ ) & ( for b₁, b₂ being strict RelStr st the carrier of b₁ misses the carrier of b₂ & b₁ in a₁ & b₂ in a₁ holds
( union_of b₁,b₂ in a₁ & sum_of b₁,b₂ in a₁ ) ) & ( for b₁ being Subset of fin_RelStr st ( for b₂ being strict RelStr st not the carrier of b₂ is empty & the carrier of b₂ is trivial & the carrier of b₂ in FinSETS holds
b₂ in b₁ ) & ( for b₂, b₃ being strict RelStr st the carrier of b₂ misses the carrier of b₃ & b₂ in b₁ & b₃ in b₁ holds
( union_of b₂,b₃ in b₁ & sum_of b₂,b₃ in b₁ ) ) holds
a₁ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines fin_RelStr_sp NECKLA_2:def 5 :

registration

cluster fin_RelStr_sp -> non empty ;
correctness

proof end;

end;

theorem Th4: :: NECKLA_2:4

for b₁ being set st b₁ in fin_RelStr_sp holds
b₁ is non empty strict finite RelStr

proof end;

theorem Th5: :: NECKLA_2:5

for b₁ being RelStr st b₁ in fin_RelStr_sp holds
the carrier of b₁ in FinSETS

proof end;

theorem Th6: :: NECKLA_2:6

for b₁ being set holds
( not b₁ in fin_RelStr_sp or b₁ is non empty strict trivial RelStr or ex b₂, b₃ being strict RelStr st
( the carrier of b₂ misses the carrier of b₃ & b₂ in fin_RelStr_sp & b₃ in fin_RelStr_sp & ( b₁ = union_of b₂,b₃ or b₁ = sum_of b₂,b₃ ) ) )

proof end;

Lemma11: the carrier of (Necklace 4) = {0,1,2,3}
by NECKLACE:2, NECKLACE:21;

theorem Th7: :: NECKLA_2:7

for b₁ being non empty strict RelStr st b₁ in fin_RelStr_sp holds
b₁ is N-free

proof end;