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
Epsilon term, which is defined to evaluate to an arbitrary value satisfying the formula
cond
.cond
is expected to contain a bound variable with de Bruijn index 0.