# Singular

Procedure from library `grobcov.lib` (see grobcov_lib).

Usage:
ADGT(ideal H, ideal T, ideal H1,ideal T1[,options]);
H: ideal in Q[a][x] hypothesis
T: ideal in Q[a][x] thesis
H1: ideal in Q[a][x] negative hypothesis, only dependent on [a] T1: ideal in Q[a][x] negative thesis
of the Proposition (H and not H1) => (T and not T1)

Return:
The list [[1,S1],[2,S2],..],
S1, S2, .. represent the set of parameter values
that must be verified as supplementary
conditions for the Proposition to become a Theorem.
They are given by default in Prep.
If the proposition is generally true,
(the proposition is already a theorem), then
the generic segment of the internal grobcov
called is also returned to provide information
about the values of the variables determined
for every value of the parameters.

Options:
An option is a pair of arguments: string,
integer. To modify the default options, pairs
of arguments -option name, value- of valid options
must be added to the call.
Option "rep",0-1: The default is ("rep",0)
and then the segments are given in canonical
P-representation.
Option ("rep",1) represents the segments
in canonical C-representation,
Option "gseg",0-1: The default is "gseg",1
and then when the proposition is generally true,
ADGT outputs a second element which is the
"generic segment" to provide supplementary information. With option "gseg",0 this is avoided.

Note:
The basering R, must be of the form Q[a][x],
(a=parameters, x=variables), and
should be defined previously. The ideals
must be defined on R.

Example:
 ```LIB "grobcov.lib"; // Determine the supplementary conditions // for the non-degenerate triangle A(-1,0), B(1,0), C(x,y) // to have an ortic non-degenerate isosceles triangle if(defined(R)){kill R;} ring R=(0,x,y),(x2,y2,x1,y1),lp; // Hypothesis H ideal H=-y*x1+(x-1)*y1+y, (x-1)*(x1+1)+y*y1, -y*x2+(x+1)*y2-y, (x+1)*(x2-1)+y*y2; // Thesis T ideal T=(x1-x)^2+y1^2-(x2-x)^2-y2^2; // Negative Hypothesis H1 ideal H1=y; // Negative Thesis T1 ideal T1=x*(y1-y2)-y*(x1-x2)+x1*y2-x2*y1; // Complementary conditions for the // Proposition (H and not H1) => (T and not T1) // to be true ADGT(H,T,H1,T1); ==> [1]: ==> [1]: ==> 1 ==> [2]: ==> [1]: ==> [1]: ==> _[1]=(x^2-y^2-1) ==> [2]: ==> [1]: ==> _[1]=(y) ==> _[2]=(x-1) ==> [2]: ==> _[1]=(y) ==> _[2]=(x+1) ==> [3]: ==> _[1]=(y^2+1) ==> _[2]=(x) ==> [2]: ==> [1]: ==> _[1]=(x) ==> [2]: ==> [1]: ==> _[1]=(y-1) ==> _[2]=(x) ==> [2]: ==> _[1]=(y) ==> _[2]=(x) ==> [3]: ==> _[1]=(y^2+1) ==> _[2]=(x) ==> [4]: ==> _[1]=(y+1) ==> _[2]=(x) //******************************************** // Example of automatic demonstrations of a theorem // The Nine Points Circle Theorem: if(defined(R1)){kill R1;} ring R1=(0,x,y),(x1,y1,x2,y2,yh,a,b,r),dp; short=0; //Hypothesis H ideal H=y*x1+y1-x*y1-y, (x-1)*(x1+1)+y*y1, -y*x2+y2+x*y2-y, (x+1)*(x2-1)+y*y2, (x1-a)^2+(y1-b)^2-r^2, (x2-a)^2+(y2-b)^2-r^2, (x-a)^2+b^2-r^2, -yh+x*y1-x1*yh+y1; // Thesis T ideal T=yh+x*y2-x2*yh-y2, (x-1-2*a)^2+(yh-2*b)^2-4*r^2, (x+1-2*a)^2+(yh-2*b)^2-4*r^2, 4*(x-a)^2+(y+yh-2*b)^2-4*r^2, (x-1-2*a)^2+(y-2*b)^2-4*r^2, (x+1-2*a)^2+(y-2*b)^2-4*r^2, 4*(x-a)^2+(yh+y-2*b)^2-4*r^2; ADGT(H,T,y,1); ==> [1]: ==> [1]: ==> 1 ==> [2]: ==> [1]: ==> [1]: ==> _[1]=0 ==> [2]: ==> [1]: ==> _[1]=(x^2-2*x+y^2+1) ==> [2]: ==> _[1]=(x^2+2*x+y^2+1) ==> [3]: ==> _[1]=(y) ==> [2]: ==> [1]: ==> Generic segment ==> [2]: ==> [1]: ==> _[1]=b ==> _[2]=a ==> _[3]=yh ==> _[4]=y2 ==> _[5]=x2 ==> _[6]=y1 ==> _[7]=x1 ==> _[8]=r^2 ==> [2]: ==> _[1]=(4*y)*b+(x^2-y^2-1) ==> _[2]=2*a+(-x) ==> _[3]=(y)*yh+(x^2-1) ==> _[4]=(x^2+2*x+y^2+1)*y2+(-2*x*y-2*y) ==> _[5]=(x^2+2*x+y^2+1)*x2+(-x^2-2*x+y^2-1) ==> _[6]=(x^2-2*x+y^2+1)*y1+(2*x*y-2*y) ==> _[7]=(x^2-2*x+y^2+1)*x1+(x^2-2*x-y^2+1) ==> _[8]=(16*y^2)*r^2+(-x^4-2*x^2*y^2+2*x^2-y^4-2*y^2-1) ==> [3]: ==> [1]: ==> [1]: ==> _[1]=0 ==> [2]: ==> [1]: ==> _[1]=(x^2-2*x+y^2+1) ==> [2]: ==> _[1]=(x^2+2*x+y^2+1) ==> [3]: ==> _[1]=(y) // Thus the theorem is true. ```