:: The Class of Series-Parallel Graphs, {I}
:: by Krzysztof Retel
::
:: Received November 18, 2002
:: Copyright (c) 2002-2021 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, NAT_1, CARD_1, ZFMISC_1, XBOOLE_0, SUBSET_1, ARYTM_3,
FUNCT_3, FUNCT_1, RELAT_1, FUNCT_2, FUNCT_4, TARSKI, FUNCOP_1, ORDERS_2,
STRUCT_0, RELAT_2, XXREAL_0, ARYTM_1, WELLORD1, CAT_1, SEQM_3, FINSET_1,
ORDINAL1, CARD_2, SQUARE_1, NECKLACE, XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, CARD_2, WELLORD1,
FINSET_1, SQUARE_1, QUIN_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, REAL_1,
NAT_1, NAT_D, RELAT_1, RELAT_2, FUNCT_3, FUNCOP_1, RELSET_1, FUNCT_1,
PARTFUN1, FUNCT_2, FUNCT_4, BINOP_1, XXREAL_0, STRUCT_0, ORDERS_2,
WAYBEL_0, WAYBEL_1, ORDERS_3;
constructors WELLORD1, REAL_1, SQUARE_1, NAT_1, QUIN_1, CARD_2, REALSET1,
ORDERS_3, WAYBEL_1, NAT_D, RELSET_1, FUNCT_4;
registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1,
FUNCT_4, FINSET_1, XREAL_0, SQUARE_1, STRUCT_0, ORDERS_2, HILBERT3,
CARD_1, RELAT_1, QUIN_1, NAT_1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin :: Preliminaries
reserve i,j,k,n for Nat;
reserve x,x1,x2,x3,y1,y2,y3 for set;
theorem :: NECKLACE:1
4 = {0,1,2,3};
theorem :: NECKLACE:2
[:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[
x2,y3],[x3,y1],[x3,y2],[x3,y3]};
::$CT
theorem :: NECKLACE:4
for x be non zero Nat holds 0 in x;
registration
let X be set;
cluster delta X -> one-to-one;
end;
theorem :: NECKLACE:5
for X being set holds card id X = card X;
registration
cluster trivial -> one-to-one for Function;
end;
theorem :: NECKLACE:6
for f,g be Function st dom f misses dom g holds rng(f +* g) = rng f \/
rng g;
theorem :: NECKLACE:7
for f,g be one-to-one Function st dom f misses dom g & rng f
misses rng g holds (f+*g)" = f" +* g";
theorem :: NECKLACE:8
for A,a,b being set holds (A --> a) +* (A --> b) = A --> b;
theorem :: NECKLACE:9
for a,b being set holds (a .--> b)" = b .--> a;
theorem :: NECKLACE:10
for a,b,c,d being set st a = b iff c = d holds (a,b) --> (c,d)"
= (c,d) --> (a,b);
scheme :: NECKLACE:sch 1
Convers{X()-> non empty set, R() -> Relation, F,G(set)-> set, P[set]}: R()~
={[F(x),G(x)] where x is Element of X(): P[x]}
provided
R() = {[G(x),F(x)] where x is Element of X(): P[x]};
theorem :: NECKLACE:11
for i,j,n be Nat holds i < j & j in Segm n implies i in Segm n;
begin :: Auxiliary Concepts
definition
let R,S be RelStr;
pred S embeds R means
:: NECKLACE:def 1
ex f being Function of R,S st f is one-to-one &
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;
end;
definition
let R,S be non empty RelStr;
redefine pred S embeds R;
reflexivity;
end;
theorem :: NECKLACE:12
for R,S,T be non empty RelStr holds R embeds S & S embeds T
implies R embeds T;
definition
let R,S be non empty RelStr;
pred R is_equimorphic_to S means
:: NECKLACE:def 2
R embeds S & S embeds R;
reflexivity;
symmetry;
end;
theorem :: NECKLACE:13
for R,S,T be non empty RelStr holds R is_equimorphic_to S & S
is_equimorphic_to T implies R is_equimorphic_to T;
notation
let R be non empty RelStr;
antonym R is parallel for R is connected;
end;
definition
let R be RelStr;
attr R is symmetric means
:: NECKLACE:def 3
the InternalRel of R is_symmetric_in the carrier of R;
end;
definition
let R be RelStr;
attr R is asymmetric means
:: NECKLACE:def 4
the InternalRel of R is asymmetric;
end;
theorem :: NECKLACE:14
for R be RelStr st R is asymmetric holds the InternalRel of R misses (
the InternalRel of R)~;
definition
let R be RelStr;
attr R is irreflexive means
:: NECKLACE:def 5
for x being set st x in the carrier of R holds
not [x,x] in the InternalRel of R;
end;
definition
let n be Nat;
func n-SuccRelStr -> strict RelStr means
:: NECKLACE:def 6
the carrier of it = n & the
InternalRel of it = {[i,i+1] where i is Element of NAT:i+1 < n};
end;
theorem :: NECKLACE:15
for n be Nat holds n-SuccRelStr is asymmetric;
theorem :: NECKLACE:16
n > 0 implies card the InternalRel of n-SuccRelStr = n-1;
definition
let R be RelStr;
func SymRelStr R -> strict RelStr means
:: NECKLACE:def 7
the carrier of it = the
carrier of R & the InternalRel of it = (the InternalRel of R) \/ (the
InternalRel of R)~;
end;
registration
let R be RelStr;
cluster SymRelStr R -> symmetric;
end;
registration
cluster non empty symmetric for RelStr;
end;
registration
let R be symmetric RelStr;
cluster the InternalRel of R -> symmetric;
end;
definition
let R be RelStr;
func ComplRelStr R -> strict RelStr means
:: NECKLACE:def 8
the carrier of it = the carrier of R &
the InternalRel of it = (the InternalRel of R)` \ id (the carrier of R);
end;
registration
let R be non empty RelStr;
cluster ComplRelStr R -> non empty;
end;
theorem :: NECKLACE:17
for S,R being RelStr holds S,R are_isomorphic implies card the
InternalRel of S = card the InternalRel of R;
begin :: Necklace n
definition
let n be Nat;
func Necklace n -> strict RelStr equals
:: NECKLACE:def 9
SymRelStr(n-SuccRelStr);
end;
registration
let n be Nat;
cluster Necklace n -> symmetric;
end;
theorem :: NECKLACE:18
the InternalRel of Necklace n = {[i,i+1] where i is Element of
NAT:i+1 < n} \/ {[i+1,i] where i is Element of NAT:i+1 < n};
theorem :: NECKLACE:19
for x be set holds x in the InternalRel of Necklace n iff ex i
being Element of NAT st i+1 < n & (x = [i,i+1] or x = [i+1,i]);
registration
let n be Nat;
cluster Necklace n -> irreflexive;
end;
theorem :: NECKLACE:20
for n be Nat holds the carrier of Necklace n = n;
registration
let n be non zero Nat;
cluster Necklace n -> non empty;
end;
registration
let n be Nat;
cluster the carrier of Necklace n -> finite;
end;
theorem :: NECKLACE:21
for n,i be Nat st i+1 < n holds [i,i+1] in the InternalRel of Necklace n;
theorem :: NECKLACE:22
for n be Nat, i being Nat st i in the carrier of Necklace n holds i < n;
theorem :: NECKLACE:23
for n be non zero Nat holds Necklace n is connected;
theorem :: NECKLACE:24
for i,j being Nat st [i,j] in the InternalRel of Necklace n
holds i = j + 1 or j = i + 1;
theorem :: NECKLACE:25
for i,j being Nat st (i = j + 1 or j = i + 1) & i in the carrier
of Necklace n & j in the carrier of Necklace n holds [i,j] in the InternalRel
of Necklace n;
theorem :: NECKLACE:26
n > 0 implies card ({[i+1,i] where i is Element of NAT:i+1 < n}) = n-1;
theorem :: NECKLACE:27
n > 0 implies card the InternalRel of Necklace n = 2*(n-1);
theorem :: NECKLACE:28
Necklace 1, ComplRelStr Necklace 1 are_isomorphic;
theorem :: NECKLACE:29
Necklace 4, ComplRelStr Necklace 4 are_isomorphic;
theorem :: NECKLACE:30
Necklace n, ComplRelStr Necklace n are_isomorphic implies n = 0 or n =
1 or n = 4;