本日のC.A.D.

座標平面において，原点 $(0,\ 0)$ が $3$ 点 $(3,\ 0)$，$(-1,\ \sqrt{3})$，$(-2,\ -2\sqrt{3})$ を頂点とする $3$ 角形の Fermat 点 ( https://en.wikipedia.org/wiki/Fermat_point ) であることを示します．

$\forall x\ \forall y \ \left( 9\le\sqrt{(x-3)^2+y^2}+\sqrt{(x+1)^2+(y-\sqrt{3})^2}+\sqrt{(x+2)^2+(y+2\sqrt{3})^2}\ \right )\ \land\ 9=3+2+4 $

? tst12([ex,ex,ex,ex,ex,ex],[r,a,b,c,x,y],andx,"0<r,r^2==3,0<=a,0<=b,0<=c,a^2==(x-3)^2+y^2,b^2==(x+1)^2+(y-r)^2,c^2==(x+2)^2+(y+2*r)^2,9>a+b+c",23);Ans();
[[],[[r,2,6],[a,2,3],[b,2,3],[c,2,3],[x,2,6],[y,2,5]]]
 *** reordering by degree.
 *** using Lazard's method (MPP17).
[c,3]
[b,4]
[a,6]
[y,13]
[x,76]
[r,1554]
time = 43min, 49,542 ms.
1 171(4,5) 5715(68,128) 5715(356,6960) 5715(4,2606) 0(2,1012) 
1[false]
time = 49,278 ms.

? tst12([ex,ex,ex,ex],[r,a,b,c],andx,"0<r,r^2==3,0<=a,0<=b,0<=c,a^2==(0-3)^2+0^2,b^2==(0+1)^2+(0-r)^2,c^2==(0+2)^2+(0+2*r)^2,9==a+b+c");Ans();
 *** using Lazard's method (MPP17).
[c,3]
[b,4]
[a,7]
[r,8]
time = 91 ms.
1 1(0,2) 1(0,2) 1(0,2) 
 *** combined adjacent 0 cells.
1[true,true,true,true]
time = 4 ms.

$\forall x\ \forall y \ \left( 9=\sqrt{(x-3)^2+y^2}+\sqrt{(x+1)^2+(y-\sqrt{3})^2}+\sqrt{(x+2)^2+(y+2\sqrt{3})^2}\ \to\ x=0\ \land\ y=0\ \right )$

? tst12([ex,ex,ex,ex,ex,ex],[r,x,y,a,b,c],andx,"0<r,r^2==3,0<=a,0<=b,0<=c,a^2==(x-3)^2+y^2,b^2==(x+1)^2+(y-r)^2,c^2==(x+2)^2+(y+2*r)^2,9==a+b+c,0<x^2+y^2");Ans();
 *** using Lazard's method (MPP17).
[c,3]
[b,4]
[a,6]
[y,14]
[x,89]
[r,1675]
time = 52min, 2,991 ms.
1 175(8,7) 5814(70,129) 5814(364,7074) 5814(4,2644) 0(2,1026) 
1[false]
time = 51,849 ms