Unknown ≠ Undefined

So MathCheck uses 3 truth values: F, U, and T

Computation is often imprecise

draw_function ; sin^2 x + cos^2 x - 1 ; dup( sin^2 x + cos^2 x - 1 ); ddn( sin^2 x + cos^2 x - 1 )

Numeric values in MathCheck may be

• precise rational numbers
• `_|_`
• an interval of two floating point values, low ≤ precise ≤ high
• `_|_` or an interval

So to MathCheck, `sqrt(sin^2 1 + cos^2 1 - 1) > 0` could in principle yield F, U, or T

`rArr` The truth value data type inside MathCheck has 7 different values:

• F, U, and T
• FU, FT, UT, and FUT, meaning F or U, F or T, and so on

Therefore

• U means “certainly undefined”, e.g. `log(-1) = 0`
• FT means “certainly defined, but we do not know more than that”
• FU means “certainly not true”, suffices for `rArr` and `hArr`
• FUT means that we know nothing