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

begin

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 Element of bool [:X,Y:];
correctness
coherence
for b₁ being Relation of X,Y holds b₁ is trivial ;

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 -> trivial reflexive symmetric strongly_connected transitive Element of bool [:X,X:];
correctness
coherence
for b₁ being Relation of X holds
( b₁ is trivial & b₁ is reflexive & b₁ is symmetric & b₁ is transitive & b₁ is strongly_connected );

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 finite strict symmetric irreflexive RelStr ;
correctness
existence
ex b₁ being RelStr st
( not b₁ is empty & b₁ is strict & b₁ is finite & b₁ is irreflexive & b₁ is symmetric );

proof end;

end;

registration

let L be irreflexive RelStr ;
cluster full -> full irreflexive SubRelStr of L;
correctness
coherence
for b₁ being full SubRelStr of L holds b₁ is irreflexive ;

proof end;

end;

registration

let L be symmetric RelStr ;
cluster full -> full symmetric SubRelStr of L;
correctness
coherence
for b₁ being full SubRelStr of L holds b₁ 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 set st
( the carrier of R = {a,b} & ( the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {} ) )

proof end;

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 ;

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;

begin

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
coherence
ComplRelStr R is irreflexive ;

proof end;

end;

registration

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

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 x9 being Element of (ComplRelStr G) st x = x9 holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9})

proof end;

begin

registration

cluster non empty trivial strict -> non empty N-free RelStr ;
correctness
coherence
for b₁ being non empty RelStr st b₁ is trivial & b₁ is strict holds
b₁ 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;

begin

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 :
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

cluster empty -> path-connected RelStr ;
correctness
coherence
for b₁ being RelStr st b₁ is empty holds
b₁ is path-connected ;

proof end;

end;

registration

cluster non empty connected -> non empty path-connected RelStr ;
correctness
coherence
for b₁ being non empty RelStr st b₁ is connected holds
b₁ 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

cluster non empty reflexive transitive path-connected -> non empty reflexive transitive connected RelStr ;
correctness
coherence
for b₁ being non empty reflexive transitive RelStr st b₁ is path-connected holds
b₁ 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 :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
( 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 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 & 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:28;

end;

theorem :: NECKLA_3:28

canceled;

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