trans

trans [ <label-exp> ] <term> => <term> .

Defines a transition, which is like an equation but without symmetry.

See eq for specification of requirements on <label-exp> and the terms.

Transitions and equations server similar, but different purpose. In particular, reductions (both with or without behavior axioms used) do not take transitions into account. Only exec also uses transitions. On the other hand, the built-in search predicate searches all possible transitions from a given term.