Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

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

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

- Preliminaries
- The cut operation for finite sequences
- The glueing catenation of finite sequences
- Two valued alternating finite sequences
- Finite subsequence of finite sequences
- Vertex sequences induced by chains
- Vertex sequences induced by simple chains, paths and ordered chains

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

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