help links subscribe changes refresh edit

	FriCAS Library Examples
ExampleExtrema ←	↑	→ ExampleIntegration2

ExampleInequalitiesViaCAD

Edit detail for ExampleInequalitiesViaCAD revision 1 of 1

	1
Editor: test1 Time: 2023/09/23 12:40:58 GMT+0
Note:

changed:
-
Recenty in sci.math.symbolic there was a question if
\begin{equation}
b^2 \geq (a - c)^2
\end{equation}
and
\begin{equation}
a^2 \geq b^2
\end{equation}
implies
\begin{equation}
c^2 \geq (a + b)^2
\end{equation}
or
\begin{equation}
c^2 \geq (a - b)^2.
\end{equation}

This can be proved by an elementary argument.
Below w show purely mechanical way based on
cylindrical algebraic decomposition (CAD).

\begin{axiom}
rC := RealClosure(Fraction(Integer))
pR := POLY(rC)

-- Replace inequalies by differences of sides
lp := [b^2 - (a - c)^2, a^2 - b^2, c^2 - (a + b)^2, c^2 - (a - b)^2]

-- Do CAD
cd := cylindricalDecomposition(lp::List(pR)
                              )$CylindricalAlgebraicDecompositionPackage(rC)

-- If implication is false, then there is opposite strict ineqality
-- in the last two inequalities.  Hence, there is counterexample where
-- all inequalities are strict.  Consequently, it is enough to look
-- only at cells of full dimension.
cd3 := [ce for ce in cd | dimension(ce) = 3];

sp3 := [samplePoint(ce) for ce in cd3]::List(List(Fraction(Integer)))
vll := [map(p +-> eval(p, [a, b, c], pp), lp) for pp in sp3];
vlq := vll::List(List(Fraction(Integer)))

good := true
-- Loop to check validity of formula at each sample point
for vl in vlq repeat
    if vl(1) > 0 and vl(2) > 0 and vl(3) < 0 and vl(4) < 0 then
        good := false

print good
\end{axiom}


Let us explain this a bit more.  CAD for list of polynomials 'l' produces collection of
cells such that any boolean formula in equations and inequalites of polynomials in 'l'
produces constant value on each cells.  And cells cover the whole space.  So, to
check validity of Boolean formula it is enough to check its validity on each cell.
Since value of the formula is constant in the cell it is enough to compute value
at single point given by 'samplePoint'.  Above we took advantage of another property:
closure of sum of cells of full dimension gives the whole space.  Since sets on
which assumptions and conclusion of our formula hold are closed we can gain
a little extra efficiency and ignore cells of lower dimension.

Recenty in sci.math.symbolic there was a question if

$\label{eq1} b^2 \geq (a - c)^2$

(1)

and

$\label{eq2} a^2 \geq b^2$

(2)

implies

$\label{eq3} c^2 \geq (a + b)^2$

(3)

$\label{eq4} c^2 \geq (a - b)^2.$

(4)

This can be proved by an elementary argument. Below w show purely mechanical way based on cylindrical algebraic decomposition (CAD).

fricas

(1) -> rC := RealClosure(Fraction(Integer))

$\label{eq5}\hbox{\axiomType{RealClosure}\ } \left({\hbox{\axiomType{Fraction}\ } \left({\hbox{\axiomType{Integer}\ }}\right)}\right)$

(5)

Type: Type

fricas

pR := POLY(rC)

$\label{eq6}\hbox{\axiomType{Polynomial}\ } \left({\hbox{\axiomType{RealClosure}\ } \left({\hbox{\axiomType{Fraction}\ } \left({\hbox{\axiomType{Integer}\ }}\right)}\right)}\right)$

(6)

Type: Type

fricas

-- Replace inequalies by differences of sides
lp := [b^2 - (a - c)^2, a^2 - b^2, c^2 - (a + b)^2, c^2 - (a - b)^2]

$\label{eq7}\begin{array}{@{}l} \displaystyle \left[{-{{c}^{2}}+{2 \ a \ c}+{{b}^{2}}-{{a}^{2}}}, \:{-{{b}^{2}}+{{a}^{2}}}, \:{{{c}^{2}}-{{b}^{2}}-{2 \ a \ b}-{{a}^{2}}}, \: \right. \ \ \displaystyle \left.{{{c}^{2}}-{{b}^{2}}+{2 \ a \ b}-{{a}^{2}}}\right]$

(7)

Type: List(Polynomial(Integer))

fricas

-- Do CAD
cd := cylindricalDecomposition(lp::List(pR)
                              )$CylindricalAlgebraicDecompositionPackage(rC)

\label{eq8}\begin{array}{@{}l}
\displaystyle
\left[{\left({\left\{{c = - 4}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 3}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 3}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 4}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 3}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{3}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\frac{3}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 3}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{5}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{3}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{5}{4}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{1}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c ={\frac{1}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c ={\frac{5}{4}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c ={\frac{3}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c ={\frac{5}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{5}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{3}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{5}{4}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{1}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c ={\frac{1}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c ={\frac{5}{4}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c ={\frac{3}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c ={\frac{5}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = - 3}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = -{\frac{3}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\frac{3}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 3}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 4}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 3}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 3}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 4}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = - 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\%A 1}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\%A 2}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\%A 3}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\%A 4}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 0}, \: \mbox{\rm false} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 4}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 3}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 3}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 4}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 3}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = -{\frac{3}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\frac{3}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 3}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{5}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{3}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{5}{4}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{1}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c ={\frac{1}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c ={\frac{5}{4}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c ={\frac{3}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c ={\frac{5}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = -{\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = -{\frac{5}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{3}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = -{\frac{5}{4}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{\left({{\left\{{c = -{\frac{1}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}}\right)}, \right.
\
\
\displaystyle
\left.\:{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\frac{1}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\frac{5}{4}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\frac{3}{2}}}, \: \mbox{\rm false} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\frac{5}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b ={\frac{1}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 3}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = -{\frac{3}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c ={\frac{3}{2}}}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 3}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 4}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 3}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = - 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 0}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 1}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 3}, \: \mbox{\rm false} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}, \: \right.
\
\
\displaystyle
\left.{\left({\left\{{c = 4}, \: \mbox{\rm true} \right\}}, \:{\left\{{b = 2}, \: \mbox{\rm true} \right\}}, \:{\left\{{a = 1}, \: \mbox{\rm true} \right\}}\right)}\right]

(8)

Type: List(Cell(RealClosure(Fraction(Integer))))

fricas

-- If implication is false, then there is opposite strict ineqality
-- in the last two inequalities.  Hence, there is counterexample where
-- all inequalities are strict.  Consequently, it is enough to look
-- only at cells of full dimension.
cd3 := [ce for ce in cd | dimension(ce) = 3];

Type: List(Cell(RealClosure(Fraction(Integer))))

fricas

sp3 := [samplePoint(ce) for ce in cd3]::List(List(Fraction(Integer)))

$\label{eq9}\begin{array}{@{}l} \displaystyle \left[{\left[ - 4, \: - 2, \: - 1 \right]}, \:{\left[ - 2, \: - 2, \: - 1 \right]}, \:{\left[ 0, \: - 2, \: - 1 \right]}, \:{\left[ 2, \: - 2, \: - 1 \right]}, \right. \ \ \displaystyle \left.\:{\left[ 4, \: - 2, \: - 1 \right]}, \:{\left[ -{\frac{5}{2}}, \: -{\frac{1}{2}}, \: - 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{5}{4}}, \: -{\frac{1}{2}}, \: - 1 \right]}, \:{\left[ 0, \: -{\frac{1}{2}}, \: - 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[{\frac{5}{4}}, \: -{\frac{1}{2}}, \: - 1 \right]}, \:{\left[{\frac{5}{2}}, \: -{\frac{1}{2}}, \: - 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{5}{2}}, \:{\frac{1}{2}}, \: - 1 \right]}, \:{\left[ -{\frac{5}{4}}, \:{\frac{1}{2}}, \: - 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[ 0, \:{\frac{1}{2}}, \: - 1 \right]}, \:{\left[{\frac{5}{4}}, \:{\frac{1}{2}}, \: - 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[{\frac{5}{2}}, \:{\frac{1}{2}}, \: - 1 \right]}, \:{\left[ - 4, \: 2, \: - 1 \right]}, \:{\left[ - 2, \: 2, \: - 1 \right]}, \:{\left[ 0, \: 2, \: - 1 \right]}, \right. \ \ \displaystyle \left.\:{\left[ 2, \: 2, \: - 1 \right]}, \:{\left[ 4, \: 2, \: - 1 \right]}, \:{\left[ - 4, \: - 2, \: 1 \right]}, \:{\left[ - 2, \: - 2, \: 1 \right]}, \:{\left[ 0, \: - 2, \: 1 \right]}, \right. \ \ \displaystyle \left.\:{\left[ 2, \: - 2, \: 1 \right]}, \:{\left[ 4, \: - 2, \: 1 \right]}, \:{\left[ -{\frac{5}{2}}, \: -{\frac{1}{2}}, \: 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{5}{4}}, \: -{\frac{1}{2}}, \: 1 \right]}, \:{\left[ 0, \: -{\frac{1}{2}}, \: 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[{\frac{5}{4}}, \: -{\frac{1}{2}}, \: 1 \right]}, \:{\left[{\frac{5}{2}}, \: -{\frac{1}{2}}, \: 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{5}{2}}, \:{\frac{1}{2}}, \: 1 \right]}, \:{\left[ -{\frac{5}{4}}, \:{\frac{1}{2}}, \: 1 \right]}, \:{\left[ 0, \:{\frac{1}{2}}, \: 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[{\frac{5}{4}}, \:{\frac{1}{2}}, \: 1 \right]}, \:{\left[{\frac{5}{2}}, \:{\frac{1}{2}}, \: 1 \right]}, \:{\left[ - 4, \: 2, \: 1 \right]}, \: \right. \ \ \displaystyle \left.{\left[ - 2, \: 2, \: 1 \right]}, \:{\left[ 0, \: 2, \: 1 \right]}, \:{\left[ 2, \: 2, \: 1 \right]}, \:{\left[ 4, \: 2, \: 1 \right]}\right]$

(9)

Type: List(List(Fraction(Integer)))

fricas

vll := [map(p +-> eval(p, [a, b, c], pp), lp) for pp in sp3];

Type: List(List(Polynomial(Fraction(Integer))))

fricas

vlq := vll::List(List(Fraction(Integer)))

$\label{eq10}\begin{array}{@{}l} \displaystyle \left[{\left[ - 5, \:{12}, \: -{35}, \: - 3 \right]}, \:{\left[ 3, \: 0, \: -{15}, \: 1 \right]}, \:{\left[ 3, \: - 4, \: - 3, \: - 3 \right]}, \: \right. \ \ \displaystyle \left.{\left[ - 5, \: 0, \: 1, \: -{15}\right]}, \:{\left[ -{2 1}, \:{12}, \: - 3, \: -{35}\right]}, \:{\left[ - 2, \: 6, \: - 8, \: - 3 \right]}, \: \right. \ \ \displaystyle \left.{\left[{\frac{3}{16}}, \:{\frac{21}{16}}, \: -{\frac{33}{1 6}}, \:{\frac{7}{16}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{3}{4}}, \: -{\frac{1}{4}}, \:{\frac{3}{4}}, \:{\frac{3}{4}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{77}{16}}, \:{\frac{21}{16}}, \:{\frac{7}{1 6}}, \: -{\frac{33}{16}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ -{12}, \: 6, \: - 3, \: - 8 \right]}, \:{\left[ - 2, \: 6, \: - 3, \: - 8 \right]}, \: \right. \ \ \displaystyle \left.{\left[{\frac{3}{16}}, \:{\frac{21}{16}}, \:{\frac{7}{1 6}}, \: -{\frac{33}{16}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{3}{4}}, \: -{\frac{1}{4}}, \:{\frac{3}{4}}, \:{\frac{3}{4}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{77}{16}}, \:{\frac{21}{16}}, \: -{\frac{3 3}{16}}, \:{\frac{7}{16}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ -{12}, \: 6, \: - 8, \: - 3 \right]}, \:{\left[ - 5, \:{12}, \: - 3, \: -{35}\right]}, \:{\left[ 3, \: 0, \: 1, \: -{15}\right]}, \: \right. \ \ \displaystyle \left.{\left[ 3, \: - 4, \: - 3, \: - 3 \right]}, \:{\left[ - 5, \: 0, \: -{15}, \: 1 \right]}, \:{\left[ -{21}, \:{12}, \: -{35}, \: - 3 \right]}, \: \right. \ \ \displaystyle \left.{\left[ -{21}, \:{12}, \: -{35}, \: - 3 \right]}, \:{\left[ - 5, \: 0, \: -{15}, \: 1 \right]}, \:{\left[ 3, \: - 4, \: - 3, \: - 3 \right]}, \: \right. \ \ \displaystyle \left.{\left[ 3, \: 0, \: 1, \: -{15}\right]}, \:{\left[ - 5, \:{12}, \: - 3, \: -{35}\right]}, \:{\left[ -{12}, \: 6, \: - 8, \: - 3 \right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{77}{16}}, \:{\frac{21}{16}}, \: -{\frac{3 3}{16}}, \:{\frac{7}{16}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{3}{4}}, \: -{\frac{1}{4}}, \:{\frac{3}{4}}, \:{\frac{3}{4}}\right]}, \: \right. \ \ \displaystyle \left.{\left[{\frac{3}{16}}, \:{\frac{21}{16}}, \:{\frac{7}{1 6}}, \: -{\frac{33}{16}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ - 2, \: 6, \: - 3, \: - 8 \right]}, \:{\left[ -{12}, \: 6, \: - 3, \: - 8 \right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{77}{16}}, \:{\frac{21}{16}}, \:{\frac{7}{1 6}}, \: -{\frac{33}{16}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ -{\frac{3}{4}}, \: -{\frac{1}{4}}, \:{\frac{3}{4}}, \:{\frac{3}{4}}\right]}, \: \right. \ \ \displaystyle \left.{\left[{\frac{3}{16}}, \:{\frac{21}{16}}, \: -{\frac{33}{1 6}}, \:{\frac{7}{16}}\right]}, \: \right. \ \ \displaystyle \left.{\left[ - 2, \: 6, \: - 8, \: - 3 \right]}, \:{\left[ -{21}, \:{12}, \: - 3, \: -{35}\right]}, \:{\left[ - 5, \: 0, \: 1, \: -{15}\right]}, \: \right. \ \ \displaystyle \left.{\left[ 3, \: - 4, \: - 3, \: - 3 \right]}, \:{\left[ 3, \: 0, \: -{15}, \: 1 \right]}, \:{\left[ - 5, \:{12}, \: -{3 5}, \: - 3 \right]}\right]$

(10)

Type: List(List(Fraction(Integer)))

fricas

good := true

$\label{eq11} \mbox{\rm true}$

(11)

Type: Boolean

fricas

-- Loop to check validity of formula at each sample point
for vl in vlq repeat
    if vl(1) > 0 and vl(2) > 0 and vl(3) < 0 and vl(4) < 0 then
        good := false

Type: Void

fricas

print good

   true

Type: Void

Let us explain this a bit more. CAD for list of polynomials l produces collection of cells such that any boolean formula in equations and inequalites of polynomials in l produces constant value on each cells. And cells cover the whole space. So, to check validity of Boolean formula it is enough to check its validity on each cell. Since value of the formula is constant in the cell it is enough to compute value at single point given by samplePoint. Above we took advantage of another property: closure of sum of cells of full dimension gives the whole space. Since sets on which assumptions and conclusion of our formula hold are closed we can gain a little extra efficiency and ignore cells of lower dimension.