:: The Class of Series-Parallel Graphs, {III}
:: by Krzysztof Retel
::
:: Received February 3, 2004
:: Copyright (c) 2004-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, RELAT_2, STRUCT_0,
FINSET_1, ORDERS_2, CARD_1, CAT_1, YELLOW_0, WELLORD1, NECKLA_2,
NECKLACE, SUBSET_1, FUNCT_1, XXREAL_0, SEQM_3, REWRITE1, FINSEQ_1, NAT_1,
ARYTM_3, FINSEQ_5, EQREL_1, MSUALG_5, CLASSES2, FUNCOP_1, FUNCT_4,
ARYTM_1, NECKLA_3, XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2,
RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, XXREAL_0, DOMAIN_1, STRUCT_0, ORDERS_2, WAYBEL_1,
FUNCOP_1, CLASSES2, NECKLACE, WAYBEL_0, FUNCT_4, REWRITE1, FINSEQ_1,
FINSEQ_5, EQREL_1, MSUALG_5, YELLOW_0, NECKLA_2, WELLORD1;
constructors NAT_1, EQREL_1, CLASSES1, TOLER_1, CLASSES2, FINSEQ_5, REWRITE1,
REALSET2, MSUALG_5, ORDERS_3, WAYBEL_1, NECKLACE, NECKLA_2, RELSET_1,
FUNCT_4;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, CARD_1, FINSEQ_1, STRUCT_0,
ORDERS_2, YELLOW_0, NECKLACE, NECKLA_2, ORDINAL1, FUNCT_4, RELSET_1,
ZFMISC_1;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
begin :: Preliminaries
reserve A,B,a,b,c,d,e,f,g,h for set;
theorem :: NECKLA_3:1
(id A)|B = id A /\ [:B,B:];
theorem :: NECKLA_3:2
id {a,b,c,d} = {[a,a],[b,b],[c,c],[d,d]};
theorem :: NECKLA_3:3
[:{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]};
registration
let X,Y be trivial set;
cluster -> trivial for Relation of X,Y;
end;
theorem :: NECKLA_3:4
for X be trivial set, R be Relation of X st R is non empty holds
ex x be object st R = {[x,x]};
registration
let X be trivial set;
cluster -> trivial reflexive symmetric transitive strongly_connected
for Relation of X;
end;
theorem :: NECKLA_3:5
for X be 1-element set, R be Relation of X holds R is_symmetric_in X;
registration
cluster non empty strict finite irreflexive symmetric for RelStr;
end;
registration
let L be irreflexive RelStr;
cluster -> irreflexive for full SubRelStr of L;
end;
registration
let L be symmetric RelStr;
cluster -> symmetric for full SubRelStr of L;
end;
theorem :: NECKLA_3:6
for R be irreflexive symmetric RelStr st card (the carrier of R) = 2
ex a,b be object st the carrier of R = {a,b} & (the InternalRel of R = {
[a,b],[b,a]} or the InternalRel of R = {});
begin :: Some facts about operations 'union_of' and 'sum_of'
registration
let R be non empty RelStr,S be RelStr;
cluster union_of(R,S) -> non empty;
cluster sum_of(R,S) -> non empty;
end;
registration
let R be RelStr, S be non empty RelStr;
cluster union_of(R,S) -> non empty;
cluster sum_of(R,S) -> non empty;
end;
registration
let R,S be finite RelStr;
cluster union_of(R,S) -> finite;
cluster sum_of(R,S) -> finite;
end;
registration
let R,S be symmetric RelStr;
cluster union_of(R,S) -> symmetric;
cluster sum_of(R,S) -> symmetric;
end;
registration
let R,S be irreflexive RelStr;
cluster union_of(R,S) -> irreflexive;
end;
theorem :: NECKLA_3:7
for R,S be irreflexive RelStr st the carrier of R misses the carrier
of S holds sum_of(R,S) is irreflexive;
theorem :: 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);
theorem :: NECKLA_3:9
for G being irreflexive RelStr, G1,G2 being RelStr st ( G =
union_of(G1,G2) or G = sum_of(G1,G2) ) holds G1 is irreflexive & G2 is
irreflexive;
theorem :: NECKLA_3:10
for G being non empty RelStr, H1,H2 being RelStr st the carrier
of H1 misses the carrier of H2 & ( the RelStr of G = union_of(H1,H2) or the
RelStr of G = sum_of(H1,H2) ) holds H1 is full SubRelStr of G & H2 is full
SubRelStr of G;
begin :: Theorems relating to the complement of RelStr
theorem :: NECKLA_3:11
the InternalRel of ComplRelStr Necklace 4 = {[0,2],[2,0],[0,3],[
3,0],[1,3],[3,1]};
registration
let R be RelStr;
cluster ComplRelStr R -> irreflexive;
end;
registration
let R be symmetric RelStr;
cluster ComplRelStr R -> symmetric;
end;
theorem :: NECKLA_3:12
for R be RelStr holds the InternalRel of R misses the
InternalRel of ComplRelStr R;
theorem :: NECKLA_3:13
for R being RelStr holds id the carrier of R misses the
InternalRel of ComplRelStr R;
theorem :: 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);
theorem :: NECKLA_3:15
for G being strict irreflexive RelStr st G is trivial holds ComplRelStr G = G
;
theorem :: NECKLA_3:16
for G being strict irreflexive RelStr holds ComplRelStr ( ComplRelStr G) = G;
theorem :: 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
);
theorem :: 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
);
theorem :: NECKLA_3:19
for G being RelStr, H being full SubRelStr of G holds the InternalRel
of ComplRelStr H = (the InternalRel of ComplRelStr G)|_2 the carrier of
ComplRelStr H;
theorem :: NECKLA_3:20
for G being non empty irreflexive RelStr, x being Element of G,
x9 being Element of ComplRelStr G st x = x9 holds ComplRelStr (subrelstr ([#]G
\ {x})) = subrelstr ([#](ComplRelStr G) \ {x9});
begin :: Another facts relating to operation 'embeds'
registration
cluster trivial strict -> N-free for non empty RelStr;
end;
theorem :: NECKLA_3:21
for R being reflexive antisymmetric RelStr, 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;
theorem :: NECKLA_3:22
for G being non empty RelStr, H being non empty full SubRelStr
of G holds G embeds H;
theorem :: NECKLA_3:23
for G being non empty RelStr, H being non empty full SubRelStr
of G st G is N-free holds H is N-free;
theorem :: NECKLA_3:24
for G being non empty irreflexive RelStr holds G embeds Necklace
4 iff ComplRelStr G embeds Necklace 4;
theorem :: NECKLA_3:25
for G being non empty irreflexive RelStr holds G is N-free iff
ComplRelStr G is N-free;
begin :: Connected Graphs
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 holds the InternalRel of R reduces x,y or
the InternalRel of R reduces y,x;
end;
registration
cluster empty -> path-connected for RelStr;
end;
registration
cluster connected -> path-connected for non empty RelStr;
end;
theorem :: NECKLA_3:26
for R being non empty transitive reflexive RelStr, x,y being
Element of R holds the InternalRel of R reduces x,y implies [x,y] in the
InternalRel of R;
registration
cluster path-connected -> connected for
non empty transitive reflexive RelStr;
end;
theorem :: NECKLA_3:27
for R be symmetric RelStr,x,y being set holds the InternalRel of
R reduces x,y implies the InternalRel of R reduces y,x;
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;
end;
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);
end;
registration
let R be non empty RelStr;
let x be Element of R;
cluster component x -> non empty;
end;
theorem :: NECKLA_3:28
for R being RelStr, x being Element of R, y be set st y in
component x holds [x,y] in EqCl the InternalRel of R;
theorem :: NECKLA_3:29
for R being RelStr, x being Element of R, 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;
theorem :: NECKLA_3:30
for R be non empty irreflexive symmetric RelStr holds R is not
path-connected implies ex G1,G2 being non empty strict irreflexive symmetric
RelStr st the carrier of G1 misses the carrier of G2 & the RelStr of R =
union_of(G1,G2);
theorem :: NECKLA_3:31
for R be non empty irreflexive symmetric RelStr holds
ComplRelStr R is not path-connected implies ex G1,G2 being non empty strict
irreflexive symmetric RelStr st the carrier of G1 misses the carrier of G2 &
the RelStr of R = sum_of(G1,G2);
theorem :: NECKLA_3:32
for G being irreflexive RelStr st G in fin_RelStr_sp holds ComplRelStr
G in fin_RelStr_sp;
theorem :: NECKLA_3:33
for R be irreflexive symmetric RelStr st card (the carrier of R)
= 2 & the carrier of R in FinSETS holds the RelStr of R in fin_RelStr_sp;
theorem :: NECKLA_3:34
for R be RelStr st R in fin_RelStr_sp holds R is symmetric;
theorem :: NECKLA_3:35
for G being RelStr, H1,H2 being non empty RelStr, x being
Element of H1, 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;
theorem :: NECKLA_3:36
for G being RelStr, H1,H2 being non empty RelStr, x being Element of
H1, y being Element of H2 st G = sum_of(H1,H2) holds not [x,y] in the
InternalRel of ComplRelStr G;
theorem :: NECKLA_3:37
for G being non empty symmetric RelStr, x being Element of G, 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;
theorem :: NECKLA_3:38
for G being non empty symmetric irreflexive RelStr, a,b,c,d
being Element of G, 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;
theorem :: NECKLA_3:39
for G being non empty irreflexive symmetric RelStr, x being
Element of G, 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 non trivial & G
is path-connected & ComplRelStr G is path-connected holds G embeds Necklace 4
;
theorem :: NECKLA_3:40
for G being non empty strict finite irreflexive symmetric RelStr st G
is N-free & the carrier of G in FinSETS holds the RelStr of G in fin_RelStr_sp;