In the normalization the formula input by the user is put into a special form
goto get through this phase. There are, however, a few commands that can be given here, and some of them are described below.
assume [ a > 0 /\ b > 0 ]The command name, as you can see, is
assume, and the syntax for the formula itself is the same as for input formulas.
prop-eqn-const" command, which simply "enables" equational constraints. Information on Equational Constraints
full-cad". This forces a full CAD of free-variable space to be constructed. (Note: if the "
cell-choice-bound" command is used, the "
full-cad" command has no effect.)