Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

**Krzysztof Retel**- University of Bialystok

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

Contents (PDF format)

- [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.

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