The Logic of Equation and Inequation Solving

`f(x)` is defined and yields 0   if and only if   `x = x_1 vv … vv x = x_n`

• we are asked to solve `sqrt(x+3) = x-3`, not `x >=``-3 ^^ sqrt(x+3) = x-3`

The undefined value of arithmetic

The undefined truth value

The reasoning operators ⇒ and ⇔

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
  • with `rArr`
• otherwise adding “`"dom"_f ^^`” often suffices