<abstract xmlns="http://www.w3.org/1999/xhtml"><p>Two construction functors: simple term with a variable and compound term with an operation and argument terms and schemes of term induction are introduced. The degree of construction as a number of used operation symbols is defined. Next, the term context is investigated. An <italic>x-context</italic> is a term which includes a variable <italic>x</italic> once only. The compound term is <italic>x-context</italic> iff the argument terms include an <italic>x-context</italic> once only. The context induction is shown and used many times. As a key concept, the context substitution is introduced. Finally, the translations and endomorphisms are expressed by context substitution.</p></abstract>

Two construction functors: simple term with a variable and compound term with an operation and argument terms and schemes of term induction are introduced. The degree of construction as a number of used operation symbols is defined. Next, the term context is investigated. An x-context is a term which includes a variable x once only. The compound term is x-context iff the argument terms include an x-context once only. The context induction is shown and used many times. As a key concept, the context substitution is introduced. Finally, the translations and endomorphisms are expressed by context substitution.

Term Context

Association of Mizar Users Białystok, Poland

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

{"article-title":"Term Context"}

Two construction functors: simple term with a variable and compound term with an operation and argument terms and schemes of term induction are introduced. The...

Term Context

Online veröffentlicht: 30. Juni 2014

Seitenbereich: 125 - 155

Eingereicht: 13. Juni 2014

DOI: https://doi.org/10.2478/forma-2014-0015

Schlüsselwörter
construction degree, context, translation, endomorphism

© 2014 Grzegorz Bancerek

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Term Context

Online veröffentlicht: 30. Juni 2014

Seitenbereich: 125 - 155

Eingereicht: 13. Juni 2014

DOI: https://doi.org/10.2478/forma-2014-0015

Schlüsselwörterconstruction degree, context, translation, endomorphism

© 2014 Grzegorz Bancerek

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Schlüsselwörter
construction degree, context, translation, endomorphism