:: NECKLA_3 semantic presentation

theorem Th1: :: NECKLA_3:1

for A, B being set holds (id A) | B = (id A) /\ [:B,B:]

proof end;

theorem :: NECKLA_3:2

for a, b, c, d being set holds id {a,b,c,d} = {[a,a],[b,b],[c,c],[d,d]}

proof end;

theorem Th3: :: NECKLA_3:3

for a, b, c, d, e, f, g, h being set holds [:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}

proof end;

registration

let X, Y be trivial set ;
cluster -> trivial Relation of X,Y;
correctness

proof end;

end;

theorem Th4: :: NECKLA_3:4

for X being trivial set
for R being Relation of X st not R is empty holds
ex x being set st R = {[x,x]}

proof end;

registration

let X be trivial set ;
cluster -> reflexive symmetric strongly_connected transitive trivial Relation of X,X;
correctness

proof end;

end;

theorem Th5: :: NECKLA_3:5

for X being non empty trivial set
for R being Relation of X holds R is_symmetric_in X

proof end;

registration

cluster non empty strict symmetric irreflexive finite RelStr ;
correctness

proof end;

end;

registration

let L be irreflexive RelStr ;
cluster full -> irreflexive full SubRelStr of L;
correctness

proof end;

end;

registration

let L be symmetric RelStr ;
cluster full -> symmetric full SubRelStr of L;
correctness

proof end;

end;

theorem Th6: :: NECKLA_3:6

for R being symmetric irreflexive RelStr st Card the carrier of R = 2 holds
ex a, b being set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )

proof end;

registration

let R be non empty RelStr ;
let S be RelStr ;
cluster union_of R,S -> non empty ;
correctness

proof end;

cluster sum_of R,S -> non empty ;
correctness

proof end;

end;

registration

let R be RelStr ;
let S be non empty RelStr ;
cluster union_of R,S -> non empty ;
correctness

proof end;

cluster sum_of R,S -> non empty ;
correctness

proof end;

end;

registration

let R, S be finite RelStr ;
cluster union_of R,S -> finite ;
correctness

proof end;

cluster sum_of R,S -> finite ;
correctness

proof end;

end;

registration

let R, S be symmetric RelStr ;
cluster union_of R,S -> symmetric ;
correctness

proof end;

cluster sum_of R,S -> symmetric ;
correctness

proof end;

end;

registration

let R, S be irreflexive RelStr ;
cluster union_of R,S -> irreflexive ;
correctness

proof end;

end;

theorem :: NECKLA_3:7

for R, S being irreflexive RelStr st the carrier of R misses the carrier of S holds
sum_of R,S is irreflexive

proof end;

theorem Th8: :: NECKLA_3:8

for R1, R2 being RelStr holds
( union_of R1,R2 = union_of R2,R1 & sum_of R1,R2 = sum_of R2,R1 )

proof end;

theorem Th9: :: NECKLA_3:9

for G being irreflexive RelStr
for G1, G2 being RelStr st ( G = union_of G1,G2 or G = sum_of G1,G2 ) holds
( G1 is irreflexive & G2 is irreflexive )

proof end;

theorem Th10: :: NECKLA_3:10

for G being non empty RelStr
for H1, H2 being RelStr st the carrier of H1 misses the carrier of H2 & ( RelStr(# the carrier of G,the InternalRel of G #) = union_of H1,H2 or RelStr(# the carrier of G,the InternalRel of G #) = sum_of H1,H2 ) holds
( H1 is full SubRelStr of G & H2 is full SubRelStr of G )

proof end;

theorem Th11: :: NECKLA_3:11

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

proof end;

registration

let R be RelStr ;
cluster ComplRelStr R -> irreflexive ;
correctness

proof end;

end;

registration

let R be symmetric RelStr ;
cluster ComplRelStr R -> symmetric irreflexive ;
correctness

proof end;

end;

theorem Th12: :: NECKLA_3:12

for R being RelStr holds the InternalRel of R misses the InternalRel of (ComplRelStr R)

proof end;

theorem Th13: :: NECKLA_3:13

for R being RelStr holds id the carrier of R misses the InternalRel of (ComplRelStr R)

proof end;

theorem Th14: :: NECKLA_3:14

for G being RelStr holds [:the carrier of G,the carrier of G:] = ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)

proof end;

theorem Th15: :: NECKLA_3:15

for G being strict irreflexive RelStr st G is trivial holds
ComplRelStr G = G

proof end;

theorem Th16: :: NECKLA_3:16

for G being strict irreflexive RelStr holds ComplRelStr (ComplRelStr G) = G

proof end;

theorem Th17: :: NECKLA_3:17

for G1, G2 being RelStr st the carrier of G1 misses the carrier of G2 holds
ComplRelStr (union_of G1,G2) = sum_of (ComplRelStr G1),(ComplRelStr G2)

proof end;

theorem Th18: :: NECKLA_3:18

for G1, G2 being RelStr st the carrier of G1 misses the carrier of G2 holds
ComplRelStr (sum_of G1,G2) = union_of (ComplRelStr G1),(ComplRelStr G2)

proof end;

theorem :: NECKLA_3:19

for G being RelStr
for H being full SubRelStr of G holds the InternalRel of (ComplRelStr H) = the InternalRel of (ComplRelStr G) |_2 the carrier of (ComplRelStr H)

proof end;

theorem Th20: :: NECKLA_3:20

for G being non empty irreflexive RelStr
for x being Element of G
for x' being Element of (ComplRelStr G) st x = x' holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'})

proof end;

registration

cluster non empty strict trivial -> non empty N-free RelStr ;
correctness

proof end;

end;

theorem :: NECKLA_3:21

for R being reflexive antisymmetric RelStr
for S being RelStr holds
( ex f being Function of R,S st
for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) iff S embeds R )

proof end;

theorem Th22: :: NECKLA_3:22

for G being non empty RelStr
for H being non empty full SubRelStr of G holds G embeds H

proof end;

theorem Th23: :: NECKLA_3:23

for G being non empty RelStr
for H being non empty full SubRelStr of G st G is N-free holds
H is N-free

proof end;

theorem Th24: :: NECKLA_3:24

for G being non empty irreflexive RelStr holds
( G embeds Necklace 4 iff ComplRelStr G embeds Necklace 4 )

proof end;

theorem Th25: :: NECKLA_3:25

for G being non empty irreflexive RelStr holds
( G is N-free iff ComplRelStr G is N-free )

proof end;

definition

let R be RelStr ;
mode path of R is RedSequence of the InternalRel of R;

end;

definition

let R be RelStr ;
attr R is path-connected means :Def1: :: NECKLA_3:def 1
for x, y being set st x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y holds
the InternalRel of R reduces y,x;

end;

:: deftheorem Def1 defines path-connected NECKLA_3:def 1 :

registration

cluster empty -> path-connected RelStr ;
correctness

proof end;

end;

registration

cluster non empty connected -> non empty path-connected RelStr ;
correctness

proof end;

end;

theorem Th26: :: NECKLA_3:26

for R being non empty reflexive transitive RelStr
for x, y being Element of R st the InternalRel of R reduces x,y holds
[x,y] in the InternalRel of R

proof end;

registration

cluster non empty reflexive transitive path-connected -> non empty reflexive transitive connected path-connected RelStr ;
correctness

proof end;

end;

theorem Th27: :: NECKLA_3:27

for R being symmetric RelStr
for x, y being set st x in the carrier of R & y in the carrier of R & the InternalRel of R reduces x,y holds
the InternalRel of R reduces y,x

proof end;

definition

let R be symmetric RelStr ;
redefine attr R is path-connected means :Def2: :: NECKLA_3:def 2
for x, y being set st x in the carrier of R & y in the carrier of R & x <> y holds
the InternalRel of R reduces x,y;
compatibility

proof end;

end;

:: deftheorem Def2 defines path-connected NECKLA_3:def 2 :

definition

let R be RelStr ;
let x be Element of R;
func component x -> Subset of R equals :: NECKLA_3:def 3
Class (EqCl the InternalRel of R),x;
coherence ;

end;

:: deftheorem defines component NECKLA_3:def 3 :

theorem Th28: :: NECKLA_3:28

for R being non empty RelStr
for x being Element of R holds x in component x by EQREL_1:28;

registration

let R be non empty RelStr ;
let x be Element of R;
cluster component x -> non empty ;
correctness by Th28;

end;

theorem Th29: :: NECKLA_3:29

for R being RelStr
for x being Element of R
for y being set st y in component x holds
[x,y] in EqCl the InternalRel of R

proof end;

theorem Th30: :: NECKLA_3:30

for R being RelStr
for x being Element of R
for A being set holds
( A = component x iff for y being set holds
( y in A iff [x,y] in EqCl the InternalRel of R ) )

proof end;

theorem Th31: :: NECKLA_3:31

for R being non empty symmetric irreflexive RelStr st not R is path-connected holds
ex G1, G2 being non empty strict symmetric irreflexive RelStr st
( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R,the InternalRel of R #) = union_of G1,G2 )

proof end;

theorem Th32: :: NECKLA_3:32

for R being non empty symmetric irreflexive RelStr st not ComplRelStr R is path-connected holds
ex G1, G2 being non empty strict symmetric irreflexive RelStr st
( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R,the InternalRel of R #) = sum_of G1,G2 )

proof end;

Lm1: for X being non empty finite set
for A, B being non empty set st X = A \/ B & A misses B holds
( Card A <` Card X & Card B <` Card X )

proof end;

theorem :: NECKLA_3:33

for G being irreflexive RelStr st G in fin_RelStr_sp holds
ComplRelStr G in fin_RelStr_sp

proof end;

theorem Th34: :: NECKLA_3:34

for R being symmetric irreflexive RelStr st Card the carrier of R = 2 & the carrier of R in FinSETS holds
RelStr(# the carrier of R,the InternalRel of R #) in fin_RelStr_sp

proof end;

theorem :: NECKLA_3:35

for R being RelStr st R in fin_RelStr_sp holds
R is symmetric

proof end;

theorem Th36: :: NECKLA_3:36

for G being RelStr
for H1, H2 being non empty RelStr
for x being Element of H1
for y being Element of H2 st G = union_of H1,H2 & the carrier of H1 misses the carrier of H2 holds
not [x,y] in the InternalRel of G

proof end;

theorem :: NECKLA_3:37

for G being RelStr
for H1, H2 being non empty RelStr
for x being Element of H1
for y being Element of H2 st G = sum_of H1,H2 holds
not [x,y] in the InternalRel of (ComplRelStr G)

proof end;

theorem Th38: :: NECKLA_3:38

for G being non empty symmetric RelStr
for x being Element of G
for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of R1,R2 & G is path-connected holds
ex b being Element of R1 st [b,x] in the InternalRel of G

proof end;

theorem Th39: :: NECKLA_3:39

for G being non empty symmetric irreflexive RelStr
for a, b, c, d being Element of G
for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_different & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds
subrelstr Z embeds Necklace 4

proof end;

theorem Th40: :: NECKLA_3:40

for G being non empty symmetric irreflexive RelStr
for x being Element of G
for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of R1,R2 & not G is trivial & G is path-connected & ComplRelStr G is path-connected holds
G embeds Necklace 4

proof end;

theorem :: NECKLA_3:41

for G being non empty strict symmetric irreflexive finite RelStr st G is N-free & the carrier of G in FinSETS holds
RelStr(# the carrier of G,the InternalRel of G #) in fin_RelStr_sp

proof end;