Vertex Sequences Induced by Chains

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]