Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

The Class of Series-Parallel Graphs. Part II


Krzysztof Retel
University of Bialystok

Summary.

In this paper we introduce two new operations on graphs: sum and union corresponding to parallel and series operation respectively. We determine $N$-free graph as the graph that does not embed Necklace $4$. We define ``fin\_RelStr" as the set of all graphs with finite carriers. We also define the smallest class of graphs which contains the one-element graph and which is closed under parallel and series operations. The goal of the article is to prove the theorem that the class of finite series-parallel graphs is the class of finite $N$-free graphs. This paper formalizes the next part of [12].

This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

MML Identifier: NECKLA_2

The terminology and notation used in this paper have been introduced in the following articles [14] [13] [18] [7] [20] [8] [1] [2] [3] [15] [17] [4] [16] [19] [11] [5] [6] [9] [10]

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[9] Bogdan Nowak and Grzegorz Bancerek. Universal classes. Journal of Formalized Mathematics, 2, 1990.
[10] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.
[11] Krzysztof Retel. The class of series --- parallel graphs. Journal of Formalized Mathematics, 14, 2002.
[12] Stephan Thomasse. On better-quasi-ordering countable series-parallel orders. \em Transactions of the American Mathematical Society, 352(6):2491--2505, 2000.
[13] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
[14] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[15] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[16] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.
[17] Wojciech A. Trybulec. Groups. Journal of Formalized Mathematics, 2, 1990.
[18] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[19] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[20] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.

Received May 29, 2003


[ Download a postscript version, MML identifier index, Mizar home page]