The Class of Series – Parallel Graphs. Part I
JOURNAL OF FORMALIZED MATHEMATICS
V olume14,Released2002,Published2003
Inst.of Computer Science,Univ.of Bia?ystok
The Class of Series–Parallel Graphs.Part I
Krzysztof Retel
University of Bia?ystok
Summary.The paper introduces some preliminary notions concerning the graph the-ory according to[18].We de?ne Necklace n as a graph with vertex{1,2,3,...,n}and edge
set{(1,2),(2,3),...,(n?1,n)}.The goal of the article is to prove that Necklace n and Com-
plement of Necklace n are isomorphic for n=0,1,4.
MML Identi?er:NECKLACE.
WWW:https://www.wendangku.net/doc/a86171252.html,/JFM/Vol14/necklace.html
The articles[21],[20],[24],[11],[1],[15],[6],[3],[22],[2],[23],[25],[27],[17],[7],[12],[19], [26],[8],[10],[9],[13],[4],[5],[14],and[16]provide the notation and terminology for this paper.
1.P RELIMINARIES
We follow the rules:n denotes a natural number and x1,x2,x3,x4,x5,y1,y2,y3denote sets.
Let x1,x2,x3,x4,x5be sets.We say that x1,x2,x3,x4,x5are mutually different if and only if: (Def.1)x1=x2and x1=x3and x1=x4and x1=x5and x2=x3and x2=x4and x2=x5and x3=x4 and x3=x5and x4=x5.
We now state several propositions:
(1)If x1,x2,x3,x4,x5are mutually different,then card{x1,x2,x3,x4,x5}=5.
(2)4={0,1,2,3}.
(3)[:{x1,x2,x3},{y1,y2,y3}:]={ x1,y1 , x1,y2 , x1,y3 , x2,y1 , x2,y2 , x2,y3 , x3,y1 , x3,
y2 , x3,y3 }.
(4)For every set x and for every natural number n such that x∈n holds x is a natural number.
(5)For every non empty natural number x holds0∈x.
Let us observe that every set which is natural is also cardinal.
Let X be a set.Observe thatδX is one-to-one.
One can prove the following proposition
(6)For every set X holds id X=X.
Let R be a trivial binary relation.One can check that dom R is trivial.
Let us observe that every function which is trivial is also one-to-one.
One can prove the following propositions:
(7)For all functions f,g such that dom f misses dom g holds rng(f+·g)=rng f∪rng g.
1c Association of Mizar Users
(8)For all one-to-one functions f ,g such that dom f misses dom g and rng f misses rng g holds (f +·g )?1=f ?1+·g ?1.
(9)
For all sets A ,a ,b holds (A ?→a )+·(A ?→b )=A ?→b .(10)
For all sets a ,b holds (a ?→.b )?1=b ?→.a .(11)For all sets a ,b ,c ,d such that a =b iff c =d holds [a ?→c ,b ?→d ]?1=[c ?→a ,d ?→b ].The scheme Convers deals with a non empty set A ,a binary relation B ,two unary functors F and G yielding sets,and a unary predicate P ,and states that:
B ={ F (x ),G (x ) ;x ranges over elements of A :P [x ]}
provided the following condition is met:
?B ={ G (x ),F (x ) ;x ranges over elements of A :P [x ]}.
Next we state the proposition
(12)For all natural numbers i ,j ,n such that i 2.A UXILIARY C ONCEPTS Let R ,S be relational structures.We say that S embeds R if and only if the condition (Def.2)is satis?ed. (Def.2) There exists a map f from R into S such that (i)f is one-to-one,and (ii)for all elements x ,y of R holds x ,y ∈the internal relation of R iff f (x ),f (y ) ∈the internal relation of S . Let R ,S be non empty relational structures.Let us note that the predicate S embeds R is re?exive.We now state the proposition (13)For all non empty relational structures R ,S ,T such that R embeds S and S embeds T holds R embeds T . Let R ,S be non empty relational structures.We say that R is equimorphic to S if and only if:(Def.3)R embeds S and S embeds R . Let us notice that the predicate R is equimorphic to S is re?exive and symmetric. Next we state the proposition (14)Let R ,S ,T be non empty relational structures.Suppose R is equimorphic to S and S is equimorphic to T .Then R is equimorphic to T . Let R be a non empty relational structure.We introduce R is parallel as an antonym of R is connected. Let R be a relational structure.We say that R is symmetric if and only if: (Def.4)The internal relation of R is symmetric in the carrier of R . Let R be a relational structure.We say that R is asymmetric if and only if: (Def.5)The internal relation of R is asymmetric. Next we state the proposition (15)Let R be a relational structure.Suppose R is asymmetric.Then the internal relation of R misses (the internal relation of R ) . Let R be a relational structure.We say that R is irre?exive if and only if: (Def.6)For every set x such that x∈the carrier of R holds x,x /∈the internal relation of R. Let n be a natural number.The functor n-SuccRelStr yields a strict relational structure and is de?ned as follows: (Def.7)The carrier of n-SuccRelStr=n and the internal relation of n-SuccRelStr={ i,i+1 ;i ranges over natural numbers:i+1 The following two propositions are true: (16)For every natural number n holds n-SuccRelStr is asymmetric. (17)If n>0,then the internal relation of n-SuccRelStr=n?1. Let R be a relational structure.The functor SymRelStr R yielding a strict relational structure is de?ned by the conditions(Def.8). (Def.8)(i)The carrier of SymRelStr R=the carrier of R,and (ii)the internal relation of SymRelStr R=(the internal relation of R)∪(the internal relation of R) . Let R be a relational structure.One can check that SymRelStr R is symmetric. Let us note that there exists a relational structure which is non empty and symmetric. Let R be a symmetric relational structure.Observe that the internal relation of R is symmetric. Let R be a relational structure.The functor ComplRelStr R yielding a strict relational structure is de?ned by the conditions(Def.9). (Def.9)(i)The carrier of ComplRelStr R=the carrier of R,and (ii)the internal relation of ComplRelStr R=(the internal relation of R)c\id the carrier of R. Let R be a non empty relational structure.Observe that ComplRelStr R is non empty. Next we state the proposition (18)Let S,R be relational structures.Suppose S and R are isomorphic.Then the internal relation of S=the internal relation of R. 3.N ECKLACE n Let n be a natural number.The functor Necklace n yielding a strict relational structure is de?ned by: (Def.10)Necklace n=SymRelStr n-SuccRelStr. Let n be a natural number.Observe that Necklace n is symmetric. We now state two propositions: (19)The internal relation of Necklace n={ i,i+1 ;i ranges over natural numbers:i+1< n}∪{ i+1,i ;i ranges over natural numbers:i+1 (20)Let x be a set.Then x∈the internal relation of Necklace n if and only if there exists a natural number i such that i+1 Let n be a natural number.One can verify that Necklace n is irre?exive. One can prove the following proposition (21)For every natural number n holds the carrier of Necklace n=n. Let n be a non empty natural number.Observe that Necklace n is non empty. Let n be a natural number.Note that the carrier of Necklace n is?nite. The following propositions are true: (22)For all natural numbers n,i such that i+1 Necklace n. (23)For every natural number n and for every natural number i such that i∈the carrier of Necklace n holds i (24)For every non empty natural number n holds Necklace n is connected. (25)For all natural numbers i,j such that i,j ∈the internal relation of Necklace n holds i=j+1or j=i+1. (26)Let i,j be natural numbers.Suppose i=j+1or j=i+1but i∈the carrier of Necklace n but j∈the carrier of Necklace n.Then i,j ∈the internal relation of Necklace n. (27)If n>0,then{ i+1,i ;i ranges over natural numbers:i+1 (28)If n>0,then the internal relation of Necklace n=2·(n?1). (29)Necklace1and ComplRelStrNecklace1are isomorphic. (30)Necklace4and ComplRelStrNecklace4are isomorphic. (31)If Necklace n and ComplRelStrNecklace n are isomorphic,then n=0or n=1or n=4. R EFERENCES [1]Grzegorz Bancerek.Cardinal numbers.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/card_1.html. [2]Grzegorz Bancerek.The fundamental properties of natural numbers.Journal of Formalized Mathematics,1,1989.http://mizar. org/JFM/Vol1/nat_1.html. [3]Grzegorz Bancerek.The ordinal numbers.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/ordinal1. html. [4]Grzegorz Bancerek.Sequences of ordinal numbers.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/ ordinal2.html. [5]Grzegorz Bancerek.Directed sets,nets,ideals,?lters,and maps.Journal of Formalized Mathematics,8,1996.https://www.wendangku.net/doc/a86171252.html,/ JFM/Vol8/waybel_0.html. [6]J′o zef Bia?as.Group and?eld de?nitions.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/realset1. html. [7]Czes?aw Byli′n ski.Basic functions and operations on functions.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/ JFM/Vol1/funct_3.html. [8]Czes?aw Byli′n ski.Functions and their basic properties.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/ funct_1.html. [9]Czes?aw Byli′n ski.Functions from a set to a set.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/funct_ 2.html. [10]Czes?aw Byli′n ski.Partial functions.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/partfun1.html. [11]Czes?aw Byli′n ski.Some basic properties of sets.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/ zfmisc_1.html. [12]Czes?aw Byli′n ski.A classical?rst order language.Journal of Formalized Mathematics,2,1990.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol2/cqc_ lang.html. [13]Czes?aw Byli′n ski.The modi?cation of a function by a function and the iteration of the composition of a function.Journal of Formalized Mathematics,2,1990.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol2/funct_4.html. [14]Czes?aw Byli′n ski.Galois connections.Journal of Formalized Mathematics,8,1996.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol8/waybel_1.html. [15]Agata Darmochwa?.Finite sets.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/finset_1.html. [16]Adam Grabowski.On the category of posets.Journal of Formalized Mathematics,8,1996.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol8/orders_ 3.html. [17]Shunichi Kobayashi.Predicate calculus for boolean valued functions.Part XII.Journal of Formalized Mathematics,11,1999.http: //https://www.wendangku.net/doc/a86171252.html,/JFM/Vol11/bvfunc24.html. [18]Stephan Thomasse.On better-quasi-ordering countable series-parallel orders.Transactions of the American Mathematical Society, 352(6):2491–2505,2000. [19]Andrzej Trybulec.Binary operations applied to functions.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/ Vol1/funcop_1.html. [20]Andrzej Trybulec.Enumerated sets.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/enumset1.html. [21]Andrzej Trybulec.Tarski Grothendieck set theory.Journal of Formalized Mathematics,Axiomatics,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/ Axiomatics/tarski.html. [22]Andrzej Trybulec.Subsets of real numbers.Journal of Formalized Mathematics,Addenda,2003.https://www.wendangku.net/doc/a86171252.html,/JFM/Addenda/ numbers.html. [23]Wojciech A.Trybulec.Partially ordered sets.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/orders_ 1.html. [24]Zinaida Trybulec.Properties of subsets.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/subset_1.html. [25]Edmund Woronowicz.Relations and their basic properties.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/ Vol1/relat_1.html. [26]Edmund Woronowicz.Relations de?ned on sets.Journal of Formalized Mathematics,1,1989.https://www.wendangku.net/doc/a86171252.html,/JFM/Vol1/ relset_1.html. [27]Edmund Woronowicz and Anna Zalewska.Properties of binary relations.Journal of Formalized Mathematics,1,1989.http://mizar. org/JFM/Vol1/relat_2.html. Received November18,2002 Published January2,2004