Requirements on the canonizer

1) An equation t = u in the theory is valid if and only if σ(t) ≡ σ(u).

2) If t is a term not in the theory, then σ(t) ≡ t

3) σ(σ(t)) ≡ σ(t)

4) If σ(t) ≡ f(t_{1}, ..., t_{n}) for a term t in the theory then σ(t_{i}) ≡ t_{i} for 1 ≤ i ≤ n.

5) vars(σ(t)) ⊆ vars(t).

Requirements on the solver

Let in the following be E = solve(e), t_{i} denote terms and x_{i} represent basic variables. 1. ⊢ e ⟺ E is in the theory

2. E ∈ {T RUE, F ALSE} or E = ⋀_{i} x_{i} = t_{i}

3. If e contains no variables, then E ∈ {T RUE, F ALSE}

4. If E = ⋀_{i} x_{i} = t_{i} then the following holds:

(a) x_{i} ∈ vars(e)

(b) for all i, j: x_{i} ∉ vars(t_{j})

(c) for all i ≠ j: x_{i} ≠ x_{j}

(d) for all i: σ(t_{i}) = t_{i}.