Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

Vertex Sequences Induced by Chains


Yatsuka Nakamura
Shinshu University, Department of Information Engineering, Nagano, Japan
Piotr Rudnicki
University of Alberta, Department of Computing Science, Edmonton, Alberta, Canada

Summary.

In the three preliminary sections to the article we define two operations on finite sequences which seem to be of general interest. The first is the $cut$ operation that extracts a contiguous chunk of a finite sequence from a position to a position. The second operation is a glueing catenation that given two finite sequences catenates them with removal of the first element of the second sequence. The main topic of the article is to define an operation which for a given chain in a graph returns the sequence of vertices through which the chain passes. We define the exact conditions when such an operation is uniquely definable. This is done with the help of the so called two-valued alternating finite sequences. We also prove theorems about the existence of simple chains which are subchains of a given chain. In order to do this we define the notion of a finite subsequence of a typed finite sequence.

This work was partially supported by Shinshu Endowment for Information Science, NSERC Grant OGP9207 and JSTF award 651-93-S009.

MML Identifier: GRAPH_2

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

Contents (PDF format)

  1. Preliminaries
  2. The cut operation for finite sequences
  3. The glueing catenation of finite sequences
  4. Two valued alternating finite sequences
  5. Finite subsequence of finite sequences
  6. Vertex sequences induced by chains
  7. Vertex sequences induced by simple chains, paths and ordered chains

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 and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
[7] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[8] Krzysztof Hryniewiecki. Graphs. Journal of Formalized Mathematics, 2, 1990.
[9] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[10] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[11] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[12] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.
[13] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[14] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received May 13, 1995


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