On Defining Functions on Trees 1

Summary. The continuation of the sequence of articles on trees (see [2], [3], [4], [5]) and on context-free grammars ([13]). We define the set of complete parse trees for a given context-free grammar. Next we define the scheme of induction for the set and the scheme of defining functions by induction on the set. For each symbol of a context-free grammar we define the terminal, the pretraversal, and the posttraversal languages. The introduced terminology is tested on the example of Peano naturals. MML Identifier:DTCONSTR. WWW:http://mizar.org/JFM/Vol5/dtconstr.htm