Contradiction

Whether this Equation is an Assignment (either LeftAssignment or RightAssignment).

Whether this Equation is a Comparison, i.e. still needs decomposing into sub-equations.

Whether this Equation is a Contradiction, i.e. represents unification failure.

Whether this Equation is an Identity, i.e. an equation between already-equal terms.

Whether this Equation is a LeftAssignment, i.e. shaped as Var = Term.

Whether this Equation is a RightAssignment, i.e. shaped as Term = Var.

The left-hand side of the equation

The right-hand side of the equation

Applies given substitution to the Equation left-hand and right-hand sides, returning the new Equation

This Equation as an Assignment, or null if isAssignment is false.

This Equation as a Comparison, or null if isComparison is false.

This Equation as a Contradiction, or null if isContradiction is false.

This Equation as an Identity, or null if isIdentity is false.

This Equation as a LeftAssignment, or null if isLeftAssignment is false.

This Equation as a RightAssignment, or null if isRightAssignment is false.

This Equation as an Assignment. @throws ClassCastException if isAssignment is false.

This Equation as a Comparison. @throws ClassCastException if isComparison is false.

This Equation as a Contradiction. @throws ClassCastException if isContradiction is false.

This Equation as an Identity. @throws ClassCastException if isIdentity is false.

This Equation as a LeftAssignment. @throws ClassCastException if isLeftAssignment is false.

This Equation as a RightAssignment. @throws ClassCastException if isRightAssignment is false.

Creates a copy of this Equation, of the same concrete subtype, with lhs and/or rhs replaced.

Creates a new Equation with lhs and rhs swapped, reclassifying it accordingly (see of).

The (variable, term) pair this Equation assigns, i.e. its Var side paired with the other side.

Turns this Equation into a Contradiction with the same lhs and rhs, regardless of its actual shape.

This Equation's lhs and rhs, as a Pair.

The single-binding Substitution this Equation amounts to, i.e. its Var side unified with the other side.

Converts this Equation to its logical representation, the binary Struct lhs = rhs.