Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

The Class of Series -- Parallel Graphs. Part I

Krzysztof Retel
University of Bialystok

Summary.

The paper introduces some preliminary notions concerning the graph theory according to [18]. We define Necklace $n$ as a graph with vertex $\{1,2,3,\dots,n\}$ and edge set $\{(1,2),(2,3),\dots,(n-1,n)\}.$ The goal of the article is to prove that Necklace $n$ and Complement of Necklace $n$ are isomorphic for $n = 0, 1, 4.$

MML Identifier: NECKLACE

The terminology and notation used in this paper have been introduced in the following 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] [16]

Contents (PDF format)

1. Preliminaries
2. Auxiliary Concepts
3. Necklace $n$

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[5] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Journal of Formalized Mathematics, 8, 1996.
[6] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.
[8] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[9] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[10] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[11] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[12] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.
[13] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[14] Czeslaw Bylinski. Galois connections. Journal of Formalized Mathematics, 8, 1996.
[15] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[16] Adam Grabowski. On the category of posets. Journal of Formalized Mathematics, 8, 1996.
[17] Shunichi Kobayashi. Predicate calculus for boolean valued functions. Part XII. Journal of Formalized Mathematics, 11, 1999.
[18] Stephan Thomasse. On better-quasi-ordering countable series-parallel orders. \em 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.
[20] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
[21] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[22] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[23] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.
[24] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[25] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[26] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.
[27] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Journal of Formalized Mathematics, 1, 1989.