We want substitution of an expression for a free variable always be allowed

- `sqrt(x)` must not imply that we are only talking about non-negative reals
- otherwise the root 3 would be lost in the following:
`11 sqrt(|x|+1) = 25 - x ⇔`

`(x < 0 ^^ 11` `sqrt(1-x)` `= 25 - x)``vv``(x >= 0 ^^ 11 sqrt(x+1) = 25 - x)`

Each undefined expression must yield a “value”

- we will see that one value suffices
- we denote it with `_|_`

Let `f` and `g` be expressions without free variables

- if `f` contains an undefined subexpression but `f` yields `a` for some `a
in RR`,

then `f = x` has a wrong root `x = a`arithmetic must be regular รก la Kleene:

undefined argument guarantees undefined result - if `f = g` yields
**T**although `f` or `g` is undefined,

then each `x in RR` is its wrong root`frac(1)(0) = frac(1)(0)` does not yield

**T**, so ”`=`“ is not reflexive!

We also want to solve `f(x) > 0` and so on

if `f` or `g` is undefined, then none of `f = g`, `f < g`, `f <= g`, … yieldsT

- so we cannot distinguish between different undefineds, so a single `_|_`
suffices

(we could build that ability to the logic but we do not want to)