Returns true if the left- and right-hand sides of this equation may be rewritten to the same normal form with respect to rs.
Returns true if this equation is a trivial equation, i.
Returns true if this equation is a trivial equation, i.e., the left- and right-hand sides of this equations are the same, and false otherwise.
Returns the left-hand side term of this equation.
Returns the right-hand side term of this equation.
Returns this equation with the left- and right-hand sides reduced by one step with respect to the term rewrite system rs.
Returns this equation with the left-hand side reduced by one step with respect to the indexed term rewrite system irsand the index of the used rule from irs.
Returns this equation with the left-hand side reduced by one step with respect to the term rewrite system rs.
Returns this equation with the left-hand side reduced to normal form with respect to the term rewrite system rs.
Returns this equation with the right-hand side reduced by one step with respect to the term rewrite system rs.
Returns this equation with the right-hand side reduced to normal form with respect to the term rewrite system rs.
Returns this equation with the left- and right-hand sides reduced to normal form with respect to the term rewrite system rs.
Returns this equation with swapped left- and right-hand sides.
Returns a rule from the left-hand side of this equation to the right-hand side of this equation.
Returns a tuple containing the left- and right-hand side terms of this equation.
Returns a list of all variables occuring in this equation.
Returns this equation with the left-hand side reduced by one step with respect to rs without any rules equal to this equation.
Returns this equation with the left-hand side reduced to normal form with respect to rs without any rules equal to this equation.
Represents an equation between two terms.
Equations are undirected so s ≈ t is identified with t ≈ s.
the left-hand side of the equation
the right-hand side of the equation