<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

Published Online: Jun 30, 2014

Page range: 125 - 155

Received: Jun 13, 2014

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

Keywords
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

Published Online: Jun 30, 2014

Page range: 125 - 155

Received: Jun 13, 2014

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

Keywordsconstruction 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)

Keywords
construction degree, context, translation, endomorphism