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 non-empty 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

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.