reduce-historical/r38/packages/geometry/geoprover.rlg

Sun Apr 18 17:57:49 2004 run on Linux

 Geoprover  1.3a  Last update  December 30, 2002
% GeoProver test file for Reduce, created on Jan 18 2003
load cali,geoprover;


off nat;

 on echo;



%in "$reduce/packages/geometry/supp.red"$
%###############################################################
%
% FILE:    supp.red
% AUTHOR:  graebe
% CREATED: 2/2002
% PURPOSE: Interface for the extended GEO syntax to Reduce
% VERSION: $Id: supp.red,v 1.1 2002/12/26 16:27:22 compalg Exp $

algebraic procedure geo_simplify u; u;


geo_simplify$

algebraic procedure geo_normal u; u;


geo_normal$

algebraic procedure geo_subs(a,b,c); sub(a=b,c);


geo_subs$


algebraic procedure geo_gbasis(polys,vars); 
  begin 
  setring(vars,{},lex); 
  setideal(uhu,polys); 
  return gbasis uhu;
  end;


geo_gbasis$


algebraic procedure geo_groebfactor(polys,vars,nondeg); 
  begin 
  setring(vars,{},lex); 
  return groebfactor(polys,nondeg);
  end;


geo_groebfactor$


algebraic procedure geo_normalf(p,polys,vars); 
  begin 
  setring(vars,{},lex); 
  return p mod polys;
  end;


geo_normalf$


algebraic procedure geo_eliminate(polys,vars,elivars); 
  begin 
  setring(vars,{},lex); 
  return eliminate(polys,elivars);
  end;


geo_eliminate$


algebraic procedure geo_solve(polys,vars); 
  solve(polys,vars);


geo_solve$


algebraic procedure geo_solveconstrained(polys,vars,nondegs); 
  begin scalar u;
  setring(vars,{},lex); 
  u:=groebfactor(polys,nondegs);
  return for each x in u join solve(x,vars);
  end;


geo_solveconstrained$


algebraic procedure geo_eval(con,sol); 
  for each x in sol collect sub(x,con);


geo_eval$


% end;




% Example Arnon
% 
% The problem:
% Let $ABCD$ be a square and $P$ a point on the line parallel to $BD$
% through $C$ such that $l(BD)=l(BP)$, where $l(BD)$ denotes the
% distance between $B$ and $D$. Let $Q$ be the intersection point of
% $BF$ and $CD$. Show that $l(DP)=l(DQ)$.
% 
% The solution:

vars_:=List(x1, x2, x3);


vars_ := {x1,x2,x3}$

% Points
A__:=Point(0,0);


a__ := {0,0}$
 B__:=Point(1,0);


b__ := {1,0}$
 P__:=Point(x1,x2);


p__ := {x1,x2}$

% coordinates
D__:=rotate(A__,B__,1/2);


d__ := {0,1}$

C__:=par_point(D__,A__,B__);


c__ := {1,1}$
 
Q__:=varpoint(D__,C__,x3);


q__ := {x3,1}$

% polynomials
polys_:=List(on_line(P__,par_line(C__,pp_line(B__,D__))),
  eq_dist(B__,D__,B__,P__), on_line(Q__,pp_line(B__,P__)));


polys_ := {x1 + x2 - 2,
 - x1**2 + 2*x1 - x2**2 + 1,
 - x1 + x2*x3 - x2 + 1}$

% conclusion
con_:=eq_dist(D__,P__,D__,Q__);


con_ := x1**2 + x2**2 - 2*x2 - x3**2 + 1$

% solution
gb_:=geo_gbasis(polys_,vars_);


gb_ := {x3**2 + 2*x3 - 2,2*x2 - x3 - 2,2*x1 + x3 - 2}$

result_:=geo_normalf(con_,gb_,vars_);


result_ := 0$



% Example CircumCenter_1
% 
% The problem:
% The intersection point of the midpoint perpendiculars is the
% center of the circumscribed circle.
% 
% The solution:

parameters_:=List(a1, a2, b1, b2, c1, c2);


parameters_ := {a1,
a2,
b1,
b2,
c1,
c2}$

% Points
A__:=Point(a1,a2);


a__ := {a1,a2}$

B__:=Point(b1,b2);


b__ := {b1,b2}$

C__:=Point(c1,c2);


c__ := {c1,c2}$

% coordinates
M__:=intersection_point(p_bisector(A__,B__),
  p_bisector(B__,C__));


m__ := {(a1**2*b2 - a1**2*c2 + a2**2*b2 - a2**2*c2 - a2*b1**2 - a2*b2**2 + a2*c1
**2 + a2*c2**2 + b1**2*c2 + b2**2*c2 - b2*c1**2 - b2*c2**2)/(2*(a1*b2 - a1*c2 - 
a2*b1 + a2*c1 + b1*c2 - b2*c1)),
( - a1**2*b1 + a1**2*c1 + a1*b1**2 + a1*b2**2 - a1*c1**2 - a1*c2**2 - a2**2*b1 +
 a2**2*c1 - b1**2*c1 + b1*c1**2 + b1*c2**2 - b2**2*c1)/(2*(a1*b2 - a1*c2 - a2*b1
 + a2*c1 + b1*c2 - b2*c1))}$

% conclusion
result_:=List( eq_dist(M__,A__,M__,B__), eq_dist(M__,A__,M__,C__) );


result_ := {0,0}$



% Example EulerLine_1
% 
% The problem:
% Euler's line: The center $M$ of the circumscribed circle,
% the orthocenter $H$ and the barycenter $S$ are collinear and $S$
% divides $MH$ with ratio 1:2.
% 
% The solution:

parameters_:=List(a1, a2, b1, b2, c1, c2);


parameters_ := {a1,
a2,
b1,
b2,
c1,
c2}$

% Points
A__:=Point(a1,a2);


a__ := {a1,a2}$

B__:=Point(b1,b2);


b__ := {b1,b2}$

C__:=Point(c1,c2);


c__ := {c1,c2}$

% coordinates
S__:=intersection_point(median(A__,B__,C__),median(B__,C__,A__));


s__ := {(a1 + b1 + c1)/3,(a2 + b2 + c2)/3}$

M__:=intersection_point(p_bisector(A__,B__),
  p_bisector(B__,C__));


m__ := {(a1**2*b2 - a1**2*c2 + a2**2*b2 - a2**2*c2 - a2*b1**2 - a2*b2**2 + a2*c1
**2 + a2*c2**2 + b1**2*c2 + b2**2*c2 - b2*c1**2 - b2*c2**2)/(2*(a1*b2 - a1*c2 - 
a2*b1 + a2*c1 + b1*c2 - b2*c1)),
( - a1**2*b1 + a1**2*c1 + a1*b1**2 + a1*b2**2 - a1*c1**2 - a1*c2**2 - a2**2*b1 +
 a2**2*c1 - b1**2*c1 + b1*c1**2 + b1*c2**2 - b2**2*c1)/(2*(a1*b2 - a1*c2 - a2*b1
 + a2*c1 + b1*c2 - b2*c1))}$

H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__));


h__ := {( - a1*a2*b1 + a1*a2*c1 + a1*b1*b2 - a1*c1*c2 - a2**2*b2 + a2**2*c2 + a2
*b2**2 - a2*c2**2 - b1*b2*c1 + b1*c1*c2 - b2**2*c2 + b2*c2**2)/(a1*b2 - a1*c2 - 
a2*b1 + a2*c1 + b1*c2 - b2*c1),
(a1**2*b1 - a1**2*c1 + a1*a2*b2 - a1*a2*c2 - a1*b1**2 + a1*c1**2 - a2*b1*b2 + a2
*c1*c2 + b1**2*c1 + b1*b2*c2 - b1*c1**2 - b2*c1*c2)/(a1*b2 - a1*c2 - a2*b1 + a2*
c1 + b1*c2 - b2*c1)}$

% conclusion
result_:=List(is_collinear(M__,H__,S__), sqrdist(S__,fixedpoint(M__,H__,1/3)));


result_ := {0,0}$



% Example Brocard_3
% 
% The problem:
% Theorem about the Brocard points:
% Let $\Delta\,ABC$ be a triangle. The circles $c_1$ through $A,B$ and
% tangent to $g(AC)$, $c_2$ through $B,C$ and tangent to $g(AB)$, and
% $c_3$ through $A,C$ and tangent to $g(BC)$ pass through a common
% point.
% 
% The solution:

parameters_:=List(u1, u2);


parameters_ := {u1,u2}$

% Points
A__:=Point(0,0);


a__ := {0,0}$

B__:=Point(1,0);


b__ := {1,0}$

C__:=Point(u1,u2);


c__ := {u1,u2}$

% coordinates
M_1_:=intersection_point(altitude(A__,A__,C__),p_bisector(A__,B__));


m_1_ := {1/2,( - u1)/(2*u2)}$

M_2_:=intersection_point(altitude(B__,B__,A__),p_bisector(B__,C__));


m_2_ := {1,(u1**2 - 2*u1 + u2**2 + 1)/(2*u2)}$

M_3_:=intersection_point(altitude(C__,C__,B__),p_bisector(A__,C__));


m_3_ := {( - u1**2 + 2*u1 - u2**2)/2,(u1**3 - u1**2 + u1*u2**2 + u2**2)/(2*u2)}$

c1_:=pc_circle(M_1_,A__);


c1_ := {u2, - u2,u1,0}$

c2_:=pc_circle(M_2_,B__);


c2_ := {u2, - 2*u2, - u1**2 + 2*u1 - u2**2 - 1,u2}$

c3_:=pc_circle(M_3_,C__);


c3_ := {u2,
u2*(u1**2 - 2*u1 + u2**2),
 - u1**3 + u1**2 - u1*u2**2 - u2**2,
0}$

P__:=other_cc_point(B__,c1_,c2_);


p__ := {(u1**3 - u1**2 + u1*u2**2 + u1 + u2**2)/(u1**4 - 2*u1**3 + 2*u1**2*u2**2
 + 3*u1**2 - 2*u1*u2**2 - 2*u1 + u2**4 + 3*u2**2 + 1),
(u2*(u1**2 - 2*u1 + u2**2 + 1))/(u1**4 - 2*u1**3 + 2*u1**2*u2**2 + 3*u1**2 - 2*
u1*u2**2 - 2*u1 + u2**4 + 3*u2**2 + 1)}$

% conclusion
result_:= on_circle(P__,c3_);


result_ := 0$



% Example Feuerbach_1
% 
% The problem:
% Feuerbach's circle or nine-point circle: The midpoint $N$ of $MH$ is
% the center of a circle that passes through nine special points, the
% three pedal points of the altitudes, the midpoints of the sides of the
% triangle and the midpoints of the upper parts of the three altitudes.
% 
% The solution:

parameters_:=List(u1, u2, u3);


parameters_ := {u1,u2,u3}$

% Points
A__:=Point(0,0);


a__ := {0,0}$

B__:=Point(u1,0);


b__ := {u1,0}$

C__:=Point(u2,u3);


c__ := {u2,u3}$

% coordinates
H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__));


h__ := {u2,(u2*(u1 - u2))/u3}$

D__:=intersection_point(pp_line(A__,B__),pp_line(H__,C__));


d__ := {u2,0}$

M__:=intersection_point(p_bisector(A__,B__),
  p_bisector(B__,C__));


m__ := {u1/2,( - u1*u2 + u2**2 + u3**2)/(2*u3)}$

N__:=midpoint(M__,H__);


n__ := {(u1 + 2*u2)/4,(u1*u2 - u2**2 + u3**2)/(4*u3)}$

% conclusion
result_:=List( eq_dist(N__,midpoint(A__,B__),N__,midpoint(B__,C__)),
  eq_dist(N__,midpoint(A__,B__),N__,midpoint(H__,C__)),
  eq_dist(N__,midpoint(A__,B__),N__,D__) );


result_ := {0,0,0}$



% Example FeuerbachTangency_1
% 
% The problem:
% For an arbitrary triangle $\Delta\,ABC$ Feuerbach's circle (nine-point
% circle) is tangent to its 4 tangent circles.
% 
% The solution:

vars_:=List(x1, x2);


vars_ := {x1,x2}$

parameters_:=List(u1, u2);


parameters_ := {u1,u2}$

% Points
A__:=Point(0,0);


a__ := {0,0}$

B__:=Point(2,0);


b__ := {2,0}$

C__:=Point(u1,u2);


c__ := {u1,u2}$

P__:=Point(x1,x2);


p__ := {x1,x2}$

% coordinates
M__:=intersection_point(p_bisector(A__,B__), p_bisector(B__,C__));


m__ := {1,(u1**2 - 2*u1 + u2**2)/(2*u2)}$

H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__));


h__ := {u1,(u1*( - u1 + 2))/u2}$

N__:=midpoint(M__,H__);


n__ := {(u1 + 1)/2,( - u1**2 + 2*u1 + u2**2)/(4*u2)}$

c1_:=pc_circle(N__,midpoint(A__,B__));


c1_ := {2*u2,
 - 2*u2*(u1 + 1),
u1**2 - 2*u1 - u2**2,
2*u1*u2}$

Q__:=pedalpoint(P__,pp_line(A__,B__));


q__ := {x1,0}$

% polynomials
polys_:=List(on_bisector(P__,A__,B__,C__), on_bisector(P__,B__,C__,A__));


polys_ := {2*( - 2*u1*x1*x2 + 4*u1*x2 + u2*x1**2 - 4*u2*x1 - u2*x2**2 + 4*u2 + 4
*x1*x2 - 8*x2),
2*( - u1**3*x2 + u1**2*u2*x1 - u1**2*u2 + u1**2*x1*x2 + 2*u1**2*x2 - u1*u2**2*x2
 - u1*u2*x1**2 + u1*u2*x2**2 - 2*u1*x1*x2 + u2**3*x1 - u2**3 - u2**2*x1*x2 + 2*
u2**2*x2 + u2*x1**2 - u2*x2**2)}$

% conclusion
con_:=is_cc_tangent(pc_circle(P__,Q__),c1_);


con_ := 16*u2*( - u1**3*x1*x2 + u1**3*x2 + u1**2*u2*x1**2 - 2*u1**2*u2*x1 - u1**
2*u2*x2**2 + u1**2*u2 + u1**2*x1**2*x2 + u1**2*x1*x2 - 2*u1**2*x2 + u1*u2**2*x1*
x2 - u1*u2**2*x2 - 2*u1*u2*x1**3 + 4*u1*u2*x1**2 - 2*u1*u2*x1 + 2*u1*u2*x2**2 - 
2*u1*x1**2*x2 + 2*u1*x1*x2 - u2**2*x1**2*x2 + u2**2*x1*x2 + u2*x1**4 - 2*u2*x1**
3 + u2*x1**2 - u2*x2**2)$

% solution
gb_:=geo_gbasis(polys_,vars_);


gb_ := {u1**2*u2*x2**2 - 2*u1**2*x2**3 - 2*u1*u2*x2**2 + 4*u1*x2**3 + u2**3*x2**
2 - u2**3 - 2*u2**2*x2**3 + 4*u2**2*x2 + u2*x2**4 - 4*u2*x2**2,
 - u1**2*u2*x2 - 2*u1**2*x2**2 + u1*u2**2*x1 - u1*u2**2 + 2*u1*u2*x2 + 4*u1*x2**
2 - u2**2*x1 - u2**2*x2**2 + 2*u2**2 + u2*x2**3 - 4*u2*x2}$

result_:=geo_normalf(con_,gb_,vars_);


result_ := 0$



% Example GeneralizedFermatPoint_1
% 
% The problem:
% A generalized theorem about Napoleon triangles:
% Let $\Delta\,ABC$ be an arbitrary triangle and $P,Q$ and $R$ the third
% vertex of isosceles triangles with equal base angles erected
% externally on the sides $BC, AC$ and $AB$ of the triangle. Then the
% lines $g(AP), g(BQ)$ and $g(CR)$ pass through a common point.
% 
% The solution:

vars_:=List(x1, x2, x3, x4, x5);


vars_ := {x1,
x2,
x3,
x4,
x5}$

parameters_:=List(u1, u2, u3);


parameters_ := {u1,u2,u3}$

% Points
A__:=Point(0,0);


a__ := {0,0}$

B__:=Point(2,0);


b__ := {2,0}$

C__:=Point(u1,u2);


c__ := {u1,u2}$

P__:=Point(x1,x2);


p__ := {x1,x2}$

Q__:=Point(x3,x4);


q__ := {x3,x4}$

R__:=Point(x5,u3);


r__ := {x5,u3}$

% polynomials
polys_:=List(eq_dist(P__,B__,P__,C__), 
  eq_dist(Q__,A__,Q__,C__),  
  eq_dist(R__,A__,R__,B__), 
  eq_angle(R__,A__,B__,P__,B__,C__), 
  eq_angle(Q__,C__,A__,P__,B__,C__));


polys_ := { - u1**2 + 2*u1*x1 - u2**2 + 2*u2*x2 - 4*x1 + 4,
 - u1**2 + 2*u1*x3 - u2**2 + 2*u2*x4,
4*(x5 - 1),
(u1*u3*x1 - 2*u1*u3 - u1*x2*x5 + u2*u3*x2 + u2*x1*x5 - 2*u2*x5 - 2*u3*x1 + 4*u3 
+ 2*x2*x5)/(x5*(u1*x1 - 2*u1 + u2*x2 - 2*x1 + 4)),
( - u1**3*x2 + u1**2*u2*x1 - 2*u1**2*u2 - u1**2*x1*x4 + u1**2*x2*x3 + 2*u1**2*x2
 + 2*u1**2*x4 - u1*u2**2*x2 + 2*u1*x1*x4 - 2*u1*x2*x3 - 4*u1*x4 + u2**3*x1 - 2*
u2**3 - u2**2*x1*x4 + u2**2*x2*x3 + 2*u2**2*x2 + 2*u2**2*x4 - 2*u2*x1*x3 - 2*u2*
x2*x4 + 4*u2*x3)/(u1**3*x1 - 2*u1**3 + u1**2*u2*x2 - u1**2*x1*x3 - 2*u1**2*x1 + 
2*u1**2*x3 + 4*u1**2 + u1*u2**2*x1 - 2*u1*u2**2 - u1*u2*x1*x4 - u1*u2*x2*x3 + 2*
u1*u2*x4 + 2*u1*x1*x3 - 4*u1*x3 + u2**3*x2 - 2*u2**2*x1 - u2**2*x2*x4 + 4*u2**2 
+ 2*u2*x1*x4 - 4*u2*x4)}$

% conclusion
con_:=is_concurrent(pp_line(A__,P__), pp_line(B__,Q__), pp_line(C__,R__));


con_ :=  - u1*u3*x1*x4 + u1*u3*x2*x3 - 2*u1*u3*x2 + 2*u1*x2*x4 + u2*x1*x4*x5 - 2
*u2*x1*x4 - u2*x2*x3*x5 + 2*u2*x2*x5 + 2*u3*x1*x4 - 2*x2*x4*x5$

% solution
sol_:=geo_solve(polys_,vars_);


sol_ := {{x1=(u1 - u2*u3 + 2)/2,
x2=(u1*u3 + u2 - 2*u3)/2,
x3=(u1 + u2*u3)/2,
x4=( - u1*u3 + u2)/2,
x5=1}}$

result_:=geo_eval(con_,sol_);


result_ := {0}$



% Example TaylorCircle_1
% 
% The problem:
% Let $\Delta\,ABC$ be an arbitrary triangle. Consider the three
% altitude pedal points and the pedal points of the perpendiculars from
% these points onto the the opposite sides of the triangle. Show that
% these 6 points are on a common circle, the {\em Taylor circle}.
% 
% The solution:

parameters_:=List(u1, u2, u3);


parameters_ := {u1,u2,u3}$

% Points
A__:=Point(u1,0);


a__ := {u1,0}$

B__:=Point(u2,0);


b__ := {u2,0}$

C__:=Point(0,u3);


c__ := {0,u3}$

% coordinates
P__:=pedalpoint(A__,pp_line(B__,C__));


p__ := {(u2*(u1*u2 + u3**2))/(u2**2 + u3**2),
(u2*u3*( - u1 + u2))/(u2**2 + u3**2)}$

Q__:=pedalpoint(B__,pp_line(A__,C__));


q__ := {(u1*(u1*u2 + u3**2))/(u1**2 + u3**2),
(u1*u3*(u1 - u2))/(u1**2 + u3**2)}$

R__:=pedalpoint(C__,pp_line(A__,B__));


r__ := {0,0}$

P_1_:=pedalpoint(P__,pp_line(A__,B__));


p_1_ := {(u2*(u1*u2 + u3**2))/(u2**2 + u3**2),0}$

P_2_:=pedalpoint(P__,pp_line(A__,C__));


p_2_ := {(u1*(u1**2*u2**2 + 2*u1*u2*u3**2 + u3**4))/(u1**2*u2**2 + u1**2*u3**2 +
 u2**2*u3**2 + u3**4),
(u3**3*(u1**2 - 2*u1*u2 + u2**2))/(u1**2*u2**2 + u1**2*u3**2 + u2**2*u3**2 + u3
**4)}$

Q_1_:=pedalpoint(Q__,pp_line(A__,B__));


q_1_ := {(u1*(u1*u2 + u3**2))/(u1**2 + u3**2),0}$

Q_2_:=pedalpoint(Q__,pp_line(B__,C__));


q_2_ := {(u2*(u1**2*u2**2 + 2*u1*u2*u3**2 + u3**4))/(u1**2*u2**2 + u1**2*u3**2 +
 u2**2*u3**2 + u3**4),
(u3**3*(u1**2 - 2*u1*u2 + u2**2))/(u1**2*u2**2 + u1**2*u3**2 + u2**2*u3**2 + u3
**4)}$

R_1_:=pedalpoint(R__,pp_line(A__,C__));


r_1_ := {(u1*u3**2)/(u1**2 + u3**2),(u1**2*u3)/(u1**2 + u3**2)}$

R_2_:=pedalpoint(R__,pp_line(B__,C__));


r_2_ := {(u2*u3**2)/(u2**2 + u3**2),(u2**2*u3)/(u2**2 + u3**2)}$

% conclusion
result_:=List( is_concyclic(P_1_,P_2_,Q_1_,Q_2_), 
  is_concyclic(P_1_,P_2_,Q_1_,R_1_),
  is_concyclic(P_1_,P_2_,Q_1_,R_2_));


result_ := {0,0,0}$



% Example Miquel_1
% 
% The problem:
% Miquels theorem: Let $\Delta\,ABC$ be a triangle. Fix arbitrary points
% $P,Q,R$ on the sides $AB, BC, AC$. Then the three circles through each
% vertex and the chosen points on adjacent sides pass through a common
% point.
% 
% The solution:

parameters_:=List(c1, c2, u1, u2, u3);


parameters_ := {c1,
c2,
u1,
u2,
u3}$

% Points
A__:=Point(0,0);


a__ := {0,0}$

B__:=Point(1,0);


b__ := {1,0}$

C__:=Point(c1,c2);


c__ := {c1,c2}$

% coordinates
P__:=varpoint(A__,B__,u1);


p__ := {u1,0}$

Q__:=varpoint(B__,C__,u2);


q__ := {c1*u2 - u2 + 1,c2*u2}$

R__:=varpoint(A__,C__,u3);


r__ := {c1*u3,c2*u3}$

X__:=other_cc_point(P__,p3_circle(A__,P__,R__),p3_circle(B__,P__,Q__));


x__ := {( - c1**4*u2*u3 + c1**4*u3**2 + c1**3*u1*u2 - c1**3*u1*u3 + 2*c1**3*u2*
u3 - c1**3*u3 - 2*c1**2*c2**2*u2*u3 + 2*c1**2*c2**2*u3**2 - 2*c1**2*u1*u2 - c1**
2*u1*u3 + c1**2*u1 - c1**2*u2*u3 + c1**2*u3 + c1*c2**2*u1*u2 - c1*c2**2*u1*u3 + 
2*c1*c2**2*u2*u3 - c1*c2**2*u3 + c1*u1**2 + c1*u1*u2 - c1*u1 - c2**4*u2*u3 + c2
**4*u3**2 - c2**2*u1*u3 + c2**2*u1 - c2**2*u2*u3 + c2**2*u3)/(c1**4*u2**2 - 2*c1
**4*u2*u3 + c1**4*u3**2 - 4*c1**3*u2**2 + 4*c1**3*u2*u3 + 2*c1**3*u2 - 2*c1**3*
u3 + 2*c1**2*c2**2*u2**2 - 4*c1**2*c2**2*u2*u3 + 2*c1**2*c2**2*u3**2 + 2*c1**2*
u1*u2 - 2*c1**2*u1*u3 + 6*c1**2*u2**2 - 2*c1**2*u2*u3 - 6*c1**2*u2 + 2*c1**2*u3 
+ c1**2 - 4*c1*c2**2*u2**2 + 4*c1*c2**2*u2*u3 + 2*c1*c2**2*u2 - 2*c1*c2**2*u3 - 
4*c1*u1*u2 + 2*c1*u1 - 4*c1*u2**2 + 6*c1*u2 - 2*c1 + c2**4*u2**2 - 2*c2**4*u2*u3
 + c2**4*u3**2 + 2*c2**2*u1*u2 - 2*c2**2*u1*u3 + 2*c2**2*u2**2 - 2*c2**2*u2*u3 -
 2*c2**2*u2 + 2*c2**2*u3 + c2**2 + u1**2 + 2*u1*u2 - 2*u1 + u2**2 - 2*u2 + 1),
(c2*(c1**2*u1*u2 - c1**2*u1*u3 + c1**2*u3 - 2*c1*u1*u2 + c2**2*u1*u2 - c2**2*u1*
u3 + c2**2*u3 + u1**2 + u1*u2 - u1))/(c1**4*u2**2 - 2*c1**4*u2*u3 + c1**4*u3**2 
- 4*c1**3*u2**2 + 4*c1**3*u2*u3 + 2*c1**3*u2 - 2*c1**3*u3 + 2*c1**2*c2**2*u2**2 
- 4*c1**2*c2**2*u2*u3 + 2*c1**2*c2**2*u3**2 + 2*c1**2*u1*u2 - 2*c1**2*u1*u3 + 6*
c1**2*u2**2 - 2*c1**2*u2*u3 - 6*c1**2*u2 + 2*c1**2*u3 + c1**2 - 4*c1*c2**2*u2**2
 + 4*c1*c2**2*u2*u3 + 2*c1*c2**2*u2 - 2*c1*c2**2*u3 - 4*c1*u1*u2 + 2*c1*u1 - 4*
c1*u2**2 + 6*c1*u2 - 2*c1 + c2**4*u2**2 - 2*c2**4*u2*u3 + c2**4*u3**2 + 2*c2**2*
u1*u2 - 2*c2**2*u1*u3 + 2*c2**2*u2**2 - 2*c2**2*u2*u3 - 2*c2**2*u2 + 2*c2**2*u3 
+ c2**2 + u1**2 + 2*u1*u2 - 2*u1 + u2**2 - 2*u2 + 1)}$

% conclusion
result_:=on_circle(X__,p3_circle(C__,Q__,R__));


result_ := 0$



% Example PappusPoint_1
% 
% The problem:
% Let $A,B,C$ and $P,Q,R$ be two triples of collinear points. Then by
% the Theorem of Pappus the intersection points $g(AQ)\wedge g(BP),
% g(AR)\wedge g(CP)$ and $g(BR)\wedge g(CQ)$ are collinear. 
% 
% Permuting $P,Q,R$ we get six such {\em Pappus lines}.  Those
% corresponding to even resp. odd permutations are concurrent.
% 
% The solution:

parameters_:=List(u1, u2, u3, u4, u5, u6, u7, u8);


parameters_ := {u1,
u2,
u3,
u4,
u5,
u6,
u7,
u8}$

% Points
A__:=Point(u1,0);


a__ := {u1,0}$

B__:=Point(u2,0);


b__ := {u2,0}$

P__:=Point(u4,u5);


p__ := {u4,u5}$

Q__:=Point(u6,u7);


q__ := {u6,u7}$

% coordinates
C__:=varpoint(A__,B__,u3);


c__ := { - u1*u3 + u1 + u2*u3,0}$

R__:=varpoint(P__,Q__,u8);


r__ := { - u4*u8 + u4 + u6*u8, - u5*u8 + u5 + u7*u8}$

% conclusion
result_:=is_concurrent(pappus_line(A__,B__,C__,P__,Q__,R__),
  pappus_line(A__,B__,C__,Q__,R__,P__), 
  pappus_line(A__,B__,C__,R__,P__,Q__));


result_ := 0$



% Example IMO/36_1
% 
% The problem:
% Let $A,B,C,D$ be four distinct points on a line, in that order. The
% circles with diameters $AC$ and $BD$ intersect at the points $X$ and
% $Y$. The line $XY$ meets $BC$ at the point $Z$. Let $P$ be a point on
% the line $XY$ different from $Z$. The line $CP$ intersects the circle
% with diameter $AC$ at the points $C$ and $M$, and the line $BP$
% intersects the circle with diameter $BD$ at the points $B$ and
% $N$. Prove that the lines $AM, DN$ and $XY$ are concurrent.
% 
% The solution:

vars_:=List(x1, x2, x3, x4, x5, x6);


vars_ := {x1,
x2,
x3,
x4,
x5,
x6}$

parameters_:=List(u1, u2, u3);


parameters_ := {u1,u2,u3}$

% Points
X__:=Point(0,1);


x__ := {0,1}$

Y__:=Point(0,-1);


y__ := {0,-1}$

M__:=Point(x1,x2);


m__ := {x1,x2}$

N__:=Point(x3,x4);


n__ := {x3,x4}$

% coordinates
P__:=varpoint(X__,Y__,u3);


p__ := {0, - 2*u3 + 1}$

Z__:=midpoint(X__,Y__);


z__ := {0,0}$

l_:=p_bisector(X__,Y__);


l_ := {0,1,0}$

B__:=line_slider(l_,u1);


b__ := {u1,0}$

C__:=line_slider(l_,u2);


c__ := {u2,0}$

A__:=line_slider(l_,x5);


a__ := {x5,0}$

D__:=line_slider(l_,x6);


d__ := {x6,0}$

% polynomials
polys_:=List(is_concyclic(X__,Y__,B__,N__), is_concyclic(X__,Y__,C__,M__),
  is_concyclic(X__,Y__,B__,D__), is_concyclic(X__,Y__,C__,A__),
  is_collinear(B__,P__,N__), is_collinear(C__,P__,M__));


polys_ := { - u1**2*x3 + u1*x3**2 + u1*x4**2 - u1 + x3,
 - u2**2*x1 + u2*x1**2 + u2*x2**2 - u2 + x1,
 - u1**2*x6 + u1*x6**2 - u1 + x6,
 - u2**2*x5 + u2*x5**2 - u2 + x5,
 - 2*u1*u3 - u1*x4 + u1 + 2*u3*x3 - x3,
 - 2*u2*u3 - u2*x2 + u2 + 2*u3*x1 - x1}$

% constraints
nondeg_:=List(x5-u2,x1-u2,x6-u1,x3-u1);


nondeg_ := { - u2 + x5,
 - u2 + x1,
 - u1 + x6,
 - u1 + x3}$

% conclusion
con_:=is_concurrent(pp_line(A__,M__),pp_line(D__,N__),pp_line(X__,Y__));


con_ :=  - x1*x4*x6 + x2*x3*x5 - x2*x5*x6 + x4*x5*x6$

% solution
sol_:=geo_solveconstrained(polys_,vars_,nondeg_);


sol_ := {{x1=(4*u2*u3**2 - 4*u2*u3)/(u2**2 + 4*u3**2 - 4*u3 + 1),
x2=( - 2*u2**2*u3 + u2**2 - 2*u3 + 1)/(u2**2 + 4*u3**2 - 4*u3 + 1),
x3=(4*u1*u3**2 - 4*u1*u3)/(u1**2 + 4*u3**2 - 4*u3 + 1),
x4=( - 2*u1**2*u3 + u1**2 - 2*u3 + 1)/(u1**2 + 4*u3**2 - 4*u3 + 1),
x5=( - 1)/u2,
x6=( - 1)/u1}}$

result_:=geo_eval(con_,sol_);


result_ := {0}$



% Example IMO/43_2
% 
% The problem:
% 
% No verbal problem description available
% 
% The solution:

vars_:=List(x1, x2);


vars_ := {x1,x2}$

parameters_:=List(u1);


parameters_ := {u1}$

% Points
B__:=Point(-1,0);


b__ := {-1,0}$

C__:=Point(1,0);


c__ := {1,0}$

% coordinates
O__:=midpoint(B__,C__);


o__ := {0,0}$

gamma_:=pc_circle(O__,B__);


gamma_ := {1,0,0,-1}$

D__:=circle_slider(O__,B__,u1);


d__ := {( - u1**2 + 1)/(u1**2 + 1),(2*u1)/(u1**2 + 1)}$

E__:=circle_slider(O__,B__,x1);


e__ := {( - x1**2 + 1)/(x1**2 + 1),(2*x1)/(x1**2 + 1)}$

F__:=circle_slider(O__,B__,x2);


f__ := {( - x2**2 + 1)/(x2**2 + 1),(2*x2)/(x2**2 + 1)}$

A__:=sym_point(B__,pp_line(O__,D__));


a__ := {( - u1**4 + 6*u1**2 - 1)/(u1**4 + 2*u1**2 + 1),(4*u1*(u1**2 - 1))/(u1**4
 + 2*u1**2 + 1)}$

J__:=intersection_point(pp_line(A__,C__), par_line(O__, pp_line(A__,D__)));


j__ := {(2*(3*u1**2 - 1))/(u1**4 + 2*u1**2 + 1),(2*u1*(u1**2 - 3))/(u1**4 + 2*u1
**2 + 1)}$

m_:=p_bisector(O__,A__);


m_ := {2*(u1**4 - 6*u1**2 + 1),8*u1*( - u1**2 + 1),u1**4 + 2*u1**2 + 1}$

P_1_:=pedalpoint(J__,m_);


p_1_ := {( - u1**8 + 20*u1**6 + 10*u1**4 - 12*u1**2 - 1)/(2*(u1**8 + 4*u1**6 + 6
*u1**4 + 4*u1**2 + 1)),
(4*u1**3*(u1**4 - 2*u1**2 - 3))/(u1**8 + 4*u1**6 + 6*u1**4 + 4*u1**2 + 1)}$

P_2_:=pedalpoint(J__,pp_line(C__,E__));


p_2_ := {(u1**4 - 2*u1**3*x1 + 6*u1**2*x1**2 + 2*u1**2 + 6*u1*x1 - 2*x1**2 + 1)/
(u1**4*x1**2 + u1**4 + 2*u1**2*x1**2 + 2*u1**2 + x1**2 + 1),
(u1**4*x1 + 2*u1**3 - 4*u1**2*x1 - 6*u1 + 3*x1)/(u1**4*x1**2 + u1**4 + 2*u1**2*
x1**2 + 2*u1**2 + x1**2 + 1)}$

P_3_:=pedalpoint(J__,pp_line(C__,F__));


p_3_ := {(u1**4 - 2*u1**3*x2 + 6*u1**2*x2**2 + 2*u1**2 + 6*u1*x2 - 2*x2**2 + 1)/
(u1**4*x2**2 + u1**4 + 2*u1**2*x2**2 + 2*u1**2 + x2**2 + 1),
(u1**4*x2 + 2*u1**3 - 4*u1**2*x2 - 6*u1 + 3*x2)/(u1**4*x2**2 + u1**4 + 2*u1**2*
x2**2 + 2*u1**2 + x2**2 + 1)}$

% polynomials
polys_:=List(on_line(E__,m_), on_line(F__,m_));


polys_ := {( - u1**4*x1**2 + 3*u1**4 - 16*u1**3*x1 + 14*u1**2*x1**2 - 10*u1**2 +
 16*u1*x1 - x1**2 + 3)/(x1**2 + 1),
( - u1**4*x2**2 + 3*u1**4 - 16*u1**3*x2 + 14*u1**2*x2**2 - 10*u1**2 + 16*u1*x2 -
 x2**2 + 3)/(x2**2 + 1)}$

% constraints
nondegs_:=List(x1-x2);


nondegs_ := {x1 - x2}$

% conclusion
con_:=List(eq_dist(J__,P_1_,J__,P_2_), eq_dist(J__,P_1_,J__,P_3_));


con_ := {(u1**8*x1**4 - 2*u1**8*x1**2 - 3*u1**8 + 16*u1**7*x1**3 + 16*u1**7*x1 -
 20*u1**6*x1**4 + 8*u1**6*x1**2 + 28*u1**6 - 112*u1**5*x1**3 - 112*u1**5*x1 + 94
*u1**4*x1**4 + 4*u1**4*x1**2 - 90*u1**4 + 240*u1**3*x1**3 + 240*u1**3*x1 - 132*
u1**2*x1**4 - 24*u1**2*x1**2 + 108*u1**2 - 144*u1*x1**3 - 144*u1*x1 + 9*x1**4 - 
18*x1**2 - 27)/(4*(u1**8*x1**4 + 2*u1**8*x1**2 + u1**8 + 4*u1**6*x1**4 + 8*u1**6
*x1**2 + 4*u1**6 + 6*u1**4*x1**4 + 12*u1**4*x1**2 + 6*u1**4 + 4*u1**2*x1**4 + 8*
u1**2*x1**2 + 4*u1**2 + x1**4 + 2*x1**2 + 1)),
(u1**8*x2**4 - 2*u1**8*x2**2 - 3*u1**8 + 16*u1**7*x2**3 + 16*u1**7*x2 - 20*u1**6
*x2**4 + 8*u1**6*x2**2 + 28*u1**6 - 112*u1**5*x2**3 - 112*u1**5*x2 + 94*u1**4*x2
**4 + 4*u1**4*x2**2 - 90*u1**4 + 240*u1**3*x2**3 + 240*u1**3*x2 - 132*u1**2*x2**
4 - 24*u1**2*x2**2 + 108*u1**2 - 144*u1*x2**3 - 144*u1*x2 + 9*x2**4 - 18*x2**2 -
 27)/(4*(u1**8*x2**4 + 2*u1**8*x2**2 + u1**8 + 4*u1**6*x2**4 + 8*u1**6*x2**2 + 4
*u1**6 + 6*u1**4*x2**4 + 12*u1**4*x2**2 + 6*u1**4 + 4*u1**2*x2**4 + 8*u1**2*x2**
2 + 4*u1**2 + x2**4 + 2*x2**2 + 1))}$

% solution
sol_:=geo_solveconstrained(polys_,vars_,nondegs_);


sol_ := {{x1=(sqrt(3)*u1**4 + 2*sqrt(3)*u1**2 + sqrt(3) - 8*u1**3 + 8*u1)/(u1**4
 - 14*u1**2 + 1),
x2=(sqrt(3)*u1**4 + 2*sqrt(3)*u1**2 + sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*u1**
2 + 1)},
{x1=(sqrt(3)*u1**4 + 2*sqrt(3)*u1**2 + sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*u1
**2 + 1),
x2=( - sqrt(3)*u1**4 - 2*sqrt(3)*u1**2 - sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*
u1**2 + 1)},
{x1=( - sqrt(3)*u1**4 - 2*sqrt(3)*u1**2 - sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*
u1**2 + 1),
x2=(sqrt(3)*u1**4 + 2*sqrt(3)*u1**2 + sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*u1**
2 + 1)},
{x1=( - sqrt(3)*u1**4 - 2*sqrt(3)*u1**2 - sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*
u1**2 + 1),
x2=( - sqrt(3)*u1**4 - 2*sqrt(3)*u1**2 - sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*
u1**2 + 1)}}$
 
result_:=geo_simplify(geo_eval(con_,sol_));


result_ := {{0,0},{0,0},{0,0},{0,0}}$



showtime;


Time: 670 ms  plus GC time: 60 ms

end;


Time for test: 670 ms, plus GC time: 60 ms