Substitution
Related Docs:
object Substitution
| package substitutions
The term order that is used for the resulting terms or formulas.
The term order that is used for the resulting terms or formulas. We require that a substitution is only applied to terms/formulas that are already sorted according to this order
Substitution that is to be used underneath num quantifiers.
Substitution that is to be used underneath num quantifiers.
Because we use De Bruijn indexes, passing quantifiers shifts the variables
in a substitution
Some kinds of substitutions can only be applied when pseudo-reduction is allowed to be performed.
Some kinds of substitutions can only be applied when pseudo-reduction
is allowed to be performed. Implementations of the following method are
allowed to multiply lc with arbitrary positive integers to
achieve this.
Re-sort an object with a new TermOrder.
Re-sort an object with a new TermOrder. It is guaranteed that
the result isSortedBy(order)
Compare the order of this Substitution with a given order.
Compare the order of this Substitution with a given order. We
use equality here, because the behaviour would be quite confusing with
the relation isSubOrderOf (remember that the substitution has
to cope with arbitrary terms/formulas that are sorted by the order)
(Since version ) see corresponding Javadoc for more information.
A substitution is a mapping from
TerFortoTerForthat replaces variables and constants with arbitrary other terms. It is required that a substitution is only applied to terms/formulas that are sorted according toorder. There are two more concrete sub-traits:SimpleSubstitution, which performs a simple replacement of constants or variables, andPseudoDivSubstitution, which can make use of pseudo-division in order to replace expressionsn * c.