:: NECKLA_2 semantic presentation

theorem Th1: :: NECKLA_2:1

for U being Universe
for X, Y being set st X in U & Y in U holds
for R being Relation of X,Y holds R in U

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 n be natural number ;
cluster -> finite Element of Rank n;
coherence

proof end;

end;

theorem Th3: :: NECKLA_2:3

for x being set st x in FinSETS holds
x 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 G be non empty RelStr ;
attr G is N-free means :Def1: :: NECKLA_2:def 1
not G 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 R, S be RelStr ;
func union_of R,S -> strict RelStr means :Def2: :: NECKLA_2:def 2
( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = the InternalRel of R \/ the InternalRel of S );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines union_of NECKLA_2:def 2 :

definition

let R, S be RelStr ;
func sum_of R,S -> strict RelStr means :Def3: :: NECKLA_2:def 3
( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = ((the InternalRel of R \/ the InternalRel of S) \/ [:the carrier of R,the carrier of S:]) \/ [:the carrier of S,the carrier of R:] );
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 X being set holds
( X in it iff ex R being strict RelStr st
( X = R & the carrier of R 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 R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in it ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in it & H2 in it holds
( union_of H1,H2 in it & sum_of H1,H2 in it ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of H1,H2 in M & sum_of H1,H2 in M ) ) holds
it c= M ) );
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 X being set st X in fin_RelStr_sp holds
X is non empty strict finite RelStr

proof end;

theorem :: NECKLA_2:5

for R being RelStr st R in fin_RelStr_sp holds
the carrier of R in FinSETS

proof end;

theorem Th6: :: NECKLA_2:6

for X being set holds
( not X in fin_RelStr_sp or X is non empty strict trivial RelStr or ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of H1,H2 or X = sum_of H1,H2 ) ) )

proof end;

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

theorem :: NECKLA_2:7

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

proof end;