page 13, Theorem 2.3.1 : The exptime upper bound, for deciding whether a
sentence of the theory of reals is true, is valid only under an
additional assumption that the alternation depth of quantifiers in the
sentence is bounded. (By the way, this result is never used in the thesis,
because all important values are expressed in the existential fragment.)