The state of equality elimination proof search.
eqs is the list of
equality constraints, and each
t ∈ eqs represents the constraint
0 = t.
les is the list of inequality constraints, and each
t ∈ eqs
represents the constraint
0 < t.
ees is the sequence of equality
elimination steps that have been used so far to obtain the current set of
constraints. The list
ees grows over time until
eqs becomes empty.
t1 succeeds and returns a value, 'commit' to that choice and
t3 with the returned value as argument. Do not backtrack
t2 even if
t3 fails. If
t1 fails outright, run
Find and return the smallest coefficient (by absolute value) in a term, along with the coefficient's variable index and the term itself. If the coefficient is negative, negate both the coefficient and the term before returning them.