Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Introduction to Trees

Grzegorz Bancerek

Warsaw University, Bialystok

Partially supported by Le Hodey Foundation.
The part of this work had been done on Mizar Workshop '89 (Fourdrain, France)
in Summer '89.
Summary.

The article consists of two parts: the first one deals with the concept of
the prefixes of a finite sequence, the second one introduces and deals with
the concept of tree. Besides some auxiliary propositions concerning
finite sequences are presented. The trees are introduced as nonempty sets
of finite sequences of natural numbers which are closed on prefixes and
on sequences of less numbers (i.e. if $\langle n_1$, $n_2$, $\dots$,
$n_k\rangle$ is a vertex (element) of a tree and $m_i \leq n_i$
for $i = 1$, $2$, $\dots$, $k$, then $\langle m_1$, $m_2$, $\dots$,
$m_k\rangle$ also is). Finite trees, elementary trees with $n$ leaves,
the leaves and the subtrees of a tree, the inserting of a tree into another
tree, with a node used for determining the place of insertion,
antichains of prefixes, and height and width of finite trees
are introduced.
MML Identifier:
TREES_1
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[8]
[2]
[7]
[9]
[4]
[3]
[5]
[1]
Contents (PDF format)
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]
Agata Darmochwal.
Finite sets.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [7]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [8]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received October 25, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]