# The Logic of Equation and Inequation Solving

Let x_1, ..., x_n be defined terms that contain no variables.

• e.g., 3, (1+sqrt(5))/2
• not e.g., a+1, 3/0

We want   f(x) = 0 ⇔ x = x_1 vv … vv x = x_n   to mean

f(x) is defined and yields 0   if and only if   x = x_1 vv … vv x = x_n.
• The equation comes as 7 sqrt(|x|-1) = x+9, not as -1 <= x <= 1 ^^ 7 sqrt(|x|-1) = x+9.
• Try x=5 in the intermediate step (x < 0 ^^ 7 sqrt(-x-1) = x+9) vv (x >= 0 ^^ 7 sqrt(x-1) = x+9).
• Thanks to regularity, _|_ can usually be ignored
• with rArr.
• Otherwise adding “|__f~| ^^” often suffices.