The index of the bound variable.
Increase the index of this variable by shift
(which can
have any sign).
Increase the index of this variable by shift
(which can
have any sign).
The sort of the bound variable.
Product of two terms (only defined if at least one of the terms is constant).
Product of two terms (only defined if at least one of the terms is constant).
Product of term with an integer.
Product of term with an integer.
Product of two terms.
Product of two terms. The resulting expression is simplified immediately if one of the terms is constant.
Sum of two terms.
Sum of two terms.
Sum of two terms.
Sum of two terms. The resulting expression is simplified immediately if one of the terms disappears.
Difference between two terms.
Difference between two terms.
Difference of two terms.
Difference of two terms. The resulting expression is simplified immediately if one of the terms disappears.
Inequality between two terms.
Inequality between two terms.
Inequality between two terms.
Inequality between two terms.
Dis-equation between two terms.
Dis-equation between two terms.
Equation between two terms.
Equation between two terms.
Inequality between two terms.
Inequality between two terms.
Inequality between two terms.
Inequality between two terms.
Return the i
th sub-expression.
Return the i
th sub-expression.
Iterator over the sub-expressions of this expression.
Iterator over the sub-expressions of this expression.
Number of sub-expressions.
Number of sub-expressions.
Negation of a term.
Negation of a term. The resulting expression is simplified immediately if one of the terms is constant.
The sub-expressions of this expression.
The sub-expressions of this expression.
Negation of a term.
Negation of a term.
Replace the subexpressions of this node with new expressions
Replace the subexpressions of this node with new expressions
Bound variables, represented using their de Bruijn index and the sort.