:: NECKLA_3 semantic presentation

theorem Th1: :: NECKLA_3:1
for b1, b2 being set holds (id b1) | b2 = (id b1) /\ [:b2,b2:]
proof end;

theorem Th2: :: NECKLA_3:2
for b1, b2, b3, b4 being set holds id {b1,b2,b3,b4} = {[b1,b1],[b2,b2],[b3,b3],[b4,b4]}
proof end;

theorem Th3: :: NECKLA_3:3
for b1, b2, b3, b4, b5, b6, b7, b8 being set holds [:{b1,b2,b3,b4},{b5,b6,b7,b8}:] = {[b1,b5],[b1,b6],[b2,b5],[b2,b6],[b1,b7],[b1,b8],[b2,b7],[b2,b8]} \/ {[b3,b5],[b3,b6],[b4,b5],[b4,b6],[b3,b7],[b3,b8],[b4,b7],[b4,b8]}
proof end;

registration
let c1, c2 be trivial set ;
cluster -> trivial Relation of a1,a2;
correctness
coherence
for b1 being Relation of c1,c2 holds b1 is trivial;
proof end;
end;

theorem Th4: :: NECKLA_3:4
for b1 being trivial set
for b2 being Relation of b1 st not b2 is empty holds
ex b3 being set st b2 = {[b3,b3]}
proof end;

registration
let c1 be trivial set ;
cluster -> reflexive symmetric strongly_connected transitive trivial Relation of a1,a1;
correctness
coherence
for b1 being Relation of c1 holds
( b1 is trivial & b1 is reflexive & b1 is symmetric & b1 is transitive & b1 is strongly_connected );
proof end;
end;

theorem Th5: :: NECKLA_3:5
for b1 being non empty trivial set
for b2 being Relation of b1 holds b2 is_symmetric_in b1
proof end;

registration
cluster non empty strict symmetric irreflexive finite RelStr ;
correctness
existence
ex b1 being RelStr st
( not b1 is empty & b1 is strict & b1 is finite & b1 is irreflexive & b1 is symmetric );
proof end;
end;

registration
let c1 be irreflexive RelStr ;
cluster full -> irreflexive full SubRelStr of a1;
correctness
coherence
for b1 being full SubRelStr of c1 holds b1 is irreflexive;
proof end;
end;

registration
let c1 be symmetric RelStr ;
cluster full -> symmetric full SubRelStr of a1;
correctness
coherence
for b1 being full SubRelStr of c1 holds b1 is symmetric;
proof end;
end;

theorem Th6: :: NECKLA_3:6
for b1 being symmetric irreflexive RelStr st Card the carrier of b1 = 2 holds
ex b2, b3 being set st
( the carrier of b1 = {b2,b3} & ( the InternalRel of b1 = {[b2,b3],[b3,b2]} or the InternalRel of b1 = {} ) )
proof end;

registration
let c1 be non empty RelStr ;
let c2 be RelStr ;
cluster union_of a1,a2 -> non empty ;
correctness
coherence
not union_of c1,c2 is empty;
proof end;
cluster sum_of a1,a2 -> non empty ;
correctness
coherence
not sum_of c1,c2 is empty;
proof end;
end;

registration
let c1 be RelStr ;
let c2 be non empty RelStr ;
cluster union_of a1,a2 -> non empty ;
correctness
coherence
not union_of c1,c2 is empty;
proof end;
cluster sum_of a1,a2 -> non empty ;
correctness
coherence
not sum_of c1,c2 is empty;
proof end;
end;

registration
let c1, c2 be finite RelStr ;
cluster union_of a1,a2 -> finite ;
correctness
coherence
union_of c1,c2 is finite;
proof end;
cluster sum_of a1,a2 -> finite ;
correctness
coherence
sum_of c1,c2 is finite;
proof end;
end;

registration
let c1, c2 be symmetric RelStr ;
cluster union_of a1,a2 -> symmetric ;
correctness
coherence
union_of c1,c2 is symmetric;
proof end;
cluster sum_of a1,a2 -> symmetric ;
correctness
coherence
sum_of c1,c2 is symmetric;
proof end;
end;

registration
let c1, c2 be irreflexive RelStr ;
cluster union_of a1,a2 -> irreflexive ;
correctness
coherence
union_of c1,c2 is irreflexive;
proof end;
end;

theorem Th7: :: NECKLA_3:7
for b1, b2 being irreflexive RelStr st the carrier of b1 misses the carrier of b2 holds
sum_of b1,b2 is irreflexive
proof end;

theorem Th8: :: NECKLA_3:8
for b1, b2 being RelStr holds
( union_of b1,b2 = union_of b2,b1 & sum_of b1,b2 = sum_of b2,b1 )
proof end;

theorem Th9: :: NECKLA_3:9
for b1 being irreflexive RelStr
for b2, b3 being RelStr st ( b1 = union_of b2,b3 or b1 = sum_of b2,b3 ) holds
( b2 is irreflexive & b3 is irreflexive )
proof end;

theorem Th10: :: NECKLA_3:10
for b1 being non empty RelStr
for b2, b3 being RelStr st the carrier of b2 misses the carrier of b3 & ( RelStr(# the carrier of b1,the InternalRel of b1 #) = union_of b2,b3 or RelStr(# the carrier of b1,the InternalRel of b1 #) = sum_of b2,b3 ) holds
( b2 is full SubRelStr of b1 & b3 is full SubRelStr of b1 )
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 c1 be RelStr ;
cluster ComplRelStr a1 -> irreflexive ;
correctness
coherence
ComplRelStr c1 is irreflexive;
proof end;
end;

registration
let c1 be symmetric RelStr ;
cluster ComplRelStr a1 -> symmetric irreflexive ;
correctness
coherence
ComplRelStr c1 is symmetric;
proof end;
end;

theorem Th12: :: NECKLA_3:12
for b1 being RelStr holds the InternalRel of b1 misses the InternalRel of (ComplRelStr b1)
proof end;

theorem Th13: :: NECKLA_3:13
for b1 being RelStr holds id the carrier of b1 misses the InternalRel of (ComplRelStr b1)
proof end;

theorem Th14: :: NECKLA_3:14
for b1 being RelStr holds [:the carrier of b1,the carrier of b1:] = ((id the carrier of b1) \/ the InternalRel of b1) \/ the InternalRel of (ComplRelStr b1)
proof end;

theorem Th15: :: NECKLA_3:15
for b1 being strict irreflexive RelStr st b1 is trivial holds
ComplRelStr b1 = b1
proof end;

theorem Th16: :: NECKLA_3:16
for b1 being strict irreflexive RelStr holds ComplRelStr (ComplRelStr b1) = b1
proof end;

theorem Th17: :: NECKLA_3:17
for b1, b2 being RelStr st the carrier of b1 misses the carrier of b2 holds
ComplRelStr (union_of b1,b2) = sum_of (ComplRelStr b1),(ComplRelStr b2)
proof end;

theorem Th18: :: NECKLA_3:18
for b1, b2 being RelStr st the carrier of b1 misses the carrier of b2 holds
ComplRelStr (sum_of b1,b2) = union_of (ComplRelStr b1),(ComplRelStr b2)
proof end;

theorem Th19: :: NECKLA_3:19
for b1 being RelStr
for b2 being full SubRelStr of b1 holds the InternalRel of (ComplRelStr b2) = the InternalRel of (ComplRelStr b1) |_2 the carrier of (ComplRelStr b2)
proof end;

theorem Th20: :: NECKLA_3:20
for b1 being non empty irreflexive RelStr
for b2 being Element of b1
for b3 being Element of (ComplRelStr b1) st b2 = b3 holds
ComplRelStr (subrelstr (([#] b1) \ {b2})) = subrelstr (([#] (ComplRelStr b1)) \ {b3})
proof end;

registration
cluster non empty strict trivial -> non empty N-free RelStr ;
correctness
coherence
for b1 being non empty RelStr st b1 is trivial & b1 is strict holds
b1 is N-free;
proof end;
end;

theorem Th21: :: NECKLA_3:21
for b1 being reflexive antisymmetric RelStr
for b2 being RelStr holds
( ex b3 being Function of b1,b2 st
for b4, b5 being Element of b1 holds
( [b4,b5] in the InternalRel of b1 iff [(b3 . b4),(b3 . b5)] in the InternalRel of b2 ) iff b2 embeds b1 )
proof end;

theorem Th22: :: NECKLA_3:22
for b1 being non empty RelStr
for b2 being non empty full SubRelStr of b1 holds b1 embeds b2
proof end;

theorem Th23: :: NECKLA_3:23
for b1 being non empty RelStr
for b2 being non empty full SubRelStr of b1 st b1 is N-free holds
b2 is N-free
proof end;

theorem Th24: :: NECKLA_3:24
for b1 being non empty irreflexive RelStr holds
( b1 embeds Necklace 4 iff ComplRelStr b1 embeds Necklace 4 )
proof end;

theorem Th25: :: NECKLA_3:25
for b1 being non empty irreflexive RelStr holds
( b1 is N-free iff ComplRelStr b1 is N-free )
proof end;

definition
let c1 be RelStr ;
mode path of a1 is RedSequence of the InternalRel of a1;
end;

definition
let c1 be RelStr ;
attr a1 is path-connected means :Def1: :: NECKLA_3:def 1
for b1, b2 being set st b1 in the carrier of a1 & b2 in the carrier of a1 & b1 <> b2 & not the InternalRel of a1 reduces b1,b2 holds
the InternalRel of a1 reduces b2,b1;
end;

:: deftheorem Def1 defines path-connected NECKLA_3:def 1 :
for b1 being RelStr holds
( b1 is path-connected iff for b2, b3 being set st b2 in the carrier of b1 & b3 in the carrier of b1 & b2 <> b3 & not the InternalRel of b1 reduces b2,b3 holds
the InternalRel of b1 reduces b3,b2 );

registration
cluster empty -> path-connected RelStr ;
correctness
coherence
for b1 being RelStr st b1 is empty holds
b1 is path-connected;
proof end;
end;

registration
cluster non empty connected -> non empty path-connected RelStr ;
correctness
coherence
for b1 being non empty RelStr st b1 is connected holds
b1 is path-connected;
proof end;
end;

theorem Th26: :: NECKLA_3:26
for b1 being non empty reflexive transitive RelStr
for b2, b3 being Element of b1 st the InternalRel of b1 reduces b2,b3 holds
[b2,b3] in the InternalRel of b1
proof end;

registration
cluster non empty reflexive transitive path-connected -> non empty reflexive transitive connected path-connected RelStr ;
correctness
coherence
for b1 being non empty reflexive transitive RelStr st b1 is path-connected holds
b1 is connected;
proof end;
end;

theorem Th27: :: NECKLA_3:27
for b1 being symmetric RelStr
for b2, b3 being set st b2 in the carrier of b1 & b3 in the carrier of b1 & the InternalRel of b1 reduces b2,b3 holds
the InternalRel of b1 reduces b3,b2
proof end;

definition
let c1 be symmetric RelStr ;
redefine attr a1 is path-connected means :Def2: :: NECKLA_3:def 2
for b1, b2 being set st b1 in the carrier of a1 & b2 in the carrier of a1 & b1 <> b2 holds
the InternalRel of a1 reduces b1,b2;
compatibility
( c1 is path-connected iff for b1, b2 being set st b1 in the carrier of c1 & b2 in the carrier of c1 & b1 <> b2 holds
the InternalRel of c1 reduces b1,b2 )
proof end;
end;

:: deftheorem Def2 defines path-connected NECKLA_3:def 2 :
for b1 being symmetric RelStr holds
( b1 is path-connected iff for b2, b3 being set st b2 in the carrier of b1 & b3 in the carrier of b1 & b2 <> b3 holds
the InternalRel of b1 reduces b2,b3 );

definition
let c1 be RelStr ;
let c2 be Element of c1;
func component c2 -> Subset of a1 equals :: NECKLA_3:def 3
 Class (EqCl the InternalRel of a1),a2;
coherence
Class (EqCl the InternalRel of c1),c2 is Subset of c1 ;
end;

:: deftheorem Def3 defines component NECKLA_3:def 3 :
for b1 being RelStr
for b2 being Element of b1 holds component b2 = Class (EqCl the InternalRel of b1),b2;

theorem Th28: :: NECKLA_3:28
for b1 being non empty RelStr
for b2 being Element of b1 holds b2 in component b2 by EQREL_1:28;

registration
let c1 be non empty RelStr ;
let c2 be Element of c1;
cluster component a2 -> non empty ;
correctness
coherence
not component c2 is empty;
by Th28;
end;

theorem Th29: :: NECKLA_3:29
for b1 being RelStr
for b2 being Element of b1
for b3 being set st b3 in component b2 holds
[b2,b3] in EqCl the InternalRel of b1
proof end;

theorem Th30: :: NECKLA_3:30
for b1 being RelStr
for b2 being Element of b1
for b3 being set holds
( b3 = component b2 iff for b4 being set holds
( b4 in b3 iff [b2,b4] in EqCl the InternalRel of b1 ) )
proof end;

theorem Th31: :: NECKLA_3:31
for b1 being non empty symmetric irreflexive RelStr st not b1 is path-connected holds
ex b2, b3 being non empty strict symmetric irreflexive RelStr st
( the carrier of b2 misses the carrier of b3 & RelStr(# the carrier of b1,the InternalRel of b1 #) = union_of b2,b3 )
proof end;

theorem Th32: :: NECKLA_3:32
for b1 being non empty symmetric irreflexive RelStr st not ComplRelStr b1 is path-connected holds
ex b2, b3 being non empty strict symmetric irreflexive RelStr st
( the carrier of b2 misses the carrier of b3 & RelStr(# the carrier of b1,the InternalRel of b1 #) = sum_of b2,b3 )
proof end;

Lemma31: for b1 being non empty finite set
for b2, b3 being non empty set st b1 = b2 \/ b3 & b2 misses b3 holds
( Card b2 <` Card b1 & Card b3 <` Card b1 )
proof end;

theorem Th33: :: NECKLA_3:33
for b1 being irreflexive RelStr st b1 in fin_RelStr_sp holds
ComplRelStr b1 in fin_RelStr_sp
proof end;

theorem Th34: :: NECKLA_3:34
for b1 being symmetric irreflexive RelStr st Card the carrier of b1 = 2 & the carrier of b1 in FinSETS holds
RelStr(# the carrier of b1,the InternalRel of b1 #) in fin_RelStr_sp
proof end;

theorem Th35: :: NECKLA_3:35
for b1 being RelStr st b1 in fin_RelStr_sp holds
b1 is symmetric
proof end;

theorem Th36: :: NECKLA_3:36
for b1 being RelStr
for b2, b3 being non empty RelStr
for b4 being Element of b2
for b5 being Element of b3 st b1 = union_of b2,b3 & the carrier of b2 misses the carrier of b3 holds
not [b4,b5] in the InternalRel of b1
proof end;

theorem Th37: :: NECKLA_3:37
for b1 being RelStr
for b2, b3 being non empty RelStr
for b4 being Element of b2
for b5 being Element of b3 st b1 = sum_of b2,b3 holds
not [b4,b5] in the InternalRel of (ComplRelStr b1)
proof end;

theorem Th38: :: NECKLA_3:38
for b1 being non empty symmetric RelStr
for b2 being Element of b1
for b3, b4 being non empty RelStr st the carrier of b3 misses the carrier of b4 & subrelstr (([#] b1) \ {b2}) = union_of b3,b4 & b1 is path-connected holds
ex b5 being Element of b3 st [b5,b2] in the InternalRel of b1
proof end;

theorem Th39: :: NECKLA_3:39
for b1 being non empty symmetric irreflexive RelStr
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1 st b6 = {b2,b3,b4,b5} & b2,b3,b4,b5 are_mutually_different & [b2,b3] in the InternalRel of b1 & [b3,b4] in the InternalRel of b1 & [b4,b5] in the InternalRel of b1 & not [b2,b4] in the InternalRel of b1 & not [b2,b5] in the InternalRel of b1 & not [b3,b5] in the InternalRel of b1 holds
subrelstr b6 embeds Necklace 4
proof end;

theorem Th40: :: NECKLA_3:40
for b1 being non empty symmetric irreflexive RelStr
for b2 being Element of b1
for b3, b4 being non empty RelStr st the carrier of b3 misses the carrier of b4 & subrelstr (([#] b1) \ {b2}) = union_of b3,b4 & not b1 is trivial & b1 is path-connected & ComplRelStr b1 is path-connected holds
b1 embeds Necklace 4
proof end;

theorem Th41: :: NECKLA_3:41
for b1 being non empty strict symmetric irreflexive finite RelStr st b1 is N-free & the carrier of b1 in FinSETS holds
RelStr(# the carrier of b1,the InternalRel of b1 #) in fin_RelStr_sp
proof end;