#### D.2.4.21 ADGT

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.
  If the proposition is false for every values of the
  parameters, then the empty list is returned.

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.
  Option "neg", 0,1: The default is "neg",0
  With option "neg",0 Rabinovitch trick is used for negative hypothesis and thesis With option "neg",1 Difference of constructible sets is used instead.

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: the triangle  A1(x1,y1), B1(x2,y2), C1(x,0), is the
    // orthic triangle of ABC
    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: the orthic triangle is isosceles
    ideal T=(x1-x)^2+y1^2-(x2-x)^2-y2^2;
    // Negative Hypothesis H1: ABC is non-degenerate
    ideal H1=y;
    // Negative Thesis T1: the orthic triangle is non-degenerate
    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)
    ==>                _[2]=(x)
    ==>             [2]:
    ==>                _[1]=(y-1)
    ==>                _[2]=(x)
    ==>             [3]:
    ==>                _[1]=(y+1)
    ==>                _[2]=(x)
    ==>             [4]:
    ==>                _[1]=(y^2+1)
    ==>                _[2]=(x)
    // Now using diference of constructible sets for negative hypothesis and thesis
    ADGT(H,T,H1,T1,"neg",1);
    ==> [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)
    ==>                _[2]=(x)
    ==>             [2]:
    ==>                _[1]=(y-1)
    ==>                _[2]=(x)
    ==>             [3]:
    ==>                _[1]=(y+1)
    ==>                _[2]=(x)
    ==>             [4]:
    ==>                _[1]=(y^2+1)
    ==>                _[2]=(x)
    // The results are identical using both methods for the negative propositions
    // - Rabinovitch or
    // - DifConsLCSets
    // EXAMPLE 2
    // Automatic Theorem Proving.
    // The nine points circle theorem.
    // Vertices of the triangle: A(-2,0), B(2,0), C(2a,2b)
    // Heigth foot: A1(x1,y1),
    // Heigth foot: B1(x2,y2),
    // Heigth foot: C1(2a,0)
    // Middle point BC:  A2(a+1,b)
    // Middle point CA:  B2 (a-1,b)
    // Middle point AB:  C2(0,0)
    // Ortocenter:   O(2x0,2y0)
    // Middle point of A and O:  A3(x0-1,y0)
    // Middle point of B and O:  B3(x0+1,y0)
    // Middle point of C and O:  C3(x0+a,y0+b)
    // Nine points circle: c:=(X-x3)^2+(Y-y3)^2-r2
    if (defined(R1)){kill R1;}
    ring R1=(0,a,b),(x1,y1,x2,y2,x0,y0,x3,y3,r2),dp;
    short=0;
    ideal H=-x1*b+(a-1)*y1+2*b,
    (a-1)*x1+b*y1+2*a-2,
    -x2*b+(a+1)*y2-2*b,
    (a+1)*x2+b*y2-2*a-2,
    -x0*y1+(x1+2)*y0-y1,
    -x0*y2+(x2-2)*y0+y2;
    ideal T=(x1-2*x3)^2+(y1-2*y3)^2-r2,
    (a+1-2*x3)^2+(b-2*y3)^2-r2,
    (x0-1-2*x3)^2+(y0-2*y3)^2-r2,
    (x2-2*x3)^2+(y2-2*y3)^2-r2,
    (a-1-2*x3)^2+(b-2*y3)^2-r2,
    (x0+1-2*x3)^2+(y0-2*y3)^2-r2,
    (2*a-2*x3)^2+4*y3^2-r2,
    4*x3^2+4*y3^2-r2,
    (x0+a-2*x3)^2+(y0+b-2*y3)^2-r2;
    ADGT(H,T,b,1);
    ==> [1]:
    ==>    [1]:
    ==>       1
    ==>    [2]:
    ==>       [1]:
    ==>          [1]:
    ==>             _[1]=0
    ==>          [2]:
    ==>             [1]:
    ==>                _[1]=(a^2+2*a+b^2+1)
    ==>             [2]:
    ==>                _[1]=(a^2-2*a+b^2+1)
    ==>             [3]:
    ==>                _[1]=(b)
    ==> [2]:
    ==>    [1]:
    ==>       Generic segment
    ==>    [2]:
    ==>       [1]:
    ==>          _[1]=r2
    ==>          _[2]=y3
    ==>          _[3]=x3
    ==>          _[4]=y0
    ==>          _[5]=x0
    ==>          _[6]=y2
    ==>          _[7]=x2
    ==>          _[8]=y1
    ==>          _[9]=x1
    ==>       [2]:
    ==>          _[1]=(4*b^2)*r2+(-a^4-2*a^2*b^2+2*a^2-b^4-2*b^2-1)
    ==>          _[2]=(4*b)*y3+(a^2-b^2-1)
    ==>          _[3]=2*x3+(-a)
    ==>          _[4]=(b)*y0+(a^2-1)
    ==>          _[5]=x0+(-a)
    ==>          _[6]=(a^2+2*a+b^2+1)*y2+(-4*a*b-4*b)
    ==>          _[7]=(a^2+2*a+b^2+1)*x2+(-2*a^2-4*a+2*b^2-2)
    ==>          _[8]=(a^2-2*a+b^2+1)*y1+(4*a*b-4*b)
    ==>          _[9]=(a^2-2*a+b^2+1)*x1+(2*a^2-4*a-2*b^2+2)
    ==>       [3]:
    ==>          [1]:
    ==>             [1]:
    ==>                _[1]=0
    ==>             [2]:
    ==>                [1]:
    ==>                   _[1]=(a^2+2*a+b^2+1)
    ==>                [2]:
    ==>                   _[1]=(a^2-2*a+b^2+1)
    ==>                [3]:
    ==>                   _[1]=(b)
    // Thus the nine point circle theorem is true for all real points excepting b=0.

User manual for Singular version 4.4.1, 2025, generated by texi2html.