Example with QEPCAD program

 

• formula is quantified for all TGX and TGY;

  inputs , outputs

      =======================================================
  
                       Quantifier Elimination
                                 in
                   Elementary Algebra and Geometry
                                 by
             Partial Cylindrical Algebraic Decomposition
  
                      Version 10 (Interactive)
                              June 1992
  
                                 by
                             Hoon Hong
                       (hhong@risc.uni-linz.ac.at)
              Research Institute for Symbolic Computation
  
      =======================================================
  
      <<QEPCAD>> Enter an informal description  between '[' and ']':

  [Wendr M2, 1. factor<=0]
  

      <<QEPCAD>> Enter a variable list:

  (A,B,TGX,TGY)
  

      <<QEPCAD>> Enter the number of free variables:

  2
  

      <<QEPCAD>> Enter a prenex formula:

  (A TGX) (A TGY) 
   
      (
        A + B <= 1 / A + B >= -1 / A - B <= 1 / A - B >= -1 
   
        /\
        (
      A^2 TGX^2 (TGY^2 + 1) + 2 A B TGX TGY ( - TGX TGY + 1) + A TGX^2 ( 
   
      TGY^2 + 1) + B^2 TGY^2 (TGX^2 + 1) - B TGY^2 (TGX^2 + 1) <= 0 
   
        )
      ). 
  

      =======================================================
  
  
      <<QEPCAD>> Before Normalization>>

  finish
  

      =======================================================
  
  
      An equivalent quantifier-free formula:
  
      ( A <= 0 /\ B >= 0 /\ B + A - 1 <= 0 /\ B + A + 1 >= 0 /\ \\
        B - A + 1 >= 0 /\ B - A - 1 <= 0 )