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


begin

theorem Th1: :: NECKLA_3:1
for A, B being set holds (id A) | B = (id A) /\ [:B,B:]
proofend;

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]}
proofend;

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]}
proofend;

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 ;
proofend;
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]}
proofend;

registration
let X be trivial set ;
cluster  ->  trivial reflexive symmetric strongly_connected transitive for Element of bool [:X,X:];
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 );
proofend;
end;

theorem Th5: :: NECKLA_3:5
for X being 1 -element set
for R being Relation of X holds R is_symmetric_in X
proofend;

registration
cluster non empty finite strict symmetric irreflexive for RelStr ;
correctness
existence
ex b1 being RelStr st
( not b1 is empty & b1 is strict & b1 is finite & b1 is irreflexive & b1 is symmetric );
proofend;
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 ;
proofend;
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 ;
proofend;
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 = {} ) )
proofend;

begin

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 ;
proofend;
cluster sum_of (R,S) ->  non empty ;
correctness
coherence
not sum_of (R,S) is empty ;
proofend;
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 ;
proofend;
cluster sum_of (R,S) ->  non empty ;
correctness
coherence
not sum_of (R,S) is empty ;
proofend;
end;

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

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

registration
let R, S be irreflexive RelStr ;
cluster union_of (R,S) ->  irreflexive ;
correctness
coherence
union_of (R,S) is irreflexive ;
proofend;
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
proofend;

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) )
proofend;

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 )
proofend;

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 )
proofend;

begin

theorem Th11: :: NECKLA_3:11
the InternalRel of (ComplRelStr (Necklace 4)) = {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}
proofend;

registration
let R be RelStr ;
cluster ComplRelStr R ->  irreflexive ;
correctness
coherence
ComplRelStr R is irreflexive ;
proofend;
end;

registration
let R be symmetric RelStr ;
cluster ComplRelStr R ->  symmetric ;
correctness
coherence
ComplRelStr R is symmetric ;
proofend;
end;

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

theorem Th13: :: NECKLA_3:13
for R being RelStr holds id the carrier of R misses the InternalRel of (ComplRelStr R)
proofend;

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)
proofend;

theorem Th15: :: NECKLA_3:15
for G being strict irreflexive RelStr st G is trivial holds
ComplRelStr G = G
proofend;

theorem Th16: :: NECKLA_3:16
for G being strict irreflexive RelStr holds ComplRelStr (ComplRelStr G) = G
proofend;

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))
proofend;

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))
proofend;

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)
proofend;

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

begin

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 ;
proofend;
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 )
proofend;

theorem Th22: :: NECKLA_3:22
for G being non empty RelStr
for H being non empty full SubRelStr of G holds G embeds H
proofend;

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
proofend;

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

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

begin

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

definition
let R be RelStr ;
attrR is path-connected  means :Def1: :: NECKLA_3:def 1
 for x, y being set st x in the carrier of R &amp; y in the carrier of R &amp; x <> y &amp; 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_:_
 for R being RelStr holds
( R is path-connected iff for x, y being set st x in the carrier of R &amp; y in the carrier of R &amp; x <> y &amp; not the InternalRel of R reduces x,y holds
the InternalRel of R reduces y,x );

registration
cluster empty  ->  path-connected for RelStr ;
correctness
coherence
for b1 being RelStr st b1 is empty holds
b1 is path-connected ;
proofend;
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 ;
proofend;
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
proofend;

registration
cluster non empty reflexive transitive path-connected  ->  non empty reflexive transitive connected for RelStr ;
correctness
coherence
for b1 being non empty reflexive transitive RelStr st b1 is path-connected holds
b1 is connected ;
proofend;
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
proofend;

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 &amp; y in the carrier of R &amp; 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 &amp; y in the carrier of R &amp; x <> y holds
the InternalRel of R reduces x,y )
proofend;
end;

:: deftheorem Def2 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 &amp; y in the carrier of R &amp; 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
proofend;

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 set holds
( y in A iff [x,y] in EqCl the InternalRel of R ) )
proofend;

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 &amp; RelStr(# the carrier of R, the InternalRel of R #) = union_of (G1,G2) )
proofend;

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 &amp; RelStr(# the carrier of R, the InternalRel of R #) = sum_of (G1,G2) )
proofend;

Lm1:  for X being non empty finite set
for A, B being non empty set st X = A \/ B &amp; A misses B holds
card A in card X
proofend;

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

theorem Th33: :: NECKLA_3:33
for R being symmetric irreflexive RelStr st card the carrier of R = 2 &amp; the carrier of R in FinSETS holds
RelStr(# the carrier of R, the InternalRel of R #) in fin_RelStr_sp
proofend;

theorem :: NECKLA_3:34
for R being RelStr st R in fin_RelStr_sp holds
R is symmetric
proofend;

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) &amp; the carrier of H1 misses the carrier of H2 holds
not [x,y] in the InternalRel of G
proofend;

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 (ComplRelStr G)
proofend;

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 &amp; subrelstr (([#] G) \ {x}) = union_of (R1,R2) &amp; G is path-connected holds
ex b being Element of R1 st [b,x] in the InternalRel of G
proofend;

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} &amp; a,b,c,d are_mutually_different &amp; [a,b] in the InternalRel of G &amp; [b,c] in the InternalRel of G &amp; [c,d] in the InternalRel of G &amp; not [a,c] in the InternalRel of G &amp; not [a,d] in the InternalRel of G &amp; not [b,d] in the InternalRel of G holds
subrelstr Z embeds Necklace 4
proofend;

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 &amp; subrelstr (([#] G) \ {x}) = union_of (R1,R2) &amp; not G is trivial &amp; G is path-connected &amp; ComplRelStr G is path-connected holds
G embeds Necklace 4
proofend;

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