Skip to main content
deleted 4 characters in body
Source Link
Reid Barton
  • 25.2k
  • 1
  • 76
  • 133
=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.53, 16 Jul 2009
                                                       
                          by                           
                       Hoon Hong                       
                  ([email protected])                
                                                       
With contributions by: Christopher W. Brown, George E. 
Collins, Mark J. Encarnacion, Jeremy R. Johnson        
Werner Krandick, Richard Liska, Scott McCallum,        
Nicolas Robidoux, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[ area of middle pentagon ]
Enter a variable list:
(a,x1,y1,x2,y2)
Enter the number of free variables:
1
Enter a prenex formula:
(E x1)(E y1)(E x2)(E y2)[ [ a >= 1/2 /\ a <= 3/4 ] /\
                          x1 > 0 /\ y1 > 0 /\ 1 - x1 - y1 < 0 /\
                          x2 > 0 /\ x2 y1 + y2 - x1 y2 - y1 < 0 /\ x1 + x2 y1 - x2 - x1 y2 < 0 /\
                          a (1/2)(y1 + x1 y2 - x2 y1 + x2) = (1/8)(0 - 1 + x1 + 2 x2 + 2 y1 + y2 + 2 x1 y2 - 2 x2 y1) ].

=======================================================

Before Normalization >
finish

An equivalent quantifier-free formula:

2 a - 1 > 0 /\ 4 a - 3 < 0


=====================  The End  =======================

-----------------------------------------------------------------------------
12 Garbage collections, 473385670 Cells and 0 Arrays reclaimed, in 8158 milliseconds.
1345504 Cells in AVAIL, 40000000 Cells in SPACE.

System time: 79624 milliseconds.
System time after the initialization: 79028 milliseconds.
-----------------------------------------------------------------------------
=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.53, 16 Jul 2009
                                                       
                          by                           
                       Hoon Hong                       
                  ([email protected])                
                                                       
With contributions by: Christopher W. Brown, George E. 
Collins, Mark J. Encarnacion, Jeremy R. Johnson        
Werner Krandick, Richard Liska, Scott McCallum,        
Nicolas Robidoux, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[ area of middle pentagon ]
Enter a variable list:
(a,x1,y1,x2,y2)
Enter the number of free variables:
1
Enter a prenex formula:
(E x1)(E y1)(E x2)(E y2)[ [ a >= 1/2 /\ a <= 3/4 ] /\
                          x1 > 0 /\ y1 > 0 /\ 1 - x1 - y1 < 0 /\
                          x2 > 0 /\ x2 y1 + y2 - x1 y2 - y1 < 0 /\ x1 + x2 y1 - x2 - x1 y2 < 0 /\
                          a (1/2)(y1 + x1 y2 - x2 y1 + x2) = (1/8)(0 - 1 + x1 + 2 x2 + 2 y1 + y2 + 2 x1 y2 - 2 x2 y1) ].

=======================================================

Before Normalization >
finish

An equivalent quantifier-free formula:

2 a - 1 > 0 /\ 4 a - 3 < 0


=====================  The End  =======================

-----------------------------------------------------------------------------
12 Garbage collections, 473385670 Cells and 0 Arrays reclaimed, in 8158 milliseconds.
1345504 Cells in AVAIL, 40000000 Cells in SPACE.

System time: 79624 milliseconds.
System time after the initialization: 79028 milliseconds.
-----------------------------------------------------------------------------
=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.53, 16 Jul 2009
                                                       
                          by                           
                       Hoon Hong                       
                  ([email protected])                
                                                       
With contributions by: Christopher W. Brown, George E. 
Collins, Mark J. Encarnacion, Jeremy R. Johnson        
Werner Krandick, Richard Liska, Scott McCallum,        
Nicolas Robidoux, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[ area of middle pentagon ]
Enter a variable list:
(a,x1,y1,x2,y2)
Enter the number of free variables:
1
Enter a prenex formula:
(E x1)(E y1)(E x2)(E y2)[ a >= 1/2 /\ a <= 3/4 /\
                          x1 > 0 /\ y1 > 0 /\ 1 - x1 - y1 < 0 /\
                          x2 > 0 /\ x2 y1 + y2 - x1 y2 - y1 < 0 /\ x1 + x2 y1 - x2 - x1 y2 < 0 /\
                          a (1/2)(y1 + x1 y2 - x2 y1 + x2) = (1/8)(0 - 1 + x1 + 2 x2 + 2 y1 + y2 + 2 x1 y2 - 2 x2 y1) ].

=======================================================

Before Normalization >
finish

An equivalent quantifier-free formula:

2 a - 1 > 0 /\ 4 a - 3 < 0


=====================  The End  =======================

-----------------------------------------------------------------------------
12 Garbage collections, 473385670 Cells and 0 Arrays reclaimed, in 8158 milliseconds.
1345504 Cells in AVAIL, 40000000 Cells in SPACE.

System time: 79624 milliseconds.
System time after the initialization: 79028 milliseconds.
-----------------------------------------------------------------------------
added 82 characters in body
Source Link
Reid Barton
  • 25.2k
  • 1
  • 76
  • 133

I used qepcad to verifycompute that there are no convex pentagons for which this ratiothe intersection of areasthe set of possible area ratios with the interval [1/2, 3/4] is 1(1/2 or, 3/4). Since the set of possible area ratios is the image of a connected space under a continuous function, and we know the set contains (1/2, 3/4), but not 1/2 or 3/4, it must equal (1/2, 3/4). Here is a log of the qepcad session.

=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.53, 16 Jul 2009
                                                       
                          by                           
                       Hoon Hong                       
                  ([email protected])                
                                                       
With contributions by: Christopher W. Brown, George E. 
Collins, Mark J. Encarnacion, Jeremy R. Johnson        
Werner Krandick, Richard Liska, Scott McCallum,        
Nicolas Robidoux, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[ area of middle pentagon ]
Enter a variable list:
(a,x1,y1,x2,y2)
Enter the number of free variables:
1
Enter a prenex formula:
(E x1)(E y1)(E x2)(E y2)[ [ a =>= 1/2 \/\ a =<= 3/4 ] /\
                          x1 > 0 /\ y1 > 0 /\ 1 - x1 - y1 < 0 /\
                          x2 > 0 /\ x2 y1 + y2 - x1 y2 - y1 < 0 /\ x1 + x2 y1 - x2 - x1 y2 < 0 /\
                          a (1/2)(y1 + x1 y2 - x2 y1 + x2) = (1/8)(0 - 1 + x1 + 2 x2 + 2 y1 + y2 + 2 x1 y2 - 2 x2 y1) ].
 

=======================================================

Before Normalization >
finish

An equivalent quantifier-free formula:

FALSE2 a - 1 > 0 /\ 4 a - 3 < 0


=====================  The End  =======================

-----------------------------------------------------------------------------
312 Garbage collections, 1229018473385670 Cells and 0 Arrays reclaimed, in 248158 milliseconds.
981901345504 Cells in AVAIL, 50000040000000 Cells in SPACE.

System time: 29279624 milliseconds.
System time after the initialization: 26479028 milliseconds.
-----------------------------------------------------------------------------

I used qepcad to verify that there are no convex pentagons for which this ratio of areas is 1/2 or 3/4. Since the set of possible area ratios is the image of a connected space under a continuous function, and we know the set contains (1/2, 3/4), it must equal (1/2, 3/4). Here is a log of the qepcad session.

=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.53, 16 Jul 2009
                                                       
                          by                           
                       Hoon Hong                       
                  ([email protected])                
                                                       
With contributions by: Christopher W. Brown, George E. 
Collins, Mark J. Encarnacion, Jeremy R. Johnson        
Werner Krandick, Richard Liska, Scott McCallum,        
Nicolas Robidoux, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[ area of middle pentagon ]
Enter a variable list:
(a,x1,y1,x2,y2)
Enter the number of free variables:
1
Enter a prenex formula:
(E x1)(E y1)(E x2)(E y2)[ [ a = 1/2 \/ a = 3/4 ] /\
                          x1 > 0 /\ y1 > 0 /\ 1 - x1 - y1 < 0 /\
                          x2 > 0 /\ x2 y1 + y2 - x1 y2 - y1 < 0 /\ x1 + x2 y1 - x2 - x1 y2 < 0 /\
                          a (1/2)(y1 + x1 y2 - x2 y1 + x2) = (1/8)(0 - 1 + x1 + 2 x2 + 2 y1 + y2 + 2 x1 y2 - 2 x2 y1) ].
 

=======================================================

Before Normalization >
finish

An equivalent quantifier-free formula:

FALSE


=====================  The End  =======================

-----------------------------------------------------------------------------
3 Garbage collections, 1229018 Cells and 0 Arrays reclaimed, in 24 milliseconds.
98190 Cells in AVAIL, 500000 Cells in SPACE.

System time: 292 milliseconds.
System time after the initialization: 264 milliseconds.
-----------------------------------------------------------------------------

I used qepcad to compute that the intersection of the set of possible area ratios with the interval [1/2, 3/4] is (1/2, 3/4). Since the set of possible area ratios is the image of a connected space under a continuous function, and we know the set contains (1/2, 3/4), but not 1/2 or 3/4, it must equal (1/2, 3/4). Here is a log of the qepcad session.

=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.53, 16 Jul 2009
                                                       
                          by                           
                       Hoon Hong                       
                  ([email protected])                
                                                       
With contributions by: Christopher W. Brown, George E. 
Collins, Mark J. Encarnacion, Jeremy R. Johnson        
Werner Krandick, Richard Liska, Scott McCallum,        
Nicolas Robidoux, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[ area of middle pentagon ]
Enter a variable list:
(a,x1,y1,x2,y2)
Enter the number of free variables:
1
Enter a prenex formula:
(E x1)(E y1)(E x2)(E y2)[ [ a >= 1/2 /\ a <= 3/4 ] /\
                          x1 > 0 /\ y1 > 0 /\ 1 - x1 - y1 < 0 /\
                          x2 > 0 /\ x2 y1 + y2 - x1 y2 - y1 < 0 /\ x1 + x2 y1 - x2 - x1 y2 < 0 /\
                          a (1/2)(y1 + x1 y2 - x2 y1 + x2) = (1/8)(0 - 1 + x1 + 2 x2 + 2 y1 + y2 + 2 x1 y2 - 2 x2 y1) ].

=======================================================

Before Normalization >
finish

An equivalent quantifier-free formula:

2 a - 1 > 0 /\ 4 a - 3 < 0


=====================  The End  =======================

-----------------------------------------------------------------------------
12 Garbage collections, 473385670 Cells and 0 Arrays reclaimed, in 8158 milliseconds.
1345504 Cells in AVAIL, 40000000 Cells in SPACE.

System time: 79624 milliseconds.
System time after the initialization: 79028 milliseconds.
-----------------------------------------------------------------------------
added 6 characters in body
Source Link
Reid Barton
  • 25.2k
  • 1
  • 76
  • 133

I used qepcad to verify that there are no convex pentagons for which this ratio of areas is 1/2 or 3/4. Since the set of possible areasarea ratios is the image of a connected space under a continuous function, and we know the set contains (1/2, 3/4), it must equal (1/2, 3/4). Here is a log of the qepcad session.

I used qepcad to verify that there are no convex pentagons for which this ratio of areas is 1/2 or 3/4. Since the set of possible areas is the image of a connected space under a continuous function, and we know the set contains (1/2, 3/4), it must equal (1/2, 3/4). Here is a log of the qepcad session.

I used qepcad to verify that there are no convex pentagons for which this ratio of areas is 1/2 or 3/4. Since the set of possible area ratios is the image of a connected space under a continuous function, and we know the set contains (1/2, 3/4), it must equal (1/2, 3/4). Here is a log of the qepcad session.

Source Link
Reid Barton
  • 25.2k
  • 1
  • 76
  • 133
Loading