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`.Restricting the domain to start with does not solve the problem.

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

The undefined value of arithmetic

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, and
- with `rArr`.

- Otherwise adding “`|__f~| ^^`” often suffices.