:: The Class of Series-Parallel Graphs, {III}
:: by Krzysztof Retel
::
:: Copyright (c) 2004-2021 Association of Mizar Users

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 for Element of bool [:X,Y:];
correctness
coherence
for b1 being Relation of X,Y holds b1 is trivial
;
;
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 object st R = {[x,x]}
proof end;

registration
let X be trivial set ;
correctness
coherence
for b1 being Relation of X 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 X being 1 -element set
for R being Relation of X holds R is_symmetric_in X
proof end;

registration
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 L be irreflexive RelStr ;
cluster full -> full irreflexive for SubRelStr of L;
correctness
coherence
for b1 being full SubRelStr of L holds b1 is irreflexive
;
proof end;
end;

registration
let L be symmetric RelStr ;
cluster full -> full symmetric for SubRelStr of L;
correctness
coherence
for b1 being full SubRelStr of L holds b1 is symmetric
;
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 object 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
coherence
not union_of (R,S) is empty
;
proof end;
cluster sum_of (R,S) -> non empty ;
correctness
coherence
not sum_of (R,S) is empty
;
proof end;
end;

registration
let R be RelStr ;
let S be non empty RelStr ;
cluster union_of (R,S) -> non empty ;
correctness
coherence
not union_of (R,S) is empty
;
proof end;
cluster sum_of (R,S) -> non empty ;
correctness
coherence
not sum_of (R,S) is empty
;
proof end;
end;

registration
let R, S be finite RelStr ;
cluster union_of (R,S) -> finite ;
correctness
coherence
union_of (R,S) is finite
;
proof end;
cluster sum_of (R,S) -> finite ;
correctness
coherence
sum_of (R,S) is finite
;
proof end;
end;

registration
let R, S be symmetric RelStr ;
cluster union_of (R,S) -> symmetric ;
correctness
coherence
union_of (R,S) is symmetric
;
proof end;
cluster sum_of (R,S) -> symmetric ;
correctness
coherence
sum_of (R,S) is symmetric
;
proof end;
end;

registration
let R, S be irreflexive RelStr ;
cluster union_of (R,S) -> irreflexive ;
correctness
coherence
union_of (R,S) is irreflexive
;
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 () = {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}
proof end;

registration
let R be RelStr ;
correctness
coherence ;
proof end;
end;

registration
let R be symmetric RelStr ;
correctness
coherence ;
proof end;
end;

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

theorem Th13: :: NECKLA_3:13
for R being RelStr holds id the carrier of R misses the InternalRel of ()
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 ()
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 () = 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 ((),())
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 ((),())
proof end;

theorem :: NECKLA_3:19
for G being RelStr
for H being full SubRelStr of G holds the InternalRel of () = the InternalRel of () |_2 the carrier of ()
proof end;

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

registration
cluster non empty trivial strict -> non empty N-free for 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 :: 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 :: 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 defines path-connected NECKLA_3:def 1 :
for R being RelStr holds
( R is path-connected iff 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 );

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

registration
cluster non empty connected -> non empty path-connected for 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 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
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 R being symmetric RelStr
for x, y being set st 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 :: 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
( R is path-connected iff 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 )
proof end;
end;

:: deftheorem defines path-connected NECKLA_3:def 2 :
for R being symmetric RelStr holds
( R is path-connected iff 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 );

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
Class ((EqCl the InternalRel of R),x) is Subset of R
;
end;

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

registration
let R be non empty RelStr ;
let x be Element of R;
cluster component x -> non empty ;
correctness
coherence
not component x is empty
;
by EQREL_1:20;
end;

theorem Th28: :: NECKLA_3:28
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 Th29: :: NECKLA_3:29
for R being RelStr
for x being Element of R
for A being set holds
( A = component x iff for y being object holds
( y in A iff [x,y] in EqCl the InternalRel of R ) )
proof end;

theorem Th30: :: NECKLA_3:30
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 Th31: :: NECKLA_3:31
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 in Segm (card X)

proof end;

theorem :: NECKLA_3:32
for G being irreflexive RelStr st G in fin_RelStr_sp holds
ComplRelStr G in fin_RelStr_sp
proof end;

theorem Th33: :: NECKLA_3:33
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:34
for R being RelStr st R in fin_RelStr_sp holds
R is symmetric
proof end;

theorem Th35: :: NECKLA_3:35
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: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 = sum_of (H1,H2) holds
not [x,y] in the InternalRel of ()
proof end;

theorem Th37: :: NECKLA_3:37
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 Th38: :: NECKLA_3:38
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_distinct & [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 Th39: :: NECKLA_3:39
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:40
for G being non empty finite strict symmetric irreflexive 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;