# 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).

Reasoning in the logic

• This has not yet been fully studied, because
MathCheck mostly only model checks, not proves.
• Many laws retain their traditional form.
• Thanks to regularity, _|_ can usually be ignored
• when both sides have the same minimal undefined subexpressions, and
• with rArr.
• Otherwise adding “|__f~| ^^” often suffices.
 prop_logic TT <=> X \/ !X prop_logic prop3_on TT <=> X \/ !X modulo 20 x*1/x = 1 <=> (!EE i: x = 2i) /\ !EE i: x=5i