equality

==

The predicate == is a binary operator defined for each visible sort and is defined in terms of evaluation. That is, for ground terms t and t' of the same sort, t == t' evaluates to true iff terms reduce to a common term. This is different from the equational = which specifies the equality of the theory.