|
|
D.2.4.22 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.
- 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.
|
|
Online Manual
